Rely-Guarantee Proofs for Total Correctness of Sieve and Findp

The proof is organized into a library project that gives some proofs for the "rg diamond" operator and two projects Sieve and FindPos for the applications.

The library contains

• the basic compatibility result between the sustains operator and interleaving, based on constraints for the involved guarantees, relies, invariants, runs predicates (runs implies no deadlock), pre- and postconditions (Init is the Precondition for both parallel algorithms).
• The basic result is used to derive several decomposition theorems for a parallel routine SPAWN# that spawns n +1 (unspecified) processes SEQ# recursively. Project Sieve uses an instance.
• The first theorem is for partial correctness (since we don't need blocking in the case studies, the "runs" predicate is simply "true", i.e., we require that the algorithms never block). It assumes that SEQ# satisfies this partial correctness constraint (+ some other predicate logic constraints given here as axioms).
• The second theorem theorem is similar, but for total correctness It assumes that SEQ# satisfies this total correctness constraint.
• A decomposition of total correctness is also proved directly for two processes this theorem. (An alternative proof would specialize the theorem for n processes with n = 2.) This theorem is instantiated for the proof of FindPos.

The application Sieve

• defines the one algorithm Rem# that will instantiate SEQ# from the generic theory. The corresponding instance of SPAWN# is the full SIEVE algorithm.
• The specification also defines suitable instances of preconditions, relies, invariants etc.
• The instantiated specification has proof obligations that justify that Rem# is correct, and that the predicate logic side conditions are ok.
• The toplevel specification just contains the main correctness theorem. Given the result of the decomposition theorem, it is easy to prove.

• defines the two algorithms SEARCH-EVEN and SEARCH-ODD for searching the even and odd indices and their parallel composition FINDP (with an assignment at the end, that computes the result).
• Again the instantiated specification has proof obligations that justify that the correctness of the parallel composition can be decomposed into some predicate logic goals, plus two main proofs of RG assertions for SEARCH-EVEN and SEARCH-ODD.
• Finally, the correctness of the parallel composition is used to prove the main theorem in the toplevel specification.

[Imprint] [Data Privacy Statement] [E-Mail]