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: |
|---|---|---|
| disj-AInvRead-callTSync | ⊦ AInvRead(t, l) ≠ callTSync(t0) | An Axiom |
| pcstepf-resRead-ARETREAD | ⊦ ls.t = t → pcstepf(gs, ls, resRead, ARetRead(t, v0)) = ready | An Axiom |
| updsel--dotpcf-dotpcf | ⊦ (s.pcf:= pcf).pcf = pcf | An Axiom |
| disj-AInvRead-callARun | ⊦ AInvRead(t, l) ≠ callARun(t0) | An Axiom |
| updsel--dott-dotil | ⊦ (ls.t:= t).il = ls.il | An Axiom |
| updsel--dotov-dott | ⊦ (ls.ov:= iv0).t = ls.t | An Axiom |
| disj-crashed-invWrite | ⊦ crashed ≠ invWrite | An Axiom |
| updsel--dotlsf-dotpcf | ⊦ (s.lsf:= lsf).pcf = s.pcf | An Axiom |
| disj-crashed-resWrite | ⊦ crashed ≠ resWrite | An Axiom |
| lstepf-invWrite-DOWRITE | ⊦ ls.t = t → lstepf(gs, ls, invWrite, ADoWrite(t)) = ls | An Axiom |
| disj-AInvWrite-callTSync | ⊦ AInvWrite(t, l, val) ≠ callTSync(t0) | An Axiom |
| updsel--dotiv-dotov | ⊦ (ls.iv:= iv).ov = ls.ov | An Axiom |
| updsel--dotil-dott | ⊦ (ls.il:= il).t = ls.t | An Axiom |
| disj-AInvWrite-callARun | ⊦ AInvWrite(t, l, val) ≠ callARun(t0) | An Axiom |
| updsel--dotil-dotov | ⊦ (ls.il:= il).ov = ls.ov | An Axiom |
| plibStep-lem | ⊦ plibStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ∨ (∃ l. a = globalAPersist(l) ∧ 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)))) ∧ lsf0 = lsf ∧ pcf0 = pcf) | A User Theorem |
| PLIBLInv | ⊦ PLIBLInv(gs, ls, pc) ↔ pc = resWrite → (gs.h | ls.t) | false = [] ∨ (gs.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) ' | An Axiom |
| upd-mkstate-dotlsf | ⊦ (mkstate(gstate, lsf, pcf).lsf:= lsf0) = mkstate(gstate, lsf0, pcf) | An Axiom |
| pre-invWrite | ⊦ pre(gs, ls, invWrite, a) ↔ a = ADoWrite(ls.t) ∧ (gs.h | ls.t) | false = [] | An Axiom |
| disj-invRead-invWrite | ⊦ invRead ≠ invWrite | An Axiom |
| sel-mkPLIBgs-doth | ⊦ mkPLIBgs(vm, vm0, h).h = h | An Axiom |
| pre-resWrite | ⊦ pre(gs, ls, resWrite, a) ↔ a = ARetWrite(ls.t) | An Axiom |
| pcstepf-resWrite-RETWRITE | ⊦ ls.t = t → pcstepf(gs, ls, resWrite, ARetWrite(t)) = ready | An Axiom |
| disj-invRead-resWrite | ⊦ invRead ≠ resWrite | An Axiom |
| updsel--dotvm-dotvm | ⊦ (gs.vm:= vm).vm = vm | An Axiom |
| updsel--dotpm-doth | ⊦ (gs.pm:= vm0).h = gs.h | An Axiom |
| lstepf-resRead-ARETREAD | ⊦ ls.t = t → lstepf(gs, ls, resRead, ARetRead(t, v0)) = ls | An Axiom |
| pcstepf-ready-TSync | ⊦ ls.t = t → pcstepf(gs, ls, ready, callTSync(t)) = ready | An Axiom |
| disj-AInvRead-ARetRead | ⊦ AInvRead(t, l) ≠ ARetRead(t0, val) | An Axiom |
| gstepf-ready | ⊦ gstepf(gs, ls, ready, a) = gs | An Axiom |
| sel-mkPLIBls-dotiv | ⊦ mkPLIBls(t, il, iv, iv0).iv = iv | An Axiom |
| upd-mkPLIBls-dott | ⊦ mkPLIBls(t, il, iv, iv0).t:= t0 = mkPLIBls(t0, il, iv, iv0) | An Axiom |
| pcstepf-invWrite-DOWRITE | ⊦ ls.t = t → pcstepf(gs, ls, invWrite, ADoWrite(t)) = resWrite | An Axiom |
| elim-mkPLIBgs | ⊦ (vm = gs.vm ∧ pm = gs.pm) ∧ h = gs.h ↔ gs = mkPLIBgs(vm, pm, h) | An Axiom |
| sel-ARetWrite-dott | ⊦ ARetWrite(t).t = t | An Axiom |
| lstepf-invRead-ADOREAD | ⊦ ls.t = t → lstepf(gs, ls, invRead, ADoRead(t)) = ls.ov:= gs.vm(ls.il) | An Axiom |
| updsel--dotov-dotil | ⊦ (ls.ov:= iv0).il = ls.il | An Axiom |
| updsel--doth-doth | ⊦ (gs.h:= h).h = h | An Axiom |
| pcstepf-ready-INVWRITE | ⊦ ls.t = t → pcstepf(gs, ls, ready, AInvWrite(t, l, v)) = invWrite | An Axiom |
| disj-callARun-globalACrash | ⊦ callARun(t) ≠ globalACrash | An Axiom |
| sel-AInvWrite-dott | ⊦ AInvWrite(t, l, val).t = t | An Axiom |
| disj-callARun-tau | ⊦ callARun(t) ≠ τ | An Axiom |
| sel-callTSync-dott | ⊦ callTSync(t).t = t | An Axiom |
| sel-mkstate-dotgstate | ⊦ mkstate(gstate, lsf, pcf).gstate = gstate | An Axiom |
| lstepf-ready-INVWRITE | ⊦ ls.t = t → lstepf(gs, ls, ready, AInvWrite(t, l, v)) = (ls.il:= l).iv:= v | An Axiom |
| not-pre-global-crash | ⊦ ¬ pre(gs, ls, pc, globalACrash) | A User Theorem |
| updsel--dotvm-doth | ⊦ (gs.vm:= vm).h = gs.h | An Axiom |
| disj-ADoWrite-globalAPersist | ⊦ ADoWrite(t) ≠ globalAPersist(l) | An Axiom |
| disj-crashed-ready | ⊦ crashed ≠ ready | An Axiom |
| disj-idle-invWrite | ⊦ idle ≠ invWrite | An Axiom |
| disj-resRead-resWrite | ⊦ resRead ≠ resWrite | An Axiom |
| disj-ARetWrite-globalAPersist | ⊦ ARetWrite(t) ≠ globalAPersist(l) | An Axiom |
| disj-ARetWrite-callARun | ⊦ ARetWrite(t) ≠ callARun(t0) | An Axiom |
| disj-ARetRead-globalACrash | ⊦ ARetRead(t, val) ≠ globalACrash | An Axiom |
| disj-idle-resWrite | ⊦ idle ≠ resWrite | An Axiom |
| inj-AInvWrite | ⊦ AInvWrite(t, l, val) = AInvWrite(t0, l0, val0) ↔ t = t0 ∧ l = l0 ∧ val = val0 | An Axiom |
| disj-invWrite-resWrite | ⊦ invWrite ≠ resWrite | An Axiom |
| updsel--dotil-dotiv | ⊦ (ls.il:= il).iv = ls.iv | An Axiom |
| disj-ADoWrite-globalACrash | ⊦ ADoWrite(t) ≠ globalACrash | An Axiom |
| elim-mkstate | ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf) | An Axiom |
| gen-PLIBLState | PLIBLState freely generated by mkPLIBls; | An Axiom |
| pre-idle | ⊦ pre(gs, ls, idle, a) ↔ a = callARun(ls.t) | An Axiom |
| disj-ADoRead-AInvRead | ⊦ ADoRead(t) ≠ AInvRead(t0, l) | An Axiom |
| disj-AInvWrite-tau | ⊦ AInvWrite(t, l, val) ≠ τ | An Axiom |
| gstepf-resRead-ARETREAD | ⊦ ls.t = t → gstepf(gs, ls, resRead, ARetRead(t, v0)) = gs | An Axiom |
| updsel--dotiv-dotiv | ⊦ (ls.iv:= iv).iv = iv | An Axiom |
| upd-mkPLIBls-dotil | ⊦ mkPLIBls(t, il, iv, iv0).il:= il0 = mkPLIBls(t, il0, iv, iv0) | An Axiom |
| sel-AInvWrite-dotval | ⊦ AInvWrite(t, l, val).val = val | An Axiom |
| disj-ARetRead-ARetWrite | ⊦ ARetRead(t, val) ≠ ARetWrite(t0) | An Axiom |
| PLIBRely | ⊦ PLIBRely(gs, t, gs0) ↔ rely(t, gs.h, gs0.h) | An Axiom |
| sel-mkstate-dotlsf | ⊦ mkstate(gstate, lsf, pcf).lsf = lsf | An Axiom |
| disj-ADoRead-ARetRead | ⊦ ADoRead(t) ≠ ARetRead(t0, val) | An Axiom |
| disj-invWrite-ready | ⊦ invWrite ≠ ready | An Axiom |
| lstep | ⊦ lstep(gs, ls, pc, a, gs0, ls0, pc0) ↔ pre(gs, ls, pc, a) ∧ ls0 = lstepf(gs, ls, pc, a) ∧ gs0 = gstepf(gs, ls, pc, a) ∧ pc0 = pcstepf(gs, ls, pc, a) | An Axiom |
| updsel--dotvm-dotpm | ⊦ (gs.vm:= vm).pm = gs.pm | An Axiom |
| case-PLIBLState | ⊦ mkPLIBls(ls.t, ls.il, ls.iv, ls.ov) = ls | An Axiom |
| disj-ARetWrite-callTSync | ⊦ ARetWrite(t) ≠ callTSync(t0) | An Axiom |
| disj-AInvRead-tau | ⊦ AInvRead(t, l) ≠ τ | An Axiom |
| gstepf-idle-ARun | ⊦ ls.t = t → gstepf(gs, ls, idle, callARun(t)) = gs | An Axiom |
| updsel--dotgstate-dotlsf | ⊦ (s.gstate:= gstate).lsf = s.lsf | An Axiom |
| case-PLIBState | ⊦ mkstate(s.gstate, s.lsf, s.pcf) = s | An Axiom |
| sel-ARetRead-dotv | ⊦ ARetRead(t, val).v = val | An Axiom |
| pcstepf-idle-ARun | ⊦ ls.t = t → pcstepf(gs, ls, idle, callARun(t)) = ready | An Axiom |
| disj-AInvRead-globalAPersist | ⊦ AInvRead(t, l) ≠ globalAPersist(l0) | An Axiom |
| disj-idle-ready | ⊦ idle ≠ ready | An Axiom |
| gstepf-invWrite-DOWRITE | ⊦ ls.t = t → gstepf(gs, ls, invWrite, ADoWrite(t)) = (gs.vm:= gs.vm(ls.il := ls.iv)).h:= (gs.h + (W(ls.t, ls.il, ls.iv), false)) | An Axiom |
| inj-AInvRead | ⊦ AInvRead(t, l) = AInvRead(t0, l0) ↔ t = t0 ∧ l = l0 | An Axiom |
| disj-globalACrash-tau | ⊦ globalACrash ≠ τ | An Axiom |
| case-PLIBGState | ⊦ mkPLIBgs(gs.vm, gs.pm, gs.h) = gs | An Axiom |
| disj-ADoWrite-AInvWrite | ⊦ ADoWrite(t) ≠ AInvWrite(t0, l, val) | An Axiom |
| disj-invWrite-resRead | ⊦ invWrite ≠ resRead | An Axiom |
| upd-mkPLIBgs-dotvm | ⊦ mkPLIBgs(vm, vm0, h).vm:= vm1 = mkPLIBgs(vm1, vm0, h) | An Axiom |
| plibStep | ⊦ plibStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalAPersist(l) ∧ 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)))) ∧ lsf0 = lsf ∧ pcf0 = pcf) | An Axiom |
| updsel--dotlsf-dotlsf | ⊦ (s.lsf:= lsf).lsf = lsf | An Axiom |
| sel-AInvRead-dotl | ⊦ AInvRead(t, l).l = l | An Axiom |
| disj-ARetWrite-tau | ⊦ ARetWrite(t) ≠ τ | An Axiom |
| disj-ARetRead-callTSync | ⊦ ARetRead(t, val) ≠ callTSync(t0) | An Axiom |
| elim-mkPLIBls | ⊦ ((t = ls.t ∧ il = ls.il) ∧ iv = ls.iv) ∧ ov = ls.ov ↔ ls = mkPLIBls(t, il, iv, ov) | An Axiom |
| disj-ADoWrite-tau | ⊦ ADoWrite(t) ≠ τ | An Axiom |
| disj-ARetRead-globalAPersist | ⊦ ARetRead(t, val) ≠ globalAPersist(l) | An Axiom |
| PLIBInv | ⊦ PLIBInv(gs, lsf, pcf) ↔ PLIBGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ PLIBLInv(gs, lsf(t), pcf(t))) | An Axiom |
| updsel--dotgstate-dotgstate | ⊦ (s.gstate:= gstate).gstate = gstate | An Axiom |
| pcstepf-ready-INVREAD | ⊦ ls.t = t → pcstepf(gs, ls, ready, AInvRead(t, l)) = invRead | An Axiom |
| disj-callARun-callTSync | ⊦ callARun(t) ≠ callTSync(t0) | An Axiom |
| inj-ARetRead | ⊦ ARetRead(t, val) = ARetRead(t0, val0) ↔ t = t0 ∧ val = val0 | An Axiom |
| inj-ARetWrite | ⊦ ARetWrite(t) = ARetWrite(t0) ↔ t = t0 | An Axiom |
| updsel--dott-dott | ⊦ (ls.t:= t).t = t | An Axiom |
| disj-ADoRead-callARun | ⊦ ADoRead(t) ≠ callARun(t0) | An Axiom |
| inj-mkPLIBgs | ⊦ mkPLIBgs(vm, vm0, h) = mkPLIBgs(vm1, vm2, h0) ↔ vm = vm1 ∧ vm0 = vm2 ∧ h = h0 | An Axiom |
| sel-mkPLIBgs-dotvm | ⊦ mkPLIBgs(vm, vm0, h).vm = vm | An Axiom |
| updsel--dotov-dotov | ⊦ (ls.ov:= iv0).ov = iv0 | An Axiom |
| PLIBGInv | ⊦ PLIBGInv(gs) ↔ allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true) | An Axiom |
| disj-callARun-globalAPersist | ⊦ callARun(t) ≠ globalAPersist(l) | An Axiom |
| pre-resRead | ⊦ pre(gs, ls, resRead, a) ↔ (∃ v0. a = ARetRead(ls.t, v0) ∧ v0 = ls.ov) | An Axiom |
| gen-PLIBGState | PLIBGState freely generated by mkPLIBgs; | An Axiom |
| disj-ready-resRead | ⊦ ready ≠ resRead | An Axiom |
| sel-mkPLIBls-dotil | ⊦ mkPLIBls(t, il, iv, iv0).il = il | An Axiom |
| pre-crashed | ⊦ pre(gs, ls, crashed, a) ↔ false | An Axiom |
| disj-AInvRead-globalACrash | ⊦ AInvRead(t, l) ≠ globalACrash | An Axiom |
| disj-ready-resWrite | ⊦ ready ≠ resWrite | An Axiom |
| inj-callTSync | ⊦ callTSync(t) = callTSync(t0) ↔ t = t0 | An Axiom |
| disj-AInvWrite-globalAPersist | ⊦ AInvWrite(t, l, val) ≠ globalAPersist(l0) | An Axiom |
| sel-callARun-dott | ⊦ callARun(t).t = t | An Axiom |
| case-PLIBPC | ⊦ pc = crashed ∨ pc = idle ∨ pc = invRead ∨ pc = invWrite ∨ pc = ready ∨ pc = resRead ∨ pc = resWrite | An Axiom |
| pre-ready | ⊦ pre(gs, ls, ready, a) ↔ a = callTSync(ls.t) ∧ (gs.h | ls.t) | false = [] ∨ (∃ l, v. a = AInvWrite(ls.t, l, v)) ∨ (∃ l. a = AInvRead(ls.t, l)) | An Axiom |
| disj-invRead-resRead | ⊦ invRead ≠ resRead | An Axiom |
| inj-mkstate | ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0 | An Axiom |
| updsel--dotpm-dotvm | ⊦ (gs.pm:= vm0).vm = gs.vm | An Axiom |
| upd-mkPLIBgs-doth | ⊦ mkPLIBgs(vm, vm0, h).h:= h0 = mkPLIBgs(vm, vm0, h0) | An Axiom |
| gen-PLIBAction | PLIBAction freely generated by globalACrash, τ, ADoRead, ADoWrite, AInvRead, AInvWrite, ARetRead, ARetWrite, callARun, callTSync, globalAPersist; | An Axiom |
| disj-globalACrash-globalAPersist | ⊦ globalACrash ≠ globalAPersist(l) | An Axiom |
| disj-crashed-resRead | ⊦ crashed ≠ resRead | An Axiom |
| inj-callARun | ⊦ callARun(t) = callARun(t0) ↔ t = t0 | An Axiom |
| updsel--dott-dotov | ⊦ (ls.t:= t).ov = ls.ov | An Axiom |
| disj-callTSync-tau | ⊦ callTSync(t) ≠ τ | An Axiom |
| sel-AInvWrite-dotloc | ⊦ AInvWrite(t, l, val).loc = l | An Axiom |
| updsel--dotpcf-dotgstate | ⊦ (s.pcf:= pcf).gstate = s.gstate | An Axiom |
| updsel--dotpcf-dotlsf | ⊦ (s.pcf:= pcf).lsf = s.lsf | An Axiom |
| disj-ADoWrite-ARetWrite | ⊦ ADoWrite(t) ≠ ARetWrite(t0) | An Axiom |
| updsel--doth-dotvm | ⊦ (gs.h:= h).vm = gs.vm | An Axiom |
| disj-idle-resRead | ⊦ idle ≠ resRead | An Axiom |
| disj-crashed-idle | ⊦ crashed ≠ idle | An Axiom |
| disj-crashed-invRead | ⊦ crashed ≠ invRead | An Axiom |
| case-PLIBAction | ⊦ a = ADoRead(a.t) ∨ a = ADoWrite(a.t) ∨ a = AInvRead(a.t, a.l) ∨ a = AInvWrite(a.t, a.loc, a.val) ∨ a = ARetRead(a.t, a.v) ∨ a = ARetWrite(a.t) ∨ a = callARun(a.t) ∨ a = callTSync(a.t) ∨ a = globalACrash ∨ a = globalAPersist(a.invAPersistl) ∨ a = τ | An Axiom |
| disj-ADoWrite-callTSync | ⊦ ADoWrite(t) ≠ callTSync(t0) | An Axiom |
| updsel--dott-dotiv | ⊦ (ls.t:= t).iv = ls.iv | An Axiom |
| updsel--dotiv-dotil | ⊦ (ls.iv:= iv).il = ls.il | An Axiom |
| gen-PLIBPC | PLIBPC freely generated by crashed, idle, invRead, invWrite, ready, resRead, resWrite; | An Axiom |
| sel-mkPLIBls-dott | ⊦ mkPLIBls(t, il, iv, iv0).t = t | An Axiom |
| updsel--dotil-dotil | ⊦ (ls.il:= il).il = il | An Axiom |
| upd-mkPLIBls-dotov | ⊦ mkPLIBls(t, il, iv, iv0).ov:= iv2 = mkPLIBls(t, il, iv, iv2) | An Axiom |
| updsel--doth-dotpm | ⊦ (gs.h:= h).pm = gs.pm | An Axiom |
| disj-AInvWrite-globalACrash | ⊦ AInvWrite(t, l, val) ≠ globalACrash | An Axiom |
| upd-mkPLIBgs-dotpm | ⊦ mkPLIBgs(vm, vm0, h).pm:= vm2 = mkPLIBgs(vm, vm2, h) | An Axiom |
| inj-ADoRead | ⊦ ADoRead(t) = ADoRead(t0) ↔ t = t0 | An Axiom |
| disj-idle-invRead | ⊦ idle ≠ invRead | An Axiom |
| disj-ADoRead-tau | ⊦ ADoRead(t) ≠ τ | An Axiom |
| updsel--dotpm-dotpm | ⊦ (gs.pm:= vm0).pm = vm0 | An Axiom |
| disj-ADoRead-AInvWrite | ⊦ ADoRead(t) ≠ AInvWrite(t0, l, val) | An Axiom |
| upd-mkstate-dotpcf | ⊦ (mkstate(gstate, lsf, pcf).pcf:= pcf0) = mkstate(gstate, lsf, pcf0) | An Axiom |
| disj-globalAPersist-tau | ⊦ globalAPersist(l) ≠ τ | An Axiom |
| inj-mkPLIBls | ⊦ mkPLIBls(t, il, iv, iv0) = mkPLIBls(t0, il0, iv1, iv2) ↔ t = t0 ∧ il = il0 ∧ iv = iv1 ∧ iv0 = iv2 | An Axiom |
| sel-mkPLIBgs-dotpm | ⊦ mkPLIBgs(vm, vm0, h).pm = vm0 | An Axiom |
| disj-ADoWrite-AInvRead | ⊦ ADoWrite(t) ≠ AInvRead(t0, l) | An Axiom |
| updsel--dotiv-dott | ⊦ (ls.iv:= iv).t = ls.t | An Axiom |
| gen-PLIBState | PLIBState freely generated by mkstate; | An Axiom |
| sel-ADoWrite-dott | ⊦ ADoWrite(t).t = t | An Axiom |
| plibInit | ⊦ plibInit(mkstate(gs, lsf, pcf)) ↔ (gs.vm = ∅ ∧ gs.pm = ∅ ∧ pcf = (λ t. idle) ∧ gs.h = []) ∧ (∀ t. lsf(t).t = t) | An Axiom |
| updsel--dotov-dotiv | ⊦ (ls.ov:= iv0).iv = ls.iv | An Axiom |
| disj-ADoRead-globalAPersist | ⊦ ADoRead(t) ≠ globalAPersist(l) | An Axiom |
| disj-ARetWrite-globalACrash | ⊦ ARetWrite(t) ≠ globalACrash | An Axiom |
| lstepf-ready-INVREAD | ⊦ ls.t = t → lstepf(gs, ls, ready, AInvRead(t, l)) = ls.il:= l | An Axiom |
| sel-AInvRead-dott | ⊦ AInvRead(t, l).t = t | An Axiom |
| disj-ADoWrite-ARetRead | ⊦ ADoWrite(t) ≠ ARetRead(t0, val) | An Axiom |
| lstepf-ready-TSync | ⊦ ls.t = t → lstepf(gs, ls, ready, callTSync(t)) = ls | An Axiom |
| sel-mkstate-dotpcf | ⊦ mkstate(gstate, lsf, pcf).pcf = pcf | An Axiom |
| updsel--dotlsf-dotgstate | ⊦ (s.lsf:= lsf).gstate = s.gstate | An Axiom |
| disj-AInvRead-AInvWrite | ⊦ AInvRead(t, l) ≠ AInvWrite(t0, l0, val) | An Axiom |
| sel-ADoRead-dott | ⊦ ADoRead(t).t = t | An Axiom |
| lstepf-resWrite-RETWRITE | ⊦ ls.t = t → lstepf(gs, ls, resWrite, ARetWrite(t)) = ls | An Axiom |
| disj-callTSync-globalAPersist | ⊦ callTSync(t) ≠ globalAPersist(l) | An Axiom |
| disj-ARetRead-callARun | ⊦ ARetRead(t, val) ≠ callARun(t0) | An Axiom |
| pre-invRead | ⊦ pre(gs, ls, invRead, a) ↔ a = ADoRead(ls.t) | An Axiom |
| disj-ADoRead-ADoWrite | ⊦ ADoRead(t) ≠ ADoWrite(t0) | An Axiom |
| upd-mkstate-dotgstate | ⊦ (mkstate(gstate, lsf, pcf).gstate:= gstate0) = mkstate(gstate0, lsf, pcf) | An Axiom |
| disj-ADoRead-ARetWrite | ⊦ ADoRead(t) ≠ ARetWrite(t0) | An Axiom |
| gstepf-invRead-ADOREAD | ⊦ ls.t = t → gstepf(gs, ls, invRead, ADoRead(t)) = gs.h:= (gs.h + (R(ls.t, ls.il, gs.vm(ls.il)), gs.h.lastPersistedOrElse(ls.il, true))) | An Axiom |
| sel-globalAPersist-dotinvAPersistl | ⊦ globalAPersist(l).invAPersistl = l | An Axiom |
| gstepf-resWrite-RETWRITE | ⊦ ls.t = t → gstepf(gs, ls, resWrite, ARetWrite(t)) = gs | An Axiom |
| disj-ADoWrite-callARun | ⊦ ADoWrite(t) ≠ callARun(t0) | An Axiom |
| disj-AInvWrite-ARetRead | ⊦ AInvWrite(t, l, val) ≠ ARetRead(t0, val0) | An Axiom |
| disj-ADoRead-callTSync | ⊦ ADoRead(t) ≠ callTSync(t0) | An Axiom |
| disj-callTSync-globalACrash | ⊦ callTSync(t) ≠ globalACrash | An Axiom |
| sel-ARetRead-dott | ⊦ ARetRead(t, val).t = t | An Axiom |
| disj-invRead-ready | ⊦ invRead ≠ ready | An Axiom |
| disj-ADoRead-globalACrash | ⊦ ADoRead(t) ≠ globalACrash | An Axiom |
| upd-mkPLIBls-dotiv | ⊦ mkPLIBls(t, il, iv, iv0).iv:= iv1 = mkPLIBls(t, il, iv1, iv0) | An Axiom |
| sel-mkPLIBls-dotov | ⊦ mkPLIBls(t, il, iv, iv0).ov = iv0 | An Axiom |
| pcstepf-invRead-ADOREAD | ⊦ ls.t = t → pcstepf(gs, ls, invRead, ADoRead(t)) = resRead | An Axiom |
| plib-inv-allReadsOK | ⊦ PLIBInv(mkPLIBgs(vm, pm, h), lsf, pcf) → allReadsOK(h) | A User Theorem |
| ACrash | ACrash(pm; vm, h, pcf){pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), vm := pm, h := h | true} | An Axiom |
| inj-globalAPersist | ⊦ globalAPersist(l) = globalAPersist(l0) ↔ l = l0 | An Axiom |
| not-pre-global-persist | ⊦ ¬ pre(gs, ls, pc, globalAPersist(l)) | A User Theorem |
| disj-AInvRead-ARetWrite | ⊦ AInvRead(t, l) ≠ ARetWrite(t0) | An Axiom |
| lstepf-idle-ARun | ⊦ ls.t = t → lstepf(gs, ls, idle, callARun(t)) = ls | An Axiom |
| updsel--dotgstate-dotpcf | ⊦ (s.gstate:= gstate).pcf = s.pcf | An Axiom |
| disj-ARetRead-tau | ⊦ ARetRead(t, val) ≠ τ | An Axiom |
| disj-AInvWrite-ARetWrite | ⊦ AInvWrite(t, l, val) ≠ ARetWrite(t0) | An Axiom |
| inj-ADoWrite | ⊦ ADoWrite(t) = ADoWrite(t0) ↔ t = t0 | An Axiom |