The structure of this thesis

Chapter 2

presents the syntax and semantics of the language we use to express abstract specifications and executable programs. The semantics is given in terms of traces. Relevant properties of the semantics are discussed.

Chapter 3

reviews Jones' original formulation of assumption-commitment reasoning [Jon81] as well as Stirling's reformulation [Sti88]. Then, Stirling's approach is adjusted to our setting and properties are presented.

Chapter 4

discusses different ways how the behaviour of two programs can be compared. One leads to a context-insensitive notion of approximation that analyzes the behaviour of a program regardless of the environment that it is executing in. The deficiencies of this relation lead us to a context-sensitive notion of approximation which also naturally induces a way of comparing the environments that programs are executing in with respect to their capabilities.

Chapter 5

takes assumption-commitment reasoning on the one hand and context-sensitive approximation on the other and merges them into our refinement relation. Properties and rules are presented. The program development methodology is given.

Chapter 6

contains the formal derivations of four shared-variable programs. Section 6.1 contains a simple example to illustrate the basic use of the calculus. Section 6.2 derives a shared-variable parallel implementation of the Warshall-algorithm. Section 6.3 derives a shared-variable parallel program to find the maximum in an array of integers. Alternative derivations are discussed. Section 6.4 treats the generalization of the maximum search problem. The first element in an array that satisfies a property is to be found. We derive a shared-variable parallel program and show how further refinement can lead to more efficiency.

Chapter 7

contains the formal derivations of two distributed, message-passing programs. Section 7.1 discusses the prefixsum algorithm (a generalization of the list ranking algorithm). First, a shared-variable solution is derived. From that, a distributed, message-passing implementation is obtained through further refinement. Section 7.2 addresses the all-pair shortest-paths problem in a graph. Shared-variable and message-passing programs are derived. We show that not every shared-variable solution lends itself as the basis of an efficient distributed implementation.

Chapter 8

discusses an n-process mutual exclusion algorithm called the tie-breaker algorithm or Peterson's algorithm. A high-level representation is given and verified. The textbook implementation is derived together with with several other, more parallel implementations.

Chapter 9

discusses related work. We employ a taxonomy that separates sequential from parallel approaches, compositional proof systems from program transformation systems and refinement calculi.

Chapter 10

presents future work. We distinguish between immediate extensions and more long-term research efforts.

Chapter 11

concludes.

Appendix A

contains the soundness proofs of the refinement rules. Moreover, the proofs of certain lemmas needed in the examples are collected here.

false Formal support for the design and verification of parallel programs has been an important research topic for a long time. Some of the approaches, for instance, attempt to generalize Hoare logic to a parallel setting and suggest syntax-directed proof systems [, , , , ]. In a different approach, Back and his colleagues generalize sequential programming by grouping independent transitions into actions that are assumed to be executed atomically []. The resulting Action systems thus inherit a lot of the theory of sequential programming despite the presence of concurrency. Other approaches require a more radical departure from sequential programming and defy easy classification, eg., [, , , ].

Independent of these efforts, traces have been realized as the adequate tool for modeling concurrent computation [, , ]. Our point of departure here is Brookes' transition trace semantics. In [], a combination of transition traces (sequences of pairs of states) together with two straightforward closure conditions (stuttering and mumbling) gives rise to an elegant, fully abstract, denotational semantics \ for a language that includes local variable declarations, synchronization and fair parallelism. The semantics validates several natural laws of concurrent programming, like, for instance, the commutativity and associativity of fair parallel composition

or the idempotence of

where abbreviates .

In this thesis, we argue that Brookes' transition trace semantics provides an ideal formal basis for the study of stepwise refinement for shared-variable and message-passing parallel programs. The pleasant meta-theory and robustness of allows for the development of a refinement calculus that, in our opinion, constitutes a contribution even in the face of a large body of existing related work. More precisely, we use a notion of context-sensitive approximation for transition traces that was introduced in [] to define a syntax-directed refinement calculus that supports compositional and inductive reasoning, local variables, fairness and reasoning about liveness properties like termination or eventual entry. Several examples will be discussed including n-process mutual exclusion algorithms and shortest-path algorithms on graphs. We will show how the calculus allows the stepwise formal derivation of the standard textbook solutions. Moreover, the refinement of shared-variable programs into distributed, message-passing programs will be demonstrated. Finally, we will illustrate how it can be used to explore the various ``degrees of implementation freedom'' of an algorithm and to uncover new and sometimes more efficient solutions.