Systematic Parallel Programming
Abstract
Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. Moreover, a large variety of very different parallel architectures exists. Porting an implementation from one machine to another may require substantial changes. This thesis addresses some of these problems by developing a formal basis for the design of parallel programs in form of a refinement calculus. The calculus allows the stepwise formal derivation of an abstract, low-level implementation from a trusted, high-level specification. The calculus thus helps structuring and documenting the development process. Portability is increased, because the introduction of a machine-dependent feature can be located in the refinement tree. Development efforts above this point in the tree are independent of that feature and are thus reusable. Moreover, the discovery of new, possibly more efficient solutions is facilitated. Last but not least, programs are correct by construction, which obviates the need for difficult debugging. Our programming/specification notation supports fair parallelism, shared-variable and message-passing concurrency, local variables and channels. It allows the development of reactive systems, that is, possibly non-terminating programs designed to interact persistently with their environment. Moreover the specification of liveness properties such as termination or eventual entry is supported by our methodology. The calculus rests on a compositional trace semantics that treats shared-variable and message-passing concurrency uniformly. The refinement relation combines a context-sensitive notion of trace inclusion and assumption-commitment reasoning to achieve compositionality. Most refinement rules are syntax-directed in the sense that each rule corresponds to a specific language construct. The calculus straddles both concurrency paradigms.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 19, 2000
- Accession Number
- ADA382625
Entities
People
- Juergen Dingel
Organizations
- Carnegie Mellon University