Design of Nondeterministic Program Termination Based on the Equivalent Transformation Computation Model

We studied the termination of nondeterministic programs, which play an important, basic role in program synthesis, and provide a foundation for proving program termination. The class of programs we consider here is based on the <I>equivalent transformation (ET)</I> computation model. Computation with this model involves the succesive application of rules to sets of clauses. Since the ET model has more expressive terms and rules than other programming languages, program termination is difficult to prove: we must take into account all possible changes of terms made by various rules. We propose a sufficient condition of ET program termination that proves termination by checking each rule in a given program. We also provide an algorithm for this check.

NONDETERMINISM ANALYSIS ON SUPERCOMPUTERS AND CLUSTERS

Interconnecting computers into clusters or computational grids promises many benefits for users of computational science and engineering, especially in terms of performance and costs. This situation is additionally supported by programming libraries like MPI and PVM, which are portable across different platforms and allow to exploit the available computing power. Consequently, the number of applications utilizing these computing structures is steadily increasing. Yet, there are also some pitfalls with possibly serious consequences, that must not be ignored by software developers. This paper describes some critical issues related to nondeterministic program behavior. With such kinds of programs different program executions are observed although the same input data are provided, leading to the irreproducibility effect, the completeness problem, and the probe effect. The impact of these effects, their weight for software developers, and how they are affected on supercomputer architectures and cluster environments are discussed. These critical issues need to be pointed out to users in order to raise their understanding and awareness of the problems. While the irreproducibility effect is believed to be sufficiently solved by record&replay mechanisms, existing solutions for the probe effect are only partially successful, and only very few approaches address the completeness problem. A simple solution for the latter is offered by automatic event manipulation and artificial replay, which is however restricted by time and memory constraints. In addition, this solution to the completeness problem also solves the probe effect in nondeterministic parallel programs.

PAL – Propositional Algorithmic Logic

The aim of propositional algorithmic logic is to investigate the properties of program connectives. Complete axiomatic systems for deterministic as well as for nondeterministic interpretations of program variables are presented. They constitute basic sets of tools useful in the practice of proving the properties of program schemes. Propositional theories of data structures, e.g. the arithmetic of natural numbers and stacks, are constructed. This shows that in many aspects PAL is close to first-order algorithmic logic. Tautologies of PAL become tautologies of algorithmic logic after replacing program variables by programs and propositional variables by formulas. Another corollary to the completeness theorem asserts that it is possible to eliminate nondeterministic program variables and replace them by schemes with deterministic atoms.