Proofs of Starvation Freedom

The proofs are organized in five KIV projects:

• The first project gives a starvation freedom proof for the Ticket Lock using an encoding of the algorithm as a transition system and global reasoning with a ranking function. It is based on a rule that adapts rule WELL-JP as defined in [MannaPnueli96] to our setting. The project also mechanizes the proof of correctness of this rule in RGITL.
• The second project defines a novel thread-local proof method for starvation freedom based on rely-guarantee reasoning and a waitsFor-Relation.
• The third project verifies that the Ticket Lock algorithm is starvation free using the thread-local proof method.
• The fourth and fifth project verify that the MCS-Queue Lock and the Filter Lock are starvation free using the same proof method.

In addition to starvation-freedom all proofs also imply mutual exclusion (simply because the invariants assert it). The global proof method simply used skip as critical section. As a small extension, the thread-local proofs instead use an anonymous program as critical section, that is shown to be linearizabile to an abstract operation, if it sequentially implements the abstract operation (simply because of mutual exclusion). The extension makes a few additions to the invariants, rely's and guarantee's necessary that are not described in the paper.

All projects make lots of use of the principle of theory instantiation:

• First a specification CONDS is defined, which gives proof obligations for a certain property (e.g. starvation freedom) as axioms.
• The theory is then often enriched to a specification THEOREM with definitions needed in the theorem, but not in the conditions (e.g. the proof obligations talk about one process, the enrichment defines the parallel program).
• The property itself (starvation freedom) is proven to be a theorem of the enriched specification.
• The abstract theory (CONDS and THEOREM) typically uses anonymous procedures and a type "state" or similar, and just has constraints on these (e.g. constraints on abstract Rely and Guarantee predicates) that are sufficient to prove the theorem.
• The theory is then instantiated with the notions of the case study: the anonymous procedure is mapped to the concrete algorithm, and "state" is mapped to the tuple of variables used in the algorithm. The Rely and guarantee predicates are instantiated with formulas specific for the algorithm. In the instantiated theory the axioms of CONDS become proof obligations. Proving them implies that the main theorem (e.g. starvation freedom) from THEOREM holds for the instance of the case study.

Global Theory and Proof of Starvation Freedom for Ticket Lock

• Specification Manna-Pnueli-WELL-JP gives as axioms the proof obligations J1 to J4 described in the [IFM 16] paper. As in [Manna Pnueli06] the rule is parameterized with a parameter "pm:param", that is instantiated to the type of process id's for the case study. The theory assumes a transition relation τ(p)(s,s0) for each process p, and their union as a transition relation τ(s,s0) for the whole parallel System. It defines intermedate assertions φ(p, j, pm) and ranking functions δ(p, j) for j = 0..m. That these imply the leadsto-theorem (which uses P,Q instead of φ, ψ in [IFM 16]) is proved using an until-lemma, which is provable with well-founded induction over the ranking function. As a remark, the theory currently uses a specific well-founded order as needed by the case study. It could of course be generalized to any well-founded order.
• The encoding of the algorithm as a transition system is given in specification TicketLock-COP, where COP(p,cj) is an individual transition of process p.
• The invariant of the case study consists of the clauses as given in the paper.
• Finally the theory is instantiated with the case study, and the proof obligations J1, J2, J3, J4 are discharged.

Theory for Thread-Local Proofs of Starvation Freedom

