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-ctrReadPSC-invFLITPSCREAD | ⊦ ctrReadPSC(t, l, n) ≠ invFLITPSCREAD(t0, l0) | An Axiom |
| gen-FLITPSCGState | FLITPSCGState freely generated by mkFLITPSCgs; | An Axiom |
| disj-callPSCCOMPLETE-doReadPSC | ⊦ callPSCCOMPLETE(t) ≠ doReadPSC(t0, l, v) | An Axiom |
| disj-pwbPSC-sfencePSC | ⊦ pwbPSC(t, l) ≠ sfencePSC(t0) | An Axiom |
| updsel--dotpcf-dotpcf | ⊦ (s.pcf:= pcf).pcf = pcf | An Axiom |
| sel-ctrIncPSC-dottid | ⊦ ctrIncPSC(t, l).tid = t | An Axiom |
| disj-ctrIncPSC-pwbPSC | ⊦ ctrIncPSC(t, l) ≠ pwbPSC(t0, l0) | An Axiom |
| disj-invFLITPSCREAD-retFLITPSCWRITE | ⊦ invFLITPSCREAD(t, l) ≠ retFLITPSCWRITE(t0) | An Axiom |
| sel-retFLITPSCREAD-dott | ⊦ retFLITPSCREAD(t, v).t = t | An Axiom |
| updsel--dotlsf-dotpcf | ⊦ (s.lsf:= lsf).pcf = s.pcf | An Axiom |
| disj-ctrIncPSC-doReadPSC | ⊦ ctrIncPSC(t, l) ≠ doReadPSC(t0, l0, v) | An Axiom |
| disj-W2-ready | ⊦ W2 ≠ ready | An Axiom |
| disj-callPSCCOMPLETE-doWritePSC | ⊦ callPSCCOMPLETE(t) ≠ doWritePSC(t0, l, v) | An Axiom |
| disj-doReadPSC-globalPSCPERSISTuscFO | ⊦ doReadPSC(t, l, v) ≠ globalPSCPERSIST_FO(l0) | An Axiom |
| disj-atomicW5-callPSCCOMPLETE | ⊦ atomicW5 ≠ callPSCCOMPLETE(t) | An Axiom |
| lstepf-W7 | ⊦ ls.t = t → lstepf(gs, ls, W7, retFLITPSCWRITE(t)) = ls | An Axiom |
| updsel--dotp-dotp | ⊦ (gs.p:= p).p = p | An Axiom |
| pcstepf-R3 | ⊦ pcstepf(gs, ls, R3, a) = R4 | An Axiom |
| updsel--dotreaders-dotwriters | ⊦ (gs.readers:= writers0).writers = gs.writers | An Axiom |
| disj-doReadPSC-sfencePSC | ⊦ doReadPSC(t, l, v) ≠ sfencePSC(t0) | An Axiom |
| gstepf-R3 | ⊦ gstepf(gs, ls, R3, a) = (gs.p:= gs.p(ls.l := gs.p(ls.l) + FO(ls.t))).readers:= gs.readers(ls.l := gs.readers(ls.l) -- ls.t) | An Axiom |
| disj-W2-W4 | ⊦ W2 ≠ W4 | An Axiom |
| upd-mkstate-dotlsf | ⊦ (mkstate(gstate, lsf, pcf).lsf:= lsf0) = mkstate(gstate, lsf0, pcf) | An Axiom |
| disj-R1-idle | ⊦ R1 ≠ idle | An Axiom |
| updsel--dotv-dotv | ⊦ (ls.v:= v).v = v | An Axiom |
| disj-callPSCCOMPLETE-globalPSCPERSISTuscW | ⊦ callPSCCOMPLETE(t) ≠ globalPSCPERSIST_W(l) | An Axiom |
| lstepf-W1 | ⊦ lstepf(gs, ls, W1, a) = ls | An Axiom |
| updsel--dott-dotl | ⊦ (ls.t:= t).l = ls.l | An Axiom |
| inj-ctrReadPSC | ⊦ ctrReadPSC(t, l, n) = ctrReadPSC(t0, l0, n0) ↔ t = t0 ∧ l = l0 ∧ n = n0 | An Axiom |
| gstepf-W3 | ⊦ gstepf(gs, ls, W3, a) = gs.p:= gs.p(ls.l := gs.p(ls.l) + W(ls.v, ls.t)) | An Axiom |
| pcstepf-ready-PSCCOMPLETE | ⊦ ls.t = t → pcstepf(gs, ls, ready, callPSCCOMPLETE(t)) = ready | An Axiom |
| PSCCRASH | PSCCRASH(; p, ctr, writers, readers, pcf) {pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), p := λ l. [], ctr := λ l. 0, readers := λ l. ∅, writers := λ l. ∅} | An Axiom |
| disj-atomicW1-sfencePSC | ⊦ atomicW1 ≠ sfencePSC(t) | An Axiom |
| sel-mkFLITPSCls-dotl | ⊦ mkFLITPSCls(t, l, v).l = l | An Axiom |
| disj-R4-W3 | ⊦ R4 ≠ W3 | An Axiom |
| disj-W5-crashed | ⊦ W5 ≠ crashed | An Axiom |
| updsel--dotctr-dotmem | ⊦ (gs.ctr:= ctr).mem = gs.mem | An Axiom |
| disj-callPSCRUN-globalPSCPERSISTuscW | ⊦ callPSCRUN(t) ≠ globalPSCPERSIST_W(l) | An Axiom |
| disj-R2-W3 | ⊦ R2 ≠ W3 | An Axiom |
| disj-callPSCRUN-retFLITPSCREAD | ⊦ callPSCRUN(t) ≠ retFLITPSCREAD(t0, v) | An Axiom |
| pre-W6 | ⊦ pre(gs, ls, W6, a) ↔ a = ctrDecPSC(ls.t, ls.l) | An Axiom |
| gstepf-ready | ⊦ gstepf(gs, ls, ready, a) = gs | An Axiom |
| disj-W5-ready | ⊦ W5 ≠ ready | An Axiom |
| disj-globalPSCPERSISTuscFO-invFLITPSCREAD | ⊦ globalPSCPERSIST_FO(l) ≠ invFLITPSCREAD(t, l0) | An Axiom |
| disj-ctrReadPSC-globalPSCPERSISTuscFO | ⊦ ctrReadPSC(t, l, n) ≠ globalPSCPERSIST_FO(l0) | An Axiom |
| gstepf-W6 | ⊦ gstepf(gs, ls, W6, a) = (gs.ctr:= gs.ctr(ls.l := gs.ctr(ls.l) - 1)).writers:= gs.writers(ls.l := gs.writers(ls.l) -- ls.t) | An Axiom |
| disj-pwbPSC-tau | ⊦ pwbPSC(t, l) ≠ τ | An Axiom |
| sel-doWritePSC-dottid | ⊦ doWritePSC(t, l, v).tid = t | An Axiom |
| upd-mkFLITPSCgs-dotp | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0) | An Axiom |
| disj-callPSCRUN-ctrIncPSC | ⊦ callPSCRUN(t) ≠ ctrIncPSC(t0, l) | An Axiom |
| FLITPSCGInv | ⊦ FLITPSCGInv(gs) ↔ ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p) | An Axiom |
| sel-doReadPSC-dotv | ⊦ doReadPSC(t, l, v).v = v | An Axiom |
| disj-atomicW5-ctrDecPSC | ⊦ atomicW5 ≠ ctrDecPSC(t, l) | An Axiom |
| disj-retFLITPSCWRITE-sfencePSC | ⊦ retFLITPSCWRITE(t) ≠ sfencePSC(t0) | An Axiom |
| disj-ctrDecPSC-invFLITPSCREAD | ⊦ ctrDecPSC(t, l) ≠ invFLITPSCREAD(t0, l0) | An Axiom |
| disj-R3-W1 | ⊦ R3 ≠ W1 | An Axiom |
| disj-invFLITPSCWRITE-retFLITPSCREAD | ⊦ invFLITPSCWRITE(t, l, v) ≠ retFLITPSCREAD(t0, v0) | An Axiom |
| disj-R1-R4 | ⊦ R1 ≠ R4 | An Axiom |
| disj-atomicW5-invFLITPSCREAD | ⊦ atomicW5 ≠ invFLITPSCREAD(t, l) | An Axiom |
| disj-R2-ready | ⊦ R2 ≠ ready | An Axiom |
| disj-ctrIncPSC-ctrReadPSC | ⊦ ctrIncPSC(t, l) ≠ ctrReadPSC(t0, l0, n) | An Axiom |
| disj-invFLITPSCREAD-pwbPSC | ⊦ invFLITPSCREAD(t, l) ≠ pwbPSC(t0, l0) | An Axiom |
| sel-invFLITPSCWRITE-dotinvFLITPSCWRITEv | ⊦ invFLITPSCWRITE(t, l, v).invFLITPSCWRITEv = v | An Axiom |
| disj-callPSCRUN-globalPSCCRASH | ⊦ callPSCRUN(t) ≠ globalPSCCRASH | An Axiom |
| disj-atomicW1-ctrReadPSC | ⊦ atomicW1 ≠ ctrReadPSC(t, l, n) | An Axiom |
| pcstepf-W6 | ⊦ pcstepf(gs, ls, W6, a) = W7 | An Axiom |
| disj-R4-crashed | ⊦ R4 ≠ crashed | An Axiom |
| updsel--dotmem-dotmem | ⊦ (gs.mem:= mem).mem = mem | An Axiom |
| disj-W4-idle | ⊦ W4 ≠ idle | An Axiom |
| disj-callPSCRUN-invFLITPSCWRITE | ⊦ callPSCRUN(t) ≠ invFLITPSCWRITE(t0, l, v) | An Axiom |
| sel-mkFLITPSCgs-dotmem | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).mem = mem | An Axiom |
| disj-ctrReadPSC-globalPSCPERSISTuscW | ⊦ ctrReadPSC(t, l, n) ≠ globalPSCPERSIST_W(l0) | An Axiom |
| disj-W1-W2 | ⊦ W1 ≠ W2 | An Axiom |
| disj-ctrReadPSC-sfencePSC | ⊦ ctrReadPSC(t, l, n) ≠ sfencePSC(t0) | An Axiom |
| sel-ctrReadPSC-dottid | ⊦ ctrReadPSC(t, l, n).tid = t | An Axiom |
| disj-R1-W1 | ⊦ R1 ≠ W1 | An Axiom |
| disj-R2-W6 | ⊦ R2 ≠ W6 | An Axiom |
| disj-ctrReadPSC-retFLITPSCREAD | ⊦ ctrReadPSC(t, l, n) ≠ retFLITPSCREAD(t0, v) | An Axiom |
| disj-R3-W4 | ⊦ R3 ≠ W4 | An Axiom |
| sel-mkstate-dotgstate | ⊦ mkstate(gstate, lsf, pcf).gstate = gstate | An Axiom |
| disj-ctrDecPSC-sfencePSC | ⊦ ctrDecPSC(t, l) ≠ sfencePSC(t0) | An Axiom |
| disj-callPSCCOMPLETE-ctrReadPSC | ⊦ callPSCCOMPLETE(t) ≠ ctrReadPSC(t0, l, n) | An Axiom |
| inj-mkFLITPSCgs | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0) = mkFLITPSCgs(mem0, p0, ctr0, writers1, writers2) ↔ mem = mem0 ∧ p = p0 ∧ ctr = ctr0 ∧ writers = writers1 ∧ writers0 = writers2 | An Axiom |
| disj-W3-W5 | ⊦ W3 ≠ W5 | An Axiom |
| disj-ctrIncPSC-tau | ⊦ ctrIncPSC(t, l) ≠ τ | An Axiom |
| disj-atomicW1-globalPSCPERSISTuscW | ⊦ atomicW1 ≠ globalPSCPERSIST_W(l) | An Axiom |
| disj-doWritePSC-globalPSCPERSISTuscFO | ⊦ doWritePSC(t, l, v) ≠ globalPSCPERSIST_FO(l0) | An Axiom |
| updsel--dotp-dotwriters | ⊦ (gs.p:= p).writers = gs.writers | An Axiom |
| not-pre-global-crash | ⊦ ¬ pre(gs, ls, pc, globalPSCCRASH) | A User Theorem |
| disj-globalPSCPERSISTuscFO-invFLITPSCWRITE | ⊦ globalPSCPERSIST_FO(l) ≠ invFLITPSCWRITE(t, l0, v) | An Axiom |
| disj-globalPSCPERSISTuscW-invFLITPSCWRITE | ⊦ globalPSCPERSIST_W(l) ≠ invFLITPSCWRITE(t, l0, v) | An Axiom |
| disj-globalPSCPERSISTuscFO-retFLITPSCREAD | ⊦ globalPSCPERSIST_FO(l) ≠ retFLITPSCREAD(t, v) | An Axiom |
| disj-W2-crashed | ⊦ W2 ≠ crashed | An Axiom |
| disj-crashed-ready | ⊦ crashed ≠ ready | An Axiom |
| updsel--dotl-dotv | ⊦ (ls.l:= l).v = ls.v | An Axiom |
| disj-W1-W5 | ⊦ W1 ≠ W5 | An Axiom |
| pre-W3 | ⊦ pre(gs, ls, W3, a) ↔ a = doWritePSC(ls.t, ls.l, ls.v) | An Axiom |
| disj-callPSCCOMPLETE-ctrDecPSC | ⊦ callPSCCOMPLETE(t) ≠ ctrDecPSC(t0, l) | An Axiom |
| disj-invFLITPSCWRITE-tau | ⊦ invFLITPSCWRITE(t, l, v) ≠ τ | An Axiom |
| disj-R1-W4 | ⊦ R1 ≠ W4 | An Axiom |
| disj-ctrReadPSC-globalPSCCRASH | ⊦ ctrReadPSC(t, l, n) ≠ globalPSCCRASH | An Axiom |
| disj-W1-ready | ⊦ W1 ≠ ready | An Axiom |
| disj-atomicW1-invFLITPSCREAD | ⊦ atomicW1 ≠ invFLITPSCREAD(t, l) | An Axiom |
| sel-invFLITPSCREAD-dott | ⊦ invFLITPSCREAD(t, l).t = t | An Axiom |
| sel-globalPSCPERSISTuscW-dotinvPSCPERSISTuscWl | ⊦ globalPSCPERSIST_W(l).invPSCPERSIST_Wl = l | An Axiom |
| disj-atomicW5-globalPSCPERSISTuscFO | ⊦ atomicW5 ≠ globalPSCPERSIST_FO(l) | An Axiom |
| inj-invFLITPSCWRITE | ⊦ invFLITPSCWRITE(t, l, v) = invFLITPSCWRITE(t0, l0, v0) ↔ t = t0 ∧ l = l0 ∧ v = v0 | An Axiom |
| lstepf-R3 | ⊦ lstepf(gs, ls, R3, a) = ls | An Axiom |
| disj-ctrDecPSC-retFLITPSCREAD | ⊦ ctrDecPSC(t, l) ≠ retFLITPSCREAD(t0, v) | An Axiom |
| sel-mkFLITPSCgs-dotp | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p | An Axiom |
| disj-R3-W7 | ⊦ R3 ≠ W7 | An Axiom |
| gen-FLITPSCAction | FLITPSCAction freely generated by atomicW1, atomicW5, globalPSCCRASH, τ, callPSCCOMPLETE, callPSCRUN, ctrDecPSC, ctrIncPSC, ctrReadPSC, doReadPSC, doWritePSC, globalPSCPERSIST_FO, globalPSCPERSIST_W, invFLITPSCREAD, invFLITPSCWRITE, pwbPSC, retFLITPSCREAD, retFLITPSCWRITE, sfencePSC ; | An Axiom |
| sel-ctrDecPSC-dotl | ⊦ ctrDecPSC(t, l).l = l | An Axiom |
| gen-FLITPSCState | FLITPSCState freely generated by mkstate; | An Axiom |
| disj-atomicW1-pwbPSC | ⊦ atomicW1 ≠ pwbPSC(t, l) | An Axiom |
| disj-R1-crashed | ⊦ R1 ≠ crashed | An Axiom |
| elim-mkstate | ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf) | An Axiom |
| disj-R1-W7 | ⊦ R1 ≠ W7 | An Axiom |
| pre-idle | ⊦ pre(gs, ls, idle, a) ↔ a = callPSCRUN(ls.t) | An Axiom |
| disj-R3-idle | ⊦ R3 ≠ idle | An Axiom |
| disj-atomicW1-doReadPSC | ⊦ atomicW1 ≠ doReadPSC(t, l, v) | An Axiom |
| disj-callPSCRUN-pwbPSC | ⊦ callPSCRUN(t) ≠ pwbPSC(t0, l) | An Axiom |
| disj-W7-crashed | ⊦ W7 ≠ crashed | An Axiom |
| disj-ctrDecPSC-globalPSCPERSISTuscFO | ⊦ ctrDecPSC(t, l) ≠ globalPSCPERSIST_FO(l0) | An Axiom |
| pcstepf-W3 | ⊦ pcstepf(gs, ls, W3, a) = W4 | An Axiom |
| sel-ctrDecPSC-dottid | ⊦ ctrDecPSC(t, l).tid = t | An Axiom |
| disj-callPSCRUN-globalPSCPERSISTuscFO | ⊦ callPSCRUN(t) ≠ globalPSCPERSIST_FO(l) | An Axiom |
| sel-pwbPSC-dottid | ⊦ pwbPSC(t, l).tid = t | An Axiom |
| disj-R2-idle | ⊦ R2 ≠ idle | An Axiom |
| disj-ctrDecPSC-pwbPSC | ⊦ ctrDecPSC(t, l) ≠ pwbPSC(t0, l0) | An Axiom |
| disj-atomicW5-retFLITPSCREAD | ⊦ atomicW5 ≠ retFLITPSCREAD(t, v) | An Axiom |
| disj-atomicW5-callPSCRUN | ⊦ atomicW5 ≠ callPSCRUN(t) | An Axiom |
| updsel--dotp-dotreaders | ⊦ (gs.p:= p).readers = gs.readers | An Axiom |
| gstepf-idle-PSCRUN | ⊦ ls.t = t → gstepf(gs, ls, idle, callPSCRUN(t)) = gs | An Axiom |
| disj-atomicW5-ctrIncPSC | ⊦ atomicW5 ≠ ctrIncPSC(t, l) | An Axiom |
| disj-R2-W5 | ⊦ R2 ≠ W5 | An Axiom |
| disj-ctrDecPSC-globalPSCCRASH | ⊦ ctrDecPSC(t, l) ≠ globalPSCCRASH | An Axiom |
| lstepf-ready-FLITPSCWRITE | ⊦ ls.t = t → lstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = (ls.l:= l0).v:= v0 | An Axiom |
| sel-invFLITPSCREAD-dotinvFLITPSCREADl | ⊦ invFLITPSCREAD(t, l).invFLITPSCREADl = l | An Axiom |
| disj-ctrReadPSC-pwbPSC | ⊦ ctrReadPSC(t, l, n) ≠ pwbPSC(t0, l0) | An Axiom |
| disj-R1-R3 | ⊦ R1 ≠ R3 | An Axiom |
| disj-callPSCRUN-retFLITPSCWRITE | ⊦ callPSCRUN(t) ≠ retFLITPSCWRITE(t0) | An Axiom |
| disj-pwbPSC-retFLITPSCREAD | ⊦ pwbPSC(t, l) ≠ retFLITPSCREAD(t0, v) | An Axiom |
| disj-retFLITPSCREAD-retFLITPSCWRITE | ⊦ retFLITPSCREAD(t, v) ≠ retFLITPSCWRITE(t0) | An Axiom |
| disj-globalPSCPERSISTuscW-invFLITPSCREAD | ⊦ globalPSCPERSIST_W(l) ≠ invFLITPSCREAD(t, l0) | An Axiom |
| pre-R2 | ⊦ pre(gs, ls, R2, a) ↔ a = ctrReadPSC(ls.t, ls.l, gs.ctr(ls.l)) | An Axiom |
| inj-globalPSCPERSISTuscW | ⊦ globalPSCPERSIST_W(l) = globalPSCPERSIST_W(l0) ↔ l = l0 | An Axiom |
| disj-atomicW1-retFLITPSCREAD | ⊦ atomicW1 ≠ retFLITPSCREAD(t, v) | An Axiom |
| inj-invFLITPSCREAD | ⊦ invFLITPSCREAD(t, l) = invFLITPSCREAD(t0, l0) ↔ t = t0 ∧ l = l0 | An Axiom |
| upd-mkFLITPSCls-dott | ⊦ mkFLITPSCls(t, l, v).t:= t0 = mkFLITPSCls(t0, l, v) | An Axiom |
| disj-atomicW5-globalPSCCRASH | ⊦ atomicW5 ≠ globalPSCCRASH | An Axiom |
| inj-callPSCCOMPLETE | ⊦ callPSCCOMPLETE(t) = callPSCCOMPLETE(t0) ↔ t = t0 | An Axiom |
| updsel--dotwriters-dotmem | ⊦ (gs.writers:= writers).mem = gs.mem | An Axiom |
| disj-atomicW5-pwbPSC | ⊦ atomicW5 ≠ pwbPSC(t, l) | An Axiom |
| disj-W4-W6 | ⊦ W4 ≠ W6 | An Axiom |
| disj-W6-idle | ⊦ W6 ≠ idle | An Axiom |
| disj-W5-idle | ⊦ W5 ≠ idle | An Axiom |
| disj-doWritePSC-pwbPSC | ⊦ doWritePSC(t, l, v) ≠ pwbPSC(t0, l0) | An Axiom |
| disj-R4-W5 | ⊦ R4 ≠ W5 | An Axiom |
| sel-mkstate-dotlsf | ⊦ mkstate(gstate, lsf, pcf).lsf = lsf | An Axiom |
| disj-callPSCCOMPLETE-pwbPSC | ⊦ callPSCCOMPLETE(t) ≠ pwbPSC(t0, l) | An Axiom |
| sel-callPSCCOMPLETE-dott | ⊦ callPSCCOMPLETE(t).t = t | An Axiom |
| disj-ctrReadPSC-doReadPSC | ⊦ ctrReadPSC(t, l, n) ≠ doReadPSC(t0, l0, v) | An Axiom |
| disj-atomicW5-globalPSCPERSISTuscW | ⊦ atomicW5 ≠ globalPSCPERSIST_W(l) | An Axiom |
| sel-doWritePSC-dotv | ⊦ doWritePSC(t, l, v).v = v | An Axiom |
| flitpscStep | ⊦ flitpscStep(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)) ∨ (∃ l. a = globalPSCPERSIST_W(l) ∧ 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))) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, gs.p(l))) ∧ ⟨p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)) ∨ a = globalPSCCRASH ∧ ⟨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⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) | An Axiom |
| updsel--dotctr-dotctr | ⊦ (gs.ctr:= ctr).ctr = ctr | 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 |
| disj-W2-W6 | ⊦ W2 ≠ W6 | An Axiom |
| lstepf-W3 | ⊦ lstepf(gs, ls, W3, a) = ls | An Axiom |
| sel-invFLITPSCWRITE-dotinvFLITPSCWRITEl | ⊦ invFLITPSCWRITE(t, l, v).invFLITPSCWRITEl = l | An Axiom |
| case-FLITPSCLState | ⊦ mkFLITPSCls(ls.t, ls.l, ls.v) = ls | An Axiom |
| inj-sfencePSC | ⊦ sfencePSC(t) = sfencePSC(t0) ↔ t = t0 | An Axiom |
| updsel--dotgstate-dotlsf | ⊦ (s.gstate:= gstate).lsf = s.lsf | An Axiom |
| disj-ctrDecPSC-tau | ⊦ ctrDecPSC(t, l) ≠ τ | An Axiom |
| upd-mkFLITPSCgs-dotmem | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).mem:= mem0 = mkFLITPSCgs(mem0, p, ctr, writers, writers0) | An Axiom |
| disj-callPSCCOMPLETE-retFLITPSCWRITE | ⊦ callPSCCOMPLETE(t) ≠ retFLITPSCWRITE(t0) | An Axiom |
| disj-callPSCCOMPLETE-invFLITPSCWRITE | ⊦ callPSCCOMPLETE(t) ≠ invFLITPSCWRITE(t0, l, v) | An Axiom |
| updsel--dotmem-dotctr | ⊦ (gs.mem:= mem).ctr = gs.ctr | An Axiom |
| sel-mkFLITPSCgs-dotctr | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr | An Axiom |
| lstepf-W6 | ⊦ lstepf(gs, ls, W6, a) = ls | An Axiom |
| disj-idle-ready | ⊦ idle ≠ ready | An Axiom |
| disj-doWritePSC-invFLITPSCREAD | ⊦ doWritePSC(t, l, v) ≠ invFLITPSCREAD(t0, l0) | An Axiom |
| disj-globalPSCPERSISTuscW-retFLITPSCWRITE | ⊦ globalPSCPERSIST_W(l) ≠ retFLITPSCWRITE(t) | An Axiom |
| disj-globalPSCPERSISTuscFO-retFLITPSCWRITE | ⊦ globalPSCPERSIST_FO(l) ≠ retFLITPSCWRITE(t) | An Axiom |
| sel-globalPSCPERSISTuscFO-dotinvPSCPERSISTuscFOl | ⊦ globalPSCPERSIST_FO(l).invPSCPERSIST_FOl = l | An Axiom |
| disj-W4-crashed | ⊦ W4 ≠ crashed | An Axiom |
| disj-doReadPSC-tau | ⊦ doReadPSC(t, l, v) ≠ τ | An Axiom |
| disj-invFLITPSCWRITE-retFLITPSCWRITE | ⊦ invFLITPSCWRITE(t, l, v) ≠ retFLITPSCWRITE(t0) | An Axiom |
| disj-atomicW1-globalPSCCRASH | ⊦ atomicW1 ≠ globalPSCCRASH | An Axiom |
| disj-globalPSCPERSISTuscFO-tau | ⊦ globalPSCPERSIST_FO(l) ≠ τ | An Axiom |
| case-FLITPSCGState | ⊦ mkFLITPSCgs(gs.mem, gs.p, gs.ctr, gs.writers, gs.readers) = gs | An Axiom |
| sel-doReadPSC-dottid | ⊦ doReadPSC(t, l, v).tid = t | An Axiom |
| disj-ctrIncPSC-invFLITPSCWRITE | ⊦ ctrIncPSC(t, l) ≠ invFLITPSCWRITE(t0, l0, v) | An Axiom |
| disj-globalPSCCRASH-pwbPSC | ⊦ globalPSCCRASH ≠ pwbPSC(t, l) | An Axiom |
| updsel--dotlsf-dotlsf | ⊦ (s.lsf:= lsf).lsf = lsf | An Axiom |
| updsel--dotwriters-dotwriters | ⊦ (gs.writers:= writers).writers = writers | An Axiom |
| lstepf-idle-PSCRUN | ⊦ ls.t = t → lstepf(gs, ls, idle, callPSCRUN(t)) = ls | An Axiom |
| disj-doWritePSC-invFLITPSCWRITE | ⊦ doWritePSC(t, l, v) ≠ invFLITPSCWRITE(t0, l0, v0) | An Axiom |
| updsel--dotreaders-dotmem | ⊦ (gs.readers:= writers0).mem = gs.mem | An Axiom |
| disj-callPSCRUN-sfencePSC | ⊦ callPSCRUN(t) ≠ sfencePSC(t0) | An Axiom |
| pcstepf-R2 | ⊦ pcstepf(gs, ls, R2, a) = (gs.ctr(ls.l) ≠ 0 ⊃ R3;R4) | An Axiom |
| disj-doReadPSC-pwbPSC | ⊦ doReadPSC(t, l, v) ≠ pwbPSC(t0, l0) | An Axiom |
| gstepf-R2 | ⊦ gstepf(gs, ls, R2, a) = (gs.ctr(ls.l) ≠ 0 ⊃ gs;gs.readers:= gs.readers(ls.l := gs.readers(ls.l) -- ls.t)) | An Axiom |
| disj-invFLITPSCWRITE-pwbPSC | ⊦ invFLITPSCWRITE(t, l, v) ≠ pwbPSC(t0, l0) | An Axiom |
| gen-FLITPSCPC | FLITPSCPC freely generated by R1, R2, R3, R4, W1, W2, W3, W4, W5, W6, W7, crashed, idle, ready; | An Axiom |
| disj-ctrDecPSC-doReadPSC | ⊦ ctrDecPSC(t, l) ≠ doReadPSC(t0, l0, v) | An Axiom |
| disj-atomicW5-doWritePSC | ⊦ atomicW5 ≠ doWritePSC(t, l, v) | An Axiom |
| disj-atomicW1-tau | ⊦ atomicW1 ≠ τ | An Axiom |
| disj-globalPSCCRASH-invFLITPSCREAD | ⊦ globalPSCCRASH ≠ invFLITPSCREAD(t, l) | An Axiom |
| disj-ctrDecPSC-globalPSCPERSISTuscW | ⊦ ctrDecPSC(t, l) ≠ globalPSCPERSIST_W(l0) | An Axiom |
| disj-R2-W2 | ⊦ R2 ≠ W2 | An Axiom |
| disj-atomicW5-tau | ⊦ atomicW5 ≠ τ | An Axiom |
| disj-R4-W2 | ⊦ R4 ≠ W2 | An Axiom |
| FLITPSCInv | ⊦ FLITPSCInv(gs, lsf, pcf) ↔ FLITPSCGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ FLITPSCLInv(gs, lsf(t), pcf(t))) | An Axiom |
| disj-W4-ready | ⊦ W4 ≠ ready | An Axiom |
| disj-R3-W6 | ⊦ R3 ≠ W6 | An Axiom |
| disj-atomicW1-ctrDecPSC | ⊦ atomicW1 ≠ ctrDecPSC(t, l) | An Axiom |
| updsel--dotgstate-dotgstate | ⊦ (s.gstate:= gstate).gstate = gstate | An Axiom |
| disj-globalPSCCRASH-sfencePSC | ⊦ globalPSCCRASH ≠ sfencePSC(t) | An Axiom |
| sel-sfencePSC-dottid | ⊦ sfencePSC(t).tid = t | An Axiom |
| lstepf-R2 | ⊦ lstepf(gs, ls, R2, a) = ls | An Axiom |
| not-pre-global-tsync | ⊦ ¬ pre(gs, ls, pc, globalPSCPERSIST_FO(l)) | A User Theorem |
| gstepf-W2 | ⊦ gstepf(gs, ls, W2, a) = (gs.ctr:= gs.ctr(ls.l := gs.ctr(ls.l) + 1)).writers:= gs.writers(ls.l := gs.writers(ls.l) ++ ls.t) | An Axiom |
| updsel--dotv-dotl | ⊦ (ls.v:= v).l = ls.l | An Axiom |
| sel-mkFLITPSCls-dott | ⊦ mkFLITPSCls(t, l, v).t = t | An Axiom |
| disj-W5-W7 | ⊦ W5 ≠ W7 | An Axiom |
| inj-mkFLITPSCls | ⊦ mkFLITPSCls(t, l, v) = mkFLITPSCls(t0, l0, v0) ↔ t = t0 ∧ l = l0 ∧ v = v0 | An Axiom |
| disj-invFLITPSCREAD-tau | ⊦ invFLITPSCREAD(t, l) ≠ τ | An Axiom |
| disj-globalPSCPERSISTuscW-retFLITPSCREAD | ⊦ globalPSCPERSIST_W(l) ≠ retFLITPSCREAD(t, v) | An Axiom |
| disj-ctrReadPSC-tau | ⊦ ctrReadPSC(t, l, n) ≠ τ | An Axiom |
| updsel--dott-dott | ⊦ (ls.t:= t).t = t | An Axiom |
| disj-ctrIncPSC-globalPSCPERSISTuscW | ⊦ ctrIncPSC(t, l) ≠ globalPSCPERSIST_W(l0) | An Axiom |
| disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscW | ⊦ globalPSCPERSIST_FO(l) ≠ globalPSCPERSIST_W(l0) | An Axiom |
| disj-W2-W3 | ⊦ W2 ≠ W3 | An Axiom |
| pre-W5 | ⊦ pre(gs, ls, W5, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t) | An Axiom |
| disj-ctrDecPSC-doWritePSC | ⊦ ctrDecPSC(t, l) ≠ doWritePSC(t0, l0, v) | An Axiom |
| disj-W1-W7 | ⊦ W1 ≠ W7 | An Axiom |
| pcstepf-W2 | ⊦ pcstepf(gs, ls, W2, a) = W3 | An Axiom |
| disj-W3-W7 | ⊦ W3 ≠ W7 | An Axiom |
| fliqtStep-lem | ⊦ flitpscStep(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)) ∨ (∃ l. a = globalPSCPERSIST_W(l) ∧ 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))) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, gs.p(l)) ∧ gs0 = gs.p:= gs.p(l := gs.p(l) -p n)) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) | A User Theorem |
| disj-R4-idle | ⊦ R4 ≠ idle | An Axiom |
| inj-retFLITPSCWRITE | ⊦ retFLITPSCWRITE(t) = retFLITPSCWRITE(t0) ↔ t = t0 | An Axiom |
| disj-W1-crashed | ⊦ W1 ≠ crashed | An Axiom |
| disj-globalPSCPERSISTuscW-tau | ⊦ globalPSCPERSIST_W(l) ≠ τ | An Axiom |
| sel-ctrReadPSC-dotl | ⊦ ctrReadPSC(t, l, n).l = l | An Axiom |
| sel-doReadPSC-dotl | ⊦ doReadPSC(t, l, v).l = l | An Axiom |
| updsel--dotreaders-dotp | ⊦ (gs.readers:= writers0).p = gs.p | An Axiom |
| disj-doReadPSC-retFLITPSCWRITE | ⊦ doReadPSC(t, l, v) ≠ retFLITPSCWRITE(t0) | An Axiom |
| disj-R1-ready | ⊦ R1 ≠ ready | An Axiom |
| disj-globalPSCCRASH-retFLITPSCREAD | ⊦ globalPSCCRASH ≠ retFLITPSCREAD(t, v) | An Axiom |
| disj-W7-ready | ⊦ W7 ≠ ready | An Axiom |
| elim-mkFLITPSCgs | ⊦ (((mem = gs.mem ∧ p = gs.p) ∧ ctr = gs.ctr) ∧ writers = gs.writers) ∧ readers = gs.readers ↔ gs = mkFLITPSCgs(mem, p, ctr, writers, readers) | An Axiom |
| disj-doWritePSC-tau | ⊦ doWritePSC(t, l, v) ≠ τ | An Axiom |
| inj-doReadPSC | ⊦ doReadPSC(t, l, v) = doReadPSC(t0, l0, v0) ↔ t = t0 ∧ l = l0 ∧ v = v0 | An Axiom |
| pre-crashed | ⊦ pre(gs, ls, crashed, a) ↔ false | An Axiom |
| updsel--dotwriters-dotreaders | ⊦ (gs.writers:= writers).readers = gs.readers | An Axiom |
| disj-W7-idle | ⊦ W7 ≠ idle | An Axiom |
| disj-retFLITPSCREAD-sfencePSC | ⊦ retFLITPSCREAD(t, v) ≠ sfencePSC(t0) | An Axiom |
| disj-doReadPSC-invFLITPSCWRITE | ⊦ doReadPSC(t, l, v) ≠ invFLITPSCWRITE(t0, l0, v0) | An Axiom |
| pcstepf-W5 | ⊦ pcstepf(gs, ls, W5, a) = W6 | An Axiom |
| disj-doWritePSC-retFLITPSCREAD | ⊦ doWritePSC(t, l, v) ≠ retFLITPSCREAD(t0, v0) | An Axiom |
| gstepf-W5 | ⊦ gstepf(gs, ls, W5, a) = gs | An Axiom |
| pre-ready | ⊦ pre(gs, ls, ready, a) ↔ (∃ l0, v0. a = invFLITPSCWRITE(ls.t, l0, v0)) ∨ (∃ l0. a = invFLITPSCREAD(ls.t, l0)) ∨ a = callPSCCOMPLETE(ls.t) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) | An Axiom |
| disj-ctrIncPSC-invFLITPSCREAD | ⊦ ctrIncPSC(t, l) ≠ invFLITPSCREAD(t0, l0) | An Axiom |
| disj-invFLITPSCREAD-retFLITPSCREAD | ⊦ invFLITPSCREAD(t, l) ≠ retFLITPSCREAD(t0, v) | An Axiom |
| PSCPERSIST_FO | PSCPERSIST_FO(l; p){choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip} | An Axiom |
| inj-mkstate | ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0 | An Axiom |
| pre-R4 | ⊦ pre(gs, ls, R4, a) ↔ a = retFLITPSCREAD(ls.t, ls.v) | An Axiom |
| disj-W3-W4 | ⊦ W3 ≠ W4 | An Axiom |
| disj-R3-W3 | ⊦ R3 ≠ W3 | An Axiom |
| disj-atomicW5-ctrReadPSC | ⊦ atomicW5 ≠ ctrReadPSC(t, l, n) | An Axiom |
| disj-callPSCCOMPLETE-ctrIncPSC | ⊦ callPSCCOMPLETE(t) ≠ ctrIncPSC(t0, l) | An Axiom |
| disj-W1-W4 | ⊦ W1 ≠ W4 | An Axiom |
| disj-W1-idle | ⊦ W1 ≠ idle | An Axiom |
| lstepf-ready-FLITPSCREAD | ⊦ ls.t = t → lstepf(gs, ls, ready, invFLITPSCREAD(t, l0)) = ls.l:= l0 | An Axiom |
| gstepf-R1 | ⊦ gstepf(gs, ls, R1, a) = gs.readers:= gs.readers(ls.l := gs.readers(ls.l) ++ ls.t) | An Axiom |
| disj-doWritePSC-globalPSCCRASH | ⊦ doWritePSC(t, l, v) ≠ globalPSCCRASH | An Axiom |
| disj-R4-ready | ⊦ R4 ≠ ready | An Axiom |
| disj-ctrIncPSC-globalPSCCRASH | ⊦ ctrIncPSC(t, l) ≠ globalPSCCRASH | An Axiom |
| sel-callPSCRUN-dott | ⊦ callPSCRUN(t).t = t | An Axiom |
| sel-retFLITPSCWRITE-dott | ⊦ retFLITPSCWRITE(t).t = t | An Axiom |
| updsel--dotpcf-dotgstate | ⊦ (s.pcf:= pcf).gstate = s.gstate | An Axiom |
| disj-ctrIncPSC-retFLITPSCWRITE | ⊦ ctrIncPSC(t, l) ≠ retFLITPSCWRITE(t0) | An Axiom |
| upd-mkFLITPSCgs-dotctr | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr:= ctr0 = mkFLITPSCgs(mem, p, ctr0, writers, writers0) | An Axiom |
| updsel--dotwriters-dotctr | ⊦ (gs.writers:= writers).ctr = gs.ctr | An Axiom |
| disj-R1-W3 | ⊦ R1 ≠ W3 | An Axiom |
| updsel--dotpcf-dotlsf | ⊦ (s.pcf:= pcf).lsf = s.lsf | An Axiom |
| inj-callPSCRUN | ⊦ callPSCRUN(t) = callPSCRUN(t0) ↔ t = t0 | An Axiom |
| disj-doWritePSC-retFLITPSCWRITE | ⊦ doWritePSC(t, l, v) ≠ retFLITPSCWRITE(t0) | An Axiom |
| upd-mkFLITPSCls-dotv | ⊦ mkFLITPSCls(t, l, v).v:= v0 = mkFLITPSCls(t, l, v0) | An Axiom |
| pre-W2 | ⊦ pre(gs, ls, W2, a) ↔ a = ctrIncPSC(ls.t, ls.l) | An Axiom |
| disj-callPSCRUN-doWritePSC | ⊦ callPSCRUN(t) ≠ doWritePSC(t0, l, v) | An Axiom |
| disj-crashed-idle | ⊦ crashed ≠ idle | An Axiom |
| updsel--dotl-dotl | ⊦ (ls.l:= l).l = l | An Axiom |
| FLITPSCLInv | ⊦ FLITPSCLInv(gs, ls, pc) ↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.readers)) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.writers)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.l, gs.writers)) ∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.p)) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → noPending(ls.t, gs.p)) ∧ (pc = W4 ∨ pc = W5 → onePendingW(ls.t, ls.l, gs.p)) ∧ (pc = W5 → FOFollowsW(ls.t, gs.p(ls.l))) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.writers)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.readers)) ∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.l, gs.readers)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.p)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.writers)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.readers)) ∧ (pc = idle ∨ pc = ready → noPendingW(ls.t, gs.p)) ∧ (pc = idle → noPending(ls.t, gs.p)) | An Axiom |
| case-FLITPSCAction | ⊦ a = atomicW1 ∨ a = atomicW5 ∨ a = callPSCCOMPLETE(a.t) ∨ a = callPSCRUN(a.t) ∨ a = ctrDecPSC(a.tid, a.l) ∨ a = ctrIncPSC(a.tid, a.l) ∨ a = ctrReadPSC(a.tid, a.l, a.n) ∨ a = doReadPSC(a.tid, a.l, a.v) ∨ a = doWritePSC(a.tid, a.l, a.v) ∨ a = globalPSCCRASH ∨ a = globalPSCPERSIST_FO(a.invPSCPERSIST_FOl) ∨ a = globalPSCPERSIST_W(a.invPSCPERSIST_Wl) ∨ a = invFLITPSCREAD(a.t, a.invFLITPSCREADl) ∨ a = invFLITPSCWRITE(a.t, a.invFLITPSCWRITEl, a.invFLITPSCWRITEv) ∨ a = pwbPSC(a.tid, a.l) ∨ a = retFLITPSCREAD(a.t, a.retFLITPSCREADv) ∨ a = retFLITPSCWRITE(a.t) ∨ a = sfencePSC(a.tid) ∨ a = τ | An Axiom |
| disj-R2-W1 | ⊦ R2 ≠ W1 | An Axiom |
| disj-ctrReadPSC-doWritePSC | ⊦ ctrReadPSC(t, l, n) ≠ doWritePSC(t0, l0, v) | An Axiom |
| disj-atomicW1-ctrIncPSC | ⊦ atomicW1 ≠ ctrIncPSC(t, l) | An Axiom |
| disj-globalPSCCRASH-globalPSCPERSISTuscFO | ⊦ globalPSCCRASH ≠ globalPSCPERSIST_FO(l) | An Axiom |
| updsel--dotmem-dotwriters | ⊦ (gs.mem:= mem).writers = gs.writers | An Axiom |
| disj-globalPSCPERSISTuscW-pwbPSC | ⊦ globalPSCPERSIST_W(l) ≠ pwbPSC(t, l0) | An Axiom |
| disj-R1-W6 | ⊦ R1 ≠ W6 | An Axiom |
| pcstepf-R4 | ⊦ pcstepf(gs, ls, R4, a) = ready | An Axiom |
| disj-ctrDecPSC-ctrReadPSC | ⊦ ctrDecPSC(t, l) ≠ ctrReadPSC(t0, l0, n) | An Axiom |
| disj-R3-crashed | ⊦ R3 ≠ crashed | An Axiom |
| disj-atomicW1-globalPSCPERSISTuscFO | ⊦ atomicW1 ≠ globalPSCPERSIST_FO(l) | An Axiom |
| disj-R2-R4 | ⊦ R2 ≠ R4 | An Axiom |
| gstepf-R4 | ⊦ ls.t = t → gstepf(gs, ls, R4, retFLITPSCREAD(t, v)) = gs | An Axiom |
| disj-R4-W1 | ⊦ R4 ≠ W1 | An Axiom |
| disj-pwbPSC-retFLITPSCWRITE | ⊦ pwbPSC(t, l) ≠ retFLITPSCWRITE(t0) | An Axiom |
| inj-retFLITPSCREAD | ⊦ retFLITPSCREAD(t, v) = retFLITPSCREAD(t0, v0) ↔ t = t0 ∧ v = v0 | An Axiom |
| updsel--dotreaders-dotctr | ⊦ (gs.readers:= writers0).ctr = gs.ctr | An Axiom |
| disj-W3-ready | ⊦ W3 ≠ ready | An Axiom |
| flitpscInit | ⊦ flitpscInit(mkstate(gs, lsf, pcf)) ↔ (gs.mem = (λ l. O) ∧ pcf = (λ tid. idle) ∧ gs.p = (λ l. []) ∧ gs.ctr = (λ l. 0) ∧ gs.readers = (λ l. ∅) ∧ gs.writers = (λ l. ∅)) ∧ (∀ t. lsf(t).t = t) | An Axiom |
| disj-callPSCCOMPLETE-invFLITPSCREAD | ⊦ callPSCCOMPLETE(t) ≠ invFLITPSCREAD(t0, l) | An Axiom |
| disj-ctrIncPSC-sfencePSC | ⊦ ctrIncPSC(t, l) ≠ sfencePSC(t0) | An Axiom |
| inj-ctrDecPSC | ⊦ ctrDecPSC(t, l) = ctrDecPSC(t0, l0) ↔ t = t0 ∧ l = l0 | An Axiom |
| updsel--dotp-dotmem | ⊦ (gs.p:= p).mem = gs.mem | An Axiom |
| disj-doReadPSC-doWritePSC | ⊦ doReadPSC(t, l, v) ≠ doWritePSC(t0, l0, v0) | An Axiom |
| disj-R4-W4 | ⊦ R4 ≠ W4 | An Axiom |
| disj-globalPSCPERSISTuscW-sfencePSC | ⊦ globalPSCPERSIST_W(l) ≠ sfencePSC(t) | An Axiom |
| inj-pwbPSC | ⊦ pwbPSC(t, l) = pwbPSC(t0, l0) ↔ t = t0 ∧ l = l0 | An Axiom |
| disj-W4-W5 | ⊦ W4 ≠ W5 | An Axiom |
| upd-mkstate-dotpcf | ⊦ (mkstate(gstate, lsf, pcf).pcf:= pcf0) = mkstate(gstate, lsf, pcf0) | An Axiom |
| disj-invFLITPSCWRITE-sfencePSC | ⊦ invFLITPSCWRITE(t, l, v) ≠ sfencePSC(t0) | An Axiom |
| disj-globalPSCCRASH-globalPSCPERSISTuscW | ⊦ globalPSCCRASH ≠ globalPSCPERSIST_W(l) | An Axiom |
| disj-globalPSCCRASH-invFLITPSCWRITE | ⊦ globalPSCCRASH ≠ invFLITPSCWRITE(t, l, v) | An Axiom |
| pcstepf-idle-PSCRUN | ⊦ ls.t = t → pcstepf(gs, ls, idle, callPSCRUN(t)) = ready | An Axiom |
| disj-R1-R2 | ⊦ R1 ≠ R2 | An Axiom |
| disj-globalPSCPERSISTuscFO-sfencePSC | ⊦ globalPSCPERSIST_FO(l) ≠ sfencePSC(t) | An Axiom |
| disj-W2-W5 | ⊦ W2 ≠ W5 | An Axiom |
| lstepf-W2 | ⊦ lstepf(gs, ls, W2, a) = ls | An Axiom |
| disj-callPSCCOMPLETE-globalPSCPERSISTuscFO | ⊦ callPSCCOMPLETE(t) ≠ globalPSCPERSIST_FO(l) | An Axiom |
| sel-doWritePSC-dotl | ⊦ doWritePSC(t, l, v).l = l | An Axiom |
| disj-ctrIncPSC-retFLITPSCREAD | ⊦ ctrIncPSC(t, l) ≠ retFLITPSCREAD(t0, v) | An Axiom |
| updsel--dott-dotv | ⊦ (ls.t:= t).v = ls.v | An Axiom |
| disj-callPSCCOMPLETE-callPSCRUN | ⊦ callPSCCOMPLETE(t) ≠ callPSCRUN(t0) | An Axiom |
| disj-W3-crashed | ⊦ W3 ≠ crashed | An Axiom |
| pre-R1 | ⊦ pre(gs, ls, R1, a) ↔ a = doReadPSC(ls.t, ls.l, ((gs.mem ⊕ gs.p))(ls.l)) | An Axiom |
| disj-ctrReadPSC-invFLITPSCWRITE | ⊦ ctrReadPSC(t, l, n) ≠ invFLITPSCWRITE(t0, l0, v) | An Axiom |
| disj-R2-W4 | ⊦ R2 ≠ W4 | An Axiom |
| disj-W6-ready | ⊦ W6 ≠ ready | An Axiom |
| upd-mkFLITPSCgs-dotwriters | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers:= writers1 = mkFLITPSCgs(mem, p, ctr, writers1, writers0) | An Axiom |
| disj-R3-ready | ⊦ R3 ≠ ready | An Axiom |
| gstepf-W7 | ⊦ ls.t = t → gstepf(gs, ls, W7, retFLITPSCWRITE(t)) = gs | An Axiom |
| disj-ctrDecPSC-invFLITPSCWRITE | ⊦ ctrDecPSC(t, l) ≠ invFLITPSCWRITE(t0, l0, v) | An Axiom |
| sel-ctrReadPSC-dotn | ⊦ ctrReadPSC(t, l, n).n = n | An Axiom |
| disj-callPSCRUN-doReadPSC | ⊦ callPSCRUN(t) ≠ doReadPSC(t0, l, v) | An Axiom |
| updsel--dotmem-dotreaders | ⊦ (gs.mem:= mem).readers = gs.readers | An Axiom |
| disj-atomicW5-sfencePSC | ⊦ atomicW5 ≠ sfencePSC(t) | An Axiom |
| disj-callPSCCOMPLETE-retFLITPSCREAD | ⊦ callPSCCOMPLETE(t) ≠ retFLITPSCREAD(t0, v) | An Axiom |
| lstepf-W5 | ⊦ lstepf(gs, ls, W5, a) = ls | An Axiom |
| disj-R4-W7 | ⊦ R4 ≠ W7 | An Axiom |
| pcstepf-R1 | ⊦ pcstepf(gs, ls, R1, a) = R2 | An Axiom |
| disj-callPSCCOMPLETE-tau | ⊦ callPSCCOMPLETE(t) ≠ τ | An Axiom |
| disj-atomicW1-atomicW5 | ⊦ atomicW1 ≠ atomicW5 | An Axiom |
| pcstepf-W7 | ⊦ pcstepf(gs, ls, W7, a) = ready | An Axiom |
| disj-doReadPSC-invFLITPSCREAD | ⊦ doReadPSC(t, l, v) ≠ invFLITPSCREAD(t0, l0) | An Axiom |
| disj-doWritePSC-globalPSCPERSISTuscW | ⊦ doWritePSC(t, l, v) ≠ globalPSCPERSIST_W(l0) | An Axiom |
| pcstepf-ready-FLITPSCWRITE | ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = W1 | An Axiom |
| sel-pwbPSC-dotl | ⊦ pwbPSC(t, l).l = l | An Axiom |
| sel-mkstate-dotpcf | ⊦ mkstate(gstate, lsf, pcf).pcf = pcf | An Axiom |
| updsel--dotctr-dotp | ⊦ (gs.ctr:= ctr).p = gs.p | An Axiom |
| updsel--dotlsf-dotgstate | ⊦ (s.lsf:= lsf).gstate = s.gstate | An Axiom |
| disj-R2-W7 | ⊦ R2 ≠ W7 | An Axiom |
| FLITPSCRely | ⊦ FLITPSCRely(gs, t, gs0) ↔ relyws(t, gs.readers, gs0.readers) ∧ relyws(t, gs.writers, gs0.writers) ∧ rely(t, gs.p, gs0.p) | An Axiom |
| updsel--dotctr-dotreaders | ⊦ (gs.ctr:= ctr).readers = gs.readers | An Axiom |
| elim-mkFLITPSCls | ⊦ (t = ls.t ∧ l = ls.l) ∧ v = ls.v ↔ ls = mkFLITPSCls(t, l, v) | An Axiom |
| disj-W6-crashed | ⊦ W6 ≠ crashed | An Axiom |
| disj-callPSCRUN-ctrDecPSC | ⊦ callPSCRUN(t) ≠ ctrDecPSC(t0, l) | An Axiom |
| pre-W1 | ⊦ pre(gs, ls, W1, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t) | An Axiom |
| disj-W2-idle | ⊦ W2 ≠ idle | An Axiom |
| disj-ctrDecPSC-ctrIncPSC | ⊦ ctrDecPSC(t, l) ≠ ctrIncPSC(t0, l0) | An Axiom |
| sel-ctrIncPSC-dotl | ⊦ ctrIncPSC(t, l).l = l | An Axiom |
| lstepf-R1 | ⊦ lstepf(gs, ls, R1, a) = ls.v:= ((gs.mem ⊕ gs.p))(ls.l) | An Axiom |
| upd-mkstate-dotgstate | ⊦ (mkstate(gstate, lsf, pcf).gstate:= gstate0) = mkstate(gstate0, lsf, pcf) | An Axiom |
| disj-W1-W6 | ⊦ W1 ≠ W6 | An Axiom |
| inj-globalPSCPERSISTuscFO | ⊦ globalPSCPERSIST_FO(l) = globalPSCPERSIST_FO(l0) ↔ l = l0 | An Axiom |
| disj-globalPSCCRASH-tau | ⊦ globalPSCCRASH ≠ τ | An Axiom |
| disj-R2-R3 | ⊦ R2 ≠ R3 | An Axiom |
| case-FLITPSCPC | ⊦ pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 ∨ pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 ∨ pc = crashed ∨ pc = idle ∨ pc = ready | An Axiom |
| disj-R3-W5 | ⊦ R3 ≠ W5 | An Axiom |
| sel-mkFLITPSCgs-dotwriters | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers = writers | An Axiom |
| upd-mkFLITPSCgs-dotreaders | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers:= writers2 = mkFLITPSCgs(mem, p, ctr, writers, writers2) | An Axiom |
| disj-invFLITPSCREAD-invFLITPSCWRITE | ⊦ invFLITPSCREAD(t, l) ≠ invFLITPSCWRITE(t0, l0, v) | An Axiom |
| disj-W5-W6 | ⊦ W5 ≠ W6 | An Axiom |
| pre-W4 | ⊦ pre(gs, ls, W4, a) ↔ a = pwbPSC(ls.t, ls.l) | An Axiom |
| pcstepf-W1 | ⊦ pcstepf(gs, ls, W1, a) = W2 | An Axiom |
| disj-doReadPSC-globalPSCPERSISTuscW | ⊦ doReadPSC(t, l, v) ≠ globalPSCPERSIST_W(l0) | An Axiom |
| updsel--dotwriters-dotp | ⊦ (gs.writers:= writers).p = gs.p | An Axiom |
| disj-callPSCRUN-tau | ⊦ callPSCRUN(t) ≠ τ | An Axiom |
| disj-callPSCCOMPLETE-sfencePSC | ⊦ callPSCCOMPLETE(t) ≠ sfencePSC(t0) | An Axiom |
| gstepf-W1 | ⊦ gstepf(gs, ls, W1, a) = gs | An Axiom |
| updsel--dotctr-dotwriters | ⊦ (gs.ctr:= ctr).writers = gs.writers | An Axiom |
| disj-callPSCCOMPLETE-globalPSCCRASH | ⊦ callPSCCOMPLETE(t) ≠ globalPSCCRASH | An Axiom |
| updsel--dotv-dott | ⊦ (ls.v:= v).t = ls.t | An Axiom |
| disj-W3-W6 | ⊦ W3 ≠ W6 | An Axiom |
| disj-R1-W5 | ⊦ R1 ≠ W5 | An Axiom |
| disj-atomicW1-callPSCRUN | ⊦ atomicW1 ≠ callPSCRUN(t) | An Axiom |
| gstepf-W4 | ⊦ gstepf(gs, ls, W4, a) = gs.p:= gs.p(ls.l := gs.p(ls.l) + FO(ls.t)) | An Axiom |
| disj-ctrReadPSC-retFLITPSCWRITE | ⊦ ctrReadPSC(t, l, n) ≠ retFLITPSCWRITE(t0) | An Axiom |
| disj-atomicW1-retFLITPSCWRITE | ⊦ atomicW1 ≠ retFLITPSCWRITE(t) | An Axiom |
| sel-mkFLITPSCls-dotv | ⊦ mkFLITPSCls(t, l, v).v = v | An Axiom |
| disj-ctrIncPSC-globalPSCPERSISTuscFO | ⊦ ctrIncPSC(t, l) ≠ globalPSCPERSIST_FO(l0) | An Axiom |
| disj-globalPSCCRASH-retFLITPSCWRITE | ⊦ globalPSCCRASH ≠ retFLITPSCWRITE(t) | An Axiom |
| sel-invFLITPSCWRITE-dott | ⊦ invFLITPSCWRITE(t, l, v).t = t | An Axiom |
| inj-ctrIncPSC | ⊦ ctrIncPSC(t, l) = ctrIncPSC(t0, l0) ↔ t = t0 ∧ l = l0 | An Axiom |
| inj-doWritePSC | ⊦ doWritePSC(t, l, v) = doWritePSC(t0, l0, v0) ↔ t = t0 ∧ l = l0 ∧ v = v0 | An Axiom |
| disj-doWritePSC-sfencePSC | ⊦ doWritePSC(t, l, v) ≠ sfencePSC(t0) | An Axiom |
| disj-atomicW1-invFLITPSCWRITE | ⊦ atomicW1 ≠ invFLITPSCWRITE(t, l, v) | An Axiom |
| disj-sfencePSC-tau | ⊦ sfencePSC(t) ≠ τ | An Axiom |
| case-FLITPSCState | ⊦ mkstate(s.gstate, s.lsf, s.pcf) = s | An Axiom |
| updsel--dotmem-dotp | ⊦ (gs.mem:= mem).p = gs.p | An Axiom |
| lstepf-R4 | ⊦ ls.t = t → lstepf(gs, ls, R4, retFLITPSCREAD(t, ls.v)) = ls | An Axiom |
| pre-W7 | ⊦ pre(gs, ls, W7, a) ↔ a = retFLITPSCWRITE(ls.t) | An Axiom |
| disj-doReadPSC-retFLITPSCREAD | ⊦ doReadPSC(t, l, v) ≠ retFLITPSCREAD(t0, v0) | An Axiom |
| disj-globalPSCPERSISTuscFO-pwbPSC | ⊦ globalPSCPERSIST_FO(l) ≠ pwbPSC(t, l0) | An Axiom |
| pcstepf-W4 | ⊦ pcstepf(gs, ls, W4, a) = W5 | An Axiom |
| pcstepf-ready-FLITPSCREAD | ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITPSCREAD(t, l0)) = R1 | An Axiom |
| disj-atomicW5-invFLITPSCWRITE | ⊦ atomicW5 ≠ invFLITPSCWRITE(t, l, v) | An Axiom |
| sel-mkFLITPSCgs-dotreaders | ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers = writers0 | An Axiom |
| disj-W4-W7 | ⊦ W4 ≠ W7 | An Axiom |
| upd-mkFLITPSCls-dotl | ⊦ mkFLITPSCls(t, l, v).l:= l0 = mkFLITPSCls(t, l0, v) | An Axiom |
| sel-retFLITPSCREAD-dotretFLITPSCREADv | ⊦ retFLITPSCREAD(t, v).retFLITPSCREADv = v | An Axiom |
| disj-retFLITPSCWRITE-tau | ⊦ retFLITPSCWRITE(t) ≠ τ | An Axiom |
| disj-W3-idle | ⊦ W3 ≠ idle | An Axiom |
| disj-callPSCRUN-ctrReadPSC | ⊦ callPSCRUN(t) ≠ ctrReadPSC(t0, l, n) | An Axiom |
| disj-R3-W2 | ⊦ R3 ≠ W2 | An Axiom |
| disj-atomicW1-doWritePSC | ⊦ atomicW1 ≠ doWritePSC(t, l, v) | An Axiom |
| disj-callPSCRUN-invFLITPSCREAD | ⊦ callPSCRUN(t) ≠ invFLITPSCREAD(t0, l) | An Axiom |
| disj-atomicW1-callPSCCOMPLETE | ⊦ atomicW1 ≠ callPSCCOMPLETE(t) | An Axiom |
| disj-atomicW5-retFLITPSCWRITE | ⊦ atomicW5 ≠ retFLITPSCWRITE(t) | An Axiom |
| disj-ctrDecPSC-retFLITPSCWRITE | ⊦ ctrDecPSC(t, l) ≠ retFLITPSCWRITE(t0) | An Axiom |
| gen-FLITPSCLState | FLITPSCLState freely generated by mkFLITPSCls; | An Axiom |
| disj-R1-W2 | ⊦ R1 ≠ W2 | An Axiom |
| not-pre-global-persist | ⊦ ¬ pre(gs, ls, pc, globalPSCPERSIST_W(l)) | A User Theorem |
| pre-R3 | ⊦ pre(gs, ls, R3, a) ↔ a = pwbPSC(ls.t, ls.l) | An Axiom |
| lstepf-W4 | ⊦ lstepf(gs, ls, W4, a) = ls | An Axiom |
| updsel--dotp-dotctr | ⊦ (gs.p:= p).ctr = gs.ctr | An Axiom |
| disj-atomicW5-doReadPSC | ⊦ atomicW5 ≠ doReadPSC(t, l, v) | An Axiom |
| updsel--dotreaders-dotreaders | ⊦ (gs.readers:= writers0).readers = writers0 | An Axiom |
| disj-W1-W3 | ⊦ W1 ≠ W3 | An Axiom |
| disj-invFLITPSCREAD-sfencePSC | ⊦ invFLITPSCREAD(t, l) ≠ sfencePSC(t0) | An Axiom |
| disj-W6-W7 | ⊦ W6 ≠ W7 | An Axiom |
| updsel--dotgstate-dotpcf | ⊦ (s.gstate:= gstate).pcf = s.pcf | An Axiom |
| disj-R4-W6 | ⊦ R4 ≠ W6 | An Axiom |
| updsel--dotl-dott | ⊦ (ls.l:= l).t = ls.t | An Axiom |
| disj-doReadPSC-globalPSCCRASH | ⊦ doReadPSC(t, l, v) ≠ globalPSCCRASH | An Axiom |
| disj-R2-crashed | ⊦ R2 ≠ crashed | An Axiom |
| disj-R3-R4 | ⊦ R3 ≠ R4 | An Axiom |
| lstepf-ready-PSCCOMPLETE | ⊦ ls.t = t → lstepf(gs, ls, ready, callPSCCOMPLETE(t)) = ls | An Axiom |
| disj-retFLITPSCREAD-tau | ⊦ retFLITPSCREAD(t, v) ≠ τ | An Axiom |
| disj-W2-W7 | ⊦ W2 ≠ W7 | An Axiom |
| disj-ctrIncPSC-doWritePSC | ⊦ ctrIncPSC(t, l) ≠ doWritePSC(t0, l0, v) | An Axiom |