Mechanically verifying concurrent programs
David M. Goldschlag · 1992
This thesis develops a sound, mechanically verified proof system suitable for the mechanical verification of both the safety and liveness properties of concurrent programs. Mechanical verification increases the trustworthiness of a proof. The properties proved may be (non-existentially quantified) first order, and the programs may be parameterized. The proof system provides a mechanized framework for reasoning about concurrent programs under a variety of fairness assumptions. It is demonstrated by the mechanically verified proofs of four concurrent programs. This thesis presents several significant results, including the first extensive mechanized use of proof rules which are theorems of an operational semantics. This research also prompted the development of both the functional variables (Boyer, Goldschlag, Kaufmann, & Moore 91) and Defn-Sk (Kaufmann 89) extensions to the Boyer-Moore logic. Thesis chapters include: (1) A formalization, in the Boyer-Moore Logic (Boyer & Moore 88a), of an interpreter for concurrent programs with non-deterministic statements. This operational semantics is the foundation for the development of a sound proof system similar to Unity (Chandy & Misra 88). (2) The presentation of Unity's major proof rules (except for superposition) as theorems about this interpreter. This includes the infinite disjunction and substitution axioms. Unity's theorems remain true for programs with non-deterministic statements. (3) The extension of the Unity logic to include the literature's notions of weak and strong fairness (Manna & Pnueli 84), and deadlock freedom. The latter two notions guarantee freedom from starvation and absence of deadlock, respectively. (4) A new proof rule for reasoning about properties that are eventually invariant. (5) A proof of an n-node mutual exclusion algorithm. (6) A proof of a minimum tree value algorithm. This proof demonstrates reasoning about programs with multiple instances of several statements and a complicated data structure. (7) A proof of an n-node dining philosopher's program under the assumptions of strong fairness and deadlock freedom. (8) A proof of an n-node delay insensitive FIFO queue, where statements correspond to Martin's production rules (Martin 87). Both the safety and liveness properties proved are non-propositional theorems. This thesis both contributes to the science of mechanized program verification and lays the groundwork for future research.