• The theory is based on rely-guarantee proof obligations. These are formulated here for an anonymous procedure COP that gets the process id "n" (a natural number) and some input "Inp", modifies some state "CS" of type cstate, and produces output "Outp". The main proof obligation is that COP satisfies a rely guarantee condition using the guarantee "Guar(m,...)", a rely "Rely(m,...)", and an Invariant "Inv". The computation starts and finishes in a state CS with Idle(m,CS).
• The axioms correspond to the premises of the rely-guarantee rule in [IFM 16] (already reduced to one operation OP_p). Input and output is suppressed in [IFM 16], as it is empty in the case studies. The notation in the paper is OP_p,R_p, G_p, I_p and idle_p for a process p instead of COP(m, ....), Rely(m,...), Guar(m, ...), Inv(m, ...) and Idle(m,..) here.
• The conclusion of the rely guarantee rule in the paper is proven as the main theorem for a procedure CSPAWN, which calls CSEQ. "CSPAWN" and "CSEQ" are written as "Par" and "Seq" in [IFM 16]. Since RGITL has a binary operator for weak-fair interleaving of processes only, running N processes in parallel is done in CSPAWN by spawning N processes recursively (if* and calls do not consume time, so all of processes start simultaneously).
• The proof of the theorem can be reduced to the case of N = 2 by induction over N. The essential argument for the case N = 2 is a basic theorem that says: "interleaving two rely-guarantee properties gives a system, which satisfies a rely-guarantee property again". The theorem uses "R -+-> G" as an abbreviation for "not (R until not G)" ("the guarantee is not violated before the rely", (cf. the expanded version of the rely-guarantee formula in [IFM 16]).
• The proof assumes the side conditions of the rely-guarantee rule for the case N = 2. These are encoded as predicate RG-restr that is defined in the specification.
• The theorems proved include several more theorems (named RG-Sound...), that show that rely-guarantee reasoning is sound for unfair interleaving (operator "∥nf") and for total correctness (which strengthens the RG property with "□ R → ◇ last") instead of partial correctness too. For more details on how such proofs work and the basic compositionality principle involved that allows to replace programs with their properties, see [RGITL14] (Section 7 specifically elaborates on rely-guarantee properties).

• The proof of the thread-local starvation freedom proof method imports the rely-guarantee results. Its theories have a similar structure than the ones for rely-guarantee.
• The proof obligations are given as axioms in specification Starvation-Free. Predicate W(m,n) is written waitsFor(p,q) in [IFM 16]. P(m) is short for "W(m) = ?" in the paper. The proof of the main theorem (note that "□ ◇ (¬ Act(m) ∧ Idle(m, CS))" trivially implies "□ (Act(m) → ◇ ¬ Act(m))") is more complex this time, there are two main difficulties.
• The first difficulty is reasoning over finiteness as exemplified e.g. by lemma never-empty-lem-3 (and similarly named lemmas of the theorem base). This lemma states: "if after some steps there is always some process in set ts0 with an empty waitset, then there is a process m0, that is always in ts0 and infinitely often has an empty waitset", which encodes one of the arguments of the proof in [IFM 16].
• The second difficulty is that we must again transfer properties that are establised for the run of a single process to properties of global runs of the system. This time the properties are of the form "□ ◇ P" (for rely-guarantee the form was R -+-> G; such a property is now already assumed in the proofs), and the property is now known for a single process only. Induction again reduces the case of N processes to the case of two.
• The two crucial lemmas are now that a formula "□ ◇ P" propagates from the left process to the interleaved system and the the (almost) opposite "◇ □ (¬ P ∧ ¬ last)" propagates out of interleaving too. Both lemmas assume, that P is stable over rely steps of the left process as encoded by the definition of P-restr in the specification (an invariant I for all states is assumed to hold) .

Thread-Local Proof of Starvation Freedom for Ticket Lock

• The Ticket lock algorithm is now directly given as a program named LTL. Atomic instructions are parallel assignments (separated with a comma), the tests of conditionals and while loops.
• The algorithm calls an anonymous Operation COP (note that this COP has nothing to do with the COP used in the generic theory) that works on some arbitrary concrete state C (disjoint from Served, Next and Lnext) instead of just doing a skip. This allows to include a linearizability argument in the proof: We assume that sequential runs of COP data refine an abstract operation AOP. This can be expresses as a contract. The diamond brackets state total correctness, and the fact that only sequential runs establish termination and the postcondition is encoded via the trivial rely condition C' = C'' (guarantee and invariant are both just true). abs is the abstraction relation from concrete to abstract states.
• We assume that initially, when CSPAWN starts to run, an abstract state a with abs(C,a) exists. The rely-guarantee proof then shows (via mutual exclusion), that an abstract state with abs(C,a) exists every time COP is called, and that during the run no other process changes C. Therefore we can apply the contract in the main RG proof. This establishes that a state a0 with abs(C,a0) and AOP(a,a0) exists again after the call of COP, implying that the call linearizes to a call of AOP (for a full proof we could embed into the framework for linearizability we defined earlier, by replacing act := true/false with adding an invoke/response event).
• The addition of linearizability adds a few new clauses to the rely's and invariants that are not given in [IFM 16]. Essentially we have add to the invariant: "If no one holds the lock then abs(C,a) holds for some a" and in the rely of process p "If the environment transfers the lock to p, then abs(C,a) holds for some a". and "if p holds the lock, then it can rely on C not being changed".
• The Rely, Guarantee, Inv and W predicates for the Ticket-Lock are defined in this specification.
• The generic rely-guarantee theory is instantiated, which gives the rely-guarantee condtion as proof obligations . The main proof steps through the algorithm by symbolic execution until it reaches the spin loop (first red node 14), where an invariant rule is applied. It then continues with the loop body until the call of COP is reached, where it splits the compound of "COP" and "Served := Served + 1" into two two goals (node 29). The right goal is for the final assignment and closes after one step. The left goal finally inducts over the number of steps necessary for COP to finish (second red node 31). Since the rely C' = C'' holds due to mutual exclusion the induction hypothesis is applicable after one step (node 60).

• Finally, the generic starvation-freedom theory is instantiated, which again gives proof obligations. The main proof for starvation freedom again steps through the algorithm until it reaches the loop. There the precondition is weakened to an invariant of the loop (by applying the cut rule at node 8 and 9, then weakening the formulas which are too strong at node 12). The proof then inducts over the number of steps needed to reach an empty waitset (red node 13). Then it splits into a branch where Served = Lnext(p), so the spin loop is left immediately (branch above node 17) and one, where after the two steps of executing one loop iteration (one step for the while-loop test, another for the loop body=skip) the induction hypothesis is applied at node 141. The left branch continues to the call of COP. By exploiting that the contract implies termination, an induction over the steps needed for COP to terminate (started at node 80, induction hypothesis applied at node 88) finally closes the goal. The branch above node 37 shows, that the rely "C' = C''" is never violated in the critical section. The (indirect) proof derives a contradiction from the assumption, that there is a minimal number N of steps, after which "C' ≠ C''" (by induction over N at node 40).

Thread-Local Proof of Starvation Freedom for MCS-Queue Lock

• The MCS-queue lock algorithm is defined as program LMCS here. It calls ACQUIRE and RELEASE subprograms. The program works on a heap of preallocated cells, one per process. The reference to the cell of process m is stored in local variable S. Accessing the heap with hp[S] gives the cell of the process. Each cell qn is of type qnode: It has a boolean qn.locked field, and a qn.nxt reference.
• The algorithm uses an an abstract queue q (a list of processes) as auxiliary variable that abstracts from the current pointer based queue. This makes it easy to determine the waiting processes and their order, without having to look into the local variables of each process.
• The instances of the predicates for the case study are given in this specification. The wait-predicate is a disjunction now. The first clause gives the case, where the process has to wait in RELEASE, the second is for the spin loop in ACQUIRE. Predicate mcs-queue connects the auxiliary abstract queue with the concrete one used by the algorithm.
• The rely-guarantee proof obligations are again created by instantiating the generic theory. The arguments are similar to the one for the TicketLock, though lengthier, since more complex predicates are involved. The main rely-guarantee proof therefore uses a lemma for the "COP;RELEASE"-part of the code, which in turn uses another lemma just for the RELEASE call.

• The proof obligations for starvation freedom are also created by instantiating the generic theory. They now are a bit easier than the RG proofs, since there are no complex side goals for guarantees. The main proof (COP-starvation-free) now uses the fact that the waitset must eventually become empty twice, once (red node 50) for the spin loop of acquire, and once (red node 375) for the spin loop of release. Induction is also needed (as before for TicketLock) for the number of steps the abstract COP needs to terminate (red node 349).

Thread-Local Proof of Starvation Freedom for Filter Lock

• The FilterLock algorithm is defined as program LFL. The current process is M, Level[M] stores the level of process M. The victim of level L is stored in the Victim-Array as Victim[L]. An auxiliary boolean variable LWait is used to mark the code section where the algorithm waits on each level. Local counter LK is used to iterate level checks for all processes. The algorithm assumes that the processes running are numbered from 0 to ProcNo (as spawned by CSPAWN), so we have ProcNo+1 processes. An entry of ProcNo+1 in the victim array signals "no victim" (the original algorithm runs processes 1 ... ProcNo and uses 0 for "no victim"). Level[M] = 0 indicates, that process M does not want to get the lock. The algorithm is slightly simplified compared to the standard one by using coarser grained atomic instructions. In particular it executes climbing one level, and setting itself as victim on the new level one atomic instruction Level[M] := Level[M] + 1, Victim[Level[M] + 1] := M, while the original algorithm does these two assignments in two steps. Without this simplification an extension of the method is needed, that deals with processes q, that "catch up" to the level of the current process p (by executing the first of the two assignments). Such a process will definitely free p from any waiting as soon as it executes the second assignment. A less important simplification is, that an if* (instead of if) is used that executes the level test (a conjunct) and the next assignment in a single step. Changing this to several steps (e.g. one for each conjunct, and one for the assigment) would require an auxiliary variable that characterizes which ones of the individual tests have been executed.
• The instances of the predicates for the case study are given in this specification. The waitsFor-predicate W(p) now becomes true on each level while the process is in the code section where wait(p) = true, while it is still the victim and while it still can find a process in the loop, it has to wait for.
• The rely-guarantee proof obligations are again created by instantiating the generic theory. The main rely-guarantee proof is split into two layers. A first lemma establies prediates "Rely" and "Guar" as Rely and Guarantee. This proof is already sufficient for mutual exclusion. A second lemma establies an additional guarantee "GuarW" assuming "Rely" and "RelyW" as rely predicates. "GuarW" and "RelyW" encode the critical information necessary to establish that waitset are decreasing (when nonempty). The proofs are suimilar to the previous rely-guarantee proofs. Each time symbolic execution reaches the same code as before the induction hypothesis can be applied (diagonal arrows), since the number of steps necessary to reach an assumed violation of the guarantee has decreased.

• Among the proof obligations for starvation freedom, the proof for main one now uses several levels of induction due to several nested loops being present. A structural induction (node 17) is used for the outer loop (inducting over the distance of the current level Level[M] to the maximal one ProcNo+1). A second induction is needed for the number of steps to reach an empty Waitset, when the waiting loop is reached (node 81). The induction is followed by an induction over the number of processes that still need to be checked in the waiting loop (distance of counter LK to ProcNo +1) at node 84. The leftmost branch above node 18 deals with the call of COP in the critical section (as before). Note that the first and the third induction use local well-founded arguments to argue progress. Using a global rank function would make it necessary to map all these arguments into a single global rank function. The second and third induction use the lazy induction scheme described in [RGITL 14], Section 6.4. This results in the diagonal blue arrows from the place where the induction hypothesis is applied back to goal which is used as induction hypothesis. Green diagonal arrows use a goal proven in one branch to prove the same goal in another branch. This allows to save the definition of auxiliary lemmas.

Back to the overview of all KIV projects.
For general informations on the KIV system and where to download it refer to this page.

Bibliography

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