Concurrent Program Design in the Extended Theory of Owicki and Gries

Goldson, D. and Dongol, B.

Feijen and van Gasteren have shown how to use the theory of Owicki and Gries to design concurrent programs, however, the lack of a formal theory of progress has meant that these designs are driven entirely by safety requirements. Proof of progress requirements are made post-hoc to the derivation and are operational in nature. In this paper, we describe the use of an extended theory of Owicki and Gries in concurrent program design. The extended theory incorporates a logic of progress, which provides opportunity to develop a program in a manner that gives proper consideration to progress requirements. Dekker's algorithm for two process mutual exclusion is chosen to illustrate the use of the extended theory.

Cite as: Goldson, D. and Dongol, B. (2005). Concurrent Program Design in the Extended Theory of Owicki and Gries. In Proc. Eleventh Computing: The Australasian Theory Symposium (CATS2005), Newcastle, Australia. CRPIT, 41. Atkinson, M. and Dehne, F., Eds. ACS. 41-50.

(from crpit.com) (local if available)