Proof step 1 from proof step-absstep-PERSIST_W-globalPERSIST_W (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)), flitStep(mkstate(gs, lsf, pcf), globalPERSIST_W(loc), mkstate(gs0, lsf0, pcf0)) ⊦ ∃ ags0, alsf0, apcf0. flitpscStep(mkstate(ags, alsf, apcf), globalPSCPERSIST_W(loc), mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0))

Rule argument

Additional information

Proof step 2 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), globalPERSIST_W(loc), mkstate(gs0, lsf0, pcf0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val) = gs0.pmem ∧ gs.fctr = gs0.fctr ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs0.pq, gs0.rfo) ∧ gs.fwriters = gs0.fwriters ∧ labs (gs0, lsf0(t), pcf0(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: abs-def: ⊦ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ↔ gabs(gs, lsf, pcf, ags, alsf, apcf) ∧ (∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t))); gabs-def: ⊦ gabs(gs, lsf, pcf, ags, alsf, apcf) ↔ ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters; ⊦ (gs.mem:= mem).writers = gs.writers; (s) ⊦ (gs.p:= p).writers = gs.writers; (s) ⊦ (gs.p:= p).p = p; (s) ⊦ (gs.mem:= mem).ctr = gs.ctr; (s) ⊦ (gs.p:= p).ctr = gs.ctr; (s) ⊦ (gs.mem:= mem).mem = mem; (s) ⊦ (gs.p:= p).mem = gs.mem; (s) ⊦ globalPSCCRASH ≠ globalPSCPERSIST_W(l); (s) ⊦ globalPSCPERSIST_FO(l) ≠ globalPSCPERSIST_W(l0); (s) ⊦ globalPSCPERSIST_W(l) = globalPSCPERSIST_W(l0) ↔ l = l0; (s) ⊦ ¬ pre(gs, ls, pc, globalPSCPERSIST_W(l)); (s) ⊦ 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); (s) ⊦ 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)); (s)

