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-ready-invRead | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = invRead → allReadsOK(gstepf(gs, ls, ready, a).h) ∧ allWritesOK(gstepf(gs, ls, ready, a).h) ∧ gstepf(gs, ls, ready, a).vm = ∅ ⊕ gstepf(gs, ls, ready, a).h ∧ gstepf(gs, ls, ready, a).pm = ∅ ⊕ (gstepf(gs, ls, ready, a).h | true) | A Proof Obligation |
| step-resRead-ready | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, resRead, a) ∧ pcstepf(gs, ls, resRead, a) = ready → allReadsOK(gstepf(gs, ls, resRead, a).h) ∧ allWritesOK(gstepf(gs, ls, resRead, a).h) ∧ gstepf(gs, ls, resRead, a).vm = ∅ ⊕ gstepf(gs, ls, resRead, a).h ∧ gstepf(gs, ls, resRead, a).pm = ∅ ⊕ (gstepf(gs, ls, resRead, a).h | true) | A Proof Obligation |
| rely-TSync | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ (gs.h | tid) | false = [] ∧ gs0 = gs → (∀ t0. rely(t0, gs.h, gs0.h)) | A User Theorem |
| step-APersist | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ PLIBLInv(gs, lsf(t), pcf(t)) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) → allReadsOK(gs0.h) ∧ allWritesOK(gs0.h) ∧ gs0.vm = ∅ ⊕ gs0.h ∧ gs0.pm = ∅ ⊕ (gs0.h | true) | A Proof Obligation |
| step-ready-invWrite | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = invWrite → allReadsOK(gstepf(gs, ls, ready, a).h) ∧ allWritesOK(gstepf(gs, ls, ready, a).h) ∧ gstepf(gs, ls, ready, a).vm = ∅ ⊕ gstepf(gs, ls, ready, a).h ∧ gstepf(gs, ls, ready, a).pm = ∅ ⊕ (gstepf(gs, ls, ready, a).h | true) | A Proof Obligation |
| step-invWrite-resWrite | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, invWrite, a) ∧ pcstepf(gs, ls, invWrite, a) = resWrite → ( allReadsOK(gstepf(gs, ls, invWrite, a).h) ∧ allWritesOK(gstepf(gs, ls, invWrite, a).h) ∧ gstepf(gs, ls, invWrite, a).vm = ∅ ⊕ gstepf(gs, ls, invWrite, a).h ∧ gstepf(gs, ls, invWrite, a).pm = ∅ ⊕ (gstepf(gs, ls, invWrite, a).h | true)) ∧ ( (gstepf(gs, ls, invWrite, a).h | lstepf(gs, ls, invWrite, a).t) | false = [] ∨ (gstepf(gs, ls, invWrite, a).h | lstepf(gs, ls, invWrite, a).t) | false = (W(lstepf(gs, ls, invWrite, a).t, lstepf(gs, ls, invWrite, a).il, lstepf(gs, ls, invWrite, a).iv), false) ') | A Proof Obligation |
| rely-reflexive | allReadsOK(h) ∧ allWritesOK(h) ∧ vm = ∅ ⊕ h ∧ pm = ∅ ⊕ (h | true) ⊦ rely(t, h, h) | A Proof Obligation |
| step-ACrash | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ PLIBLInv(gs, lsf(t), pcf(t)) → ⟪pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟫ ((allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ PLIBLInv(gs, lsf(t), pcf(t))) | A Proof Obligation |
| other-PLIBLInv | ⊦ PLIBGInv(gs) ∧ PLIBLInv(gs, ls, pc) ∧ ls.t ≠ ls0.t ∧ PLIBLInv(gs, ls0, pc0) ∧ lstep(gs, ls, pc, a, gs0, ls1, pc1) → PLIBLInv(gs0, ls0, pc0) | An Axiom |
| stable-PLIBLInv | ⊦ PLIBGInv(gs) ∧ PLIBLInv(gs, ls, pc) ∧ PLIBGInv(gs0) ∧ PLIBRely(gs, ls.t, gs0) → PLIBLInv(gs0, ls, pc) | An Axiom |
| stable-resWrite | ⊦ ( ( (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ ((gs.h | ls.t) | false = [] ∨ (gs.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) ')) ∧ allReadsOK(gs0.h) ∧ allWritesOK(gs0.h) ∧ gs0.vm = ∅ ⊕ gs0.h ∧ gs0.pm = ∅ ⊕ (gs0.h | true)) ∧ rely(ls.t, gs.h, gs0.h) → (gs0.h | ls.t) | false = [] ∨ (gs0.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) ' | A Proof Obligation |
| definedness-APersist | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ firstVolWrite(l, gs.h) < # gs.h → (∀ l0. (l = l0 ⊃ firstVolWrite(l, gs.h) < # gs.h;true)) ∧ firstVolWrite(l, gs.h) ≤ # gs.h ∧ firstVolWrite(l, gs.h) < # gs.h ∧ firstVolWrite(l, gs.h) + 1 ≤ # gs.h | A Proof Obligation |
| step-resWrite-ready | ⊦ ( (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ ((gs.h | ls.t) | false = [] ∨ (gs.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) ')) ∧ pre(gs, ls, resWrite, a) ∧ pcstepf(gs, ls, resWrite, a) = ready → allReadsOK(gstepf(gs, ls, resWrite, a).h) ∧ allWritesOK(gstepf(gs, ls, resWrite, a).h) ∧ gstepf(gs, ls, resWrite, a).vm = ∅ ⊕ gstepf(gs, ls, resWrite, a).h ∧ gstepf(gs, ls, resWrite, a).pm = ∅ ⊕ (gstepf(gs, ls, resWrite, a).h | true) | A Proof Obligation |
| PLIBInv-thm | ⊦ PLIBInv(gs, lsf, pcf) ∧ plibStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) → PLIBInv(gs0, lsf0, pcf0) | An Axiom |
| init-state-inv | (gs.vm = ∅ ∧ gs.pm = ∅ ∧ pcf = (λ t. idle) ∧ gs.h = []) ∧ (∀ t. t = lsf(t).t) ⊦ PLIBInv(gs, lsf, pcf) | A Proof Obligation |
| rely-invWrite-resWrite | ⊦ ls.t ≠ t0 ∧ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, invWrite, a) ∧ pcstepf(gs, ls, invWrite, a) = resWrite → rely(t0, gs.h, gstepf(gs, ls, invWrite, a).h) | A Proof Obligation |
| rely-PLIBLInv | ⊦ ls.t ≠ t0 ∧ PLIBGInv(gs) ∧ PLIBLInv(gs, ls, pc) ∧ lstep(gs, ls, pc, a, gs0, ls0, pc0) → PLIBRely(gs, t0, gs0) | An Axiom |
| rely-invRead-resRead | ⊦ ls.t ≠ t0 ∧ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, invRead, a) ∧ pcstepf(gs, ls, invRead, a) = resRead → rely(t0, gs.h, gstepf(gs, ls, invRead, a).h) | A Proof Obligation |
| step-invRead-resRead | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, invRead, a) ∧ pcstepf(gs, ls, invRead, a) = resRead → allReadsOK(gstepf(gs, ls, invRead, a).h) ∧ allWritesOK(gstepf(gs, ls, invRead, a).h) ∧ gstepf(gs, ls, invRead, a).vm = ∅ ⊕ gstepf(gs, ls, invRead, a).h ∧ gstepf(gs, ls, invRead, a).pm = ∅ ⊕ (gstepf(gs, ls, invRead, a).h | true) | A Proof Obligation |
| step-PLIBLInv | ⊦ PLIBGInv(gs) ∧ PLIBLInv(gs, ls, pc) ∧ lstep(gs, ls, pc, a, gs0, ls0, pc0) → PLIBGInv(gs0) ∧ PLIBLInv(gs0, ls0, pc0) ∧ ls.t = ls0.t | An Axiom |
| step-idle-ready | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, idle, a) ∧ pcstepf(gs, ls, idle, a) = ready → allReadsOK(gstepf(gs, ls, idle, a).h) ∧ allWritesOK(gstepf(gs, ls, idle, a).h) ∧ gstepf(gs, ls, idle, a).vm = ∅ ⊕ gstepf(gs, ls, idle, a).h ∧ gstepf(gs, ls, idle, a).pm = ∅ ⊕ (gstepf(gs, ls, idle, a).h | true) | A Proof Obligation |
| rely-APersist | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) → (∀ t0. rely(t0, gs.h, gs0.h)) | A Proof Obligation |
| step-ready-ready | ⊦ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ pre(gs, ls, ready, a) ∧ pcstepf(gs, ls, ready, a) = ready → allReadsOK(gstepf(gs, ls, ready, a).h) ∧ allWritesOK(gstepf(gs, ls, ready, a).h) ∧ gstepf(gs, ls, ready, a).vm = ∅ ⊕ gstepf(gs, ls, ready, a).h ∧ gstepf(gs, ls, ready, a).pm = ∅ ⊕ (gstepf(gs, ls, ready, a).h | true) | A Proof Obligation |