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: |
|---|---|---|
| absloc-persistfirstFO | ⊦ el = [] ∨ ¬ el.head.R? → (absloc(el, rset, FO(t) ' + fowl) ↔ absloc(el, rset, fowl)) | A User Theorem |
| abs-firstPersistW-is-in-hist | ⊦ abs(h, rs, p) ∧ firstPersistW(p(l)) < # p(l) → (h |W | l) | false ≠ [] | A User Theorem |
| absloc-addReadReader | ⊦ absloc(el, rset, fowl) → absloc(el + R(t, l, v) ', rset ++ t, fowl) | A User Theorem |
| absloc-prepend-FO | ⊦ absloc(el, rset, fowl) → absloc(el, rset, FO(t) ' + fowl) | A User Theorem |
| abs-persistFO | ⊦ allReadsOK(h) ∧ p(l) = FO(t) ' + fowl → (abs(h, rs, p(l := fowl)) ↔ abs(h, rs, p)) | A User Theorem |
| abs-leading-last-FO-no-pending | ⊦ abs(h, rs, p) ∧ allReadsOK(h) ∧ noPendingW(t, p) ∧ p(l) = FO(t) ' + fowl ∧ ¬ FO(t) ∈ fowl ∧ ¬ t ∈ rs(l) → ((h | l) | t) | false = [] | A User Theorem |
| absloc-addWriteFO | ⊦ (∀ e. e ∈ el ∧ e.R? → e.t ≠ t) → (absloc(el, rset, fowl + FO(t) ') ↔ absloc(el, rset, fowl)) | A User Theorem |
| absloc-recW-FO | ⊦ absloc(W(t, l, v) ' + el, rset, FO(t0) ' + fowl) ↔ absloc(W(t, l, v) ' + el, rset, fowl) | An Axiom |
| absloc-no-W-leading-W | ⊦ fowl |W | t = [] → ¬ absloc(W(t, l, v) ' + el, rset, fowl) | A User Theorem |
| abs-addRead | ⊦ t ∈ rs(l) → (abs(h + (R(t, l, v), b) ', rs, p) ↔ abs(h, rs, p)) | A User Theorem |
| absloc-recW-FO-one2 | ⊦ ¬ absloc(W(t, l, v) ' + el, rset, FO(t0) ') | A User Theorem |
| abs-firstVolWrite-head | ⊦ abs(h, rs, p) ∧ p(l) = W(v, t) ' + fowl → h[firstVolWrite(l, h)] = (W(t, l, v), false) | A User Theorem |
| abs-addReadReader | ⊦ abs(h, rs, p) → abs(h + (R(t, l, v), b) ', rs(l := rs(l) ++ t), p) | A User Theorem |
| absloc-addWrite | ⊦ absloc(el + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el, rset, fowl) | A User Theorem |
| absloc-recW-W-one3 | ⊦ absloc(W(t, l, v) ', rset, W(v0, t0) ') ↔ t0 = t ∧ v0 = v | A User Theorem |
| abs-single-FO-one-pending | ⊦ abs(h, rs, p) ∧ allReadsOK(h) ∧ onePendingW(t, l0, p) ∧ FOFollowsW(t, p(l0)) ∧ isPersistFO(n, p(l)) ∧ ¬ FO(t) ∈ p(l) -p n ∧ FO(t) ∈ p(l) ∧ ¬ t ∈ rs(l) → ((h | l) | t) | false = [] | A User Theorem |
| absloc-recW-FO-one | ⊦ absloc(W(t, l, v) ', rset, FO(t0) ' + fowl) ↔ absloc(W(t, l, v) ', rset, fowl) | A User Theorem |
| abs-leading-last-FO-one-pending | ⊦ abs(h, rs, p) ∧ allReadsOK(h) ∧ onePendingW(t, l0, p) ∧ FOFollowsW(t, p(l0)) ∧ p(l) = FO(t) ' + fowl ∧ ¬ FO(t) ∈ fowl ∧ ¬ t ∈ rs(l) → ((h | l) | t) | false = [] | A User Theorem |
| abs-persistFO-weak | ⊦ allReadsOK(h) ∧ isPersistFO(n, p(l)) ∧ abs(h, rs, p) → abs(h, rs, p(l := p(l) -p n)) | A User Theorem |
| abs-loc-no-w-no-fo-then-no-pending | ⊦ absloc(events((h | l) | false), rset, fowl) ∧ fowl |W | t = [] ∧ ¬ FO(t) ∈ fowl ∧ ¬ t ∈ rset → ((h | l) | t) | false = [] | A User Theorem |
| abs-addReadFO | ⊦ t ∈ rs(l) → (abs(h, rs(l := rs(l) -- t), p(l := p(l) + FO(t) ')) ↔ abs(h, rs, p)) | A User Theorem |
| abs-persistWrite | ⊦ p(l) = W(v, t) ' + fowl ∧ abs(h, rs, p) ∧ h[firstVolWrite(l, h)] = (W(t, l, v), false) → abs(h.take(firstVolWrite(l, h)) + (W(t, l, v), true) ' + persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)), rs, p(l := fowl)) | A User Theorem |
| abs-addWrite | ⊦ abs(h + (W(t, l, v), false) ', rs, p(l := p(l) + W(v, t) ')) ↔ abs(h, rs, p) | A User Theorem |
| absloc-recW-empty | ⊦ ¬ absloc(W(t, l, v) ' + el, rset, []) | An Axiom |
| abs-leading-write-h-restricted-non-empty | ⊦ abs(h, rs, p) ∧ p(l) = W(v, t) ' + fowl → (h |W | l) | false ≠ [] | A User Theorem |
| absloc-persistWrite | ⊦ absloc(events((h0 | l) | false) + W(t, l, v) ' + events((h1 | l) | false), rset, W(v0, t0) ' + fowl) ∧ (h0 |W | l) | false = [] → absloc(events((h0 | l) | false) + events((persistDependentReads(l, h1) | l) | false), rset, fowl) | A User Theorem |
| abs-loc-no-w-last-fo-then-no-pending | ⊦ absloc(events((h | l) | false), rset, fowl) ∧ allReadsOKInd(mem, persisted, h) ∧ persisted(l) ∧ isPersistFO(n, fowl) ∧ (fowl -p n)|W | t = [] ∧ ¬ FO(t) ∈ fowl -p n ∧ FO(t) ∈ fowl ∧ ¬ t ∈ rset → ((h | l) | t) | false = [] | A User Theorem |
| absloc-recR | ⊦ absloc(R(t, l, v) ' + el, rset, fowl) ↔ (¬ t ∈ rset → FO(t) ∈ fowl) ∧ absloc(el, rset, fowl) | An Axiom |
| abs-persist-firstPersistW | ⊦ abs(h, rs, p) ∧ firstPersistW(p(l)) < # p(l) ∧ h[firstVolWrite(l, h)] = (e, bv) → abs (h.take(firstVolWrite(l, h)) + (e, true) ' + persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)), rs, p(l := p(l) -p firstPersistW(p(l)))) | A User Theorem |
| abs-single-FO-no-pending | ⊦ abs(h, rs, p) ∧ allReadsOK(h) ∧ noPendingW(t, p) ∧ isPersistFO(n, p(l)) ∧ ¬ FO(t) ∈ p(l) -p n ∧ FO(t) ∈ fowl ∧ ¬ t ∈ rs(l) → ((h | l) | t) | false = [] | A User Theorem |
| absloc-persistFO | ⊦ (el = [] ∨ ¬ el.head.R?) ∧ absloc(el, rset, fowl) ∧ isPersistFO(n, fowl) → absloc(el, rset, fowl -p n) | A User Theorem |
| counterzero | ⊦ ctr(l) = 0 ∧ ctrok(ctr, ws) ∧ writersOk(p, ws) → p(l) |W = [] | A User Theorem |
| absloc-persist-DependentReads | ⊦ absloc(events((h | l) | false), rset, fowl) → absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl) | A User Theorem |
| absloc-recW-empty-one | ⊦ ¬ absloc(W(t, l, v) ', rset, []) | A User Theorem |
| absloc-recW-W-one | ⊦ absloc(W(t, l, v) ', rset, W(v0, t0) ' + fowl) ↔ t0 = t ∧ v0 = v ∧ fowl |W = [] | A User Theorem |
| abs-def-reduce | ⊦ abs(h, rs, p) → (abs(h0, rs0, p0) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l)) → absloc(events((h0 | l) | false), rs0(l), p0(l)))) | A User Theorem |
| absloc-recR-one | ⊦ absloc(R(t, l, v) ', rset, fowl) ↔ (¬ t ∈ rset → FO(t) ∈ fowl) ∧ fowl |W = [] | A User Theorem |
| absloc-addReadFO | ⊦ t ∈ rset → (absloc(el, rset -- t, fowl + FO(t) ') ↔ absloc(el, rset, fowl)) | A User Theorem |
| absloc-addReader | ⊦ absloc(el, rset, fowl) → absloc(el, rset ++ t, fowl) | A User Theorem |
| pofl-empty-all-l-persisted | ⊦ p(l) |W = [] ∧ allReadsOK(h) ∧ abs(h, rs, p) → (h | l) | false = [] | A User Theorem |
| absloc-recW-W-one2 | ⊦ absloc(W(t, l, v) ' + el, rset, W(v0, t0) ') ↔ t0 = t ∧ v0 = v ∧ absloc(el, rset, []) | A User Theorem |
| abs-addWriteFO | ⊦ ((h | t) | false)|R = [] → (abs(h, rs, p(l := p(l) + FO(t) ')) ↔ abs(h, rs, p)) | A User Theorem |
| absloc-base | ⊦ absloc([], rset, fowl) ↔ fowl |W = [] | An Axiom |
| absloc-persist-firstPersistW | ⊦ absloc(events((h.take(firstVolWrite(l, h)) | l) | false) + W(t, l, v) ' + events((h.drop(firstVolWrite(l, h) + 1) | l) | false), rset, fowl) ∧ firstPersistW(fowl) < # fowl → absloc (events((h.take(firstVolWrite(l, h)) | l) | false) + events((persistDependentReads(l, h.drop(firstVolWrite(l, h) + 1)) | l) | false), rset, fowl -p firstPersistW(fowl)) | A User Theorem |
| abs-def | ⊦ abs(h, rs, p) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l))) | An Axiom |
| abs-loc-no-w-last-firstfo-then-no-pending | ⊦ absloc(events((h | l) | false), rset, FO(t) ' + fowl) ∧ allReadsOKInd(mem, persisted, h) ∧ persisted(l) ∧ fowl |W | t = [] ∧ ¬ FO(t) ∈ fowl ∧ ¬ t ∈ rset → ((h | l) | t) | false = [] | A User Theorem |
| abs-h-p-nowritesh-allpersisted | ⊦ p(l) |W = [] ∧ allReadsOK(h) ∧ abs(h, rs, p) → ((h | l) | t) | false = [] | A User Theorem |
| abs-apply-persist-FO | ⊦ fowl[n].FO? ∧ n < # fowl → v ⊕ (fowl -p n) = v ⊕ fowl | A User Theorem |
| absloc-recW-FO-one3 | ⊦ ¬ absloc(W(t, l, v) ', rset, FO(t0) ') | A User Theorem |
| abs-apply-firstPersistW | ⊦ abs(h, rs, p) ∧ firstPersistW(p(l)) < # p(l) ∧ h[firstVolWrite(l, h)] = (e, bv) → mem(l := e.v) ⊕ p(l := p(l) -p firstPersistW(p(l))) = mem ⊕ p | A User Theorem |
| absloc-addRead | ⊦ t ∈ rset → (absloc(el + R(t, l, v) ', rset, fowl) ↔ absloc(el, rset, fowl)) | A User Theorem |
| absloc-recW-W | ⊦ absloc(W(t, l, v) ' + el, rset, W(v0, t0) ' + fowl) ↔ t0 = t ∧ v0 = v ∧ absloc(el, rset, fowl) | An Axiom |
| absloc-persist-leading-firstPersistW | ⊦ absloc(W(t, l, v) ' + events((h | l) | false), rset, fowl) → absloc(events((persistDependentReads(l, h) | l) | false), rset, fowl -p firstPersistW(fowl)) | A User Theorem |
| abs-h-p-nowritesh-lastPersisted | ⊦ p(l) |W = [] ∧ allReadsOK(h) ∧ abs(h, rs, p) → h.lastPersistedOrElse(l, true) | A User Theorem |
| abs-firstPersistW-firstVolWrite-correct-loc | ⊦ abs(h, rs, p) ∧ firstPersistW(p(l)) < # p(l) ∧ h[firstVolWrite(l, h)] = (e, bv) → e.l = l | A User Theorem |
| abs-firstPersistW-is-firstVolWrite | ⊦ abs(h, rs, p) ∧ firstPersistW(p(l)) < # p(l) ∧ h[firstVolWrite(l, h)] = (e, bv) → p(l)[firstPersistW(p(l))].val = e.v | A User Theorem |
| abs-noReadFO | ⊦ t ∈ rs(l) ∧ (h | l) | false = [] → (abs(h, rs(l := rs(l) -- t), p) ↔ abs(h, rs, p)) | A User Theorem |
| abs-h-p-nowritesh-allpersisted-aux | ⊦ fowl |W = [] ∧ allReadsOK(h) ∧ absloc(events((h | l) | false), rset, fowl) → ((h | l) | t) | false = [] | A User Theorem |
| abs-firstPersistW-in-p-when-firstVolWrite-in-h | ⊦ abs(h, rs, p) → (firstPersistW(p(l)) < # p(l) ↔ firstVolWrite(l, h) < # h) | A User Theorem |
| absloc-nowritesp-nowritesh | ⊦ fowl |W = [] ∧ absloc(events((h | l) | false), rset, fowl) → ((h | l) | false)|W = [] | A User Theorem |