This project defines the major nonblocking progress properties wait-freedom, obstruction-freedom and lock-freedom in Rely-Guarantee Interval Temporal Logic (RGITL), as described in the journal article submitted to the ITL special issue of AMAI 2012. A preliminary version of this article can be found here. In particular, it proofs a decomposition theorem for the global progress property of lock-freedom, which is based on a rely-guarantee decomposition theorem that is also derived in KIV (see below).
The aim of the project is to highlight the core correctness arguments of the RG theorem (Theorem 6 in the paper), and of the decomposition theorem of lock-freedom (Theorem 7). Additional predicates (e.g., for invariants or pre- postconditions) and possible reductions, which might be useful for applications of these theorems, are deliberately not considered here (hence, ``stream-lined version''). You can start by having a look at the specification structure of the KIV-project spec-overview. The relation of these KIV-specifications w.r.t. the definitions and theorems / lemmas in the paper, is described below.
Both wait-freedom and obstruction-freedom are defined as contracts for a generic procedure OP# that works on a generic state S. This corresponds to definitions (30) and (31) in the paper. The definitions typically assume safety conditions Rely(m, S', S'') to be met by OP#(m; S)'s environment at all times. These are established by rely-guarantee reasoning. Specification RG-Conds defines the corresponding local RG conditions (in particular, the RG contract for one individual OP as the axiom "op-rg") and in specification RG-Theorem, one can find the RG decomposition proof SPAWN-sust-rg that the local RG conditions are sufficient to establish RG globally, according to Theorem 6 in the paper. Both RG reasoning and the definition of lock-freedom takes the unfair interleaving of an arbitrary number of procedures OP# into account. This interleaving is recursively defined in the overall system SPAWN#, corresponding to Fig. 5 in the paper. The global RG conditions are defined in specification RGto-act.
Lock-freedom requires that at all times, eventually one of the interleaved operations progresses (by setting its activity flag from true to false). The main decomposition of lock-freedom (Theorem 7 from the paper), is shown in theorem SPAWN-is-lockfree in KIV (in specification Lockfreedom-Theorem), corresponding to (32) in the paper. The necessary strengthening of RG conditions to include the activity function is also defined in specification RGto-act. The global progress follows from sufficient local termination conditions, defined in specification Lockfree-Conds as temporal contracts for the abstract procedure OP#. This corresponds to formulas (33) and (34) in the paper.
The main lemmas of the decomposition proof from Appendix C, are as follows. Lemmas 1 and 2 from the paper, correspond to lemmas SEQ-progress and SEQ-progress-plus-rg in KIV, respectively. The central lifting Lemma 3 corresponds to lockfree-main in KIV. Lemma 4 from the paper is lemma progress-1-notrg-ev-2 in KIV. (The symmetric case is shown in lemma progress-2-notrg-ev-1.) Finally, Lemma 5 from the paper is shown in KIV-lemma notrg-ev-1-2.