Refinement as a basis for concurrent program design
Edgar Knapp · 1992
We advocate the design of reliable concurrent programs by stepwise refinement. We argue that top-down refinement is a practicable method for designing concurrent systems and allows the construction of programs in a scientific and disciplined manner. In our method, a program and its proof of correctness are developed hand in hand. Programming this way can be described as transforming a specification by formal manipulations into a program satisfying it. As a formal framework for reasoning about concurrent programs we chose Chandy and Misra's theory of UNITY. It allows the elegant design of rigorous correctness arguments by employing powerful proof rules rather than operational considerations. Two crucial properties of any formal system are soundness and completeness. Soundness is the basic healthiness criterion for any theory. Completeness is vital for the construction of programs since in a complete programming logic failure to construct a program from a given specification is due to an inadequate specification or a wrong design decision, rather than a weakness in the reasoning system. The soundness and completeness of UNITY logic has been an open problem for several years. The first part of our thesis provides a soundness and completeness theorem for UNITY, based on temporal logic. The milestone on the way to soundness and completeness are two predicate transformers for concurrency: wlt, a mapping capturing progress under (unconditional) fairness, and wsafe, a mapping dealing with safety properties. In the second part of our thesis, we develop a theory of refinement. We give two refinement principles and show that in combination they subsume data refinement. We present a number of heuristics for program design that have proved useful in applications of our theory. We illustrate our theory using a number of small examples. To show that our refinement principles are also applicable to more complex problems, we present a case study in which we construct an efficient concurrent Maximum Flow algorithm. An appendix contains certain implementation issues. We give specifications for a scanner and parser for a programming language based on UNITY from which code implementing scanner and parser is generated automatically. We also define a notion of normal form for UNITY programs and present a normalizer and interpreter for UNITY based programs.