This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| ren-invFLITPSCWRITE | ⊦ ren(invFLITPSCWRITE(t, l, v), ags, alsf) = AInvWrite(t, l, v) | An Axiom |
| step-absstep-W4-W5-tau-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W4, pcf0(t) = W5, apcf(t) = apc, notMember(t, gs.readers) ∧ oneMember(t, ls.l, gs.writers) ∧ onePendingW(t, ls.l, gs.p), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ onePendingW(t, ls0.l, gs0.p) ∧ FOFollowsW(t, gs0.p(ls0.l)), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, W4, pwbPSC(t, l)) ∧ gs0 = gstepf(gs, ls, W4, pwbPSC(t, l)) ∧ ls0 = lstepf(gs, ls, W4, pwbPSC(t, l)) ∧ W5 = pcstepf(gs, ls, W4, pwbPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| ren-ctrIncPSC | ⊦ ren(ctrIncPSC(t, l), ags, alsf) = τ | An Axiom |
| step-absstep-R1-R2-doReadPSC-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R1, pcf0(t) = R2, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ oneMember(t, ls0.l, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, ADoRead(ls.t)) → ags0 = gstepf(ags, als, apc, ADoRead(ls.t)) ∧ als0 = lstepf(ags, als, apc, ADoRead(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, ADoRead(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))) ∧ gs0 = gstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))) ∧ ls0 = lstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))) ∧ R2 = pcstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = invRead ∧ ls.l = als.il ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| ren-callPSCCOMPLETE | ⊦ ren(callPSCCOMPLETE(t), ags, alsf) = callTSync(t) | An Axiom |
| step-absstep-W6-W7-tau-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W6, pcf0(t) = W7, apcf(t) = apc, notMember(t, gs.readers) ∧ oneMember(t, ls.l, gs.writers) ∧ noPending(t, gs.p), notMember(t, gs0.readers) ∧ notMember(t, gs0.writers) ∧ noPending(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, W6, ctrDecPSC(t, l)) ∧ gs0 = gstepf(gs, ls, W6, ctrDecPSC(t, l)) ∧ ls0 = lstepf(gs, ls, W6, ctrDecPSC(t, l)) ∧ W7 = pcstepf(gs, ls, W6, ctrDecPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| gabs-def | ⊦ gabs(gs, lsf, pcf, ags, alsf, apcf) ↔ ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p) | An Axiom |
| step-absstep-idle-ready-callPSCRUN-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = idle, pcf0(t) = ready, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p) ∧ noPending(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, callARun(ls.t)) → ags0 = gstepf(ags, als, apc, callARun(ls.t)) ∧ als0 = lstepf(ags, als, apc, callARun(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, callARun(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, idle, callPSCRUN(ls.t)) ∧ gs0 = gstepf(gs, ls, idle, callPSCRUN(ls.t)) ∧ ls0 = lstepf(gs, ls, idle, callPSCRUN(ls.t)) ∧ ready = pcstepf(gs, ls, idle, callPSCRUN(ls.t)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = idle ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []) ⊦ pre(ags, als, apc, callARun(ls.t)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = ready ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags0.h | l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-PSCCRASH-globalPSCCRASH | FLITPSCInv(gs, lsf, pcf), FLITPSCInv(gs0, lsf0, pcf0), PLIBInv(ags, alsf, apcf), flitpscStep(mkstate(gs, lsf, pcf), globalPSCCRASH, mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ ∃ ags0, alsf0, apcf0. plibStep(mkstate(ags, alsf, apcf), globalACrash, mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) | A Proof Obligation |
| step-absstep-W2-W3-tau-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W2, pcf0(t) = W3, apcf(t) = apc, notMember(t, gs.readers) ∧ notMember(t, gs.writers) ∧ noPendingW(t, gs.p) ∧ noPending(t, gs.p), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ noPending(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, W2, ctrIncPSC(t, l)) ∧ gs0 = gstepf(gs, ls, W2, ctrIncPSC(t, l)) ∧ ls0 = lstepf(gs, ls, W2, ctrIncPSC(t, l)) ∧ W3 = pcstepf(gs, ls, W2, ctrIncPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = invWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| step-absstep-ready-R1-invFLITPSCREAD-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = ready, pcf0(t) = R1, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, AInvRead(ls.t, l0)) → ags0 = gstepf(ags, als, apc, AInvRead(ls.t, l0)) ∧ als0 = lstepf(ags, als, apc, AInvRead(ls.t, l0)) ∧ apc0 = pcstepf(ags, als, apc, AInvRead(ls.t, l0)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, ready, invFLITPSCREAD(ls.t, l0)) ∧ gs0 = gstepf(gs, ls, ready, invFLITPSCREAD(ls.t, l0)) ∧ ls0 = lstepf(gs, ls, ready, invFLITPSCREAD(ls.t, l0)) ∧ R1 = pcstepf(gs, ls, ready, invFLITPSCREAD(ls.t, l0)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = ready ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []) ⊦ pre(ags, als, apc, AInvRead(ls.t, l0)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = invRead ∧ ls0.l = als0.il ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags0.h | l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-PSCPERSIST_FO-tau | FLITPSCInv(gs, lsf, pcf), FLITPSCInv(gs0, lsf0, pcf0), PLIBInv(ags, alsf, apcf), flitpscStep(mkstate(gs, lsf, pcf), globalPSCPERSIST_FO(l), mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags, alsf, apcf)) | A Proof Obligation |
| ren-invFLITPSCREAD | ⊦ ren(invFLITPSCREAD(t, l), ags, alsf) = AInvRead(t, l) | An Axiom |
| ren-retFLITPSCWRITE | ⊦ ren(retFLITPSCWRITE(t), ags, alsf) = ARetWrite(t) | An Axiom |
| step-absstep-PSCPERSIST_W-globalPSCPERSIST_W | FLITPSCInv(gs, lsf, pcf), FLITPSCInv(gs0, lsf0, pcf0), PLIBInv(ags, alsf, apcf), flitpscStep(mkstate(gs, lsf, pcf), globalPSCPERSIST_W(l), mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ ∃ ags0, alsf0, apcf0. plibStep(mkstate(ags, alsf, apcf), globalAPersist(l), mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) | A Proof Obligation |
| ren-retFLITPSCREAD | ⊦ ren(retFLITPSCREAD(t, v), ags, alsf) = ARetRead(t, v) | An Axiom |
| step-absstep-W7-ready-retFLITPSCWRITE-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W7, pcf0(t) = ready, apcf(t) = apc, notMember(t, gs.readers) ∧ notMember(t, gs.writers) ∧ noPending(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ARetWrite(ls.t)) → ags0 = gstepf(ags, als, apc, ARetWrite(ls.t)) ∧ als0 = lstepf(ags, als, apc, ARetWrite(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, ARetWrite(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, W7, retFLITPSCWRITE(ls.t)) ∧ gs0 = gstepf(gs, ls, W7, retFLITPSCWRITE(ls.t)) ∧ ls0 = lstepf(gs, ls, W7, retFLITPSCWRITE(ls.t)) ∧ ready = pcstepf(gs, ls, W7, retFLITPSCWRITE(ls.t)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []) ⊦ pre(ags, als, apc, ARetWrite(ls.t)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = ready ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags0.h | l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-W7-ready-retFLITPSCWRITE-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W7, pcf0(t) = ready, apcf(t) = apc, notMember(t, gs.readers) ∧ notMember(t, gs.writers) ∧ noPending(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, ARetWrite(ls.t)) → ags0 = gstepf(ags, als, apc, ARetWrite(ls.t)) ∧ als0 = lstepf(ags, als, apc, ARetWrite(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, ARetWrite(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, W7, retFLITPSCWRITE(ls.t)) ∧ gs0 = gstepf(gs, ls, W7, retFLITPSCWRITE(ls.t)) ∧ ls0 = lstepf(gs, ls, W7, retFLITPSCWRITE(ls.t)) ∧ ready = pcstepf(gs, ls, W7, retFLITPSCWRITE(ls.t)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| ren-sfencePSC | ⊦ ren(sfencePSC(t), ags, alsf) = τ | An Axiom |
| step-absstep-W6-W7-tau-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W6, pcf0(t) = W7, apcf(t) = apc, notMember(t, gs.readers) ∧ oneMember(t, ls.l, gs.writers) ∧ noPending(t, gs.p), notMember(t, gs0.readers) ∧ notMember(t, gs0.writers) ∧ noPending(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W6, ctrDecPSC(t, l)) ∧ gs0 = gstepf(gs, ls, W6, ctrDecPSC(t, l)) ∧ ls0 = lstepf(gs, ls, W6, ctrDecPSC(t, l)) ∧ W7 = pcstepf(gs, ls, W6, ctrDecPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = resWrite ∧ (ls0.l = als.il ∧ ls0.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls0.t) | false = []) | A Proof Obligation |
| ren-globalPSCCRASH | ⊦ ren(globalPSCCRASH, ags, alsf) = globalACrash | An Axiom |
| step-absstep-ready-W1-invFLITPSCWRITE-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = ready, pcf0(t) = W1, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.readers) ∧ notMember(t, gs0.writers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, AInvWrite(ls.t, l0, v0)) → ags0 = gstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)) ∧ als0 = lstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)) ∧ apc0 = pcstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)) ∧ gs0 = gstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)) ∧ ls0 = lstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)) ∧ W1 = pcstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = ready ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| step-absstep-idle-ready-callPSCRUN-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = idle, pcf0(t) = ready, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p) ∧ noPending(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, callARun(ls.t)) → ags0 = gstepf(ags, als, apc, callARun(ls.t)) ∧ als0 = lstepf(ags, als, apc, callARun(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, callARun(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, idle, callPSCRUN(ls.t)) ∧ gs0 = gstepf(gs, ls, idle, callPSCRUN(ls.t)) ∧ ls0 = lstepf(gs, ls, idle, callPSCRUN(ls.t)) ∧ ready = pcstepf(gs, ls, idle, callPSCRUN(ls.t)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = idle ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| step-absstep-R3-R4-tau-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R3, pcf0(t) = R4, apcf(t) = apc, notMember(t, gs.writers) ∧ oneMember(t, ls.l, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, R3, pwbPSC(t, l)) ∧ gs0 = gstepf(gs, ls, R3, pwbPSC(t, l)) ∧ ls0 = lstepf(gs, ls, R3, pwbPSC(t, l)) ∧ R4 = pcstepf(gs, ls, R3, pwbPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = resRead ∧ ls0.v = als.ov ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags.h | l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-R2-R4-tau-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R2, pcf0(t) = R4, apcf(t) = apc, notMember(t, gs.writers) ∧ oneMember(t, ls.l, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ gs0 = gstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ ls0 = lstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ R4 = pcstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = []) ∧ (gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = resRead ∧ ls0.v = als.ov ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags.h | l) | ls0.t) | false = []) | A Proof Obligation |
| ren-doReadPSC | ⊦ ren(doReadPSC(t, l, v), ags, alsf) = ADoRead(t) | An Axiom |
| ren-callPSCRUN | ⊦ ren(callPSCRUN(t), ags, alsf) = callARun(t) | An Axiom |
| step-absstep-ready-ready-callPSCCOMPLETE-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = ready, pcf0(t) = ready, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, callTSync(ls.t)) → ags0 = gstepf(ags, als, apc, callTSync(ls.t)) ∧ als0 = lstepf(ags, als, apc, callTSync(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, callTSync(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, ready, callPSCCOMPLETE(ls.t)) ∧ gs0 = gstepf(gs, ls, ready, callPSCCOMPLETE(ls.t)) ∧ ls0 = lstepf(gs, ls, ready, callPSCCOMPLETE(ls.t)) ∧ ready = pcstepf(gs, ls, ready, callPSCCOMPLETE(ls.t)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = ready ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []) ⊦ pre(ags, als, apc, callTSync(ls.t)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = ready ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags0.h | l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-W2-W3-tau-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W2, pcf0(t) = W3, apcf(t) = apc, notMember(t, gs.readers) ∧ notMember(t, gs.writers) ∧ noPendingW(t, gs.p) ∧ noPending(t, gs.p), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ noPending(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W2, ctrIncPSC(t, l)) ∧ gs0 = gstepf(gs, ls, W2, ctrIncPSC(t, l)) ∧ ls0 = lstepf(gs, ls, W2, ctrIncPSC(t, l)) ∧ W3 = pcstepf(gs, ls, W2, ctrIncPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = invWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = invWrite ∧ (ls0.l = als.il ∧ ls0.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls0.t) | false = []) | A Proof Obligation |
| ren-globalPSCPERSIST_W | ⊦ ren(globalPSCPERSIST_W(l), ags, alsf) = globalAPersist(l) | An Axiom |
| ren-doWritePSC | ⊦ ren(doWritePSC(t, l, v), ags, alsf) = ADoWrite(t) | An Axiom |
| step-absstep-W5-W6-tau-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W5, pcf0(t) = W6, apcf(t) = apc, notMember(t, gs.readers) ∧ oneMember(t, ls.l, gs.writers) ∧ onePendingW(t, ls.l, gs.p) ∧ FOFollowsW(t, gs.p(ls.l)), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ noPending(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W5, sfencePSC(t)) ∧ gs0 = gstepf(gs, ls, W5, sfencePSC(t)) ∧ ls0 = lstepf(gs, ls, W5, sfencePSC(t)) ∧ W6 = pcstepf(gs, ls, W5, sfencePSC(t)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = resWrite ∧ (ls0.l = als.il ∧ ls0.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls0.t) | false = []) | A Proof Obligation |
| ren-pwbPSC | ⊦ ren(pwbPSC(t, l), ags, alsf) = τ | An Axiom |
| ren-ctrDecPSC | ⊦ ren(ctrDecPSC(t, l), ags, alsf) = τ | An Axiom |
| abs-def | ⊦ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ↔ gabs(gs, lsf, pcf, ags, alsf, apcf) ∧ (∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t))) | An Axiom |
| step-absstep-R2-R3-tau-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R2, pcf0(t) = R3, apcf(t) = apc, notMember(t, gs.writers) ∧ oneMember(t, ls.l, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ oneMember(t, ls0.l, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ gs0 = gstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ ls0 = lstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ R3 = pcstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = []) ∧ (gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| step-absstep-R2-R3-tau-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R2, pcf0(t) = R3, apcf(t) = apc, notMember(t, gs.writers) ∧ oneMember(t, ls.l, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ oneMember(t, ls0.l, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ gs0 = gstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ ls0 = lstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ R3 = pcstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = []) ∧ (gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = resRead ∧ ls0.v = als.ov ∧ (∀ l0. l0 ≠ ls0.l ∧ ¬ FO(ls0.t) ∈ gs0.p(l0) → ((ags.h | l0) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-R4-ready-retFLITPSCREAD-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R4, pcf0(t) = ready, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, ARetRead(ls.t, v)) → ags0 = gstepf(ags, als, apc, ARetRead(ls.t, v)) ∧ als0 = lstepf(ags, als, apc, ARetRead(ls.t, v)) ∧ apc0 = pcstepf(ags, als, apc, ARetRead(ls.t, v)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, R4, retFLITPSCREAD(ls.t, v)) ∧ gs0 = gstepf(gs, ls, R4, retFLITPSCREAD(ls.t, v)) ∧ ls0 = lstepf(gs, ls, R4, retFLITPSCREAD(ls.t, v)) ∧ ready = pcstepf(gs, ls, R4, retFLITPSCREAD(ls.t, v)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| step-absstep-W3-W4-doWritePSC-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W3, pcf0(t) = W4, apcf(t) = apc, notMember(t, gs.readers) ∧ oneMember(t, ls.l, gs.writers) ∧ noPending(t, gs.p), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ onePendingW(t, ls0.l, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, ADoWrite(ls.t)) → ags0 = gstepf(ags, als, apc, ADoWrite(ls.t)) ∧ als0 = lstepf(ags, als, apc, ADoWrite(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, ADoWrite(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, W3, doWritePSC(ls.t, l, v)) ∧ gs0 = gstepf(gs, ls, W3, doWritePSC(ls.t, l, v)) ∧ ls0 = lstepf(gs, ls, W3, doWritePSC(ls.t, l, v)) ∧ W4 = pcstepf(gs, ls, W3, doWritePSC(ls.t, l, v)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = invWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| ren-tau | ⊦ ren(τ, ags, alsf) = τ | An Axiom |
| step-absstep-ready-ready-callPSCCOMPLETE-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = ready, pcf0(t) = ready, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, callTSync(ls.t)) → ags0 = gstepf(ags, als, apc, callTSync(ls.t)) ∧ als0 = lstepf(ags, als, apc, callTSync(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, callTSync(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, ready, callPSCCOMPLETE(ls.t)) ∧ gs0 = gstepf(gs, ls, ready, callPSCCOMPLETE(ls.t)) ∧ ls0 = lstepf(gs, ls, ready, callPSCCOMPLETE(ls.t)) ∧ ready = pcstepf(gs, ls, ready, callPSCCOMPLETE(ls.t)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = ready ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| ren-globalPSCPERSIST_FO | ⊦ ren(globalPSCPERSIST_FO(l), ags, alsf) = τ | An Axiom |
| step-absstep-R3-R4-tau-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R3, pcf0(t) = R4, apcf(t) = apc, notMember(t, gs.writers) ∧ oneMember(t, ls.l, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, R3, pwbPSC(t, l)) ∧ gs0 = gstepf(gs, ls, R3, pwbPSC(t, l)) ∧ ls0 = lstepf(gs, ls, R3, pwbPSC(t, l)) ∧ R4 = pcstepf(gs, ls, R3, pwbPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| step-absstep-W1-W2-tau-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W1, pcf0(t) = W2, apcf(t) = apc, notMember(t, gs.readers) ∧ notMember(t, gs.writers) ∧ noPendingW(t, gs.p), notMember(t, gs0.readers) ∧ notMember(t, gs0.writers) ∧ noPendingW(t, gs0.p) ∧ noPending(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W1, sfencePSC(t)) ∧ gs0 = gstepf(gs, ls, W1, sfencePSC(t)) ∧ ls0 = lstepf(gs, ls, W1, sfencePSC(t)) ∧ W2 = pcstepf(gs, ls, W1, sfencePSC(t)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = invWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = invWrite ∧ (ls0.l = als.il ∧ ls0.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-W3-W4-doWritePSC-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W3, pcf0(t) = W4, apcf(t) = apc, notMember(t, gs.readers) ∧ oneMember(t, ls.l, gs.writers) ∧ noPending(t, gs.p), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ onePendingW(t, ls0.l, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ADoWrite(ls.t)) → ags0 = gstepf(ags, als, apc, ADoWrite(ls.t)) ∧ als0 = lstepf(ags, als, apc, ADoWrite(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, ADoWrite(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, W3, doWritePSC(ls.t, l, v)) ∧ gs0 = gstepf(gs, ls, W3, doWritePSC(ls.t, l, v)) ∧ ls0 = lstepf(gs, ls, W3, doWritePSC(ls.t, l, v)) ∧ W4 = pcstepf(gs, ls, W3, doWritePSC(ls.t, l, v)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = invWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []) ⊦ pre(ags, als, apc, ADoWrite(ls.t)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = resWrite ∧ (ls0.l = als0.il ∧ ls0.v = als0.iv) ∧ (((ags0.h | ls0.l) | ls0.t) | false = (W(ls0.t, ls0.l, ls0.v), false) ' ∨ ((ags0.h | ls0.l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-ready-W1-invFLITPSCWRITE-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = ready, pcf0(t) = W1, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.readers) ∧ notMember(t, gs0.writers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, AInvWrite(ls.t, l0, v0)) → ags0 = gstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)) ∧ als0 = lstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)) ∧ apc0 = pcstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)) ∧ gs0 = gstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)) ∧ ls0 = lstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)) ∧ W1 = pcstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = ready ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []) ⊦ pre(ags, als, apc, AInvWrite(ls.t, l0, v0)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = invWrite ∧ (ls0.l = als0.il ∧ ls0.v = als0.iv) ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags0.h | l) | ls0.t) | false = []) | A Proof Obligation |
| abs-init | flitpscInit(mkstate(gs, lsf, pcf)), FLITPSCInv(gs, lsf, pcf) ⊦ ∃ ags, alsf, apcf. plibInit(mkstate(ags, alsf, apcf)) ∧ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) | A Proof Obligation |
| step-absstep-W4-W5-tau-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W4, pcf0(t) = W5, apcf(t) = apc, notMember(t, gs.readers) ∧ oneMember(t, ls.l, gs.writers) ∧ onePendingW(t, ls.l, gs.p), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ onePendingW(t, ls0.l, gs0.p) ∧ FOFollowsW(t, gs0.p(ls0.l)), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W4, pwbPSC(t, l)) ∧ gs0 = gstepf(gs, ls, W4, pwbPSC(t, l)) ∧ ls0 = lstepf(gs, ls, W4, pwbPSC(t, l)) ∧ W5 = pcstepf(gs, ls, W4, pwbPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = resWrite ∧ (ls0.l = als.il ∧ ls0.v = als.iv) ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags.h | l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-ready-R1-invFLITPSCREAD-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = ready, pcf0(t) = R1, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, AInvRead(ls.t, l0)) → ags0 = gstepf(ags, als, apc, AInvRead(ls.t, l0)) ∧ als0 = lstepf(ags, als, apc, AInvRead(ls.t, l0)) ∧ apc0 = pcstepf(ags, als, apc, AInvRead(ls.t, l0)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, ready, invFLITPSCREAD(ls.t, l0)) ∧ gs0 = gstepf(gs, ls, ready, invFLITPSCREAD(ls.t, l0)) ∧ ls0 = lstepf(gs, ls, ready, invFLITPSCREAD(ls.t, l0)) ∧ R1 = pcstepf(gs, ls, ready, invFLITPSCREAD(ls.t, l0)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = ready ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| step-absstep-R4-ready-retFLITPSCREAD-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R4, pcf0(t) = ready, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ARetRead(ls.t, v)) → ags0 = gstepf(ags, als, apc, ARetRead(ls.t, v)) ∧ als0 = lstepf(ags, als, apc, ARetRead(ls.t, v)) ∧ apc0 = pcstepf(ags, als, apc, ARetRead(ls.t, v)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, R4, retFLITPSCREAD(ls.t, v)) ∧ gs0 = gstepf(gs, ls, R4, retFLITPSCREAD(ls.t, v)) ∧ ls0 = lstepf(gs, ls, R4, retFLITPSCREAD(ls.t, v)) ∧ ready = pcstepf(gs, ls, R4, retFLITPSCREAD(ls.t, v)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []) ⊦ pre(ags, als, apc, ARetRead(ls.t, v)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = ready ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags0.h | l) | ls0.t) | false = []) | A Proof Obligation |
| labs-def | ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = invRead) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → apc = resRead) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 → apc = invWrite) ∧ (pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → apc = resWrite) ∧ (pc = R1 → ls.l = als.il) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.v = als.ov) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.l = als.il ∧ ls.v = als.iv) ∧ (pc = idle ∨ pc = ready ∨ pc = R1 ∨ pc = R4 ∨ pc = W1 ∨ pc = W5 → (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = [])) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → (∀ l. ((ags.h | l) | ls.t) | false = [])) ∧ (pc = R2 ∨ pc = R3 → (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = [])) ∧ (pc = R2 → gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ∧ (pc = W4 → ((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = []) | An Axiom |
| step-absstep-R1-R2-doReadPSC-same | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R1, pcf0(t) = R2, apcf(t) = apc, notMember(t, gs.writers) ∧ notMember(t, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ oneMember(t, ls0.l, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ADoRead(ls.t)) → ags0 = gstepf(ags, als, apc, ADoRead(ls.t)) ∧ als0 = lstepf(ags, als, apc, ADoRead(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, ADoRead(ls.t)), allReadsOK(ags0.h) ∧ allWritesOK(ags0.h) ∧ ags0.vm = ∅ ⊕ ags0.h ∧ ags0.pm = ∅ ⊕ (ags0.h | true), pre(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))) ∧ gs0 = gstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))) ∧ ls0 = lstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))) ∧ R2 = pcstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = invRead ∧ ls.l = als.il ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = []) ⊦ pre(ags, als, apc, ADoRead(ls.t)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = resRead ∧ ls0.v = als0.ov ∧ (∀ l0. l0 ≠ ls0.l ∧ ¬ FO(ls0.t) ∈ gs0.p(l0) → ((ags0.h | l0) | ls0.t) | false = []) ∧ (gs0.ctr(ls0.l) = 0 → ((ags0.h | ls0.l) | ls0.t) | false = []) | A Proof Obligation |
| step-absstep-R2-R4-tau-other | ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = R2, pcf0(t) = R4, apcf(t) = apc, notMember(t, gs.writers) ∧ oneMember(t, ls.l, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(t, gs0.p), PLIBLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs0, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ gs0 = gstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ ls0 = lstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ R4 = pcstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = []) ∧ (gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []), lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = []) | A Proof Obligation |
| abs-theorem | FLITPSCInv(gs, lsf, pcf), FLITPSCInv(gs0, lsf0, pcf0), PLIBInv(ags, alsf, apcf), flitpscStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)), ren(a, ags, alsf) = aa ⊦ (aa = τ ⊃ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags, alsf, apcf)) ;∃ ags0, alsf0, apcf0. plibStep(mkstate(ags, alsf, apcf), aa, mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) ) | An Axiom |
| ren-ctrReadPSC | ⊦ ren(ctrReadPSC(t, l, ctr(l)), ags, alsf) = τ | An Axiom |