[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Theorem step-absstep-W4-W5-tau-other

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), 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), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W4, pcf0(t) = W5, apcf(t) = apc, notMember(t, gs.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ ¬ SF ∈ gs.bq(t) ∧ gs.rfo(t) = [] ∧ (gs.bq(t) = [] ∨ gs.bq(t) = W(ls.loc, ls.val) ') ∧ (gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val)), notMember(t, gs0.freaders) ∧ oneMember(t, ls0.loc, gs0.fwriters) ∧ FOFollowsW(t, gs0.bq(t), gs0.pq(ls0.loc), ls0.loc) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ (gs0.bq(t) = [] ∨ gs0.bq(t) = FO(ls0.loc) ' ∨ gs0.bq(t) = W(ls0.loc, ls0.val) ' + FO(ls0.loc) ') ∧ (gs0.bq(t) ≠ [] ∧ gs0.bq(t).head.W? → gs0.bq(t).head = W(ls0.loc, ls0.val)), FLITPSCLInv(ags, als, apc), t ≠ t0, lsf(t0).t = t0, FLITLInv(gs, lsf(t0), pcf(t0)), FLITLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), pre(gs, ls, W4, τ) ∧ gs0 = gstepf(gs, ls, W4, τ) ∧ ls0 = lstepf(gs, ls, W4, τ) ∧ W5 = pcstepf(gs, ls, W4, τ), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4) ∧ ls.loc = als.l ∧ ls.val = als.v, lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v)

View the proof

Infos about the proof