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.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ oneMember(ls.t, ls.l, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R2, a) ∧ pcstepf(gs, ls, R2, a) = R4 → relyws(t0, gs.readers, gstepf(gs, ls, R2, a).readers) ∧ relyws(t0, gs.writers, gstepf(gs, ls, R2, a).writers) ∧ rely(t0, gs.p, gstepf(gs, ls, R2, a).p) | A Proof Obligation |
| step-W5-W6 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ onePendingW(ls.t, ls.l, gs.p) ∧ FOFollowsW(ls.t, gs.p(ls.l))) ∧ pre(gs, ls, W5, a) ∧ pcstepf(gs, ls, W5, a) = W6 → ( ctrok(gstepf(gs, ls, W5, a).ctr, gstepf(gs, ls, W5, a).writers) ∧ writersOk(gstepf(gs, ls, W5, a).p, gstepf(gs, ls, W5, a).writers) ∧ pendingOk(gstepf(gs, ls, W5, a).p)) ∧ notMember(lstepf(gs, ls, W5, a).t, gstepf(gs, ls, W5, a).readers) ∧ oneMember(lstepf(gs, ls, W5, a).t, lstepf(gs, ls, W5, a).l, gstepf(gs, ls, W5, a).writers) ∧ noPending(lstepf(gs, ls, W5, a).t, gstepf(gs, ls, W5, a).p) | A Proof Obligation |
| step-R2-R3 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ oneMember(ls.t, ls.l, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R2, a) ∧ pcstepf(gs, ls, R2, a) = R3 → ( ctrok(gstepf(gs, ls, R2, a).ctr, gstepf(gs, ls, R2, a).writers) ∧ writersOk(gstepf(gs, ls, R2, a).p, gstepf(gs, ls, R2, a).writers) ∧ pendingOk(gstepf(gs, ls, R2, a).p)) ∧ notMember(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).writers) ∧ oneMember(lstepf(gs, ls, R2, a).t, lstepf(gs, ls, R2, a).l, gstepf(gs, ls, R2, a).readers) ∧ noPendingW(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).p) | A Proof Obligation |
| rely-W4-W5 | ⊦ ls.t ≠ t0 ∧ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ onePendingW(ls.t, ls.l, gs.p)) ∧ pre(gs, ls, W4, a) ∧ pcstepf(gs, ls, W4, a) = W5 → relyws(t0, gs.readers, gstepf(gs, ls, W4, a).readers) ∧ relyws(t0, gs.writers, gstepf(gs, ls, W4, a).writers) ∧ rely(t0, gs.p, gstepf(gs, ls, W4, a).p) | A Proof Obligation |
| step-R3-R4 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ oneMember(ls.t, ls.l, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R3, a) ∧ pcstepf(gs, ls, R3, a) = R4 → ( ctrok(gstepf(gs, ls, R3, a).ctr, gstepf(gs, ls, R3, a).writers) ∧ writersOk(gstepf(gs, ls, R3, a).p, gstepf(gs, ls, R3, a).writers) ∧ pendingOk(gstepf(gs, ls, R3, a).p)) ∧ notMember(lstepf(gs, ls, R3, a).t, gstepf(gs, ls, R3, a).writers) ∧ notMember(lstepf(gs, ls, R3, a).t, gstepf(gs, ls, R3, a).readers) ∧ noPendingW(lstepf(gs, ls, R3, a).t, gstepf(gs, ls, R3, a).p) | A Proof Obligation |
| rely-reflexive | ctrok(ctr, writers) ∧ writersOk(p, writers) ∧ pendingOk(p) ⊦ relyws(t, readers, readers) ∧ relyws(t, writers, writers) ∧ rely(t, p, p) | A Proof Obligation |
| step-W6-W7 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, W6, a) ∧ pcstepf(gs, ls, W6, a) = W7 → ( ctrok(gstepf(gs, ls, W6, a).ctr, gstepf(gs, ls, W6, a).writers) ∧ writersOk(gstepf(gs, ls, W6, a).p, gstepf(gs, ls, W6, a).writers) ∧ pendingOk(gstepf(gs, ls, W6, a).p)) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).readers) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).writers) ∧ noPending(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).p) | A Proof Obligation |
| rely-R1-R2 | ⊦ ls.t ≠ t0 ∧ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R1, a) ∧ pcstepf(gs, ls, R1, a) = R2 → relyws(t0, gs.readers, gstepf(gs, ls, R1, a).readers) ∧ relyws(t0, gs.writers, gstepf(gs, ls, R1, a).writers) ∧ rely(t0, gs.p, gstepf(gs, ls, R1, a).p) | A Proof Obligation |
| step-PSCPERSIST_W | ⊦ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ FLITPSCLInv(gs, lsf(t), pcf(t)) ∧ firstPersistW(gs.p(l)) < # gs.p(l) ∧ gs0 = (gs.mem:= gs.mem(l := gs.p(l)[firstPersistW(gs.p(l))].val)).p:= gs.p(l := gs.p(l) -p firstPersistW(gs.p(l))) → ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p) | A Proof Obligation |
| stable-FLITPSCLInv | ⊦ FLITPSCGInv(gs) ∧ FLITPSCLInv(gs, ls, pc) ∧ FLITPSCGInv(gs0) ∧ FLITPSCRely(gs, ls.t, gs0) → FLITPSCLInv(gs0, ls, pc) | An Axiom |
| stable-idle | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p) ∧ noPending(ls.t, gs.p)) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.writers) ∧ notMember(ls.t, gs0.readers) ∧ noPendingW(ls.t, gs0.p) ∧ noPending(ls.t, gs0.p) | A Proof Obligation |
| stable-W3 | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ noPending(ls.t, gs.p)) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.readers) ∧ oneMember(ls.t, ls.l, gs0.writers) ∧ noPending(ls.t, gs0.p) | A Proof Obligation |
| definedness-W6 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, W6, a) → (∀ l0. (ls.l = l0 ⊃ gs.ctr(ls.l) ≥ 1;true)) | A Proof Obligation |
| rely-R2-R3 | ⊦ ls.t ≠ t0 ∧ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ oneMember(ls.t, ls.l, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R2, a) ∧ pcstepf(gs, ls, R2, a) = R3 → relyws(t0, gs.readers, gstepf(gs, ls, R2, a).readers) ∧ relyws(t0, gs.writers, gstepf(gs, ls, R2, a).writers) ∧ rely(t0, gs.p, gstepf(gs, ls, R2, a).p) | A Proof Obligation |
| rely-PSCPERSIST_FO | ⊦ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ (∃ n. isPersistFO(n, gs.p(l))) ∧ ⟨p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟩ (gs0 = gs) → (∀ t0. relyws(t0, gs.readers, gs0.readers) ∧ relyws(t0, gs.writers, gs0.writers) ∧ rely(t0, gs.p, gs0.p)) | A Proof Obligation |
| rely-PSCPERSIST_W | ⊦ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ firstPersistW(gs.p(l)) < # gs.p(l) ∧ gs0 = (gs.mem:= gs.mem(l := gs.p(l)[firstPersistW(gs.p(l))].val)).p:= gs.p(l := gs.p(l) -p firstPersistW(gs.p(l))) → (∀ t0. relyws(t0, gs.readers, gs0.readers) ∧ relyws(t0, gs.writers, gs0.writers) ∧ rely(t0, gs.p, gs0.p)) | A Proof Obligation |
| step-W1-W2 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ notMember(ls.t, gs.writers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, W1, a) ∧ pcstepf(gs, ls, W1, a) = W2 → ( ctrok(gstepf(gs, ls, W1, a).ctr, gstepf(gs, ls, W1, a).writers) ∧ writersOk(gstepf(gs, ls, W1, a).p, gstepf(gs, ls, W1, a).writers) ∧ pendingOk(gstepf(gs, ls, W1, a).p)) ∧ notMember(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).readers) ∧ notMember(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).writers) ∧ noPendingW(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).p) ∧ noPending(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).p) | A Proof Obligation |
| step-FLITPSCLInv | ⊦ FLITPSCGInv(gs) ∧ FLITPSCLInv(gs, ls, pc) ∧ lstep(gs, ls, pc, a, gs0, ls0, pc0) → FLITPSCGInv(gs0) ∧ FLITPSCLInv(gs0, ls0, pc0) ∧ ls.t = ls0.t | An Axiom |
| definedness-R2 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ oneMember(ls.t, ls.l, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R2, a) → (gs.ctr(ls.l) ≠ 0 ⊃ true;true) | A Proof Obligation |
| stable-R2 | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ oneMember(ls.t, ls.l, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.writers) ∧ oneMember(ls.t, ls.l, gs0.readers) ∧ noPendingW(ls.t, gs0.p) | A Proof Obligation |
| other-FLITPSCLInv | ⊦ FLITPSCGInv(gs) ∧ FLITPSCLInv(gs, ls, pc) ∧ ls.t ≠ ls0.t ∧ FLITPSCLInv(gs, ls0, pc0) ∧ lstep(gs, ls, pc, a, gs0, ls1, pc1) → FLITPSCLInv(gs0, ls0, pc0) | An Axiom |
| stable-W2 | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ notMember(ls.t, gs.writers) ∧ noPendingW(ls.t, gs.p) ∧ noPending(ls.t, gs.p)) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.readers) ∧ notMember(ls.t, gs0.writers) ∧ noPendingW(ls.t, gs0.p) ∧ noPending(ls.t, gs0.p) | A Proof Obligation |
| rely-W6-W7 | ⊦ ls.t ≠ t0 ∧ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, W6, a) ∧ pcstepf(gs, ls, W6, a) = W7 → relyws(t0, gs.readers, gstepf(gs, ls, W6, a).readers) ∧ relyws(t0, gs.writers, gstepf(gs, ls, W6, a).writers) ∧ rely(t0, gs.p, gstepf(gs, ls, W6, a).p) | A Proof Obligation |
| stable-W5 | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ onePendingW(ls.t, ls.l, gs.p) ∧ FOFollowsW(ls.t, gs.p(ls.l))) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.readers) ∧ oneMember(ls.t, ls.l, gs0.writers) ∧ onePendingW(ls.t, ls.l, gs0.p) ∧ FOFollowsW(ls.t, gs0.p(ls.l)) | A Proof Obligation |
| rely-R3-R4 | ⊦ ls.t ≠ t0 ∧ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ oneMember(ls.t, ls.l, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R3, a) ∧ pcstepf(gs, ls, R3, a) = R4 → relyws(t0, gs.readers, gstepf(gs, ls, R3, a).readers) ∧ relyws(t0, gs.writers, gstepf(gs, ls, R3, a).writers) ∧ rely(t0, gs.p, gstepf(gs, ls, R3, a).p) | A Proof Obligation |
| init-state-inv | (gs.mem = (λ l. O) ∧ pcf = (λ tid. idle) ∧ gs.p = (λ l. []) ∧ gs.ctr = (λ l. 0) ∧ gs.readers = (λ l. ∅) ∧ gs.writers = (λ l. ∅)) ∧ (∀ t. t = lsf(t).t) ⊦ FLITPSCInv(gs, lsf, pcf) | A Proof Obligation |
| stable-R1 | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.writers) ∧ notMember(ls.t, gs0.readers) ∧ noPendingW(ls.t, gs0.p) | A Proof Obligation |
| step-W7-ready | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ notMember(ls.t, gs.writers) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, W7, a) ∧ pcstepf(gs, ls, W7, a) = ready → ( ctrok(gstepf(gs, ls, W7, a).ctr, gstepf(gs, ls, W7, a).writers) ∧ writersOk(gstepf(gs, ls, W7, a).p, gstepf(gs, ls, W7, a).writers) ∧ pendingOk(gstepf(gs, ls, W7, a).p)) ∧ notMember(lstepf(gs, ls, W7, a).t, gstepf(gs, ls, W7, a).writers) ∧ notMember(lstepf(gs, ls, W7, a).t, gstepf(gs, ls, W7, a).readers) ∧ noPendingW(lstepf(gs, ls, W7, a).t, gstepf(gs, ls, W7, a).p) | A Proof Obligation |
| FLITPSCInv-thm | ⊦ FLITPSCInv(gs, lsf, pcf) ∧ flitpscStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) → FLITPSCInv(gs0, lsf0, pcf0) | An Axiom |
| step-ready-R1 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = R1 → ( ctrok(gstepf(gs, ls, ready, a).ctr, gstepf(gs, ls, ready, a).writers) ∧ writersOk(gstepf(gs, ls, ready, a).p, gstepf(gs, ls, ready, a).writers) ∧ pendingOk(gstepf(gs, ls, ready, a).p)) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).writers) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).readers) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).p) | A Proof Obligation |
| step-PSCCRASH | ⊦ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ FLITPSCLInv(gs, lsf(t), pcf(t)) → ⟪p := gs.p, ctr := gs.ctr, writers := gs.writers, readers := gs.readers; PSCCRASH(; p, ctr, writers, readers, pcf); gs := (((gs.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟫ ((ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ FLITPSCLInv(gs, lsf(t), pcf(t))) | A Proof Obligation |
| step-W2-W3 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ notMember(ls.t, gs.writers) ∧ noPendingW(ls.t, gs.p) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, W2, a) ∧ pcstepf(gs, ls, W2, a) = W3 → ( ctrok(gstepf(gs, ls, W2, a).ctr, gstepf(gs, ls, W2, a).writers) ∧ writersOk(gstepf(gs, ls, W2, a).p, gstepf(gs, ls, W2, a).writers) ∧ pendingOk(gstepf(gs, ls, W2, a).p)) ∧ notMember(lstepf(gs, ls, W2, a).t, gstepf(gs, ls, W2, a).readers) ∧ oneMember(lstepf(gs, ls, W2, a).t, lstepf(gs, ls, W2, a).l, gstepf(gs, ls, W2, a).writers) ∧ noPending(lstepf(gs, ls, W2, a).t, gstepf(gs, ls, W2, a).p) | A Proof Obligation |
| step-R2-R4 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ oneMember(ls.t, ls.l, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R2, a) ∧ pcstepf(gs, ls, R2, a) = R4 → ( ctrok(gstepf(gs, ls, R2, a).ctr, gstepf(gs, ls, R2, a).writers) ∧ writersOk(gstepf(gs, ls, R2, a).p, gstepf(gs, ls, R2, a).writers) ∧ pendingOk(gstepf(gs, ls, R2, a).p)) ∧ notMember(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).writers) ∧ notMember(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).readers) ∧ noPendingW(lstepf(gs, ls, R2, a).t, gstepf(gs, ls, R2, a).p) | A Proof Obligation |
| step-ready-W1 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = W1 → ( ctrok(gstepf(gs, ls, ready, a).ctr, gstepf(gs, ls, ready, a).writers) ∧ writersOk(gstepf(gs, ls, ready, a).p, gstepf(gs, ls, ready, a).writers) ∧ pendingOk(gstepf(gs, ls, ready, a).p)) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).readers) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).writers) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).p) | A Proof Obligation |
| stable-W7 | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ notMember(ls.t, gs.writers) ∧ noPending(ls.t, gs.p)) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.readers) ∧ notMember(ls.t, gs0.writers) ∧ noPending(ls.t, gs0.p) | A Proof Obligation |
| rely-W2-W3 | ⊦ ls.t ≠ t0 ∧ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ notMember(ls.t, gs.writers) ∧ noPendingW(ls.t, gs.p) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, W2, a) ∧ pcstepf(gs, ls, W2, a) = W3 → relyws(t0, gs.readers, gstepf(gs, ls, W2, a).readers) ∧ relyws(t0, gs.writers, gstepf(gs, ls, W2, a).writers) ∧ rely(t0, gs.p, gstepf(gs, ls, W2, a).p) | A Proof Obligation |
| definedness-PSCPERSIST_W | ⊦ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ firstPersistW(gs.p(l)) < # gs.p(l) → (∀ l0. (l = l0 ⊃ gs.p(l)[firstPersistW(gs.p(l))].W? ∧ firstPersistW(gs.p(l)) < # gs.p(l);true)) | A Proof Obligation |
| step-W3-W4 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, W3, a) ∧ pcstepf(gs, ls, W3, a) = W4 → ( ctrok(gstepf(gs, ls, W3, a).ctr, gstepf(gs, ls, W3, a).writers) ∧ writersOk(gstepf(gs, ls, W3, a).p, gstepf(gs, ls, W3, a).writers) ∧ pendingOk(gstepf(gs, ls, W3, a).p)) ∧ notMember(lstepf(gs, ls, W3, a).t, gstepf(gs, ls, W3, a).readers) ∧ oneMember(lstepf(gs, ls, W3, a).t, lstepf(gs, ls, W3, a).l, gstepf(gs, ls, W3, a).writers) ∧ onePendingW(lstepf(gs, ls, W3, a).t, lstepf(gs, ls, W3, a).l, gstepf(gs, ls, W3, a).p) | A Proof Obligation |
| step-R4-ready | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R4, a) ∧ pcstepf(gs, ls, R4, a) = ready → ( ctrok(gstepf(gs, ls, R4, a).ctr, gstepf(gs, ls, R4, a).writers) ∧ writersOk(gstepf(gs, ls, R4, a).p, gstepf(gs, ls, R4, a).writers) ∧ pendingOk(gstepf(gs, ls, R4, a).p)) ∧ notMember(lstepf(gs, ls, R4, a).t, gstepf(gs, ls, R4, a).writers) ∧ notMember(lstepf(gs, ls, R4, a).t, gstepf(gs, ls, R4, a).readers) ∧ noPendingW(lstepf(gs, ls, R4, a).t, gstepf(gs, ls, R4, a).p) | A Proof Obligation |
| stable-W1 | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ notMember(ls.t, gs.writers) ∧ noPendingW(ls.t, gs.p)) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.readers) ∧ notMember(ls.t, gs0.writers) ∧ noPendingW(ls.t, gs0.p) | A Proof Obligation |
| step-idle-ready | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, idle, a) ∧ pcstepf(gs, ls, idle, a) = ready → ( ctrok(gstepf(gs, ls, idle, a).ctr, gstepf(gs, ls, idle, a).writers) ∧ writersOk(gstepf(gs, ls, idle, a).p, gstepf(gs, ls, idle, a).writers) ∧ pendingOk(gstepf(gs, ls, idle, a).p)) ∧ notMember(lstepf(gs, ls, idle, a).t, gstepf(gs, ls, idle, a).writers) ∧ notMember(lstepf(gs, ls, idle, a).t, gstepf(gs, ls, idle, a).readers) ∧ noPendingW(lstepf(gs, ls, idle, a).t, gstepf(gs, ls, idle, a).p) | A Proof Obligation |
| step-PSCPERSIST_FO | ⊦ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ (∃ n. isPersistFO(n, gs.p(l))) → ⟪p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) | A Proof Obligation |
| stable-W4 | ⊦ ( ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ onePendingW(ls.t, ls.l, gs.p)) ∧ ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p)) ∧ relyws(ls.t, gs.readers, gs0.readers) ∧ relyws(ls.t, gs.writers, gs0.writers) ∧ rely(ls.t, gs.p, gs0.p) → notMember(ls.t, gs0.readers) ∧ oneMember(ls.t, ls.l, gs0.writers) ∧ onePendingW(ls.t, ls.l, gs0.p) | A Proof Obligation |
| rely-W3-W4 | ⊦ ls.t ≠ t0 ∧ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ noPending(ls.t, gs.p)) ∧ pre(gs, ls, W3, a) ∧ pcstepf(gs, ls, W3, a) = W4 → relyws(t0, gs.readers, gstepf(gs, ls, W3, a).readers) ∧ relyws(t0, gs.writers, gstepf(gs, ls, W3, a).writers) ∧ rely(t0, gs.p, gstepf(gs, ls, W3, a).p) | A Proof Obligation |
| step-R1-R2 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, R1, a) ∧ pcstepf(gs, ls, R1, a) = R2 → ( ctrok(gstepf(gs, ls, R1, a).ctr, gstepf(gs, ls, R1, a).writers) ∧ writersOk(gstepf(gs, ls, R1, a).p, gstepf(gs, ls, R1, a).writers) ∧ pendingOk(gstepf(gs, ls, R1, a).p)) ∧ notMember(lstepf(gs, ls, R1, a).t, gstepf(gs, ls, R1, a).writers) ∧ oneMember(lstepf(gs, ls, R1, a).t, lstepf(gs, ls, R1, a).l, gstepf(gs, ls, R1, a).readers) ∧ noPendingW(lstepf(gs, ls, R1, a).t, gstepf(gs, ls, R1, a).p) | A Proof Obligation |
| step-W4-W5 | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.readers) ∧ oneMember(ls.t, ls.l, gs.writers) ∧ onePendingW(ls.t, ls.l, gs.p)) ∧ pre(gs, ls, W4, a) ∧ pcstepf(gs, ls, W4, a) = W5 → ( ctrok(gstepf(gs, ls, W4, a).ctr, gstepf(gs, ls, W4, a).writers) ∧ writersOk(gstepf(gs, ls, W4, a).p, gstepf(gs, ls, W4, a).writers) ∧ pendingOk(gstepf(gs, ls, W4, a).p)) ∧ notMember(lstepf(gs, ls, W4, a).t, gstepf(gs, ls, W4, a).readers) ∧ oneMember(lstepf(gs, ls, W4, a).t, lstepf(gs, ls, W4, a).l, gstepf(gs, ls, W4, a).writers) ∧ onePendingW(lstepf(gs, ls, W4, a).t, lstepf(gs, ls, W4, a).l, gstepf(gs, ls, W4, a).p) ∧ FOFollowsW(lstepf(gs, ls, W4, a).t, gstepf(gs, ls, W4, a).p(lstepf(gs, ls, W4, a).l)) | A Proof Obligation |
| step-ready-ready | ⊦ ( (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ notMember(ls.t, gs.writers) ∧ notMember(ls.t, gs.readers) ∧ noPendingW(ls.t, gs.p)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = ready → ( ctrok(gstepf(gs, ls, ready, a).ctr, gstepf(gs, ls, ready, a).writers) ∧ writersOk(gstepf(gs, ls, ready, a).p, gstepf(gs, ls, ready, a).writers) ∧ pendingOk(gstepf(gs, ls, ready, a).p)) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).writers) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).readers) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).p) | A Proof Obligation |
| rely-FLITPSCLInv | ⊦ ls.t ≠ t0 ∧ FLITPSCGInv(gs) ∧ FLITPSCLInv(gs, ls, pc) ∧ lstep(gs, ls, pc, a, gs0, ls0, pc0) → FLITPSCRely(gs, t0, gs0) | An Axiom |