Type-based homeomorphic embedding for online termination

Online termination techniques dynamically guarantee termination of computations by supervising them in such a way that computations whose termination can no longer be guaranteed are stopped. Homeomorphic Embedding (HEm) has proven to be very useful for online termination provided that the computations supervised are performed over a finite signature, i.e., the number of constants and function symbols involved is finite. However, there are many situations, for example numeric computations, which involve an infinite signature and thus HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination. However, the existing techniques either do not provide systematic means for generating such extensions or the extensions are too simplistic and do not produce the expected results in practice. We propose Type-based Homeomorphic Embedding (TbHEm) as an extension of the standard, untyped, HEm. By taking static information about the behavior of the computation into account, expressed as types, TbHEm allows obtaining more precise results than those of the previous extensions to HEm for the case of infinite signatures. We show that the existing extensions to HEm which are currently used in state-of-the-art specialization tools can be reconstructed as instances of TbHEm. We illustrate the applicability of our proposal in a realistic case study: partial evaluation of an interpreter. We argue that the results obtained provide empirical evidence of the interest of our proposal.     

Lower bounds for decision problems in imaginary,norm-Euclidean quadratic integer rings

We prove lower bounds for the complexity of deciding several relations in imaginary, norm-Euclidean quadratic integer rings, where computations are assumed to be relative to a basis of piecewise-linear operations. In particular, we establish lower bounds for deciding coprimality in these rings, which yield lower bounds for gcd computations. In each imaginary, norm-Euclidean quadratic integer ring, a known binary-like gcd algorithm has complexity that is quadratic in our lower bound.     

An adaptive,error-free computation based on the 4×4 determinant method

The 4×4 determinant method makes it possible to unify geometric processing by the computations of 4×4 determinants composed of homogeneous coordinants vectors of four points or coefficient vectors of four plane equations. Because the method needs not require a division operation, error-free geometric computation is not difficult to realize by means of integer arithemtic of appropriate data length. The present paper proposes an error-free, efficient computing method, which computes the 4×4 determinants by adaptively selecting integer arithmetic of variable data length. This technique is discussed theoretically and experimentally.     

Finite Integer Computations: An Algebraic Foundation for Their Correctness

Even though computations on finite integer representations are as old as computers themselves, there is one problem that has been inexcusably neglected: integer computations in programming languages do not operate on the ring of integer numbers but only on finite subsets of it. Changing the size of integer representations may change the results of operations performed on them in unexpected ways. In particular, increasing the representation size of intermediate results during computation may lead to incorrect final results. In this paper, we develop an algebraic foundation for integer arithmetic under changing representation sizes and, in particular, a criterion for safely replacing one finite integer arithmetic by another. This safety criterion has also been verified in the theorem prover Isabelle/HOL. Based on this formal development, we not only reveal and explain an inconsistency in the Java Card integer arithmetic but also propose an optimization for Java Card integer expressions and their safe transformation into Java Card bytecode. We also discuss the application of this safety criterion to constant folding, a standard compiler optimization, for Java and C compilers. Received August 2004 Revised January 2006 Accepted February 2006 by C. B. Jones     

Synchronous,asynchronous, and causally ordered communication

Summary.  This article studies characteristic properties of synchronous and asynchronous message communications in distributed systems. Based on the causality relation between events in computations with asynchronous communications, we characterize computations which are realizable with synchronous communications, which respect causal order, or where messages between two processes are always received in the order sent. It is shown that the corresponding computation classes form a strict hierarchy. Furthermore, an axiomatic definition of distributed computations with synchronous communications is given, and it is shown that several informal characterizations of such computations are equivalent when they are formalized appropriately. As an application, we use our results to show that the distributed termination detection algorithm by Dijkstra et al. is correct under a weaker synchrony assumption than originally stated. Received: November 1992/Accepted: July 1995     

Efficient termination detection for loosely synchronousapplications in multicomputers

We propose a simple algorithm which is based on edge-coloring of system graphs for termination detection of loosely synchronous computations. The proposed algorithm is fully symmetric in that all processors run syntactically identical code and can detect global termination at the same time. Under the 1-port communication model, the algorithm is optimal in terms of termination delay, the difference between the time when a global termination occurs and the time it is detected, in a number of structures-chain, ring of even number of nodes, k-ary n-cube and k-ary n-mesh of low degree, where k is even; and near-optimal for other cases. The optimality analysis is based on results from a related problem, periodic gossiping in edge-colored graphs. This algorithm has been applied to some practical cases in which the overhead due to its execution is found to be insignificant     

Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

While automated verification of imperative programs has been studied intensively, proving termination of programs with explicit pointer arithmetic fully automatically was still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that over-approximates all possible runs of a program and that can be used to prove memory safety. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.     

Solid Modeling Based on a New Paradigm

The technique of solid modeling is essential in CAD/CAM applications, and is currently well established. However, problems remain, such as the lack of uniformity in geometric computations and the lack of stability of Boolean operations of two solids. In this paper, we introduce a theoretical solid modeling system that operates on boundary representations of polyhedral objects and is based on a new paradigm. The characteristics of the system are the following: (I) in Boolean Operations and modeling transformations, all geometric computations are performed by the 4 × 4 determinant method or the 4 × 4 matrix method in homogeneous space, which allows the system to avoid division operations, (2) all geometric computations are performed by the exact integer arithmetic, which makes the geometric algorithms stable and simple, and (3) primitive solids are constructed consistently in the integer domain, and the consistency is assured throughout Boolean operations and transformations.     

A ρ-calculus of explicit constraint application

Theoretical presentations of the rewriting or ρ-calculus often treat the matching constraint computations as an atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a more realistic view: computations needed in order to find the solutions of a matching equation can have an important impact on the (efficiency of the) calculus for some matching theories and the substitution application usually involves a term traversal. Following the works on explicit substitutions in the λ-calculus, we present two versions of the ρ-calculus, one with explicit matching and one with explicit substitutions, together with a version that combines the two and considers efficiency issues and more precisely the composition of substitutions. The approach is general, allowing for potential extensions to various matching theories. We establish the confluence of the calculus and the termination of the explicit constraint handling and application sub-calculus.