How this thesis addresses these problems

Traces have been known as a powerful model of concurrency for a long time. In recent work [Bro96b,Bro97], Stephen Brookes has taken a particular kind of trace, called transition traces, and shown how they give rise to a fully abstract model for concurrent computation that is tractable, supports different levels of granularity, and is reasonably architecture-independent. Transition traces thus make an excellent candidate for a model that meets the requirements mentioned above. The purpose of this thesis is to equip Brookes' model with a viable software development methodology. In particular, we propose a refinement calculus that allows the formal, stepwise development of shared-variable and distributed, message-passing parallel programs from trusted, abstract specifications.

A refinement calculus consists of a specification and programming notation, a refinement relation and a set of rules that govern this relation. For a specification and programming notation to provide a useful basis for a calculus it should have certain properties:

• The notation should allow the expression of all necessary aspects of the development process. Thus, it should leave room for abstract, nondeterministic specifications, but also for concrete, executable programs. Such a language has been called a wide-spectrum language [CIP85].
• The notation should support fair parallel computation. A huge number of fairness notions exist [Fra86]. We will concentrate on weak fairness. More precisely, we assume that every process that is enabled continuously, will eventually be allowed to execute. Fairness is a useful minimal assumption. On the one hand, it can be expected to be met by any reasonable scheduler. On the other hand, it is useful because it frees the user from having to consider concrete scheduling policies and implementations and thus helps avoiding overly detailed, operational reasoning. Fairness is a good example of an abstraction that hides unnecessary detail while preserving essential properties.
• The notation should support shared-variable and message-passing concurrency. Both are equally important paradigms. We deem a uniform treatment an important step towards architecture independence.
• The notation should support local variables and channels. In general, it is good programming style to limit the scope of variables to their places of usage. This principle is especially true for parallel programs, because local variables can make reasoning about parallel programs substantially more tractable. Knowing, for instance, that variable x is local, means that other processes can neither read nor write x. Thus, the environment cannot invalidate program properties involving x, not can it be influenced by changes to x. Local variable declarations thus provide another useful abstraction tool. On the one hand, they allow abstraction from parts of the internal workings of the body of the declaration. On the other hand, they allow abstraction from the possible influence of the environment on certain properties program properties.

Moreover, the refinement relation itself also should meet certain minimal requirements.

• The relation should support stepwise, top-down program development and compositional reasoning. Structured programming and compositionality are important weapons against the complexity of parallel programming. To be most effective, refinement should support sequences of small, manageable development steps and thus allow the exploration of different design decisions and alternative implementations. Note that this requires the refinement relation to be reflexive and transitive. The soundness proof of each step should be compositional, that is, refinement between two programs composite programs should be derivable by showing refinement between corresponding subprograms. The refinement of a large, complex program should be reducible to the hopefully easier task of finding refinements for its parts.
• be context-sensitive. Typically, refinement is carried out in context. That is, an abstract component C is to be replaced by a more concrete one C' in a particular context E. Using information about the specific nature of E makes this replacement substantially more powerful and may provide information crucial for establishing the soundness of the refinement step. In other words, C' may refine C only in context E. In all other contexts, the refinement may fail and replacing C by C' would be unsound.
• support the introduction of local variables and channels. On the specification level, computations are often described in very abstract terms. During the course of the refinement it may then be necessary to flesh out the implementation details of these abstract computations. This very often requires the introduction of local variables, which, for example, step over and array, or compute temporary results. The effect of the local variables should be given solely by their effect on global variables, that is, changes to local variables should be unobservable outside their scope.
• allow a seamless treatment of both concurrency paradigms. It should be possible to refine a shared-variable program into a distributed, message-passing program and vice versa.
• support the specification and reasoning about liveness properties. The initial, top-level specification of the program to be developed must be able to express liveness properties. In the concurrent world, liveness properties are important. The user must be able to specify and prove that, for instance, a request will eventually be acknowledged, or a process will eventually be allowed to enter a critical region.

Finally, note that the rules should also have certain properties.

• The set of rules should be expressive, that is, they should allow the development of a substantial class of interesting programs.
• The set of rules should be user-friendly, that is, the rules should not be overly cumbersome or to numerous.

Note that this work will not attempt to address performance, complexity, or implementation issues. The semantics will concentrate on the sequences of states a program runs through during execution and will thus be geared towards correctness. Consequently, if two programs exhibit the same traces they will be equated in the semantics regardless of their performance. Whether the model can be augmented with cost measures, or be efficiently implemented, is left for future research.

Moreover, we will not consider data-refinement, or data-reification. We regard data-reification as an largely orthogonal program development technique that should easily mesh with our work here on procedural or operations refinement.