Proof step 3 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ flitStep(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)) ∨ (∃ tid. a = doWrite(tid, gs.bq(tid).head.l, gs.bq(tid).head.v) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head.W?) ∧ gs0 = (gs.pq:= gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid))).bq:= gs.bq(tid := gs.bq(tid).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ tid, l. a = (oneMember(tid, l, gs.fwriters) ⊃ doWriteFO(tid, l);propFO(tid, l)) ∧ (∃ n. n < # gs.bq(tid) ∧ isPropFO(n, l, gs.bq(tid))) ∧ ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)) ∨ (∃ tid. a = propSF(tid) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head = SF ∧ (∀ l. ¬ FO(tid) ∈ gs.pq(l))) ∧ gs0 = gs.bq:= gs.bq(tid := gs.bq(tid).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ loc. a = globalPERSIST_W(loc) ∧ (gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.W?) ∧ gs0 = (gs.pmem:= gs.pmem(loc := gs.pq(loc).head.val)).pq:= gs.pq(loc := gs.pq(loc).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ loc. a = globalPERSIST_FO(loc) ∧ (gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.FO?) ∧ gs0 = gs.pq:= gs.pq(loc := gs.pq(loc).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalCRASH ∧ ⟨pq := gs.pq, fctr := gs.fctr, bq := gs.bq, fwriters := gs.fwriters, freaders := gs.freaders, rfo := gs.rfo; CRASH(; pq, fctr, bq, fwriters, freaders, rfo, pcf); gs := (((((gs.pq:= pq).fctr:= fctr).bq:= bq).fwriters:= fwriters).freaders:= freaders).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)

• Proof step 5:

  (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalPERSIST_W(loc), gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ (∃ tid. globalPERSIST_W(loc) = doWrite(tid, gs.bq(tid).head.l, gs.bq(tid).head.v) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head.W?) ∧ gs0 = (gs.pq:= gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid))).bq:= gs.bq(tid := gs.bq(tid).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ tid, l. globalPERSIST_W(loc) = (oneMember(tid, l, gs.fwriters) ⊃ doWriteFO(tid, l);propFO(tid, l)) ∧ (∃ n. n < # gs.bq(tid) ∧ isPropFO(n, l, gs.bq(tid))) ∧ ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)) ∨ (∃ tid. globalPERSIST_W(loc) = propSF(tid) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head = SF ∧ (∀ l. ¬ FO(tid) ∈ gs.pq(l))) ∧ gs0 = gs.bq:= gs.bq(tid := gs.bq(tid).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ loc0. globalPERSIST_W(loc) = globalPERSIST_W(loc0) ∧ (gs.pq(loc0) ≠ [] ∧ gs.pq(loc0).head.W?) ∧ gs0 = (gs.pmem:= gs.pmem(loc0 := gs.pq(loc0).head.val)).pq:= gs.pq(loc0 := gs.pq(loc0).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ loc0. globalPERSIST_W(loc) = globalPERSIST_FO(loc0) ∧ (gs.pq(loc0) ≠ [] ∧ gs.pq(loc0).head.FO?) ∧ gs0 = gs.pq:= gs.pq(loc0 := gs.pq(loc0).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ globalPERSIST_W(loc) = globalCRASH ∧ ⟨pq := gs.pq, fctr := gs.fctr, bq := gs.bq, fwriters := gs.fwriters, freaders := gs.freaders, rfo := gs.rfo; CRASH(; pq, fctr, bq, fwriters, freaders, rfo, pcf); gs := (((((gs.pq:= pq).fctr:= fctr).bq:= bq).fwriters:= fwriters).freaders:= freaders).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val) = gs0.pmem ∧ gs.fctr = gs0.fctr ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs0.pq, gs0.rfo) ∧ gs.fwriters = gs0.fwriters ∧ labs (gs0, lsf0(t), pcf0(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Used terms: pcf0, globalPERSIST_W(loc), lsf, gs0, pcf, lsf0, gs

Proof step 4 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)) ∧ n < # gs.bq(t0) ∧ isPropFO(n, l, gs.bq(t0)) ∧ ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(t0, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ loc = loc0 ∧ gs.pq(loc0) ≠ [] ∧ gs.pq(loc0).head.W? ∧ gs0 = (gs.pmem:= gs.pmem(loc0 := gs.pq(loc0).head.val)).pq:= gs.pq(loc0 := gs.pq(loc0).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf, ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val) = gs0.pmem ∧ gs.fctr = gs0.fctr ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs0.pq, gs0.rfo) ∧ gs.fwriters = gs0.fwriters ∧ labs (gs0, lsf0(t), pcf0(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: ⊦ globalCRASH ≠ globalPERSIST_W(loc); (s) ⊦ globalPERSIST_FO(loc) ≠ globalPERSIST_W(loc0); (s) ⊦ globalPERSIST_W(loc) = globalPERSIST_W(loc0) ↔ loc = loc0; (s) ⊦ globalPERSIST_W(loc) ≠ propSF(t); (s) ⊦ doWrite(t, loc, v) ≠ globalPERSIST_W(loc0); (s) ⊦ ¬ pre(gs, ls, pc, globalPERSIST_W(l)); (s) ⊦ 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); (s)

Proof step 6 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 7:

  ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(t0, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), n < # gs.bq(t0), FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val) = gs0.pmem ∧ gs.fctr = gs0.fctr ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs0.pq, gs0.rfo) ∧ gs.fwriters = gs0.fwriters ∧ labs (gs0, lsf0(t), pcf0(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

• Proof step 21:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, gs0 = (gs.pmem:= gs.pmem(loc0 := gs.pq(loc0).head.val)).pq:= gs.pq(loc0 := gs.pq(loc0).tail), loc = loc0, lsf0 = lsf, pcf0 = pcf, gs.pq(loc0) ≠ [], gs.pq(loc0).head.W?, FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val) = gs0.pmem ∧ gs.fctr = gs0.fctr ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs0.pq, gs0.rfo) ∧ gs.fwriters = gs0.fwriters ∧ labs (gs0, lsf0(t), pcf0(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 7 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 8:

  ⟨PROP_FO(t0, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), pq = gs.pq, rfo = gs.rfo, n < # gs.bq(t0), FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val) = gs0.pmem ∧ gs.fctr = gs0.fctr ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs0.pq, gs0.rfo) ∧ gs.fwriters = gs0.fwriters ∧ labs (gs0, lsf0(t), pcf0(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 8 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic split applied rule split left

And obtained the following new goals

• Proof step 9:

  ⟨gs := ((gs.pq:= pq0).bq:= bq0).rfo:= rfo0⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ⟨PROP_FO(t0, l, fwriters; pq, bq, rfo)⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), pq = gs.pq, rfo = gs.rfo, n < # gs.bq(t0), FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val) = gs0.pmem ∧ gs.fctr = gs0.fctr ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs0.pq, gs0.rfo) ∧ gs.fwriters = gs0.fwriters ∧ labs (gs0, lsf0(t), pcf0(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 9 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 10:

  ⟨PROP_FO(t0, l, fwriters; pq, bq, rfo)⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), gs0 = ((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf0 = lsf, pcf0 = pcf, pq = gs.pq, rfo = gs.rfo, n < # gs.bq(t0), FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val) = gs0.pmem ∧ gs.fctr = gs0.fctr ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs0.pq, gs0.rfo) ∧ gs.fwriters = gs0.fwriters ∧ labs (gs0, lsf0(t), pcf0(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 10 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ⟨PROP_FO(t0, l, gs.fwriters; pq, bq, rfo)⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), pq = gs.pq, rfo = gs.rfo, gs.bq(t0) ≠ [], n < # gs.bq(t0), FLITInv(gs, lsf, pcf), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), pq0, rfo0) ∧ labs (((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s) ⊦ (gs.bq:= bq).fwriters = gs.fwriters; (s) ⊦ (gs.rfo:= bq0).fwriters = gs.fwriters; (s) ⊦ (gs.rfo:= bq0).rfo = bq0; (s) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ (gs.bq:= bq).pq = gs.pq; (s) ⊦ (gs.rfo:= bq0).pq = gs.pq; (s) ⊦ (gs.pq:= pq).fctr = gs.fctr; (s) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s) ⊦ (gs.rfo:= bq0).fctr = gs.fctr; (s) ⊦ (gs.pq:= pq).pmem = gs.pmem; (s) ⊦ (gs.bq:= bq).pmem = gs.pmem; (s) ⊦ (gs.rfo:= bq0).pmem = gs.pmem; (s)

Proof step 11 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic unfold applied rule call left

And obtained the following new goals

• Proof step 12:

  ⟨choose n with n < # bq(tid) ∧ isPropFO(n, l, bq(tid)) in pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n) ifnone skip⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), pq = gs.pq, rfo = gs.rfo, tid = t0, gs.bq(t0) ≠ [], n < # gs.bq(t0), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), pq0, rfo0) ∧ labs (((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: decl: PROP_FO(tid, l, fwriters; pq, bq, rfo) {choose n with n < # bq(tid) ∧ isPropFO(n, l, bq(tid)) in pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n) ifnone skip };

Proof step 12 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic symbolic execution applied rule choose left

And obtained the following new goals

• Proof step 13:

  ⟨pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n)⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), pq = gs.pq, rfo = gs.rfo, tid = t0, gs.bq(t0) ≠ [], n0 < # gs.bq(t0), n < # bq(tid), FLITInv(gs, lsf, pcf), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n0, l, gs.bq(t0)), isPropFO(n, l, bq(tid)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), pq0, rfo0) ∧ labs (((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

