Formal verification of programs in the functional data-flow parallel language

The article is devoted to the methods of proving parallel programs correctness, that are based on the axiomatic approach. Formal system for functional data-flow parallel programming language Pifagor is described. On the basis of this system programs correctness could be proved.     

A wide instruction word architecture for parallel execution of logic programs coded in BSL

This paper begins by describing BSL, a new logic programming language fundamentally different from Prolog. BSL is a nondeterministic Algol-class language whose programs have a natural translation to first order logic; executing a BSL program without free variables amounts to proving the corresponding first order sentence. A new approach is proposed for parallel execution of logic programs coded in BSL, that relies on advanced compilation techniques for extracting fine grain parallelism from sequential code. We describe a new “Very Long Instruction Word” (VLIW) architecture for parallel execution of BSL programs. The architecture, now being designed at the IBM Thomas J. Watson Research Center, avoids the synchronization and communication delays (normally associated with parallel execution of logic programs on multiprocessors), by determining data dependences between operations at compile time, and by coupling the processing elements very tightly, via a single central shared register file. A simulator for the architecture has been implemented and some simulation results are reported in the paper, which are encouraging.     

Livelocks in parallel programs

This paper is the second of a two-part series exploring the subtle correctness criterion of the absence of livelocks in parallel programs. In this paper we are concerned with the issue of proving this correctness criterion. It is shown that livelocks are not preserved by reduction, implying that reduction cannot be used directly in proving the absence of livelocks. Two applicable proof techniques are also presented. One is based on the notion of establishing sufficient conditions for livelock-freedom; the other is an extension of the well-founded set method for proving termination in sequential programs.     

A proof system for concurrent ADA programs

A subset of ADA is introduced, ADA-CF, to study the basic synchronization and communication primitive of ADA, the rendezvous. Basing ourselves on the techniques introduced by Apt, Francez and de Roever for their CSP proof system, we develop a Hoare-style proof system for proving partial correctness properties which is sound and relatively complete. The proof system is then extended to deal with safety, deadlock, termination and failure. No prior exposure of the reader to parallel program proving techniques is presupposed. Two non-trivial example proofs are given of ADA-CF programs; the first one concerns a buffered producer-consumer algorithm, the second one a parallel sorting algorithm due to Brinch Hansen. Features of ADA expressing dynamic process creation and realtime constraints are not covered by our proof methods. Consequently, we do not claim that the methods described can be extended to full ADA without serious additional further research.     

A Structured Temporal Logic Language:XYZ/SE

In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is the basis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a general conpositional verification method in the XYZ system concerning the sequential case.     

Transformational methodology for proving termination of logic programs

A methodology for proving the termination of well-moded logic programs is developed by reducing the termination problem of logic programs to that of term rewriting systems. A transformation procedure is presented to derive a term rewriting system from a given well-moded logic program such that the termination of the derived rewrite system implies the termination of the logic program for all well-moded queries under a class of selection rules. This facilitates applicability of a vast source of termination orderings proposed in the literature on term rewriting, for proving termination of logic programs. The termination of various benchmark programs has been established with this approach. Unlike other mechanizable approaches, the proposed approach does not require any preprocessing and works well, even in the presence of mutual recursion. The transformation has also been implemented as a front end to Rewrite Rule Laboratory (RRL) and has been used in establishing termination of nontrivial Prolog programs such as a prototype compiler for ProCoS, PL₀ language.     

The Evolution of Concurrent Programs

Process algebra are formal languages used for the rigorous specification and analysis of concurrent systems. By using a process algebra as the target language of a genetic programming system, the derivation of concurrent programs satisfying given problem specifications is possible. A genetic programming system based on Koza's model has been implemented. The target language used is Milner's CCS process algebra, and is chosen for its conciseness and simplicity. The genetic programming environment needs a few adaptations to the computational characteristics of concurrent programs. In particular, means for efficiently controlling the exponentially large computation spaces that are common with process algebra must be addressed. Experimental runs of the system successfully evolved a number of non–iterative CCS systems, hence proving the potential of evolutionary approaches to concurrent system development.     

Parallel program design using high-level Petri nets

