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: |
|---|---|---|
| rely-R2-R4 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ oneMember(ls.t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R2, a) ∧ pcstepf(gs, ls, R2, a) = R4 → relyws(t0, gs.freaders, gstepf(gs, ls, R2, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, R2, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, R2, a).pq, gstepf(gs, ls, R2, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, R2, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, R2, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, R2, a).rfo(t0) = gstepf(gs, ls, R2, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, R2, a).rfo(t0) + SF ' = gstepf(gs, ls, R2, a).bq(t0) ∨ gstepf(gs, ls, R2, a).rfo(t0) = gstepf(gs, ls, R2, a).bq(t0)) | A Proof Obligation |
| rely-PROP_SF | ⊦ ( 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)) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head = SF ∧ (∀ l. ¬ FO(tid) ∈ gs.pq(l))) ∧ gs0 = gs.bq:= gs.bq(tid := gs.bq(tid).tail) → (∀ t0. relyws(t0, gs.freaders, gs0.freaders) ∧ relyws(t0, gs.fwriters, gs0.fwriters) ∧ rely(t0, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(t0) ⊒w gs0.bq(t0) ∧ (gs.rfo(t0) = [] → gs0.rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gs0.rfo(t0) = gs0.bq(t0)) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs0.rfo(t0) + SF ' = gs0.bq(t0) ∨ gs0.rfo(t0) = gs0.bq(t0))) | A Proof Obligation |
| step-R2-R3 | ⊦ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ oneMember(ls.t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R2, a) ∧ pcstepf(gs, ls, R2, a) = R3 → ( ctrok(gstepf(gs, ls, R2, a).fctr, gstepf(gs, ls, R2, a).fwriters) ∧ writersOk(gstepf(gs, ls, R2, a).bq, gstepf(gs, ls, R2, a).pq, gstepf(gs, ls, R2, a).fwriters) ∧ pendingOk(gstepf(gs, ls, R2, a).bq, gstepf(gs, ls, R2, a).pq) ∧ SFTrailing(gstepf(gs, ls, R2, a).bq) ∧ readFOsOk(gstepf(gs, ls, R2, a).rfo, gstepf(gs, ls, R2, a).fwriters)) ∧ noPendingW(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).bq, gstepf(gs, ls, R2, a).pq) ∧ notMember(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).fwriters) ∧ oneMember(lstepf(gs, ls, R2, a).t, lstepf(gs, ls, R2, a).loc, gstepf(gs, ls, R2, a).freaders) ∧ ¬ SF ∈ gstepf(gs, ls, R2, a).bq(lstepf(gs, ls, R2, a).t) ∧ gstepf(gs, ls, R2, a).rfo(lstepf(gs, ls, R2, a).t) = gstepf(gs, ls, R2, a).bq(lstepf(gs, ls, R2, a).t) | A Proof Obligation |
| step-W5-W6 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = FO(ls.loc) ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ pre(gs, ls, W5, a) ∧ pcstepf(gs, ls, W5, a) = W6 → ( ctrok(gstepf(gs, ls, W5, a).fctr, gstepf(gs, ls, W5, a).fwriters) ∧ writersOk(gstepf(gs, ls, W5, a).bq, gstepf(gs, ls, W5, a).pq, gstepf(gs, ls, W5, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W5, a).bq, gstepf(gs, ls, W5, a).pq) ∧ SFTrailing(gstepf(gs, ls, W5, a).bq) ∧ readFOsOk(gstepf(gs, ls, W5, a).rfo, gstepf(gs, ls, W5, a).fwriters)) ∧ notMember(lstepf(gs, ls, W5, a).t, gstepf(gs, ls, W5, a).freaders) ∧ oneMember(lstepf(gs, ls, W5, a).t, lstepf(gs, ls, W5, a).loc, gstepf(gs, ls, W5, a).fwriters) ∧ FOFollowsW (lstepf(gs, ls, W5, a).t, gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t), gstepf(gs, ls, W5, a).pq(lstepf(gs, ls, W5, a).loc), lstepf(gs, ls, W5, a).loc) ∧ gstepf(gs, ls, W5, a).rfo(lstepf(gs, ls, W5, a).t) = [] ∧ ( gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) = [] ∨ gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) = SF ' ∨ gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) = FO(lstepf(gs, ls, W5, a).loc) ' + SF ' ∨ gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) = W(lstepf(gs, ls, W5, a).loc, lstepf(gs, ls, W5, a).val) ' + FO(lstepf(gs, ls, W5, a).loc) ' + SF ') ∧ ( gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) ≠ [] ∧ gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t).head.W? → gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t).head = W(lstepf(gs, ls, W5, a).loc, lstepf(gs, ls, W5, a).val)) | A Proof Obligation |
| rely-W4-W5 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ pre(gs, ls, W4, a) ∧ pcstepf(gs, ls, W4, a) = W5 → relyws(t0, gs.freaders, gstepf(gs, ls, W4, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, W4, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, W4, a).pq, gstepf(gs, ls, W4, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, W4, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, W4, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, W4, a).rfo(t0) = gstepf(gs, ls, W4, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, W4, a).rfo(t0) + SF ' = gstepf(gs, ls, W4, a).bq(t0) ∨ gstepf(gs, ls, W4, a).rfo(t0) = gstepf(gs, ls, W4, a).bq(t0)) | A Proof Obligation |
| rely-PROP_W | ⊦ ( 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)) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head.W?) ∧ gs0 = (gs.pq:= gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid))).bq:= gs.bq(tid := gs.bq(tid).tail) → (∀ t0. relyws(t0, gs.freaders, gs0.freaders) ∧ relyws(t0, gs.fwriters, gs0.fwriters) ∧ rely(t0, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(t0) ⊒w gs0.bq(t0) ∧ (gs.rfo(t0) = [] → gs0.rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gs0.rfo(t0) = gs0.bq(t0)) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs0.rfo(t0) + SF ' = gs0.bq(t0) ∨ gs0.rfo(t0) = gs0.bq(t0))) | A Proof Obligation |
| stable-W6 | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = SF ' ∨ gs.bq(ls.t) = FO(ls.loc) ' + SF ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.freaders) ∧ oneMember(ls.t, ls.loc, gs0.fwriters) ∧ FOFollowsW(ls.t, gs0.bq(ls.t), gs0.pq(ls.loc), ls.loc) ∧ gs0.rfo(ls.t) = [] ∧ (gs0.bq(ls.t) = [] ∨ gs0.bq(ls.t) = SF ' ∨ gs0.bq(ls.t) = FO(ls.loc) ' + SF ' ∨ gs0.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs0.bq(ls.t) ≠ [] ∧ gs0.bq(ls.t).head.W? → gs0.bq(ls.t).head = W(ls.loc, ls.val)) | A Proof Obligation |
| definedness-PERSIST_W | ⊦ ( 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)) ∧ gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.W? → (∀ fl. (loc = fl ⊃ gs.pq(loc).head.W? ∧ gs.pq(loc) ≠ [];true)) ∧ (∀ fl. (loc = fl ⊃ gs.pq(loc) ≠ [];true)) | A Proof Obligation |
| step-R3-R4 | ⊦ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ oneMember(ls.t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R3, a) ∧ pcstepf(gs, ls, R3, a) = R4 → ( ctrok(gstepf(gs, ls, R3, a).fctr, gstepf(gs, ls, R3, a).fwriters) ∧ writersOk(gstepf(gs, ls, R3, a).bq, gstepf(gs, ls, R3, a).pq, gstepf(gs, ls, R3, a).fwriters) ∧ pendingOk(gstepf(gs, ls, R3, a).bq, gstepf(gs, ls, R3, a).pq) ∧ SFTrailing(gstepf(gs, ls, R3, a).bq) ∧ readFOsOk(gstepf(gs, ls, R3, a).rfo, gstepf(gs, ls, R3, a).fwriters)) ∧ noPendingW(lstepf(gs, ls, R3, a).t, gstepf(gs, ls, R3, a).bq, gstepf(gs, ls, R3, a).pq) ∧ notMember(lstepf(gs, ls, R3, a).t, gstepf(gs, ls, R3, a).fwriters) ∧ notMember(lstepf(gs, ls, R3, a).t, gstepf(gs, ls, R3, a).freaders) ∧ ¬ SF ∈ gstepf(gs, ls, R3, a).bq(lstepf(gs, ls, R3, a).t) ∧ gstepf(gs, ls, R3, a).rfo(lstepf(gs, ls, R3, a).t) = gstepf(gs, ls, R3, a).bq(lstepf(gs, ls, R3, a).t) | A Proof Obligation |
| step-W6-W7 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = SF ' ∨ gs.bq(ls.t) = FO(ls.loc) ' + SF ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ pre(gs, ls, W6, a) ∧ pcstepf(gs, ls, W6, a) = W7 → ( ctrok(gstepf(gs, ls, W6, a).fctr, gstepf(gs, ls, W6, a).fwriters) ∧ writersOk(gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq, gstepf(gs, ls, W6, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq) ∧ SFTrailing(gstepf(gs, ls, W6, a).bq) ∧ readFOsOk(gstepf(gs, ls, W6, a).rfo, gstepf(gs, ls, W6, a).fwriters)) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).freaders) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).fwriters) ∧ noPending(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, W6, a).bq(lstepf(gs, ls, W6, a).t) ∧ gstepf(gs, ls, W6, a).rfo(lstepf(gs, ls, W6, a).t) = [] ∧ gstepf(gs, ls, W6, a).rfo(lstepf(gs, ls, W6, a).t) = gstepf(gs, ls, W6, a).bq(lstepf(gs, ls, W6, a).t) | A Proof Obligation |
| rely-reflexive | ctrok(fctr, fwriters) ∧ writersOk(bq, pq, fwriters) ∧ pendingOk(bq, pq) ∧ SFTrailing(bq) ∧ readFOsOk(rfo, fwriters) ⊦ relyws(t, freaders, freaders) ∧ relyws(t, fwriters, fwriters) ∧ rely(t, pq, bq, pq, bq) ∧ bq(t) ⊒w bq(t) ∧ (rfo(t) = [] → rfo(t) = []) ∧ (rfo(t) = bq(t) → rfo(t) = bq(t)) ∧ (rfo(t) + SF ' = bq(t) → rfo(t) + SF ' = bq(t) ∨ rfo(t) = bq(t)) | A Proof Obligation |
| rely-R1-R2 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R1, a) ∧ pcstepf(gs, ls, R1, a) = R2 → relyws(t0, gs.freaders, gstepf(gs, ls, R1, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, R1, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, R1, a).pq, gstepf(gs, ls, R1, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, R1, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, R1, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, R1, a).rfo(t0) = gstepf(gs, ls, R1, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, R1, a).rfo(t0) + SF ' = gstepf(gs, ls, R1, a).bq(t0) ∨ gstepf(gs, ls, R1, a).rfo(t0) = gstepf(gs, ls, R1, a).bq(t0)) | A Proof Obligation |
| stable-W3 | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ noPending(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ gs.bq(ls.t) = []) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.freaders) ∧ oneMember(ls.t, ls.loc, gs0.fwriters) ∧ noPending(ls.t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = [] ∧ gs0.bq(ls.t) = [] | A Proof Obligation |
| definedness-W6 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = SF ' ∨ gs.bq(ls.t) = FO(ls.loc) ' + SF ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ pre(gs, ls, W6, a) → gs.bq(ls.t) = [] ∧ (∀ l. ¬ FO(ls.t) ∈ gs.pq(l)) → (∀ fl. (ls.loc = fl ⊃ gs.fctr(ls.loc) ≥ 1;true)) | A Proof Obligation |
| step-PROP_FO | ⊦ ( 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)) ∧ (∃ n. n < # gs.bq(tid) ∧ isPropFO(n, l, gs.bq(tid))) → ⟪fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟫ ( 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)) | A Proof Obligation |
| rely-R2-R3 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ oneMember(ls.t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R2, a) ∧ pcstepf(gs, ls, R2, a) = R3 → relyws(t0, gs.freaders, gstepf(gs, ls, R2, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, R2, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, R2, a).pq, gstepf(gs, ls, R2, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, R2, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, R2, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, R2, a).rfo(t0) = gstepf(gs, ls, R2, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, R2, a).rfo(t0) + SF ' = gstepf(gs, ls, R2, a).bq(t0) ∨ gstepf(gs, ls, R2, a).rfo(t0) = gstepf(gs, ls, R2, a).bq(t0)) | A Proof Obligation |
| step-W1-W2 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, W1, a) ∧ pcstepf(gs, ls, W1, a) = W2 → ( ctrok(gstepf(gs, ls, W1, a).fctr, gstepf(gs, ls, W1, a).fwriters) ∧ writersOk(gstepf(gs, ls, W1, a).bq, gstepf(gs, ls, W1, a).pq, gstepf(gs, ls, W1, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W1, a).bq, gstepf(gs, ls, W1, a).pq) ∧ SFTrailing(gstepf(gs, ls, W1, a).bq) ∧ readFOsOk(gstepf(gs, ls, W1, a).rfo, gstepf(gs, ls, W1, a).fwriters)) ∧ notMember(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).freaders) ∧ notMember(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).fwriters) ∧ noPendingW(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).bq, gstepf(gs, ls, W1, a).pq) ∧ ( gstepf(gs, ls, W1, a).rfo(lstepf(gs, ls, W1, a).t) = gstepf(gs, ls, W1, a).bq(lstepf(gs, ls, W1, a).t) ∨ gstepf(gs, ls, W1, a).rfo(lstepf(gs, ls, W1, a).t) + SF ' = gstepf(gs, ls, W1, a).bq(lstepf(gs, ls, W1, a).t)) | A Proof Obligation |
| rely-W5-W6 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = FO(ls.loc) ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ pre(gs, ls, W5, a) ∧ pcstepf(gs, ls, W5, a) = W6 → relyws(t0, gs.freaders, gstepf(gs, ls, W5, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, W5, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, W5, a).pq, gstepf(gs, ls, W5, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, W5, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, W5, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, W5, a).rfo(t0) = gstepf(gs, ls, W5, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, W5, a).rfo(t0) + SF ' = gstepf(gs, ls, W5, a).bq(t0) ∨ gstepf(gs, ls, W5, a).rfo(t0) = gstepf(gs, ls, W5, a).bq(t0)) | A Proof Obligation |
| definedness-R2 | ⊦ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ oneMember(ls.t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R2, a) → (gs.fctr(ls.loc) ≠ 0 ⊃ true;true) | A Proof Obligation |
| FLITInv-thm | ⊦ FLITInv(gs, lsf, pcf) ∧ flitStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) → FLITInv(gs0, lsf0, pcf0) | An Axiom |
| stable-R2 | ⊦ ( ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ oneMember(ls.t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → noPendingW(ls.t, gs0.bq, gs0.pq) ∧ notMember(ls.t, gs0.fwriters) ∧ oneMember(ls.t, ls.loc, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = gs0.bq(ls.t) | A Proof Obligation |
| rely-PERSIST_FO | ⊦ ( 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)) ∧ (gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.FO?) ∧ gs0 = gs.pq:= gs.pq(loc := gs.pq(loc).tail) → (∀ t0. relyws(t0, gs.freaders, gs0.freaders) ∧ relyws(t0, gs.fwriters, gs0.fwriters) ∧ rely(t0, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(t0) ⊒w gs0.bq(t0) ∧ (gs.rfo(t0) = [] → gs0.rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gs0.rfo(t0) = gs0.bq(t0)) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs0.rfo(t0) + SF ' = gs0.bq(t0) ∨ gs0.rfo(t0) = gs0.bq(t0))) | A Proof Obligation |
| stable-W2 | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) ∨ gs.rfo(ls.t) + SF ' = gs.bq(ls.t))) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.freaders) ∧ notMember(ls.t, gs0.fwriters) ∧ noPendingW(ls.t, gs0.bq, gs0.pq) ∧ (gs0.rfo(ls.t) = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t)) | A Proof Obligation |
| other-FLITLInv | ⊦ FLITGInv(gs) ∧ FLITLInv(gs, ls, pc) ∧ ls.t ≠ ls0.t ∧ FLITLInv(gs, ls0, pc0) ∧ lstep(gs, ls, pc, a, gs0, ls1, pc1) → FLITLInv(gs0, ls0, pc0) | An Axiom |
| stable-FLITLInv | ⊦ FLITGInv(gs) ∧ FLITLInv(gs, ls, pc) ∧ FLITGInv(gs0) ∧ FLITRely(gs, ls.t, gs0) → FLITLInv(gs0, ls, pc) | An Axiom |
| rely-W6-W7 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = SF ' ∨ gs.bq(ls.t) = FO(ls.loc) ' + SF ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ pre(gs, ls, W6, a) ∧ pcstepf(gs, ls, W6, a) = W7 → relyws(t0, gs.freaders, gstepf(gs, ls, W6, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, W6, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, W6, a).pq, gstepf(gs, ls, W6, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, W6, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, W6, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, W6, a).rfo(t0) = gstepf(gs, ls, W6, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, W6, a).rfo(t0) + SF ' = gstepf(gs, ls, W6, a).bq(t0) ∨ gstepf(gs, ls, W6, a).rfo(t0) = gstepf(gs, ls, W6, a).bq(t0)) | A Proof Obligation |
| rely-R3-R4 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ oneMember(ls.t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R3, a) ∧ pcstepf(gs, ls, R3, a) = R4 → relyws(t0, gs.freaders, gstepf(gs, ls, R3, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, R3, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, R3, a).pq, gstepf(gs, ls, R3, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, R3, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, R3, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, R3, a).rfo(t0) = gstepf(gs, ls, R3, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, R3, a).rfo(t0) + SF ' = gstepf(gs, ls, R3, a).bq(t0) ∨ gstepf(gs, ls, R3, a).rfo(t0) = gstepf(gs, ls, R3, a).bq(t0)) | A Proof Obligation |
| stable-W5 | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = FO(ls.loc) ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.freaders) ∧ oneMember(ls.t, ls.loc, gs0.fwriters) ∧ FOFollowsW(ls.t, gs0.bq(ls.t), gs0.pq(ls.loc), ls.loc) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = [] ∧ (gs0.bq(ls.t) = [] ∨ gs0.bq(ls.t) = FO(ls.loc) ' ∨ gs0.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ') ∧ (gs0.bq(ls.t) ≠ [] ∧ gs0.bq(ls.t).head.W? → gs0.bq(ls.t).head = W(ls.loc, ls.val)) | A Proof Obligation |
| init-state-inv | ( gs.pmem = (λ l. O) ∧ pcf = (λ tid. idle) ∧ gs.pq = (λ l. []) ∧ gs.fctr = (λ l. 0) ∧ gs.freaders = (λ l. ∅) ∧ gs.fwriters = (λ l. ∅) ∧ gs.bq = (λ t. []) ∧ gs.rfo = (λ t. [])) ∧ (∀ t. t = lsf(t).t) ⊦ FLITInv(gs, lsf, pcf) | A Proof Obligation |
| definedness-PROP_SF | ⊦ ( 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)) ∧ gs.bq(tid) ≠ [] ∧ gs.bq(tid).head = SF ∧ (∀ l. ¬ FO(tid) ∈ gs.pq(l)) → (∀ t. (tid = t ⊃ gs.bq(tid) ≠ [];true)) | A Proof Obligation |
| step-PROP_W | ⊦ ( 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)) ∧ FLITLInv(gs, lsf(t), pcf(t)) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head.W?) ∧ gs0 = (gs.pq:= gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid))).bq:= gs.bq(tid := gs.bq(tid).tail) → 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) | A Proof Obligation |
| stable-R1 | ⊦ ( ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → noPendingW(ls.t, gs0.bq, gs0.pq) ∧ notMember(ls.t, gs0.fwriters) ∧ notMember(ls.t, gs0.freaders) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = gs0.bq(ls.t) | A Proof Obligation |
| step-W7-ready | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPending(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, W7, a) ∧ pcstepf(gs, ls, W7, a) = ready → ( ctrok(gstepf(gs, ls, W7, a).fctr, gstepf(gs, ls, W7, a).fwriters) ∧ writersOk(gstepf(gs, ls, W7, a).bq, gstepf(gs, ls, W7, a).pq, gstepf(gs, ls, W7, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W7, a).bq, gstepf(gs, ls, W7, a).pq) ∧ SFTrailing(gstepf(gs, ls, W7, a).bq) ∧ readFOsOk(gstepf(gs, ls, W7, a).rfo, gstepf(gs, ls, W7, a).fwriters)) ∧ notMember(lstepf(gs, ls, W7, a).t, gstepf(gs, ls, W7, a).fwriters) ∧ notMember(lstepf(gs, ls, W7, a).t, gstepf(gs, ls, W7, a).freaders) ∧ noPendingW(lstepf(gs, ls, W7, a).t, gstepf(gs, ls, W7, a).bq, gstepf(gs, ls, W7, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, W7, a).bq(lstepf(gs, ls, W7, a).t) ∧ gstepf(gs, ls, W7, a).rfo(lstepf(gs, ls, W7, a).t) = gstepf(gs, ls, W7, a).bq(lstepf(gs, ls, W7, a).t) | A Proof Obligation |
| step-ready-R1 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = R1 → ( ctrok(gstepf(gs, ls, ready, a).fctr, gstepf(gs, ls, ready, a).fwriters) ∧ writersOk(gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq, gstepf(gs, ls, ready, a).fwriters) ∧ pendingOk(gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq) ∧ SFTrailing(gstepf(gs, ls, ready, a).bq) ∧ readFOsOk(gstepf(gs, ls, ready, a).rfo, gstepf(gs, ls, ready, a).fwriters)) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).fwriters) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).freaders) ∧ ¬ SF ∈ gstepf(gs, ls, ready, a).bq(lstepf(gs, ls, ready, a).t) ∧ gstepf(gs, ls, ready, a).rfo(lstepf(gs, ls, ready, a).t) = gstepf(gs, ls, ready, a).bq(lstepf(gs, ls, ready, a).t) | A Proof Obligation |
| step-PERSIST_FO | ⊦ ( 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)) ∧ FLITLInv(gs, lsf(t), pcf(t)) ∧ (gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.FO?) ∧ gs0 = gs.pq:= gs.pq(loc := gs.pq(loc).tail) → 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) | A Proof Obligation |
| rely-FLITLInv | ⊦ ls.t ≠ t0 ∧ FLITGInv(gs) ∧ FLITLInv(gs, ls, pc) ∧ lstep(gs, ls, pc, a, gs0, ls0, pc0) → FLITRely(gs, t0, gs0) | An Axiom |
| stable-crashed | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ noPending(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.fwriters) ∧ notMember(ls.t, gs0.freaders) ∧ noPendingW(ls.t, gs0.bq, gs0.pq) ∧ noPending(ls.t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = gs0.bq(ls.t) | A Proof Obligation |
| step-R2-R4 | ⊦ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ oneMember(ls.t, ls.loc, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R2, a) ∧ pcstepf(gs, ls, R2, a) = R4 → ( ctrok(gstepf(gs, ls, R2, a).fctr, gstepf(gs, ls, R2, a).fwriters) ∧ writersOk(gstepf(gs, ls, R2, a).bq, gstepf(gs, ls, R2, a).pq, gstepf(gs, ls, R2, a).fwriters) ∧ pendingOk(gstepf(gs, ls, R2, a).bq, gstepf(gs, ls, R2, a).pq) ∧ SFTrailing(gstepf(gs, ls, R2, a).bq) ∧ readFOsOk(gstepf(gs, ls, R2, a).rfo, gstepf(gs, ls, R2, a).fwriters)) ∧ noPendingW(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).bq, gstepf(gs, ls, R2, a).pq) ∧ notMember(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).fwriters) ∧ notMember(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).freaders) ∧ ¬ SF ∈ gstepf(gs, ls, R2, a).bq(lstepf(gs, ls, R2, a).t) ∧ gstepf(gs, ls, R2, a).rfo(lstepf(gs, ls, R2, a).t) = gstepf(gs, ls, R2, a).bq(lstepf(gs, ls, R2, a).t) | A Proof Obligation |
| step-W2-W3 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) ∨ gs.rfo(ls.t) + SF ' = gs.bq(ls.t))) ∧ pre(gs, ls, W2, a) ∧ pcstepf(gs, ls, W2, a) = W3 → ( ctrok(gstepf(gs, ls, W2, a).fctr, gstepf(gs, ls, W2, a).fwriters) ∧ writersOk(gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq, gstepf(gs, ls, W2, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq) ∧ SFTrailing(gstepf(gs, ls, W2, a).bq) ∧ readFOsOk(gstepf(gs, ls, W2, a).rfo, gstepf(gs, ls, W2, a).fwriters)) ∧ notMember(lstepf(gs, ls, W2, a).t, gstepf(gs, ls, W2, a).freaders) ∧ oneMember(lstepf(gs, ls, W2, a).t, lstepf(gs, ls, W2, a).loc, gstepf(gs, ls, W2, a).fwriters) ∧ noPending(lstepf(gs, ls, W2, a).t, gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, W2, a).bq(lstepf(gs, ls, W2, a).t) ∧ gstepf(gs, ls, W2, a).rfo(lstepf(gs, ls, W2, a).t) = [] ∧ gstepf(gs, ls, W2, a).bq(lstepf(gs, ls, W2, a).t) = [] | A Proof Obligation |
| rely-W1-W2 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, W1, a) ∧ pcstepf(gs, ls, W1, a) = W2 → relyws(t0, gs.freaders, gstepf(gs, ls, W1, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, W1, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, W1, a).pq, gstepf(gs, ls, W1, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, W1, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, W1, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, W1, a).rfo(t0) = gstepf(gs, ls, W1, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, W1, a).rfo(t0) + SF ' = gstepf(gs, ls, W1, a).bq(t0) ∨ gstepf(gs, ls, W1, a).rfo(t0) = gstepf(gs, ls, W1, a).bq(t0)) | A Proof Obligation |
| step-PROP_SF | ⊦ ( 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)) ∧ FLITLInv(gs, lsf(t), pcf(t)) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head = SF ∧ (∀ l. ¬ FO(tid) ∈ gs.pq(l))) ∧ gs0 = gs.bq:= gs.bq(tid := gs.bq(tid).tail) → 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) | A Proof Obligation |
| step-ready-W1 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = W1 → ( ctrok(gstepf(gs, ls, ready, a).fctr, gstepf(gs, ls, ready, a).fwriters) ∧ writersOk(gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq, gstepf(gs, ls, ready, a).fwriters) ∧ pendingOk(gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq) ∧ SFTrailing(gstepf(gs, ls, ready, a).bq) ∧ readFOsOk(gstepf(gs, ls, ready, a).rfo, gstepf(gs, ls, ready, a).fwriters)) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).freaders) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).fwriters) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, ready, a).bq(lstepf(gs, ls, ready, a).t) ∧ gstepf(gs, ls, ready, a).rfo(lstepf(gs, ls, ready, a).t) = gstepf(gs, ls, ready, a).bq(lstepf(gs, ls, ready, a).t) | A Proof Obligation |
| step-CRASH | ⊦ ( 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)) ∧ FLITLInv(gs, lsf(t), pcf(t)) → ⟪pq := gs.pq, fctr := gs.fctr, bq := gs.bq, fwriters := gs.fwriters, freaders := gs.freaders, rfo := gs.rfo; CRASH(; pq, fctr, bq, fwriters, freaders, rfo, pcf); gs := (((((gs.pq:= pq).fctr:= fctr).bq:= bq).fwriters:= fwriters).freaders:= freaders).rfo:= rfo⟫ ( ( 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)) ∧ FLITLInv(gs, lsf(t), pcf(t))) | A Proof Obligation |
| stable-W7 | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPending(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.freaders) ∧ notMember(ls.t, gs0.fwriters) ∧ noPending(ls.t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = [] ∧ gs0.rfo(ls.t) = gs0.bq(ls.t) | A Proof Obligation |
| rely-W2-W3 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) ∨ gs.rfo(ls.t) + SF ' = gs.bq(ls.t))) ∧ pre(gs, ls, W2, a) ∧ pcstepf(gs, ls, W2, a) = W3 → relyws(t0, gs.freaders, gstepf(gs, ls, W2, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, W2, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, W2, a).pq, gstepf(gs, ls, W2, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, W2, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, W2, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, W2, a).rfo(t0) = gstepf(gs, ls, W2, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, W2, a).rfo(t0) + SF ' = gstepf(gs, ls, W2, a).bq(t0) ∨ gstepf(gs, ls, W2, a).rfo(t0) = gstepf(gs, ls, W2, a).bq(t0)) | A Proof Obligation |
| rely-PROP_FO | ⊦ ( 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)) ∧ (∃ n. n < # gs.bq(tid) ∧ isPropFO(n, l, gs.bq(tid))) ∧ ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs) → (∀ t0. relyws(t0, gs.freaders, gs0.freaders) ∧ relyws(t0, gs.fwriters, gs0.fwriters) ∧ rely(t0, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(t0) ⊒w gs0.bq(t0) ∧ (gs.rfo(t0) = [] → gs0.rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gs0.rfo(t0) = gs0.bq(t0)) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs0.rfo(t0) + SF ' = gs0.bq(t0) ∨ gs0.rfo(t0) = gs0.bq(t0))) | A Proof Obligation |
| step-R4-ready | ⊦ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R4, a) ∧ pcstepf(gs, ls, R4, a) = ready → ( ctrok(gstepf(gs, ls, R4, a).fctr, gstepf(gs, ls, R4, a).fwriters) ∧ writersOk(gstepf(gs, ls, R4, a).bq, gstepf(gs, ls, R4, a).pq, gstepf(gs, ls, R4, a).fwriters) ∧ pendingOk(gstepf(gs, ls, R4, a).bq, gstepf(gs, ls, R4, a).pq) ∧ SFTrailing(gstepf(gs, ls, R4, a).bq) ∧ readFOsOk(gstepf(gs, ls, R4, a).rfo, gstepf(gs, ls, R4, a).fwriters)) ∧ notMember(lstepf(gs, ls, R4, a).t, gstepf(gs, ls, R4, a).fwriters) ∧ notMember(lstepf(gs, ls, R4, a).t, gstepf(gs, ls, R4, a).freaders) ∧ noPendingW(lstepf(gs, ls, R4, a).t, gstepf(gs, ls, R4, a).bq, gstepf(gs, ls, R4, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, R4, a).bq(lstepf(gs, ls, R4, a).t) ∧ gstepf(gs, ls, R4, a).rfo(lstepf(gs, ls, R4, a).t) = gstepf(gs, ls, R4, a).bq(lstepf(gs, ls, R4, a).t) | A Proof Obligation |
| step-W3-W4 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ noPending(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ gs.bq(ls.t) = []) ∧ pre(gs, ls, W3, a) ∧ pcstepf(gs, ls, W3, a) = W4 → ( ctrok(gstepf(gs, ls, W3, a).fctr, gstepf(gs, ls, W3, a).fwriters) ∧ writersOk(gstepf(gs, ls, W3, a).bq, gstepf(gs, ls, W3, a).pq, gstepf(gs, ls, W3, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W3, a).bq, gstepf(gs, ls, W3, a).pq) ∧ SFTrailing(gstepf(gs, ls, W3, a).bq) ∧ readFOsOk(gstepf(gs, ls, W3, a).rfo, gstepf(gs, ls, W3, a).fwriters)) ∧ notMember(lstepf(gs, ls, W3, a).t, gstepf(gs, ls, W3, a).freaders) ∧ oneMember(lstepf(gs, ls, W3, a).t, lstepf(gs, ls, W3, a).loc, gstepf(gs, ls, W3, a).fwriters) ∧ ¬ SF ∈ gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t) ∧ gstepf(gs, ls, W3, a).rfo(lstepf(gs, ls, W3, a).t) = [] ∧ ( gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t) = [] ∨ gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t) = W(lstepf(gs, ls, W3, a).loc, lstepf(gs, ls, W3, a).val) ') ∧ ( gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t) ≠ [] ∧ gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t).head.W? → gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t).head = W(lstepf(gs, ls, W3, a).loc, lstepf(gs, ls, W3, a).val)) | A Proof Obligation |
| step-idle-ready | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ noPending(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, idle, a) ∧ pcstepf(gs, ls, idle, a) = ready → ( ctrok(gstepf(gs, ls, idle, a).fctr, gstepf(gs, ls, idle, a).fwriters) ∧ writersOk(gstepf(gs, ls, idle, a).bq, gstepf(gs, ls, idle, a).pq, gstepf(gs, ls, idle, a).fwriters) ∧ pendingOk(gstepf(gs, ls, idle, a).bq, gstepf(gs, ls, idle, a).pq) ∧ SFTrailing(gstepf(gs, ls, idle, a).bq) ∧ readFOsOk(gstepf(gs, ls, idle, a).rfo, gstepf(gs, ls, idle, a).fwriters)) ∧ notMember(lstepf(gs, ls, idle, a).t, gstepf(gs, ls, idle, a).fwriters) ∧ notMember(lstepf(gs, ls, idle, a).t, gstepf(gs, ls, idle, a).freaders) ∧ noPendingW(lstepf(gs, ls, idle, a).t, gstepf(gs, ls, idle, a).bq, gstepf(gs, ls, idle, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, idle, a).bq(lstepf(gs, ls, idle, a).t) ∧ gstepf(gs, ls, idle, a).rfo(lstepf(gs, ls, idle, a).t) = gstepf(gs, ls, idle, a).bq(lstepf(gs, ls, idle, a).t) | A Proof Obligation |
| step-PERSIST_W | ⊦ ( 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)) ∧ FLITLInv(gs, lsf(t), pcf(t)) ∧ (gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.W?) ∧ gs0 = (gs.pmem:= gs.pmem(loc := gs.pq(loc).head.val)).pq:= gs.pq(loc := gs.pq(loc).tail) → 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) | A Proof Obligation |
| stable-W1 | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.freaders) ∧ notMember(ls.t, gs0.fwriters) ∧ noPendingW(ls.t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = gs0.bq(ls.t) | A Proof Obligation |
| step-FLITLInv | ⊦ FLITGInv(gs) ∧ FLITLInv(gs, ls, pc) ∧ lstep(gs, ls, pc, a, gs0, ls0, pc0) → FLITGInv(gs0) ∧ FLITLInv(gs0, ls0, pc0) ∧ ls.t = ls0.t | An Axiom |
| rely-PERSIST_W | ⊦ ( 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)) ∧ (gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.W?) ∧ gs0 = (gs.pmem:= gs.pmem(loc := gs.pq(loc).head.val)).pq:= gs.pq(loc := gs.pq(loc).tail) → (∀ t0. relyws(t0, gs.freaders, gs0.freaders) ∧ relyws(t0, gs.fwriters, gs0.fwriters) ∧ rely(t0, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(t0) ⊒w gs0.bq(t0) ∧ (gs.rfo(t0) = [] → gs0.rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gs0.rfo(t0) = gs0.bq(t0)) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs0.rfo(t0) + SF ' = gs0.bq(t0) ∨ gs0.rfo(t0) = gs0.bq(t0))) | A Proof Obligation |
| stable-W4 | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.freaders) ∧ oneMember(ls.t, ls.loc, gs0.fwriters) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = [] ∧ (gs0.bq(ls.t) = [] ∨ gs0.bq(ls.t) = W(ls.loc, ls.val) ') ∧ (gs0.bq(ls.t) ≠ [] ∧ gs0.bq(ls.t).head.W? → gs0.bq(ls.t).head = W(ls.loc, ls.val)) | A Proof Obligation |
| definedness-PERSIST_FO | ⊦ ( 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)) ∧ gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.FO? → (∀ fl. (loc = fl ⊃ gs.pq(loc) ≠ [];true)) | A Proof Obligation |
| stable-ready | ⊦ ( ( ( 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)) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ 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)) ∧ relyws(ls.t, gs.freaders, gs0.freaders) ∧ relyws(ls.t, gs.fwriters, gs0.fwriters) ∧ rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(ls.t) ⊒w gs0.bq(ls.t) ∧ (gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = []) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t)) ∧ (gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t)) → notMember(ls.t, gs0.fwriters) ∧ notMember(ls.t, gs0.freaders) ∧ noPendingW(ls.t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = gs0.bq(ls.t) | A Proof Obligation |
| step-R1-R2 | ⊦ ( ( 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)) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, R1, a) ∧ pcstepf(gs, ls, R1, a) = R2 → ( ctrok(gstepf(gs, ls, R1, a).fctr, gstepf(gs, ls, R1, a).fwriters) ∧ writersOk(gstepf(gs, ls, R1, a).bq, gstepf(gs, ls, R1, a).pq, gstepf(gs, ls, R1, a).fwriters) ∧ pendingOk(gstepf(gs, ls, R1, a).bq, gstepf(gs, ls, R1, a).pq) ∧ SFTrailing(gstepf(gs, ls, R1, a).bq) ∧ readFOsOk(gstepf(gs, ls, R1, a).rfo, gstepf(gs, ls, R1, a).fwriters)) ∧ noPendingW(lstepf(gs, ls, R1, a).t, gstepf(gs, ls, R1, a).bq, gstepf(gs, ls, R1, a).pq) ∧ notMember(lstepf(gs, ls, R1, a).t, gstepf(gs, ls, R1, a).fwriters) ∧ oneMember(lstepf(gs, ls, R1, a).t, lstepf(gs, ls, R1, a).loc, gstepf(gs, ls, R1, a).freaders) ∧ ¬ SF ∈ gstepf(gs, ls, R1, a).bq(lstepf(gs, ls, R1, a).t) ∧ gstepf(gs, ls, R1, a).rfo(lstepf(gs, ls, R1, a).t) = gstepf(gs, ls, R1, a).bq(lstepf(gs, ls, R1, a).t) | A Proof Obligation |
| rely-W3-W4 | ⊦ ls.t ≠ t0 ∧ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ noPending(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ gs.bq(ls.t) = []) ∧ pre(gs, ls, W3, a) ∧ pcstepf(gs, ls, W3, a) = W4 → relyws(t0, gs.freaders, gstepf(gs, ls, W3, a).freaders) ∧ relyws(t0, gs.fwriters, gstepf(gs, ls, W3, a).fwriters) ∧ rely(t0, gs.pq, gs.bq, gstepf(gs, ls, W3, a).pq, gstepf(gs, ls, W3, a).bq) ∧ gs.bq(t0) ⊒w gstepf(gs, ls, W3, a).bq(t0) ∧ (gs.rfo(t0) = [] → gstepf(gs, ls, W3, a).rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gstepf(gs, ls, W3, a).rfo(t0) = gstepf(gs, ls, W3, a).bq(t0)) ∧ ( gs.rfo(t0) + SF ' = gs.bq(t0) → gstepf(gs, ls, W3, a).rfo(t0) + SF ' = gstepf(gs, ls, W3, a).bq(t0) ∨ gstepf(gs, ls, W3, a).rfo(t0) = gstepf(gs, ls, W3, a).bq(t0)) | A Proof Obligation |
| step-W4-W5 | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.freaders) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ pre(gs, ls, W4, a) ∧ pcstepf(gs, ls, W4, a) = W5 → ( ctrok(gstepf(gs, ls, W4, a).fctr, gstepf(gs, ls, W4, a).fwriters) ∧ writersOk(gstepf(gs, ls, W4, a).bq, gstepf(gs, ls, W4, a).pq, gstepf(gs, ls, W4, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W4, a).bq, gstepf(gs, ls, W4, a).pq) ∧ SFTrailing(gstepf(gs, ls, W4, a).bq) ∧ readFOsOk(gstepf(gs, ls, W4, a).rfo, gstepf(gs, ls, W4, a).fwriters)) ∧ notMember(lstepf(gs, ls, W4, a).t, gstepf(gs, ls, W4, a).freaders) ∧ oneMember(lstepf(gs, ls, W4, a).t, lstepf(gs, ls, W4, a).loc, gstepf(gs, ls, W4, a).fwriters) ∧ FOFollowsW (lstepf(gs, ls, W4, a).t, gstepf(gs, ls, W4, a).bq(lstepf(gs, ls, W4, a).t), gstepf(gs, ls, W4, a).pq(lstepf(gs, ls, W4, a).loc), lstepf(gs, ls, W4, a).loc) ∧ ¬ SF ∈ gstepf(gs, ls, W4, a).bq(lstepf(gs, ls, W4, a).t) ∧ gstepf(gs, ls, W4, a).rfo(lstepf(gs, ls, W4, a).t) = [] ∧ ( gstepf(gs, ls, W4, a).bq(lstepf(gs, ls, W4, a).t) = [] ∨ gstepf(gs, ls, W4, a).bq(lstepf(gs, ls, W4, a).t) = FO(lstepf(gs, ls, W4, a).loc) ' ∨ gstepf(gs, ls, W4, a).bq(lstepf(gs, ls, W4, a).t) = W(lstepf(gs, ls, W4, a).loc, lstepf(gs, ls, W4, a).val) ' + FO(lstepf(gs, ls, W4, a).loc) ') ∧ ( gstepf(gs, ls, W4, a).bq(lstepf(gs, ls, W4, a).t) ≠ [] ∧ gstepf(gs, ls, W4, a).bq(lstepf(gs, ls, W4, a).t).head.W? → gstepf(gs, ls, W4, a).bq(lstepf(gs, ls, W4, a).t).head = W(lstepf(gs, ls, W4, a).loc, lstepf(gs, ls, W4, a).val)) | A Proof Obligation |
| definedness-PROP_W | ⊦ ( 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)) ∧ gs.bq(tid) ≠ [] ∧ gs.bq(tid).head.W? → (∀ fl. ((gs.bq(tid).head.FO? ∨ gs.bq(tid).head.W?) ∧ gs.bq(tid) ≠ []) ∧ (gs.bq(tid).head.l = fl ⊃ ((gs.bq(tid).head.FO? ∨ gs.bq(tid).head.W?) ∧ gs.bq(tid) ≠ []) ∧ gs.bq(tid).head.W? ∧ gs.bq(tid) ≠ [];true)) ∧ (∀ t. (tid = t ⊃ gs.bq(tid) ≠ [];true)) | A Proof Obligation |
| step-ready-ready | ⊦ ( ( 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)) ∧ notMember(ls.t, gs.fwriters) ∧ notMember(ls.t, gs.freaders) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ ¬ SF ∈ gs.bq(ls.t) ∧ gs.rfo(ls.t) = gs.bq(ls.t)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = ready → ( ctrok(gstepf(gs, ls, ready, a).fctr, gstepf(gs, ls, ready, a).fwriters) ∧ writersOk(gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq, gstepf(gs, ls, ready, a).fwriters) ∧ pendingOk(gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq) ∧ SFTrailing(gstepf(gs, ls, ready, a).bq) ∧ readFOsOk(gstepf(gs, ls, ready, a).rfo, gstepf(gs, ls, ready, a).fwriters)) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).fwriters) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).freaders) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, ready, a).bq(lstepf(gs, ls, ready, a).t) ∧ gstepf(gs, ls, ready, a).rfo(lstepf(gs, ls, ready, a).t) = gstepf(gs, ls, ready, a).bq(lstepf(gs, ls, ready, a).t) | A Proof Obligation |