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: |
|---|---|---|
| step-absstep-PROP_SF-propSF | FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), propSF(tid), mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ ∃ ags0, alsf0, apcf0. flitpscStep(mkstate(ags, alsf, apcf), sfencePSC(tid), mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) | A Proof Obligation |
| step-absstep-W4-W5-tau-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ (gs.bq(t) = [] ∨ gs.bq(t) = W(ls.loc, ls.val) ') ∧ (gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val)), notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ FOFollowsW(t, gs0.bq(t), gs0.pq(ls0.loc), ls0.loc) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ (gs0.bq(t) = [] ∨ gs0.bq(t) = FO(ls0.loc) ' ∨ gs0.bq(t) = W(ls0.loc, ls0.val) ' + FO(ls0.loc) ') ∧ (gs0.bq(t) ≠ [] ∧ gs0.bq(t).head.W? → gs0.bq(t).head = W(ls0.loc, ls0.val)), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, W4, τ) ∧ gs0 = gstepf(gs, ls, W4, τ) ∧ ls0 = lstepf(gs, ls, W4, τ) ∧ W5 = pcstepf(gs, ls, W4, τ), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4) ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| step-absstep-W7-ready-retFLITWRITE-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ notMember(t, gs.fwriters) ∧ noPending(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, retFLITPSCWRITE(ls.t)) → ags0 = gstepf(ags, als, apc, retFLITPSCWRITE(ls.t)) ∧ als0 = lstepf(ags, als, apc, retFLITPSCWRITE(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, retFLITPSCWRITE(ls.t)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, W7, retFLITWRITE(ls.t)) ∧ gs0 = gstepf(gs, ls, W7, retFLITWRITE(ls.t)) ∧ ls0 = lstepf(gs, ls, W7, retFLITWRITE(ls.t)) ∧ ready = pcstepf(gs, ls, W7, retFLITWRITE(ls.t)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = W7 ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ pre(ags, als, apc, retFLITPSCWRITE(ls.t)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = ready | A Proof Obligation |
| step-absstep-PERSIST_FO-globalPERSIST_FO | FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), globalPERSIST_FO(loc), mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ ∃ ags0, alsf0, apcf0. flitpscStep(mkstate(ags, alsf, apcf), globalPSCPERSIST_FO(loc), mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) | A Proof Obligation |
| ren-doWriteFO | ⊦ ren(doWriteFO(t, l), ags, alsf) = pwbPSC(t, l) | An Axiom |
| ren-ctrInc | ⊦ ren(ctrInc(t, l), ags, alsf) = ctrIncPSC(t, l) | An Axiom |
| gabs-def | ⊦ gabs(gs, lsf, pcf, ags, alsf, apcf) ↔ ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters | An Axiom |
| step-absstep-W3-W4-tau-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ noPending(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ gs.bq(t) = [], notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ (gs0.bq(t) = [] ∨ gs0.bq(t) = W(ls0.loc, ls0.val) ') ∧ (gs0.bq(t) ≠ [] ∧ gs0.bq(t).head.W? → gs0.bq(t).head = W(ls0.loc, ls0.val)), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, W3, τ) ∧ gs0 = gstepf(gs, ls, W3, τ) ∧ ls0 = lstepf(gs, ls, W3, τ) ∧ W4 = pcstepf(gs, ls, W3, τ), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = W3 ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| ren-globalPERSIST_FO | ⊦ ren(globalPERSIST_FO(l), ags, alsf) = globalPSCPERSIST_FO(l) | An Axiom |
| step-absstep-ready-W1-invFLITWRITE-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.fwriters) ∧ notMember(t, gs.freaders) ∧ noPendingW(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.freaders) ∧ notMember(t, gs0.fwriters) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) → ags0 = gstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) ∧ als0 = lstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) ∧ apc0 = pcstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)) ∧ gs0 = gstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)) ∧ ls0 = lstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)) ∧ W1 = pcstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = ready, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| ren-ctrDec | ⊦ ren(ctrDec(t, l), ags, alsf) = ctrDecPSC(t, l) | An Axiom |
| ren-doRead | ⊦ ren(doRead(t, l, v), ags, alsf) = doReadPSC(t, l, v) | An Axiom |
| ren-invFLITREAD | ⊦ ren(invFLITREAD(t, l), ags, alsf) = invFLITPSCREAD(t, l) | An Axiom |
| step-absstep-W6-W7-ctrDec-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ FOFollowsW(t, gs.bq(t), gs.pq(ls.loc), ls.loc) ∧ gs.rfo(t) = [] ∧ (gs.bq(t) = [] ∨ gs.bq(t) = SF ' ∨ gs.bq(t) = FO(ls.loc) ' + SF ' ∨ gs.bq(t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val)), notMember(t, gs0.freaders) ∧ notMember(t, gs0.fwriters) ∧ noPending(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ctrDecPSC(ls.t, loc)) → ags0 = gstepf(ags, als, apc, ctrDecPSC(ls.t, loc)) ∧ als0 = lstepf(ags, als, apc, ctrDecPSC(ls.t, loc)) ∧ apc0 = pcstepf(ags, als, apc, ctrDecPSC(ls.t, loc)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, W6, ctrDec(ls.t, loc)) ∧ gs0 = gstepf(gs, ls, W6, ctrDec(ls.t, loc)) ∧ ls0 = lstepf(gs, ls, W6, ctrDec(ls.t, loc)) ∧ W7 = pcstepf(gs, ls, W6, ctrDec(ls.t, loc)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6))) ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ pre(ags, als, apc, ctrDecPSC(ls.t, loc)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = W7 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v | A Proof Obligation |
| step-absstep-CRASH-globalCRASH | FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), globalCRASH, mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ ∃ ags0, alsf0, apcf0. flitpscStep(mkstate(ags, alsf, apcf), globalPSCCRASH, mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) | A Proof Obligation |
| step-absstep-W7-ready-retFLITWRITE-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ notMember(t, gs.fwriters) ∧ noPending(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, retFLITPSCWRITE(ls.t)) → ags0 = gstepf(ags, als, apc, retFLITPSCWRITE(ls.t)) ∧ als0 = lstepf(ags, als, apc, retFLITPSCWRITE(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, retFLITPSCWRITE(ls.t)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, W7, retFLITWRITE(ls.t)) ∧ gs0 = gstepf(gs, ls, W7, retFLITWRITE(ls.t)) ∧ ls0 = lstepf(gs, ls, W7, retFLITWRITE(ls.t)) ∧ ready = pcstepf(gs, ls, W7, retFLITWRITE(ls.t)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = W7 ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| ren-globalCRASH | ⊦ ren(globalCRASH, ags, alsf) = globalPSCCRASH | An Axiom |
| step-absstep-R1-R2-doRead-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ notMember(t, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ oneMember(t, ls0.loc, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) → ags0 = gstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ als0 = lstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ apc0 = pcstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ gs0 = gstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ ls0 = lstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ R2 = pcstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R1 ∧ ls.loc = als.l ⊦ pre(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = R2 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v | A Proof Obligation |
| step-absstep-PROP_W-doWrite | FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), doWrite(tid, bq(tid).head.l, bq(tid).head.v), mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ ∃ ags0, alsf0, apcf0. flitpscStep(mkstate(ags, alsf, apcf), doWritePSC(tid, bq(tid).head.l, bq(tid).head.v), mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) | A Proof Obligation |
| step-absstep-ready-ready-callFLITCOMPLETE-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.fwriters) ∧ notMember(t, gs.freaders) ∧ noPendingW(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, callPSCCOMPLETE(ls.t)) → ags0 = gstepf(ags, als, apc, callPSCCOMPLETE(ls.t)) ∧ als0 = lstepf(ags, als, apc, callPSCCOMPLETE(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, callPSCCOMPLETE(ls.t)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, ready, callFLITCOMPLETE(ls.t)) ∧ gs0 = gstepf(gs, ls, ready, callFLITCOMPLETE(ls.t)) ∧ ls0 = lstepf(gs, ls, ready, callFLITCOMPLETE(ls.t)) ∧ ready = pcstepf(gs, ls, ready, callFLITCOMPLETE(ls.t)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = ready, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| step-absstep-R3-R4-pwb-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ oneMember(t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, pwbPSC(ls.t, loc)) → ags0 = gstepf(ags, als, apc, pwbPSC(ls.t, loc)) ∧ als0 = lstepf(ags, als, apc, pwbPSC(ls.t, loc)) ∧ apc0 = pcstepf(ags, als, apc, pwbPSC(ls.t, loc)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R3, pwb(ls.t, loc)) ∧ gs0 = gstepf(gs, ls, R3, pwb(ls.t, loc)) ∧ ls0 = lstepf(gs, ls, R3, pwb(ls.t, loc)) ∧ R4 = pcstepf(gs, ls, R3, pwb(ls.t, loc)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R3 ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ pre(ags, als, apc, pwbPSC(ls.t, loc)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = R4 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v | A Proof Obligation |
| step-absstep-R2-R3-ctrRead-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ oneMember(t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ oneMember(t, ls0.loc, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) → ags0 = gstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ als0 = lstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ apc0 = pcstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ gs0 = gstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ ls0 = lstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ R3 = pcstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R2 ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| step-absstep-PERSIST_W-globalPERSIST_W | FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), globalPERSIST_W(loc), mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ ∃ ags0, alsf0, apcf0. flitpscStep(mkstate(ags, alsf, apcf), globalPSCPERSIST_W(loc), mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) | A Proof Obligation |
| step-absstep-ready-R1-invFLITREAD-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.fwriters) ∧ notMember(t, gs.freaders) ∧ noPendingW(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, invFLITPSCREAD(ls.t, loc0)) → ags0 = gstepf(ags, als, apc, invFLITPSCREAD(ls.t, loc0)) ∧ als0 = lstepf(ags, als, apc, invFLITPSCREAD(ls.t, loc0)) ∧ apc0 = pcstepf(ags, als, apc, invFLITPSCREAD(ls.t, loc0)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, ready, invFLITREAD(ls.t, loc0)) ∧ gs0 = gstepf(gs, ls, ready, invFLITREAD(ls.t, loc0)) ∧ ls0 = lstepf(gs, ls, ready, invFLITREAD(ls.t, loc0)) ∧ R1 = pcstepf(gs, ls, ready, invFLITREAD(ls.t, loc0)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = ready ⊦ pre(ags, als, apc, invFLITPSCREAD(ls.t, loc0)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = R1 ∧ ls0.loc = als0.l | A Proof Obligation |
| step-absstep-W1-W2-tau-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ notMember(t, gs.fwriters) ∧ noPendingW(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.freaders) ∧ notMember(t, gs0.fwriters) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ (gs0.rfo(t) = gs0.bq(t) ∨ gs0.rfo(t) + SF ' = gs0.bq(t)), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, W1, sfence(t)) ∧ gs0 = gstepf(gs, ls, W1, sfence(t)) ∧ ls0 = lstepf(gs, ls, W1, sfence(t)) ∧ W2 = pcstepf(gs, ls, W1, sfence(t)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = W1 ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| step-absstep-W3-W4-tau-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ noPending(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ gs.bq(t) = [], notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ (gs0.bq(t) = [] ∨ gs0.bq(t) = W(ls0.loc, ls0.val) ') ∧ (gs0.bq(t) ≠ [] ∧ gs0.bq(t).head.W? → gs0.bq(t).head = W(ls0.loc, ls0.val)), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W3, τ) ∧ gs0 = gstepf(gs, ls, W3, τ) ∧ ls0 = lstepf(gs, ls, W3, τ) ∧ W4 = pcstepf(gs, ls, W3, τ), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = W3 ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ (ags.mem = gs0.pmem ∧ ags.ctr = gs0.fctr ∧ reorder(ags.p, gs0.pq, gs0.rfo) ∧ ags.writers = gs0.fwriters) ∧ ls0.t = als.t ∧ apc = (W(ls0.loc, ls0.val) ∈ gs0.bq(ls0.t) ⊃ W3;W4) ∧ ls0.loc = als.l ∧ ls0.val = als.v | A Proof Obligation |
| ren-invFLITWRITE | ⊦ ren(invFLITWRITE(t, l, v), ags, alsf) = invFLITPSCWRITE(t, l, v) | An Axiom |
| step-absstep-ready-W1-invFLITWRITE-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.fwriters) ∧ notMember(t, gs.freaders) ∧ noPendingW(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.freaders) ∧ notMember(t, gs0.fwriters) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) → ags0 = gstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) ∧ als0 = lstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) ∧ apc0 = pcstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)) ∧ gs0 = gstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)) ∧ ls0 = lstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)) ∧ W1 = pcstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = ready ⊦ pre(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = W1 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v | A Proof Obligation |
| ren-pwb | ⊦ ren(pwb(t, l), ags, alsf) = pwbPSC(t, l) | An Axiom |
| step-absstep-R2-R4-ctrRead-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ oneMember(t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) → ags0 = gstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ als0 = lstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ apc0 = pcstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ gs0 = gstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ ls0 = lstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ R4 = pcstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R2 ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ pre(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = R4 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v | A Proof Obligation |
| step-absstep-ready-R1-invFLITREAD-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.fwriters) ∧ notMember(t, gs.freaders) ∧ noPendingW(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, invFLITPSCREAD(ls.t, loc0)) → ags0 = gstepf(ags, als, apc, invFLITPSCREAD(ls.t, loc0)) ∧ als0 = lstepf(ags, als, apc, invFLITPSCREAD(ls.t, loc0)) ∧ apc0 = pcstepf(ags, als, apc, invFLITPSCREAD(ls.t, loc0)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, ready, invFLITREAD(ls.t, loc0)) ∧ gs0 = gstepf(gs, ls, ready, invFLITREAD(ls.t, loc0)) ∧ ls0 = lstepf(gs, ls, ready, invFLITREAD(ls.t, loc0)) ∧ R1 = pcstepf(gs, ls, ready, invFLITREAD(ls.t, loc0)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = ready, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| ren-doWrite | ⊦ ren(doWrite(t, l, v), ags, alsf) = doWritePSC(t, l, v) | An Axiom |
| step-absstep-W2-W3-ctrInc-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ notMember(t, gs.fwriters) ∧ noPendingW(t, gs.bq, gs.pq) ∧ (gs.rfo(t) = gs.bq(t) ∨ gs.rfo(t) + SF ' = gs.bq(t)), notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ noPending(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ gs0.bq(t) = [], FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, ctrIncPSC(ls.t, loc)) → ags0 = gstepf(ags, als, apc, ctrIncPSC(ls.t, loc)) ∧ als0 = lstepf(ags, als, apc, ctrIncPSC(ls.t, loc)) ∧ apc0 = pcstepf(ags, als, apc, ctrIncPSC(ls.t, loc)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, W2, ctrInc(ls.t, loc)) ∧ gs0 = gstepf(gs, ls, W2, ctrInc(ls.t, loc)) ∧ ls0 = lstepf(gs, ls, W2, ctrInc(ls.t, loc)) ∧ W3 = pcstepf(gs, ls, W2, ctrInc(ls.t, loc)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2) ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| step-absstep-W6-W7-ctrDec-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ FOFollowsW(t, gs.bq(t), gs.pq(ls.loc), ls.loc) ∧ gs.rfo(t) = [] ∧ (gs.bq(t) = [] ∨ gs.bq(t) = SF ' ∨ gs.bq(t) = FO(ls.loc) ' + SF ' ∨ gs.bq(t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val)), notMember(t, gs0.freaders) ∧ notMember(t, gs0.fwriters) ∧ noPending(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, ctrDecPSC(ls.t, loc)) → ags0 = gstepf(ags, als, apc, ctrDecPSC(ls.t, loc)) ∧ als0 = lstepf(ags, als, apc, ctrDecPSC(ls.t, loc)) ∧ apc0 = pcstepf(ags, als, apc, ctrDecPSC(ls.t, loc)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, W6, ctrDec(ls.t, loc)) ∧ gs0 = gstepf(gs, ls, W6, ctrDec(ls.t, loc)) ∧ ls0 = lstepf(gs, ls, W6, ctrDec(ls.t, loc)) ∧ W7 = pcstepf(gs, ls, W6, ctrDec(ls.t, loc)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6))) ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| step-absstep-R2-R3-ctrRead-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ oneMember(t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ oneMember(t, ls0.loc, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) → ags0 = gstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ als0 = lstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ apc0 = pcstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ gs0 = gstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ ls0 = lstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ R3 = pcstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R2 ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ pre(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = R3 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v | A Proof Obligation |
| step-absstep-R3-R4-pwb-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ oneMember(t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, pwbPSC(ls.t, loc)) → ags0 = gstepf(ags, als, apc, pwbPSC(ls.t, loc)) ∧ als0 = lstepf(ags, als, apc, pwbPSC(ls.t, loc)) ∧ apc0 = pcstepf(ags, als, apc, pwbPSC(ls.t, loc)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R3, pwb(ls.t, loc)) ∧ gs0 = gstepf(gs, ls, R3, pwb(ls.t, loc)) ∧ ls0 = lstepf(gs, ls, R3, pwb(ls.t, loc)) ∧ R4 = pcstepf(gs, ls, R3, pwb(ls.t, loc)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R3 ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| ren-callRUN | ⊦ ren(callRUN(t), ags, alsf) = callPSCRUN(t) | An Axiom |
| ren-propFO | ⊦ ren(propFO(tid, l), ags, alsf) = τ | An Axiom |
| step-absstep-W5-W6-tau-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ FOFollowsW(t, gs.bq(t), gs.pq(ls.loc), ls.loc) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ (gs.bq(t) = [] ∨ gs.bq(t) = FO(ls.loc) ' ∨ gs.bq(t) = W(ls.loc, ls.val) ' + FO(ls.loc) ') ∧ (gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val)), notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ FOFollowsW(t, gs0.bq(t), gs0.pq(ls0.loc), ls0.loc) ∧ gs0.rfo(t) = [] ∧ (gs0.bq(t) = [] ∨ gs0.bq(t) = SF ' ∨ gs0.bq(t) = FO(ls0.loc) ' + SF ' ∨ gs0.bq(t) = W(ls0.loc, ls0.val) ' + FO(ls0.loc) ' + SF ') ∧ (gs0.bq(t) ≠ [] ∧ gs0.bq(t).head.W? → gs0.bq(t).head = W(ls0.loc, ls0.val)), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W5, τ) ∧ gs0 = gstepf(gs, ls, W5, τ) ∧ ls0 = lstepf(gs, ls, W5, τ) ∧ W6 = pcstepf(gs, ls, W5, τ), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5)) ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ (ags.mem = gs0.pmem ∧ ags.ctr = gs0.fctr ∧ reorder(ags.p, gs0.pq, gs0.rfo) ∧ ags.writers = gs0.fwriters) ∧ ls0.t = als.t ∧ apc = (W(ls0.loc, ls0.val) ∈ gs0.bq(ls0.t) ⊃ W3;(FO(ls0.loc) ∈ gs0.bq(ls0.t) ⊃ W4;(SF ∈ gs0.bq(ls0.t) ⊃ W5;W6))) ∧ ls0.loc = als.l ∧ ls0.val = als.v | A Proof Obligation |
| ren-callFLITCOMPLETE | ⊦ ren(callFLITCOMPLETE(t), ags, alsf) = callPSCCOMPLETE(t) | An Axiom |
| step-absstep-ready-ready-callFLITCOMPLETE-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.fwriters) ∧ notMember(t, gs.freaders) ∧ noPendingW(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, callPSCCOMPLETE(ls.t)) → ags0 = gstepf(ags, als, apc, callPSCCOMPLETE(ls.t)) ∧ als0 = lstepf(ags, als, apc, callPSCCOMPLETE(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, callPSCCOMPLETE(ls.t)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, ready, callFLITCOMPLETE(ls.t)) ∧ gs0 = gstepf(gs, ls, ready, callFLITCOMPLETE(ls.t)) ∧ ls0 = lstepf(gs, ls, ready, callFLITCOMPLETE(ls.t)) ∧ ready = pcstepf(gs, ls, ready, callFLITCOMPLETE(ls.t)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = ready ⊦ pre(ags, als, apc, callPSCCOMPLETE(ls.t)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = ready | A Proof Obligation |
| step-absstep-R4-ready-retFLITREAD-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ notMember(t, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, retFLITPSCREAD(ls.t, val)) → ags0 = gstepf(ags, als, apc, retFLITPSCREAD(ls.t, val)) ∧ als0 = lstepf(ags, als, apc, retFLITPSCREAD(ls.t, val)) ∧ apc0 = pcstepf(ags, als, apc, retFLITPSCREAD(ls.t, val)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R4, retFLITREAD(ls.t, val)) ∧ gs0 = gstepf(gs, ls, R4, retFLITREAD(ls.t, val)) ∧ ls0 = lstepf(gs, ls, R4, retFLITREAD(ls.t, val)) ∧ ready = pcstepf(gs, ls, R4, retFLITREAD(ls.t, val)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R4 ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ pre(ags, als, apc, retFLITPSCREAD(ls.t, val)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = ready | A Proof Obligation |
| ren-ctrRead | ⊦ ren(ctrRead(t, l, n), ags, alsf) = ctrReadPSC(t, l, n) | An Axiom |
| ren-retFLITWRITE | ⊦ ren(retFLITWRITE(t), ags, alsf) = retFLITPSCWRITE(t) | 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-PROP_FO-doWriteFO | oneMember(tid, als.l, gs.fwriters), FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), doWriteFO(tid, l), mkstate(gs0, lsf0, pcf0)), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ⊦ ∃ ags0, alsf0, apcf0. flitpscStep(mkstate(ags, alsf, apcf), pwbPSC(tid, l), mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) | A Proof Obligation |
| ren-tau | ⊦ ren(τ, ags, alsf) = τ | An Axiom |
| ren-globalPERSIST_W | ⊦ ren(globalPERSIST_W(l), ags, alsf) = globalPSCPERSIST_W(l) | An Axiom |
| step-absstep-W1-W2-tau-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ notMember(t, gs.fwriters) ∧ noPendingW(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.freaders) ∧ notMember(t, gs0.fwriters) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ (gs0.rfo(t) = gs0.bq(t) ∨ gs0.rfo(t) + SF ' = gs0.bq(t)), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W1, sfence(t)) ∧ gs0 = gstepf(gs, ls, W1, sfence(t)) ∧ ls0 = lstepf(gs, ls, W1, sfence(t)) ∧ W2 = pcstepf(gs, ls, W1, sfence(t)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = W1 ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ (ags.mem = gs0.pmem ∧ ags.ctr = gs0.fctr ∧ reorder(ags.p, gs0.pq, gs0.rfo) ∧ ags.writers = gs0.fwriters) ∧ ls0.t = als.t ∧ apc = (SF ∈ gs0.bq(ls0.t) ⊃ W1;W2) ∧ ls0.loc = als.l ∧ ls0.val = als.v | A Proof Obligation |
| step-absstep-R1-R2-doRead-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ notMember(t, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ oneMember(t, ls0.loc, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) → ags0 = gstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ als0 = lstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ apc0 = pcstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ gs0 = gstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ ls0 = lstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ R2 = pcstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R1 ∧ ls.loc = als.l, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| ren-retFLITREAD | ⊦ ren(retFLITREAD(t, v), ags, alsf) = retFLITPSCREAD(t, v) | An Axiom |
| step-absstep-PROP_FO-tau | ¬ oneMember(tid, als.l, gs.fwriters), FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), propFO(tid, 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 |
| step-absstep-idle-ready-callRUN-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.fwriters) ∧ notMember(t, gs.freaders) ∧ noPendingW(t, gs.bq, gs.pq) ∧ noPending(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, callPSCRUN(ls.t)) → ags0 = gstepf(ags, als, apc, callPSCRUN(ls.t)) ∧ als0 = lstepf(ags, als, apc, callPSCRUN(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, callPSCRUN(ls.t)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, idle, callRUN(ls.t)) ∧ gs0 = gstepf(gs, ls, idle, callRUN(ls.t)) ∧ ls0 = lstepf(gs, ls, idle, callRUN(ls.t)) ∧ ready = pcstepf(gs, ls, idle, callRUN(ls.t)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = idle ⊦ pre(ags, als, apc, callPSCRUN(ls.t)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = ready | A Proof Obligation |
| step-absstep-R2-R4-ctrRead-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ oneMember(t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), noPendingW(t, gs0.bq, gs0.pq) ∧ notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) → ags0 = gstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ als0 = lstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ apc0 = pcstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ gs0 = gstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ ls0 = lstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))) ∧ R4 = pcstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R2 ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| abs-init | flitInit(mkstate(gs, lsf, pcf)), FLITInv(gs, lsf, pcf) ⊦ ∃ ags, alsf, apcf. flitpscInit(mkstate(ags, alsf, apcf)) ∧ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) | A Proof Obligation |
| step-absstep-W4-W5-tau-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ (gs.bq(t) = [] ∨ gs.bq(t) = W(ls.loc, ls.val) ') ∧ (gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val)), notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ FOFollowsW(t, gs0.bq(t), gs0.pq(ls0.loc), ls0.loc) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ (gs0.bq(t) = [] ∨ gs0.bq(t) = FO(ls0.loc) ' ∨ gs0.bq(t) = W(ls0.loc, ls0.val) ' + FO(ls0.loc) ') ∧ (gs0.bq(t) ≠ [] ∧ gs0.bq(t).head.W? → gs0.bq(t).head = W(ls0.loc, ls0.val)), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W4, τ) ∧ gs0 = gstepf(gs, ls, W4, τ) ∧ ls0 = lstepf(gs, ls, W4, τ) ∧ W5 = pcstepf(gs, ls, W4, τ), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4) ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ (ags.mem = gs0.pmem ∧ ags.ctr = gs0.fctr ∧ reorder(ags.p, gs0.pq, gs0.rfo) ∧ ags.writers = gs0.fwriters) ∧ ls0.t = als.t ∧ apc = (W(ls0.loc, ls0.val) ∈ gs0.bq(ls0.t) ⊃ W3;(FO(ls0.loc) ∈ gs0.bq(ls0.t) ⊃ W4;W5)) ∧ ls0.loc = als.l ∧ ls0.val = als.v | A Proof Obligation |
| ren-sfence | ⊦ ren(sfence(t), ags, alsf) = τ | An Axiom |
| step-absstep-idle-ready-callRUN-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.fwriters) ∧ notMember(t, gs.freaders) ∧ noPendingW(t, gs.bq, gs.pq) ∧ noPending(t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, callPSCRUN(ls.t)) → ags0 = gstepf(ags, als, apc, callPSCRUN(ls.t)) ∧ als0 = lstepf(ags, als, apc, callPSCRUN(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, callPSCRUN(ls.t)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, idle, callRUN(ls.t)) ∧ gs0 = gstepf(gs, ls, idle, callRUN(ls.t)) ∧ ls0 = lstepf(gs, ls, idle, callRUN(ls.t)) ∧ ready = pcstepf(gs, ls, idle, callRUN(ls.t)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = idle, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| step-absstep-R4-ready-retFLITREAD-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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, noPendingW(t, gs.bq, gs.pq) ∧ notMember(t, gs.fwriters) ∧ notMember(t, gs.freaders) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = gs.bq(t), notMember(t, gs0.fwriters) ∧ notMember(t, gs0.freaders) ∧ noPendingW(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(ags, als, apc, retFLITPSCREAD(ls.t, val)) → ags0 = gstepf(ags, als, apc, retFLITPSCREAD(ls.t, val)) ∧ als0 = lstepf(ags, als, apc, retFLITPSCREAD(ls.t, val)) ∧ apc0 = pcstepf(ags, als, apc, retFLITPSCREAD(ls.t, val)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, R4, retFLITREAD(ls.t, val)) ∧ gs0 = gstepf(gs, ls, R4, retFLITREAD(ls.t, val)) ∧ ls0 = lstepf(gs, ls, R4, retFLITREAD(ls.t, val)) ∧ ready = pcstepf(gs, ls, R4, retFLITREAD(ls.t, val)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = R4 ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | A Proof Obligation |
| step-absstep-W2-W3-ctrInc-same | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ notMember(t, gs.fwriters) ∧ noPendingW(t, gs.bq, gs.pq) ∧ (gs.rfo(t) = gs.bq(t) ∨ gs.rfo(t) + SF ' = gs.bq(t)), notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ noPending(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ gs0.bq(t) = [], FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ctrIncPSC(ls.t, loc)) → ags0 = gstepf(ags, als, apc, ctrIncPSC(ls.t, loc)) ∧ als0 = lstepf(ags, als, apc, ctrIncPSC(ls.t, loc)) ∧ apc0 = pcstepf(ags, als, apc, ctrIncPSC(ls.t, loc)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, W2, ctrInc(ls.t, loc)) ∧ gs0 = gstepf(gs, ls, W2, ctrInc(ls.t, loc)) ∧ ls0 = lstepf(gs, ls, W2, ctrInc(ls.t, loc)) ∧ W3 = pcstepf(gs, ls, W2, ctrInc(ls.t, loc)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2) ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ pre(ags, als, apc, ctrIncPSC(ls.t, loc)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = W3 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v | A Proof Obligation |
| step-absstep-W5-W6-tau-other | ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ FOFollowsW(t, gs.bq(t), gs.pq(ls.loc), ls.loc) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ (gs.bq(t) = [] ∨ gs.bq(t) = FO(ls.loc) ' ∨ gs.bq(t) = W(ls.loc, ls.val) ' + FO(ls.loc) ') ∧ (gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val)), notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ FOFollowsW(t, gs0.bq(t), gs0.pq(ls0.loc), ls0.loc) ∧ gs0.rfo(t) = [] ∧ (gs0.bq(t) = [] ∨ gs0.bq(t) = SF ' ∨ gs0.bq(t) = FO(ls0.loc) ' + SF ' ∨ gs0.bq(t) = W(ls0.loc, ls0.val) ' + FO(ls0.loc) ' + SF ') ∧ (gs0.bq(t) ≠ [] ∧ gs0.bq(t).head.W? → gs0.bq(t).head = W(ls0.loc, ls0.val)), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, W5, τ) ∧ gs0 = gstepf(gs, ls, W5, τ) ∧ ls0 = lstepf(gs, ls, W5, τ) ∧ W6 = pcstepf(gs, ls, W5, τ), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5)) ∧ ls.loc = als.l ∧ ls.val = als.v, 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ 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) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) | 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 = R1) ∧ (pc = R2 → apc = R2) ∧ (pc = R3 → apc = R3) ∧ (pc = R4 → apc = R4) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.loc = als.l) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.val = als.v) ∧ (pc = W1 → apc = W1) ∧ (pc = W2 → apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2)) ∧ (pc = W3 → apc = W3) ∧ (pc = W4 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4)) ∧ (pc = W5 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5))) ∧ (pc = W6 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6)))) ∧ (pc = W7 → apc = W7) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.loc = als.l) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.val = als.v) | An Axiom |
| abs-theorem | FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(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. flitpscStep(mkstate(ags, alsf, apcf), aa, mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0)) ) | An Axiom |
| ren-propSF | ⊦ ren(propSF(t), ags, alsf) = sfencePSC(t) | An Axiom |