Petri nets are proposed as a general-purpose design and modelling tool for parallel programs. The advantages of Petri nets for this purpose are discussed, and a solution to the Dining Philosophers problem is developed using simple Place-Transition nets. The limitations of Place-Transition nets are described, and the Dining Philosophers problem is used to illustrate how Coloured Petri nets can overcome these limitations. A more complex example of a Coloured Petri net is then given, and it is shown how a collection of processes in the Occam programming language can be developed directly from the properties of the net. Another Petri net model of a simple process farm is given, and a solution is developed in Parallel C: this further highlights the suitability of Petri nets as a design tool for parallel programs.     

Issues in the Design and Control of Parallel Rule-Firing Production Systems

The parallel execution of rules in a production system provides the potential for faster execution, but increases the complexity of control and design issues. We address two issues: controlling the execution of productions without introducing serial bottlenecks and maintaining correctness during the course of simultaneous rule executions. Two novel rule-firing policies are described: an asynchronous rule-firing policy that causes rules to be executed as soon as they become enabled and a task-based scheduler that allows multiple independent tasks to run asynchronously with respect to each other while allowing rules to execute either synchronously or asynchronously within the context of each task. Previous research in parallel rule-firing systems has indicated that a serializable result cannot be guaranteed without a run-time mechanism for detecting potentially harmful rule interactions. Our analysis of such mechanisms indicates that their overhead is prohibitive for asynchronous rule-firing systems. In exchange for improved performance, we trade the guarantee of serializability for the somewhat weaker claim that correct parallel rule-firing programs may be designed, given the appropriate language mechanisms. We present a simple locking scheme for working memory, which, when coupled with the appropriate language idioms, allows serializable programs to be developed without incurring the expense of run-time interference detection. The experimental results of this research are presented in the context of UMass Parallel OPS5, a rule-based language that incorporates parallelism at the rule, action, and match levels, and provides language constructs for supporting the design of parallel rule-based programs. Results are presented for a number of programs illustrating common AI paradigms including search, inference, and constraint satisfaction problems.     

Verification and synthesis of addition programs under the rules of correctness of statements

Deductive verification and synthesis of binary addition programs are carried out on the base of the rules of proving the correctness for statements of the predicate programming language P. The paper presents key fragments of verification and synthesis of the programs for the Ripple carry, Carry look-ahead and Ling adders. The correctness conditions of the programs were translated into the specification language of the PVS verification system. The proof is found to be a tedious procedure as compared with the ordinary programming. However, for program synthesis, the development of theories and proofs on PVS are easier and faster than for program verification.     

Essence of generalized partial computation

Generalized partial computation (GPC) is a program optimization principle based on partial computation and theorem proving. Conventional partial computation methods (or partial evaluators) explicitly make use of only given parameter values to partially evaluate programs. However, GPC explicitly utilizes not only given values but also the following information: (1) logical structure of a program to be partially evaluated; (2) abstract data type of a programming language. The main purpose of this paper is to present comprehensible examples of GPC. Graphical notations, called GPC trees, are introduced to visibly describe GPC processes.     

Visual Parallel Programming and Determinancy: A Language Specification,an Analysis Technique,and a Programming Tool

Phred is a visual parallel programming language in which programs can be statically analyzed for deterministic behavior. This paper presents the Phred language, techniques for analyzing the language, and a programming environment which supports Phred programming. There are many methods for specifying synchronization and data sharing in parallel programs. The Phred programmer uses graph constructs for describing parallelism, synchronization, and data sharing. These graphs are formally described in this paper as a graph grammar. The use of graphs in Phred provides an intuitive and visual representation for parallel computations. The inadvertent specification of nondeterministic computations is a common error in parallel programming. Phred addresses the issue of determinacy by visually indicating regions of a program where nondeterminacy may exist. This analysis and its integration into a programming environment is presented here. The Phred programming environment supports the specification, analysis, and execution of Phred programs. The distribution of the programming environment itself over several workstations is also described.     

Correct and Robust Programs

The design of programs which are both correct and robust is investigated. It is argued that the notion of an exception is a valuable tool for structuring the specification, design, verification, and modification of such programs. The syntax and semantics of a language with procedures and exception handling are presented. A deductive system is proposed for proving total correctness and robustness properties of programs written in this language. The system is both sound and complete. It supports proof modularization, in that it allows one to reason separately about fault-free and fault-tolerant system properties. Since the programming languages considered closely resembles CLU or Ada, the presented deductive system is easily adaptable for verifying total correctness and robustness properties of programs written in these, or similar, languages.     

Automatic generation of self-scheduling programs

