Multiprogram Design in the theory of Owicki and Gries
Doug Goldson · Electronic workshops in computing · 2001
This paper introduces the theory of Owicki and Gries as a method for the design (as opposed to the verification) of multiprograms (concurrent programs). The theory is applied to a problem of barrier synchronisation for two (and more) programs. The problem is well chosen because it is easy to state yet not easy to solve, and it therefore shows the difficulties of multiprogram design very well. The effectiveness of the theory to manage multiprogram design, and in the control of complexity, emerges quite well from the exercise.