Hoare Logic for Parallel Programs
Leonor Prensa Nieto · 2016
In the following theories a formalization of the Owicki-Gries and the rely-guarantee methods is presented. These methods are widely used for cor-rectness proofs of parallel imperative programs with shared variables. We define syntax, semantics and proof rules in Isabelle/HOL. The proof rules also provide for programs parameterized in the number of parallel compo-nents. Their correctness w.r.t. the semantics is proven. Completeness proofs for both methods are extended to the new case of parameterized programs. (These proofs have not been formalized in Isabelle. They can be found in [1].) Using this formalizations we verify several non-trivial examples for parameterized and non-parameterized programs. For the automatic gener-ation of verification conditions with the Owicki-Gries method we define a tactic based on the proof rules. The most involved examples are the veri-fication of two garbage-collection algorithms, the second one parameterized in the number of mutators.