Techniques are described for the automatic generation of self-scheduling parallel programs. Both scheduling algorithms and the concurrent components of applications are expressed in a high-level concurrent language. Partitioning and data dependency information are expressed by simple control statements, which may be generated either automatically or manually. A self-scheduling compiler, implemented as a source-to-source transformation, takes application code, control statements, and scheduling routines and generates a new program that can schedule its own execution on a parallel computer. The approach has several advantages compared to previous proposals. It generates programs that are portable over a wide range of parallel computers. There is no need to embed special control structures in application programs. The use of a high-level language to express applications and scheduling algorithms facilitates the development, modification, and reuse of parallel programs     

Toward formal development of programs from algebraic specifications: Parameterisation revisited

Parameterisation is an important mechanism for structuring programs and specifications into modular units. The interplay between parameterisation (of programs and of specifications) and specification (of parameterised and of non-parameterised programs) is analysed, exposing important semantic and methodological differences between specifications of parameterised programs and parameterised specifications. The extension of parameterisation mechanisms to the higher-order case is considered, both for parameterised programs and parameterised specifications, and the methodological consequences of such an extension are explored.A specification formalism with parameterisation of an arbitrary order is presented. Its denotational-style semantics is accompanied by an inference system for proving that an object satisfies a specification. The formalism includes the basic specification-building operations of the ASL specification language and is institution independent.     

BRAVE—a parallel logic language for artificial intelligence

This paper presents the first results for the implementation of the logic language BRAVE on a parallel architecture. We explain the operational semantics of BRAVE with common programming examples and show how both and and or parallelism can be exploited and controlled using BRAVE syntax. The design of an abstract machine for the parallel execution of BRAVE is given along with the principles of compilation and example codings. Results are presented from running example programs on a three-processor prototype, using an interpreter for BRAVE written in C.     

Support for Parallel and Concurrent Programming in C++

C++ was originally designed as a sequential programming language. For development of multithreaded applications, libraries, such as Pthreads, Windows threads, and Boost, are traditionally used. The C++11 standard introduced some basic concepts and means for developing parallel and concurrent programs, but the direct use of these low-level means requires high programming skills and significant efforts. The absence of high-level models of parallelism in C++ is somewhat compensated for by various parallel libraries and directive parallelization tools (such as OpenMP), as well as by language extensions supported by some compilers (Intel CilkPlus). Nevertheless, we still require more advanced means to express parallelism in programs at the level of language standard and language library. In this survey, we consider the means for parallel and concurrent programming that are included into the C++17 standard, as well as some capabilities that are to be expected in the future standards.     

CODE: a unified approach to parallel programming

The authors describe CODE (computation-oriented display environment), which can be used to develop modular parallel programs graphically in an environment built around fill-in templates. It also lets programs written in any sequential language be incorporated into parallel programs targeted for any parallel architecture. Broad expressive power was obtained in CODE by including abstractions of all the dependency types that occur in the widely used parallel-computation models and by keeping the form used to specify firing rules general. The CODE programming language is a version of generalized dependency graphs designed to encode the unified parallel-computation model. A simple example is used to illustrate the abstraction level in specifying dependencies and how they are separated from the computation-unit specification. The most important CODE concepts are described by developing a declarative, hierarchical program with complex firing rules and multiple dependency types     

Engineering parallel symbolic programs in GPH

We investigate the claim that functional languages offer low-cost parallelism in the context of symbolic programs on modest parallel architectures. In our investigation we present the first comparative study of the construction of large applications in a parallel functional language, in our case in Glasgow Parallel Haskell (GP H). The applications cover a range of application areas, use several parallel programming paradigms, and are measured on two very different parallel architectures. On the applications level the most significant result is that we are able to achieve modest wall-clock speedups (between factors of 2 and 10) over the optimised sequential versions for all but one of the programs. Speedups are obtained even for programs that were not written with the intention of being parallelised. These gains are achieved with a relatively small programmer-effort. One reason for the relative ease of parallelisation is the use of evaluation strategies, a new parallel programming technique that separates the algorithm from the co-ordination of parallel behaviour. On the language level we show that the combination of lazy and parallel evaluation is useful for achieving a high level of abstraction. In particular we can describe top-level parallelism, and also preserve module abstraction by describing parallelism over the data structures provided at the module interface (‘data-oriented parallelism’). Furthermore, we find that the determinism of the language is helpful, as is the largely implicit nature of parallelism in GP H. Copyright © 1999 John Wiley & Sons, Ltd.