• Proof step 18:

  ⟨skip⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), pq = gs.pq, rfo = gs.rfo, tid = t0, gs.bq(t0) ≠ [], n < # gs.bq(t0), FLITInv(gs, lsf, pcf), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)), ∀ n. ¬(n < # bq(tid) ∧ isPropFO(n, l, bq(tid))) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), pq0, rfo0) ∧ labs (((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 13 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 14:

  pq(l := pq(l) + FO(tid)) = pq0, bq(tid := bq(tid) -p n) = bq0, rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n)) = rfo0, ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), pq = gs.pq, rfo = gs.rfo, tid = t0, gs.bq(t0) ≠ [], n < # bq(tid), n0 < # gs.bq(t0), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, bq(tid)), isPropFO(n0, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), pq0, rfo0) ∧ labs (((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 14 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), gs.bq(t0) ≠ [], n0 < # gs.bq(t0), n < # gs.bq(t0), FLITInv(gs, lsf, pcf), FLITInv (((gs.pq:= gs.pq(l := gs.pq(l) + FO(t0) ')).bq:= gs.bq(t0 := gs.bq(t0) -p n)).rfo:= gs.rfo(t0 := (t0 ∈ gs.fwriters(l) ⊃ gs.rfo(t0);gs.rfo(t0) -p n)), lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n0, l, gs.bq(t0)), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder (ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs.pq(l := gs.pq(l) + FO(t0) '), gs.rfo(t0 := (t0 ∈ gs.fwriters(l) ⊃ gs.rfo(t0);gs.rfo(t0) -p n))) ∧ labs ( ((gs.pq:= gs.pq(l := gs.pq(l) + FO(t0) ')).bq:= gs.bq(t0 := gs.bq(t0) -p n)) .rfo:= gs.rfo(t0 := (t0 ∈ gs.fwriters(l) ⊃ gs.rfo(t0);gs.rfo(t0) -p n)), lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: ⊦ x + a = x + a '; (s)

