Applications of RGITL

This page gives an overview of some applications of the temporal logic framework Rely-Guarantee Interval Temporal Logic (RGITL), which is implemented in KIV. The logic can be applied to verify decomposition theorems, e.g., rely-guarantee (RG) rules, as well as to apply these theorems to prove specific concurrent algorithms correct. The proofs typically address both safety and liveness properties.

Global Decomposition Theory

The global decomposition theory defines a rely-guarantee theorem which lifts proof obligations about non-interleaved executions to invariants of the overall (interleaved) system. Furthermore, a decomposition theorem for linearizability respectively lock-freedom is defined. Linearizability is a major correctness condition for concurrent algorithms which ensures that all operations appear to take affect atomically between their invocation and response. Lock-freedom is a global progress condition of non-blocking algorithms which ensures global progress even if single processes fail. Here is a graphical overview of the KIV project RGI-Global that specifies and verifies these theorems.

• The concurrent system model is defined in specification CSPAWN. It is based on a generic behavior of single processes (CSEQ), which can terminate or execute finitely or infinitely often skip steps or a generic interface procedure COP. This procedure accesses the overall program state CS which abstracts all process-local states and the process-shared state.
• The rely-guaratee proof obligations refer to executions of COP only and are specified in RG-Conds. The lifting of these properties to global invariants of CSPAWN is shown in specification RG-Theorem.
• We also define an abstract concurrent system ASPAWN where processes execute an abstract procedure AOP on an abstract state AS. The refinement proof between CSPAWN and ASPAWN then ensures that the concrete system CSPAWN is linearizable Refine-Theorem. It is based on the refinement proof obligation between COP and AOP which is defined in specification Refine-Conds. Note that the refinement theorem for COP and AOP may assume the invariants established by the rely-guarantee theory.
• The improved theory of nonblocking properties includes termination conditions for wait-freedom, lock-freedom and obstruction-freedom. In particular, the termination proofs of lock-freedom (and obstruction-freedom) use an additional predicate unchanged, which describes interference freedom. These termination proofs ensure that the nonfairly interleaved system always progresses, i.e., some operation always eventually becomes inactive Lockfreedom-Theorem (cf. to this project overview for a previous version of lock-freedom decomposition).
• Here is the previous version of the full decomposition theory as described in papers [FAC09] and [MPC10] theory old.

Local Instances of the Global Decomposition Theory

We define several instances of the global theory, which permit to better exploit the symmetry of concrete concurrent algorithms by splitting the overall program state CS into its process-local and global parts. Specifications can then consider only a small fix number (two or three) of process-local states which represent the entire system, instead of quantifying over all local states. These instances introduce a new disjointness predicate "Disj" to describe disjointness properties between two local states (such properties are defined in predicate "Inv" in the global theory). In the following, we present three such instances in an increasing order of expressiveness.

• Local instance L-I allows specifications to consider at most two processes (with local states LS and LSQ). The resulting simpler local proof obligations for rely-guarantee reasoning, linearizability and lock-freedom are contained in specifications Local-RG-Conds, Local-Refine-Conds and Local-Lockfree-Conds respectively. The mapping of the local predicates to corresponding predicates of the global theory is defined in specifications Local-Imp-Global-RG, Local-Imp-Global-Refine and Local-Imp-Global-Lockfree. These specifications also contain the proofs that the new local proof obligations are indeed an instance of the global ones (cf. the corresponding theorem base summaries).
• Local instance L-II simply extends the first instance L-I with process identifiers, which are part of each process-local state.
• Local instance L-III extends the second instance L-II by allowing rely conditions to consider the local state of the other process as well. As a consequence, the local proof obligations now have to consider three local states.

Case Studies

We have applied the theory above to prove memory-safety, linearizability and lock-freedom of several concurrent stack and queue algorithms. The algorithms either run in an environment with support for automatic garbage collection GC (hence memory leaks are avoided by GC) or they apply a memory reclamation scheme to avoid memory leaks (e.g., a global pool of reusable memory locations or hazard pointers). All case studies are based on a generic theory of heap paths "path-reachable" from the KIV library with basic data types KIV library.

In the table below, the first column is the underlying algorithm; column Overview gives a graphical overview of all specifications of a case study; the algorithms, verification conditions and the actual proofs (rely-guarantee, linearizability, lock-freedom, optionally absence of leaks) of a case study are reachable from columns Algos, VCs and Proofs respectively. The first row for instance describes the verification of a simple version of Treiber's non-blocking stack algorithm under GC using the global theory (RGI-Global), whereas the second row describes the verification of a similar algorithm under GC, using a local instance (L-I), which allows for simpler specifications (that do not quantify over all process identifiers).

[1] This is the refined version of "LStack-FreeSet", where the algebraic free-set is replaced by a (further) free-stack implementation for custom memory management. Moreover, the modification counter is incremented with the removal of a stack-node only.

[2] This is the refined version of "LStack-HazardPointers", where read and write operations on hazard pointer entries are non-atomic, as specified in NA-RW.

The stack verification (GStack-GC) has been published in [FAC09] (linearizability); the queue algorithm (GQueue-GC) in [FAC09] (linearizability) and [MPC10] (lock-freedom); the stack with hazard pointers (LStack-HazardPointers) in [ICTAC11] (memory-safety, linearizability, lock-freedom, wait-freedom of scan-operation).

Here you can find all our publications and an overview of all KIV projects. For general informations about KIV or download please refer to this page.

Bibliography

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