CSR 1-97 Compiler Correctness using Algebraic
Operational Semantics
K. Stephenson
We design a general algebraic model for operational semantics using computable algebras involving total functions. We apply this Algebraic Operational Semantics to the problem of determining the correctness of compilation. We produce an equational correctness criterion (which is of P1 complexity to validate since it involves total functions only), and we give a general strategy for correctness proofs. A result is that a compiler is correct if, and only if, it is correct over one step of time for any correctly initialised system. We illustrate our method by considering a compiler from while programs to a low-level register machine language.
CSR 2-97 Computation of Viscoelastic Cable Coating Flows
I. Mutlu, P. Townsend and M. F. Webster
A viscoelastic analysis is presented for model tube tooling, draw-down and combined geometry flows encountered in the cable coating industries. The work investigates the development of stress fields and studies the effect of varying entry flow stress boundary conditions. The analysis takes into account tube tooling and draw-down flow sections individually, and in combination. The flow behaviour of wire-coating grade low-density polyethylene is studied assuming a viscoelastic, isothermal flow, and employing a Taylor-Petrov-Galerkin finite element scheme with an exponential Phan-Thien/Tanner constitutive model.
CSR 3-97 Coupled and Decoupled Schemes for Viscoelastic Wire-Coating Flows
I. Mutlu, P. Townsend and M. F. Webster
Tube tooling extrusion coating is simulated for a low density polymer melt using a finite element method and a single-mode exponential Phan-Thien/Tanner constitutive model. A time-stepping Taylor-Galerkin/pressure-correction scheme is employed under both coupled and decoupled solution approaches. Stress response and pressure drop across the flow are investigated. For longer relaxation times, shear and tensile stress do not vary significantly throughout the flow, whilst pressure drop is found to be most sensitive to the quality of the model fit to the shear experimental data.
CSR 4-97 Temporal Acceleration Techniques for Viscoelastic Flows
H. Matallah, P. Townsend and M.F. Webster
This paper presents a finite element study based on a technique associated with time extrapolation to accelerate convergence rate to steady state for viscoelastic flows. The approach adopted is a local extrapolation method attributed to Neville. Temporal extrapolation is embedded within a time-marching Taylor-Galerkin/pressure-correction scheme as applied to the solution of model channel flow, 4:1 plane contraction flow and flow past a circular cylinder. In particular, consideration is given to obtaining steady-state solutions for an Oldroyd-B model. When extrapolation is performed for stress and velocity or pressure, stress and velocity overshoot, which consequently leads to divergence. In contrast, a stable numerical scheme emerges when only the stress is extrapolated.
CSR 5-97 Multi-mode Viscoelastic Simulations of Cable-coating Flows
H. Matallah, P. Townsend and M.F. Webster
This study combines a single and multi-mode viscoelastic analysis for wire-coating flows. The numerical simulations utilise a finite element time-stepping technique, a Taylor-Petrov-Galerkin/pressure-correction scheme. An exponential Phan-Thien/Tanner model is used to predict pressure-drop and residual stress for this process. A coupled approach is used for a single mode approximation. In contrast, for multi-mode calculations, a decoupled approach is adopted for pragmatism. Rheometrical data fitting is performed for steady shear and pure extensional flows, considering both high and low density grade polymers. Simulations are conducted to match pressure-drop/flowrate data for a capillary rheometer flow and results are presented for a tube-tooling wire-coating flow with a draw-down section.
CSR 6-97 Coarse Grain Parallel Finite Element Simulations for Incompressible Flows
P.W. Grant, M.F. Webster and X. Zhang
Parallel simulation of incompressible fluid flows is considered on networks of homogeneous workstations. Coarse-grain parallelization of a Taylor-Galerkin/pressure-correction finite element algorithm are discussed, taking into account network communication costs. The main issues include the parallelization of system assembly, and iterative and direct solvers, that are of common interest to finite element and general numerical computation. The parallelization strategies are implemented on a Sun workstation cluster using the PVM (Parallel Virtual Machine) message passing library. Test results are obtained with a maximum of nineteen workstations and various PVM configurations are exhibited. Parallel efficiency close to ideal has been achieved for some strategies adopted. It is suggested that loadbalancing may not always be beneficial on distributed platforms with broadcasting communication connection.
CSR 7-97 Recovery and Stress-splitting Schemes for Viscoelastic Flows
H. Matallah, P. Townsend and M.F. Webster
Various recovery and stress splitting schemes are investigated numerically for an Oldroyd-B model within the general framework of a time stepping fractional-staged finite element formulation, that of a Taylor-Galerkin/pressure correction method with consistent streamline upwinding. Smooth and nonsmooth planar flows are cited and both creeping and inertial conditions are considered. Problems addressed including flow through 4:1 contraction geometries, with rounded or sharp re-entrant corners, and flow past a cylinder. Vortex behaviour and scheme performance is analysed. The Recovery-based schemes are stability enhancing, being superior in higher De attenuation over Conventional and EVSS alternatives. It is the recovery aspect, and not the stress-splitting, that is the key element responsible for this improvement. Considerable care must be exercised with time-stepping schemes of the pressure-correction form to sustain accuracy and stability.
CSR 8-97 Algebraic Models of Superscalar Microprocessor Implementations: A Case Study
A.C.J. Fox and N.A. Harman
We extend a set of algebraic tools for microprocessors to model superscalar implementations, develop existing correctness models to accommodate advanced timing relationships, and consider formal verification. We illustrate our tools and techniques with an in-depth treatment of an example superscalar implementation. We are particularly interested in models of time and temporal abstraction. Clocks divide time into (not necessarily equal) segments, defined by the natural timing of the computational process of a device. We formally relate clocks by surjective, monotonic maps. In the case of superscalar microprocessors, the normal relationship between `architectural time' and `implementation time' is complicated by the fact that events that are distinct in time at the architectural level can occur simultaneously at the implementation level.
CSR 9-97 Computable Functions and Semicomputable Sets on Many-sorted Algebras
J.V. Tucker and J.I. Zucker
This is an introduction to the theory of functions and sets that are computable by algorithms defined on arbitrary many-sorted algebras. The algorithms are formalised by means of imperative programming languages, including languages based on the `while' construct, with and without arrays. The basic properties and results about computable functions (e.g., universality theorems) and semicomputability (e.g., definability) are treated in detail. There is a study of computable functions on algebras of real numbers. This is generalised to a new account of functions that are computable and computably approximable on topological partial algebras. A survey of other models of computation and appropriate equivalence theorems for abstract algebras is provided. Also included are accounts of connections with the theories of computable algebra and computable analysis, and a short history of generalisations of computability theory to algebras. This is a chapter for S Abramsky, D Gabbay and T S E Maibaum (editors), Handbook of Logic in Computer Science. Volume V, Oxford University Press, (in press).
CSR 10-97 Computation by While Programs on Topological Partial Algebras
J.V. Tucker and J.I. Zucker
The language of `while' programs is a fundamental model for imperative programming on any data type. It leads to a generalisation of the theory of computable functions on the natural numbers to the theory of computable functions on any many-sorted algebra. The language is used to express many algorithms in scientific computing where `while' programs are applied to continuous data. In the theory of data, continuous data types are modelled by topological many-sorted algebras. We study both exact and approximate computations by `while' programs, and `while' programs with arrays, over topological many-sorted algebras with partial operations. First, we establish that partial operations are necessary in order to compute a wide range of continuous functions. We prove basic continuity properties of our abstract computability: Any partial function computable over a partial topological algebra by a `while'-array program is continuous. Any set semicomputable, or computable, over a partial topological algebra by a `while'-array program is open, or clopen, respectively.
Secondly, we contrast exact and approximate computations. The class of functions that can be computed exactly can be quite limited. We show that on connected total algebras, the `while' and `while'-array computable functions are precisely those that are explicitly definable by terms. We show that for certain general classes of topological algebras, the total functions that can be approximated by `while' programs are precisely those that can be effectively approximated by terms. This property we call generalised Weierstrass approximation. An application of this result is that a function on the set R of reals is computable in the sense of computable analysis if, and only if, it is `while' approximable on a simple algebra based on R.
CSR 11-97 SewEx - A flex Based Expert System for Sewage Treatment Works Support
M.L.E. Dixon, P.W. Grant and L.G. Moseley
The development of an expert system for sewage treatment works management SewEx is described. This was built with the flex expert system toolkit. The system allows the diagnosis of problems in sewage sites which are managed by Welsh Water and accesses the surface assets database over a company network. Other uses of SewEx, such as what--if scenarios, maintenance and refurbishment are also outlined. A brief description of a tool, RuleGen, is given, which was built to ease the construction of the flex rule base. SewEx is currently on test at various sewage treatment works throughout parts of Wales and Herefordshire.
CSR 12-97 Modelling and Rendering Graphics Scenes Composed of Multiple Volumetric Datasets
Adrian LEU and Min Chen
This paper presents a method for modelling graphics scenes consisting of multiple volumetric objects. A two-level hierarchical representation is employed, which enables the reduction of the overall storage consumption as well as rendering time. With this approach, different objects can be derived from the same volumetric dataset, and 2D images can be trivially integrated into a scene. The paper also describes an efficient algorithm for rendering such scenes on ordinary workstations, and addresses issues concerning memory requirements and disk swapping.