Proof step 15 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), gs.bq(t0) ≠ [], n < # gs.bq(t0), n0 < # gs.bq(t0), FLITInv (((gs.pq:= gs.pq(l := gs.pq(l) + FO(t0) ')).bq:= gs.bq(t0 := gs.bq(t0) -p n)).rfo:= gs.rfo(t0 := (t0 ∈ gs.fwriters(l) ⊃ gs.rfo(t0);gs.rfo(t0) -p n)), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), isPropFO(n0, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), t0 ∈ gs.fwriters(l), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder (ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs.pq(l := gs.pq(l) + FO(t0) '), gs.rfo(t0 := (t0 ∈ gs.fwriters(l) ⊃ gs.rfo(t0);gs.rfo(t0) -p n))) ∧ labs ( ((gs.pq:= gs.pq(l := gs.pq(l) + FO(t0) ')).bq:= gs.bq(t0 := gs.bq(t0) -p n)) .rfo:= gs.rfo(t0 := (t0 ∈ gs.fwriters(l) ⊃ gs.rfo(t0);gs.rfo(t0) -p n)), lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: ⊦ oneMember(t, l, tsf) → (t ∈ tsf(l0) ↔ l = l0); (s) ⊦ globalPERSIST_W(loc) ≠ propFO(t, loc0); (s) Used formulas: t0 ∈ gs.fwriters(l)

Proof step 16 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), # gs.fwriters(l) ≠ 0, gs.bq(t0) ≠ [], gs.fwriters(l) ≠ ∅, n < # gs.bq(t0), n0 < # gs.bq(t0), FLITInv(((gs.pq:= gs.pq(l := gs.pq(l) + FO(t0) ')).bq:= gs.bq(t0 := gs.bq(t0) -p n)).rfo:= gs.rfo(t0 := gs.rfo(t0)), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), isPropFO(n0, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), t0 ∈ gs.fwriters(l), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs.pq(l := gs.pq(l) + FO(t0) '), gs.rfo(t0 := gs.rfo(t0))) ∧ labs (((gs.pq:= gs.pq(l := gs.pq(l) + FO(t0) ')).bq:= gs.bq(t0 := gs.bq(t0) -p n)).rfo:= gs.rfo(t0 := gs.rfo(t0)), lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 17 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ globalPERSIST_W(loc) ≠ propFO(t, loc0); (s) ⊦ doWriteFO(t, loc) ≠ globalPERSIST_W(loc0); (s) Used formulas: oneMember(t0, l, gs.fwriters)

Proof step 18 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic symbolic execution applied rule skip left

And obtained the following new goals

