Lecture 9: Liveness under Compassion A. PnueliLiveness Under General FairnessNext, we will consider methods for proving response properties under generalfairness. This means that, in addition to justice requirements, we should alsoconsider the presence of compassion requirements.Deductive Verification of Reactive Systems, NYU, Fall, 2007 213Lecture 9: Liveness under Compassion A. PnueliTwo Types of FairnessRecall the two types of fairness that were traditionally introduced into the formalmodel ofreactive systems:• Weak fairness (Justice):• If transition τ is continuously enabled, it must be taken infinitely many times.• Equivalently, there must be infinitely many states at which τ is disabled ortaken.• Guarantees that every concurrent process will eventually progress.• Strong fairness (Compassion):• If transition τ is infinitely often enabled, it must be taken infinitely many times.• Guarantees that competition on a shared resource is arbitrated in a fair way.Deductive Verification of Reactive Systems, NYU, Fall, 2007 214Lecture 9: Liveness under Compassion A. PnueliIn the Model of Fair Discrete Systems (FDS)This has been abstracted as follows:• . . .• J = {J1, . . . , Jk} A set of justice (weak fairness) requirements.Ensure that a computation hasinfinitely many Ji-states for eachJi, i = 1, . . . , k.• C = {hp1, q1i, . . . hpn, qni} A set of compassion (strong fairness)requirements.Infinitely many pi-states imply infinitely many qi-states.Note that a justice requirement J can be obtained as a special caseof a compassion requirement(1, J).Question: Why do we need both types?Deductive Verification of Reactive Systems, NYU, Fall, 2007 215Lecture 9: Liveness under Compassion A. PnueliAnswer: Justice is Easy, Compassion isComplexThis used to be the consensus, manifested in modelcheckingand deductive verification.In this presentation, we claim that this is not necessarilythe case, and illustrate it on the process ofdeductiveverification.Deductive Verification of Reactive Systems, NYU, Fall, 2007 216Lecture 9: Liveness under Compassion A. PnueliVerifying Response Under JusticeRule J-WELLFor a well-founded domain (A, )assertions p, q,ϕ, h1, . . . , hn,justice requirementsJ1, . . . , Jn,and ranking functionsδ1, . . . , δn: Σ 7→ AJ1. p ⇒ q ∨ϕJ2.ϕ⇒n_j=1hjJ3.ϕ∧ ρ ⇒ q0∨ϕ0For i = 1, . . . , nJ4. hi∧ ρ ⇒ q0∨ (h0i∧ δi= δ0i) ∨n_j=1(h0j∧ δi δ0j)J5. hi⇒ ¬Jip ⇒ q— — Easy!!!Deductive Verification of Reactive Systems, NYU, Fall, 2007 217Lecture 9: Liveness under Compassion A. PnueliResponse Under General Fairness (Legacy)Rule F-WELL [MP91]For a well-founded domain A : (W, ),assertions p, q,ϕ, h1, . . . , hn,fairness requirements F1, . . . , Fn∈ J ∪ C,and ranking functions δ1, . . . , δn, where each δi: Σ 7→ AF1. p ⇒ q ∨ϕF2.ϕ⇒Wnj=1hjF3.ϕ∧ ρ ⇒ q0∨ϕ0For i = 1, . . . , nF4. hi∧ ρ ⇒ q0∨ (h0i∧ δi= δ0i) ∨Wnj=1(h0j∧ δi δ0j)F5. If Fi= (pi, qi) ∈ C thenC5. hi⇒ ¬qiC6. (D\{(pi, qi)}) |= (hi⇒ (pi∨ ¬hi)Otherwise (Fi= Ji∈ J ),J5. hi⇒ ¬Jip ⇒ q— — Complex, Recursive!!!Deductive Verification of Reactive Systems, NYU, Fall, 2007 218Lecture 9: Liveness under Compassion A. PnueliSo What’s New? A Flat Rule for CompassionRule C-WELLFor a well-founded domain (A, )assertions p, q,ϕ, h1, . . . , hn,compassion requirements(p1, q1), . . . , (pn, qn),and ranking functionsδ1, . . . , δn: Σ 7→ AW1. p ⇒ q ∨ϕW2.ϕ⇒n_j=1(pj∧ hj)W3.ϕ∧ ρ ⇒ q0∨ϕ0For i = 1, . . . , nW4. hi∧ ρ ⇒ q0∨ (h0i∧ δi= δ0i) ∨n_j=1(p0j∧ h0j∧ δi δ0j)W5. hi⇒ ¬qip ⇒ qRepresent Justice as degenerate compassion.Deductive Verification of Reactive Systems, NYU, Fall, 2007 219Lecture 9: Liveness under Compassion A. PnueliExample: Program COND-TERMConsider the following program COND-TERM:x, y : natural init x = 0`1: while y > 0 do`2: x := {0, 1}`3: y := y + 1 − 2x`4:Prove the response property at−`1⇒ at−`4under the compassionrequirement(at−`3∧ x = 0, 0), implying that x can assume the value 0 at location`3only finitely many times.Consider the following rank-abstracted version of this program:X, Y : {0, 1} init X = 0 D : {−1, 0, 1}Compassion (at−`3∧ X = 0, 0), (D < 0, D > 0)`1: while Y = 1 do`2: X := {0, 1}`3: (Y, D) := if X = 0 then (1, 1)elfe Y = 1 then {(1, −1), (0, −1)}else (0, 0)`4:Deductive Verification of Reactive Systems, NYU, Fall, 2007 220Lecture 9: Liveness under Compassion A. PnueliModel Checking + Helpful Assertions ExtractionWishing to verify init ⇒ g.X := States reachable from an init-state by a g-free path.d := 0Repeat until X stabilizes1. Decompose X into MSCC’s.2. Let C be a terminal MSCC.3. If C is compassionate — construct a counter example.4. Otherwise, ∃ a compassion requirement (p, q) ∈ C s.t. Ccontains a p-state but no q-state.5. d := d + 1; Fd:= (p, q); hd:= kCk.6. X := X − (C ∩ kpk)If X = ∅ then property is valid and the auxiliary constructs provide adeductive proof.Deductive Verification of Reactive Systems, NYU, Fall, 2007 221Lecture 9: Liveness under Compassion A. PnueliIllustrate on Abstract COND-TERMF3: (D < 0, D > 0) `2; F5: (1, ¬at−`2)`1, Y : 0; F1: (1, ¬at−`1)`4`1, Y : 1, D : −1`3, Y : 1, X : 0`1, Y : 1, D : 1; F6: (1, ¬at−`1)`3, Y : 1, X : 1; F4: (1, ¬at−`3)F2: (at−`3∧ X = 0, 0)Deductive Verification of Reactive Systems, NYU, Fall, 2007 222Lecture 9: Liveness under Compassion A. PnueliPending States`3, Y : 1, X : 1`2`1, Y : 0; F1: (1, ¬at−`1)`1, Y : 1, D : −1`3, Y : 1, X : 0`1, Y : 1, D : 1Deductive Verification of Reactive Systems, NYU, Fall, 2007 223Lecture 9: Liveness under Compassion A. PnueliRemoving K1F2: (at−`3∧ X = 0, 0)`2`1, Y : 1, D : −1`3, Y : 1, X : 0`1, Y : 1, D : 1`3, Y : 1, X : 1Deductive Verification of Reactive Systems, NYU, Fall, 2007 224Lecture 9: Liveness under Compassion A. PnueliRemoving K2F3: (D < 0, D > 0) `2`1, Y : 1, D : −1 `1, Y : 1, D : 1`3, Y : 1, X : 1Deductive Verification of Reactive Systems, NYU, Fall, 2007 225Lecture 9: Liveness under Compassion A. PnueliRemoving K3`3, Y : 1, X : 1; F4: (1, ¬at−`3)`2`1, Y : 1, D : 1Deductive Verification of Reactive Systems, NYU, Fall, 2007 226Lecture 9: Liveness under Compassion A. PnueliRemoving K4`2; F5: (1, ¬at−`2)`1, Y : 1, D : 1Deductive Verification of Reactive Systems, NYU, Fall, 2007 227Lecture 9: