| Symbol | Specification | Kind | Type |
|---|
| # . | list-data | f | List('a) → Nat |
| # . | set-basic | f | Set('a) → Nat |
| #oc | list-perm | f | 'a × List('a) → Nat |
| . ' | list | f | 'a → List('a) |
| . + . | nat-basic | f | Nat × Nat → Nat |
| . + . | list-data | f | 'a × List('a) → List('a) |
| . + . | list | f | List('a) × List('a) → List('a) |
| . + . | list | f | List('a) × 'a → List('a) |
| . ++ . | list-dup | f | List('a) × 'a → List('a) |
| . ++ . | set-basic | f | Set('a) × 'a → Set('a) |
| . +1 | nat-basic | f | Nat → Nat |
| . +2 . | list | f | 'a × 'a → List('a) |
| . - . | nat | pf | Nat × Nat → Nat with λ n, m. n ≥ m |
| . -- . | set-union | f | Set('a) × 'a → Set('a) |
| . -1 | nat-basic | pf | Nat → Nat with λ n. n ≠ 0 |
| . -1l . | list-del | f | List('a) × 'a → List('a) |
| . -l . | list-del | f | List('a) × 'a → List('a) |
| . -p . | list-del | f | List('a) × Nat → List('a) |
| . .FO? | FOW | p | FOW |
| . .FO? | Bevent | p | Bevent |
| . .FOWs ( . ) | FLIT-preds | f | List(Bevent) × T × L → List(FOW) |
| . .FOs? | FLIT-preds | p | (T → Type(List(Bevent))) |
| . .W? | FOW | p | FOW |
| . .W? | Bevent | p | Bevent |
| . .bq | FLIT | f | FLITGState → T → List(Bevent) |
| . .bq:= . | FLIT | f | FLITGState × (T → List(Bevent)) → FLITGState |
| . .butlast | list-last | pf | List('a) → List('a) with λ x. x ≠ [] |
| . .count ( . ) | filter-count | f | List('a) × ('a → Bool) → Nat |
| . .count ( . ) | filter-count | pf | List('a) × Nat × Nat × ('a → Bool) → Nat with λ x, m, n, p. m ≤ n ∧ n ≤ # x |
| . .distinct | list-dup | f | List('a) → List('a) |
| . .drop ( . ) | list-del | pf | List('a) × Nat → List('a) with λ x, n. n ≤ # x |
| . .dropRight ( . ) | list-last | pf | List('a) × Nat → List('a) with λ x, n. n ≤ # x |
| . .exists ( . ) | forall-indexWhere | p | List('a) × ('a → Type(Bool)) |
| . .fctr | FLIT | f | FLITGState → L → Nat |
| . .fctr | FLIT | pf | FLITAction → L → Nat with λ a.
λ l.
(∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW6(fctr, l, fwriters, tid, fctr0, fwriters0))
∨ (∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW2(fctr, l, fwriters, tid, fctr0, fwriters0)) |
| . .fctr:= . | FLIT | f | FLITGState × (L → Nat) → FLITGState |
| . .fctr0 | FLIT | pf | FLITAction → L → Nat with λ a.
λ l.
(∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW6(fctr, l, fwriters, tid, fctr0, fwriters0))
∨ (∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW2(fctr, l, fwriters, tid, fctr0, fwriters0)) |
| . .filter ( . ) | filter-count | f | List('a) × ('a → Bool) → List('a) |
| . .filter ( . ) | set-union | f | Set('a) × ('a → Bool) → Set('a) |
| . .foldLeft ( . ) | list | f | List('a) × 'b × ('b × 'a → 'b) → 'b |
| . .forall ( . ) | forall-indexWhere | p | List('a) × ('a → Type(Bool)) |
| . .freaders | FLIT | f | FLITGState → L → Set(T) |
| . .freaders:= . | FLIT | f | FLITGState × (L → Set(T)) → FLITGState |
| . .fwriters | FLIT | f | FLITGState → L → Set(T) |
| . .fwriters | FLIT | pf | FLITAction → L → Set(T) with λ a.
λ l.
(∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW6(fctr, l, fwriters, tid, fctr0, fwriters0))
∨ (∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW2(fctr, l, fwriters, tid, fctr0, fwriters0)) |
| . .fwriters:= . | FLIT | f | FLITGState × (L → Set(T)) → FLITGState |
| . .fwriters0 | FLIT | pf | FLITAction → L → Set(T) with λ a.
λ l.
(∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW6(fctr, l, fwriters, tid, fctr0, fwriters0))
∨ (∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW2(fctr, l, fwriters, tid, fctr0, fwriters0)) |
| . .gstate | FLIT | f | FLITState → FLITGState |
| . .gstate:= . | FLIT | f | FLITState × FLITGState → FLITState |
| . .head | list-data | pf | List('a) → 'a with λ x. x ≠ [] |
| . .indexOf ( . ) | list-del | f | List('a) × 'a → Nat |
| . .indexWhere ( . ) | forall-indexWhere | f | List('a) × ('a → Bool) → Nat |
| . .invFLITREADloc | FLIT | pf | FLITAction → L with λ a. ∃ tid, l. a = invFLITREAD(tid, l) |
| . .invFLITWRITEloc | FLIT | pf | FLITAction → L with λ a. ∃ tid, l, v. a = invFLITWRITE(tid, l, v) |
| . .invFLITWRITEval | FLIT | pf | FLITAction → V with λ a. ∃ tid, l, v. a = invFLITWRITE(tid, l, v) |
| . .invPERSIST_FOloc | FLIT | pf | FLITAction → L with λ a. ∃ l. a = globalPERSIST_FO(l) |
| . .invPERSIST_Wloc | FLIT | pf | FLITAction → L with λ a. ∃ l. a = globalPERSIST_W(l) |
| . .l | Bevent | pf | Bevent → L with λ be. be.FO? ∨ be.W? |
| . .l | FLIT | pf | FLITAction → L with λ a.
(∃ tid, l. a = pwb(tid, l)) ∨ (∃ tid, l. a = propFO(tid, l))
∨ (∃ tid, l. a = doWriteFO(tid, l)) ∨ (∃ tid, l, v. a = doWrite(tid, l, v))
∨ (∃ tid, l, v. a = doRead(tid, l, v)) ∨ (∃ tid, l, n. a = ctrRead(tid, l, n))
∨ (∃ tid, l. a = ctrInc(tid, l)) ∨ (∃ tid, l. a = ctrDec(tid, l)) |
| . .last | list-last | pf | List('a) → 'a with λ x. x ≠ [] |
| . .loc | FLIT | f | FLITLState → L |
| . .loc | FLIT | pf | FLITAction → L with λ a.
(∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW6(fctr, l, fwriters, tid, fctr0, fwriters0))
∨ (∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW2(fctr, l, fwriters, tid, fctr0, fwriters0)) |
| . .loc:= . | FLIT | f | FLITLState × L → FLITLState |
| . .lsf | FLIT | f | FLITState → T → FLITLState |
| . .lsf:= . | FLIT | f | FLITState × (T → FLITLState) → FLITState |
| . .map ( . ) | list | f | List('a) × ('a → 'b) → List('b) |
| . .map ( . ) | set-union | f | Set('a) × ('a → 'b) → Set('b) |
| . .n | FLIT | pf | FLITAction → Nat with λ a. ∃ tid, l, n. a = ctrRead(tid, l, n) |
| . .pcf | FLIT | f | FLITState → T → FLITPC |
| . .pcf:= . | FLIT | f | FLITState × (T → FLITPC) → FLITState |
| . .pmem | FLIT | f | FLITGState → L → V |
| . .pmem:= . | FLIT | f | FLITGState × (L → V) → FLITGState |
| . .pq | FLIT | f | FLITGState → L → List(FOW) |
| . .pq:= . | FLIT | f | FLITGState × (L → List(FOW)) → FLITGState |
| . .retFLITREADval | FLIT | pf | FLITAction → V with λ a. ∃ tid, v. a = retFLITREAD(tid, v) |
| . .rfo | FLIT | f | FLITGState → T → List(Bevent) |
| . .rfo:= . | FLIT | f | FLITGState × (T → List(Bevent)) → FLITGState |
| . .sublist ( . ) | list-del | pf | List('a) × Nat × Nat → List('a) with λ x, n, m. n + m ≤ # x |
| . .t | FLIT | f | FLITLState → T |
| . .t | FLIT | pf | FLITAction → T with λ a.
(∃ tid. a = retFLITWRITE(tid)) ∨ (∃ tid, v. a = retFLITREAD(tid, v))
∨ (∃ tid, l, v. a = invFLITWRITE(tid, l, v)) ∨ (∃ tid, l. a = invFLITREAD(tid, l))
∨ (∃ tid. a = callRUN(tid)) ∨ (∃ tid. a = callFLITCOMPLETE(tid))
∨ (∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW6(fctr, l, fwriters, tid, fctr0, fwriters0))
∨ (∃ fctr, l, fwriters, tid, fctr0, fwriters0.
a = atomicW2(fctr, l, fwriters, tid, fctr0, fwriters0)) |
| . .t:= . | FLIT | f | FLITLState × T → FLITLState |
| . .tail | list-data | pf | List('a) → List('a) with λ x. x ≠ [] |
| . .take ( . ) | list-del | pf | List('a) × Nat → List('a) with λ x, n. n ≤ # x |
| . .takeRight ( . ) | list-del | pf | List('a) × Nat → List('a) with λ x, n. n ≤ # x |
| . .tid | FOW | f | FOW → T |
| . .tid | FLIT | pf | FLITAction → T with λ a.
(∃ tid. a = sfence(tid)) ∨ (∃ tid, l. a = pwb(tid, l)) ∨ (∃ tid. a = propSF(tid))
∨ (∃ tid, l. a = propFO(tid, l)) ∨ (∃ tid, l. a = doWriteFO(tid, l))
∨ (∃ tid, l, v. a = doWrite(tid, l, v)) ∨ (∃ tid, l, v. a = doRead(tid, l, v))
∨ (∃ tid, l, n. a = ctrRead(tid, l, n)) ∨ (∃ tid, l. a = ctrInc(tid, l))
∨ (∃ tid, l. a = ctrDec(tid, l)) |
| . .v | Bevent | pf | Bevent → V with λ be. be.W? |
| . .v | FLIT | pf | FLITAction → V with λ a. (∃ tid, l, v. a = doWrite(tid, l, v)) ∨ (∃ tid, l, v. a = doRead(tid, l, v)) |
| . .val | FLIT | f | FLITLState → V |
| . .val | FOW | pf | FOW → V with λ fow. fow.W? |
| . .val:= . | FLIT | f | FLITLState × V → FLITLState |
| . < . | nat-basic | p | Nat × Nat |
| . < . | list-data | p | List('a) × List('a) |
| . > . | nat | p | Nat × Nat |
| . [ . := . ] | list-getput | pf | List('a) × Nat × 'a → List('a) with λ x, n, a. n < # x |
| . [ . ] | list-getput | pf | List('a) × Nat → 'a with λ x, n. n < # x |
| . \ . | list-set | f | List('a) × List('a) → List('a) |
| . \ . | set-union | f | Set('a) × Set('a) → Set('a) |
| . | . | FLITPSC-preds | f | List(FOW) × T → List(FOW) |
| . |FO | FLITPSC-preds | f | List(FOW) → List(FOW) |
| . |SF . | FLIT-preds | f | List(Bevent) × L → List(Bevent) |
| . |W | FLITPSC-preds | f | List(FOW) → List(FOW) |
| . |WL . | FLIT-preds | f | List(Bevent) × L → List(Bevent) |
| . ∈ . | list | p | 'a × List('a) |
| . ∈ . | set-basic | p | 'a × Set('a) |
| . ∩ . | set-union | f | Set('a) × Set('a) → Set('a) |
| . ∪ . | list-set | f | List('a) × List('a) → List('a) |
| . ∪ . | set-union | f | Set('a) × Set('a) → Set('a) |
| . ≤ . | nat | p | Nat × Nat |
| . ≥ . | nat | p | Nat × Nat |
| . ⊆ . | list-set | p | List('a) × List('a) |
| . ⊆ . | set-basic | p | Set('a) × Set('a) |
| . ⊆m . | list-perm | p | List('a) × List('a) |
| . ⊑ . | list-last | p | List('a) × List('a) |
| . ⊒ . | list-last | p | List('a) × List('a) |
| . ⊒w . | FLIT-preds | p | List(Bevent) × List(Bevent) |
| . ⊕ . | FLITPSC-preds | f | V × List(FOW) → V |
| . ⊕ . | FLITPSC-preds | f | (L → V) × (L → List(FOW)) → L → V |
| . ⊕ . | FLIT-preds | f | V × List(Bevent) → V |
| . ⊕ . | FLIT-preds | f | (L → V) × List(Bevent) → L → V |
| . intersect . | list-set | f | List('a) × List('a) → List('a) |
| . zip . | filter-count | f | List('a) × List('b) → List(('a, 'b)) |
| [] | list-data | c | List('a) |
| { . } | set-union | f | 'a → Set('a) |
| τ | FLIT | c | FLITAction |
| ∅ | set-basic | c | Set('a) |
| ∅ | memory | f | L → V |
| Bevent | Bevent | s | |
| CRASH | FLIT | pr | : (L → List(FOW)) × (L → Nat) × (T → List(Bevent)) × (L → Set(T)) × (L → Set(T)) ×
(T → List(Bevent)) × (T → FLITPC) |
| FLITAction | FLIT | s | |
| FLITCOMPLETE | FLIT | pr | T × (L → List(FOW)) × (T → List(Bevent)) : |
| FLITGInv | FLIT | p | FLITGState |
| FLITGState | FLIT | s | |
| FLITInv | FLIT | p | FLITGState × (T → Type(FLITLState)) × (T → Type(FLITPC)) |
| FLITLInv | FLIT | p | FLITGState × FLITLState × FLITPC |
| FLITLState | FLIT | s | |
| FLITPC | FLIT | s | |
| FLITREAD | FLIT | pr | L × T × (L → V) × (L → List(FOW)) × (L → Nat)
: (T → List(Bevent)) × (L → Set(T)) × (T → List(Bevent))
: V |
| FLITRely | FLIT | p | FLITGState × T × FLITGState |
| FLITState | FLIT | s | |
| FLITWRITE | FLIT | pr | L × V × T × (L → List(FOW)) : (L → Nat) × (T → List(Bevent)) × (L → Set(T)) |
| FO | FOW | f | T → FOW |
| FO | Bevent | f | L → Bevent |
| FOFollowsW | FLITPSC-preds | p | T × List(FOW) |
| FOFollowsW | FLIT-preds | p | T × List(Bevent) × (L → Type(List(FOW))) × L |
| FOFollowsW | FLIT-preds | p | T × List(Bevent) × List(FOW) × L |
| FOW | FOW | s | |
| L | memory | s | |
| List | list-data | s | |
| Nat | nat-basic | s | |
| O | memory | c | V |
| PERSIST_FO | FLIT | pr | L : (L → List(FOW)) |
| PERSIST_W | FLIT | pr | L : (L → V) × (L → List(FOW)) |
| PROP_FO | FLIT | pr | T × L × (L → Set(T)) : (L → List(FOW)) × (T → List(Bevent)) × (T → List(Bevent)) (nondeterministic) |
| PROP_SF | FLIT | pr | T × (L → List(FOW)) : (T → List(Bevent)) |
| PROP_W | FLIT | pr | T : (L → List(FOW)) × (T → List(Bevent)) |
| R1 | FLIT | c | FLITPC |
| R2 | FLIT | c | FLITPC |
| R3 | FLIT | c | FLITPC |
| R4 | FLIT | c | FLITPC |
| RUN | FLIT | pr | : |
| SF | Bevent | c | Bevent |
| SFTrailing | FLIT-preds | p | (T → Type(List(Bevent))) |
| Set | set-basic | s | |
| T | memory | s | |
| V | memory | s | |
| W | FOW | f | V × T → FOW |
| W | Bevent | f | L × V → Bevent |
| W1 | FLIT | c | FLITPC |
| W2 | FLIT | c | FLITPC |
| W3 | FLIT | c | FLITPC |
| W4 | FLIT | c | FLITPC |
| W5 | FLIT | c | FLITPC |
| W6 | FLIT | c | FLITPC |
| W7 | FLIT | c | FLITPC |
| a | FLIT-proofs | v | FLITAction |
| atomicW2 | FLIT | f | (L → Nat) × L × (L → Set(T)) × T × (L → Nat) × (L → Set(T)) → FLITAction |
| atomicW6 | FLIT | f | (L → Nat) × L × (L → Set(T)) × T × (L → Nat) × (L → Set(T)) → FLITAction |
| be | FLIT-proofs | v | Bevent |
| bel | FLIT-proofs | v | List(Bevent) |
| bq | FLIT-proofs | v | T → List(Bevent) |
| bv | FLIT-proofs | v | Bool |
| callFLITCOMPLETE | FLIT | f | T → FLITAction |
| callRUN | FLIT | f | T → FLITAction |
| crashed | FLIT | c | FLITPC |
| ctrDec | FLIT | f | T × L → FLITAction |
| ctrInc | FLIT | f | T × L → FLITAction |
| ctrRead | FLIT | f | T × L × Nat → FLITAction |
| ctrok | FLITPSC-preds | p | (L → Type(Nat)) × (L → Type(Set(T))) |
| disj | list-dup | p | List('a) × List('a) |
| disjoint | set-union | p | Set('a) × Set('a) |
| doRead | FLIT | f | T × L × V → FLITAction |
| doWrite | FLIT | f | T × L × V → FLITAction |
| doWriteFO | FLIT | f | T × L → FLITAction |
| dups | list-dup | p | List('a) |
| fctr | FLIT-proofs | v | L → Nat |
| fillfirst | list-last | f | Nat × 'a × List('a) → List('a) |
| fl | FLIT-proofs | v | L |
| flitInit | FLIT | p | FLITState |
| flitStep | FLIT | p | FLITState × FLITAction × FLITState |
| fow | FLIT-proofs | v | FOW |
| fowl | FLIT-proofs | v | List(FOW) |
| freaders | FLIT-proofs | v | L → Set(T) |
| frome | list-del | f | List('a) × 'a → List('a) |
| fv | FLIT-proofs | v | V |
| fwriters | FLIT-proofs | v | L → Set(T) |
| glb | FLIT-proofs | v | Nat |
| globalCRASH | FLIT | c | FLITAction |
| globalPERSIST_FO | FLIT | f | L → FLITAction |
| globalPERSIST_W | FLIT | f | L → FLITAction |
| gs | FLIT-proofs | v | FLITGState |
| gstate | FLIT-proofs | v | FLITGState |
| gstepf | FLIT | f | FLITGState × FLITLState × FLITPC × FLITAction → FLITGState |
| idle | FLIT | c | FLITPC |
| invFLITREAD | FLIT | f | T × L → FLITAction |
| invFLITREADloc | FLIT-proofs | v | L |
| invFLITWRITE | FLIT | f | T × L × V → FLITAction |
| invFLITWRITEloc | FLIT-proofs | v | L |
| invFLITWRITEval | FLIT-proofs | v | V |
| invPERSIST_FOloc | FLIT-proofs | v | L |
| invPERSIST_Wloc | FLIT-proofs | v | L |
| isPropFO | FLIT-preds | p | Nat × L × List(Bevent) |
| l | FLIT-proofs | v | L |
| loc | FLIT-proofs | v | L |
| ls | FLIT-proofs | v | FLITLState |
| lsf | FLIT-proofs | v | T → FLITLState |
| lstep | FLIT | p | FLITGState × FLITLState × FLITPC × FLITAction × FLITGState × FLITLState × FLITPC |
| lstepf | FLIT | f | FLITGState × FLITLState × FLITPC × FLITAction → FLITLState |
| mkFLITgs | FLIT | f | (L → V) × (L → List(FOW)) × (L → Nat) × (T → List(Bevent)) × (L → Set(T)) × (L → Set(T)) ×
(T → List(Bevent))
→ FLITGState |
| mkFLITls | FLIT | f | T × L × V → FLITLState |
| mklist | list-last | f | 'a × Nat → List('a) |
| mkstate | FLIT | f | FLITGState × (T → FLITLState) × (T → FLITPC) → FLITState |
| n | FLIT-proofs | v | Nat |
| noPending | FLITPSC-preds | p | T × (L → Type(List(FOW))) |
| noPending | FLIT-preds | p | T × (T → Type(List(Bevent))) × (L → Type(List(FOW))) |
| noPendingW | FLITPSC-preds | p | T × (L → Type(List(FOW))) |
| noPendingW | FLIT-preds | p | T × (T → Type(List(Bevent))) × (L → Type(List(FOW))) |
| notMember | FLITPSC-preds | p | T × (L → Type(Set(T))) |
| oneMember | FLITPSC-preds | p | T × L × (L → Type(Set(T))) |
| onePendingW | FLITPSC-preds | p | T × L × (L → Type(List(FOW))) |
| pc | FLIT-proofs | v | FLITPC |
| pcf | FLIT-proofs | v | T → FLITPC |
| pcstepf | FLIT | f | FLITGState × FLITLState × FLITPC × FLITAction → FLITPC |
| pendingOk | FLITPSC-preds | p | (L → Type(List(FOW))) |
| pendingOk | FLIT-preds | p | (T → Type(List(Bevent))) × (L → Type(List(FOW))) |
| perm | list-perm | p | List('a) × List('a) |
| pmem | FLIT-proofs | v | L → V |
| pq | FLIT-proofs | v | L → List(FOW) |
| pre | FLIT | p | FLITGState × FLITLState × FLITPC × FLITAction |
| propFO | FLIT | f | T × L → FLITAction |
| propSF | FLIT | f | T → FLITAction |
| pwb | FLIT | f | T × L → FLITAction |
| readFOsOk | FLIT-preds | p | (T → Type(List(Bevent))) × (L → Type(Set(T))) |
| ready | FLIT | c | FLITPC |
| rely | FLIT-preds | p | T × (L → Type(List(FOW))) × (T → Type(List(Bevent))) × (L → Type(List(FOW))) × (T → Type(List(Bevent))) |
| rely | FLIT-preds | p | T × L × List(FOW) × List(Bevent) × List(FOW) × List(Bevent) |
| relyp | FLITPSC-preds | p | T × List(FOW) × List(FOW) |
| relyp | FLITPSC-preds | p | T × (L → Type(List(FOW))) × (L → Type(List(FOW))) |
| relyws | FLITPSC-preds | p | T × (L → Type(Set(T))) × (L → Type(Set(T))) |
| relyws | FLITPSC-preds | p | T × Set(T) × Set(T) |
| retFLITREAD | FLIT | f | T × V → FLITAction |
| retFLITREADval | FLIT-proofs | v | V |
| retFLITWRITE | FLIT | f | T → FLITAction |
| rev | list-last | f | List('a) → List('a) |
| rfo | FLIT-proofs | v | T → List(Bevent) |
| s | FLIT-proofs | v | FLITState |
| sfence | FLIT | f | T → FLITAction |
| t | FLIT-proofs | v | T |
| tid | FLIT-proofs | v | T |
| ts | FLIT-proofs | v | Set(T) |
| v | FLIT-proofs | v | V |
| val | FLIT-proofs | v | V |
| wl | FLIT-proofs | v | L |
| writersOk | FLITPSC-preds | p | (L → Type(List(FOW))) × (L → Type(Set(T))) |
| writersOk | FLIT-preds | p | (T → Type(List(Bevent))) × (L → Type(List(FOW))) × (L → Type(Set(T))) |