• Proof step 19:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, bq = bq0, fwriters = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), pq = gs.pq, pq = pq0, rfo = gs.rfo, rfo = rfo0, tid = t0, gs.bq(t0) ≠ [], n < # gs.bq(t0), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ n. ¬(n < # bq(tid) ∧ isPropFO(n, l, bq(tid))), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), pq0, rfo0) ∧ labs (((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 19 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_W(loc) = (oneMember(t0, l, gs.fwriters) ⊃ doWriteFO(t0, l);propFO(t0, l)), gs.bq(t0) ≠ [], n < # gs.bq(t0), FLITInv(gs, lsf, pcf), FLITInv(((gs.pq:= gs.pq).bq:= gs.bq).rfo:= gs.rfo, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)), ∀ n0. ¬ n0 < # gs.bq(t0) ∨ ¬ isPropFO(n0, l, gs.bq(t0)) ⊦ firstPersistW(ags.p(loc)) < # ags.p(loc) ∧ gs.pmem(loc) = ags.p(loc)[firstPersistW(ags.p(loc))].val ∧ reorder(ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), gs.pq, gs.rfo) ∧ labs (((gs.pq:= gs.pq).bq:= gs.bq).rfo:= gs.rfo, lsf(t), pcf(t), (ags.mem:= gs.pmem(loc := ags.p(loc)[firstPersistW(ags.p(loc))].val)).p:= ags.p(loc := ags.p(loc) -p firstPersistW(ags.p(loc))), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 20 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 21 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, gs.pq(loc0) ≠ [], gs.pq(loc0).head.W?, FLITInv(gs, lsf, pcf), FLITInv((gs.pmem:= gs.pmem(loc0 := gs.pq(loc0).head.val)).pq:= gs.pq(loc0 := gs.pq(loc0).tail), lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc0)) < # ags.p(loc0) ∧ gs.pmem(loc0 := ags.p(loc0)[firstPersistW(ags.p(loc0))].val) = gs.pmem(loc0 := gs.pq(loc0).head.val) ∧ reorder(ags.p(loc0 := ags.p(loc0) -p firstPersistW(ags.p(loc0))), gs.pq(loc0 := gs.pq(loc0).tail), gs.rfo) ∧ labs ((gs.pmem:= gs.pmem(loc0 := gs.pq(loc0).head.val)).pq:= gs.pq(loc0 := gs.pq(loc0).tail), lsf(t), pcf(t), (ags.mem:= gs.pmem(loc0 := ags.p(loc0)[firstPersistW(ags.p(loc0))].val)).p:= ags.p(loc0 := ags.p(loc0) -p firstPersistW(ags.p(loc0))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.pmem:= pmem).fwriters = gs.fwriters; (s) ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s) ⊦ (gs.pmem:= pmem).rfo = gs.rfo; (s) ⊦ (gs.pq:= pq).rfo = gs.rfo; (s) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ (gs.pmem:= pmem).fctr = gs.fctr; (s) ⊦ (gs.pq:= pq).fctr = gs.fctr; (s) ⊦ (gs.pmem:= pmem).pmem = pmem; (s) ⊦ (gs.pq:= pq).pmem = gs.pmem; (s)

Proof step 22 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 23:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = fow + fowl, ags.writers = gs.fwriters, gs.pq(loc0) ≠ [], fow.W?, FLITInv((gs.pmem:= gs.pmem(loc0 := fow.val)).pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc0)) < # ags.p(loc0) ∧ gs.pmem(loc0 := ags.p(loc0)[firstPersistW(ags.p(loc0))].val) = gs.pmem(loc0 := fow.val) ∧ reorder(ags.p(loc0 := ags.p(loc0) -p firstPersistW(ags.p(loc0))), gs.pq(loc0 := fowl), gs.rfo) ∧ labs ((gs.pmem:= gs.pmem(loc0 := fow.val)).pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), (ags.mem:= gs.pmem(loc0 := ags.p(loc0)[firstPersistW(ags.p(loc0))].val)).p:= ags.p(loc0 := ags.p(loc0) -p firstPersistW(ags.p(loc0))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: gs.pq(loc0), fow, fowl

Proof step 23 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = fow ' + fowl, ags.writers = gs.fwriters, fow.W?, FLITInv(gs, lsf, pcf), FLITInv((gs.pmem:= gs.pmem(loc0 := fow.val)).pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc0)) < # ags.p(loc0) ∧ gs.pmem(loc0 := ags.p(loc0)[firstPersistW(ags.p(loc0))].val) = gs.pmem(loc0 := fow.val) ∧ reorder(ags.p(loc0 := ags.p(loc0) -p firstPersistW(ags.p(loc0))), gs.pq(loc0 := fowl), gs.rfo) ∧ labs ((gs.pmem:= gs.pmem(loc0 := fow.val)).pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), (ags.mem:= gs.pmem(loc0 := ags.p(loc0)[firstPersistW(ags.p(loc0))].val)).p:= ags.p(loc0 := ags.p(loc0) -p firstPersistW(ags.p(loc0))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

Proof step 24 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 25:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = fow ' + fowl, ags.writers = gs.fwriters, fow = W(val, t0), fow.W?, FLITInv((gs.pmem:= gs.pmem(loc0 := val)).pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ firstPersistW(ags.p(loc0)) < # ags.p(loc0) ∧ gs.pmem(loc0 := ags.p(loc0)[firstPersistW(ags.p(loc0))].val) = gs.pmem(loc0 := val) ∧ reorder(ags.p(loc0 := ags.p(loc0) -p firstPersistW(ags.p(loc0))), gs.pq(loc0 := fowl), gs.rfo) ∧ labs ((gs.pmem:= gs.pmem(loc0 := val)).pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), (ags.mem:= gs.pmem(loc0 := ags.p(loc0)[firstPersistW(ags.p(loc0))].val)).p:= ags.p(loc0 := ags.p(loc0) -p firstPersistW(ags.p(loc0))), alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: ⊦ fow.W? → (val = fow.val ∧ tid = fow.tid ↔ fow = W(val, tid)); (elim) Used terms: fow, val, t0

Proof step 25 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = W(val, t0) ' + fowl, ags.writers = gs.fwriters, FLITInv(gs, lsf, pcf), FLITInv((gs.pmem:= gs.pmem(loc0 := val)).pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), W(val, t0) ∈ gs.pq(loc0), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ lsf(t).t = alsf(t).t ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) = ready → apcf(t) = ready) ∧ (pcf(t) = crashed → apcf(t) = crashed) ∧ (pcf(t) = R1 → apcf(t) = R1) ∧ (pcf(t) = R2 → apcf(t) = R2) ∧ (pcf(t) = R3 → apcf(t) = R3) ∧ (pcf(t) = R4 → apcf(t) = R4) ∧ (pcf(t) = R1 ∨ pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → lsf(t).loc = alsf(t).l) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → lsf(t).val = alsf(t).v) ∧ (pcf(t) = W1 → apcf(t) = W1) ∧ (pcf(t) = W2 → apcf(t) = (SF ∈ gs.bq(lsf(t).t) ⊃ W1;W2)) ∧ (pcf(t) = W3 → apcf(t) = W3) ∧ (pcf(t) = W4 → apcf(t) = (W(lsf(t).loc, lsf(t).val) ∈ gs.bq(lsf(t).t) ⊃ W3;W4)) ∧ (pcf(t) = W5 → apcf(t) = (W(lsf(t).loc, lsf(t).val) ∈ gs.bq(lsf(t).t) ⊃ W3;(FO(lsf(t).loc) ∈ gs.bq(lsf(t).t) ⊃ W4;W5))) ∧ (pcf(t) = W6 → apcf(t) = (W(lsf(t).loc, lsf(t).val) ∈ gs.bq(lsf(t).t) ⊃ W3;(FO(lsf(t).loc) ∈ gs.bq(lsf(t).t) ⊃ W4;(SF ∈ gs.bq(lsf(t).t) ⊃ W5;W6)))) ∧ (pcf(t) = W7 → apcf(t) = W7) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → lsf(t).loc = alsf(t).l) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → lsf(t).val = alsf(t).v)

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = R1) ∧ (pc = R2 → apc = R2) ∧ (pc = R3 → apc = R3) ∧ (pc = R4 → apc = R4) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.loc = als.l) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.val = als.v) ∧ (pc = W1 → apc = W1) ∧ (pc = W2 → apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2)) ∧ (pc = W3 → apc = W3) ∧ (pc = W4 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4)) ∧ ( pc = W5 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5))) ∧ ( pc = W6 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3 ;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6)) )) ∧ (pc = W7 → apc = W7) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.loc = als.l) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.val = als.v); a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ (gs.pmem:= pmem).bq = gs.bq; (s) ⊦ (gs.pq:= pq).bq = gs.bq; (s) ⊦ W(v, tid).val = v; (s) ⊦ reorder(p, pq, rfo) ∧ pq(l) = W(v, t) ' + fowl → p(l)[firstPersistW(p(l))] = W(v, t); (s) ⊦ reorder(p, pq, rfo) ∧ pq(l) = W(v, t) ' + fowl → reorder(p(l := p(l) -p firstPersistW(p(l))), pq(l := fowl), rfo); (ss) ⊦ reorder(p, pq, rfo) ∧ pq(l) = W(v, t) ' + fowl → firstPersistW(p(l)) < # p(l); (ss) ⊦ W(v, tid).W?; (s)

Proof step 26 from proof step-absstep-PERSIST_W-globalPERSIST_W (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = R1) ∧ (pc = R2 → apc = R2) ∧ (pc = R3 → apc = R3) ∧ (pc = R4 → apc = R4) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.loc = als.l) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.val = als.v) ∧ (pc = W1 → apc = W1) ∧ (pc = W2 → apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2)) ∧ (pc = W3 → apc = W3) ∧ (pc = W4 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4)) ∧ ( pc = W5 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5))) ∧ ( pc = W6 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3 ;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6)) )) ∧ (pc = W7 → apc = W7) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.loc = als.l) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.val = als.v); Used terms: t