Development of parallel programs on shared data-structures -- Revised version

TL;DR

This paper introduces a formal system for developing correct parallel programs on shared data structures, using auxiliary variables for specification and verification, demonstrated through several complex algorithms.

Contribution

It presents a compositional reformulation of the Owicki/Gries method, allowing flexible use of auxiliary variables for program development and correctness proof.

Findings

System is sound and relatively complete.

Successfully developed three complex algorithms.

Extended method to nonterminating programs like Dekker's algorithm.

Abstract

A syntax-directed formal system for the development of totally correct programs with respect to an unfair shared-state parallel while-language is proposed. The system can be understood as a compositional reformulation of the Owicki/Gries method for verification of parallel programs. Auxiliary variables are used both as a specification tool to eliminate undesirable implementations, and as a verification tool to make it possible to prove that an already finished program satisfies a particular specification. Auxiliary variables may be of any sort, and it is up to the user to define the auxiliary structure he prefers. Moreover, the auxiliary structure is only a part of the logic. This means that auxiliary variables do not have to be implemented as if they were ordinary programming variables. The system is proved sound and relatively complete with respect to an operational semantics and employed to develop three nontrivial algorithms: the Dining-Philosophers, the Bubble-Lattice-Sort and the Set-Partition algorithms. Finally, a related method for the development of (possibly nonterminating) programs with respect to four properties is described. This approach is then used to develop Dekker's algorithm.