| 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 |
| . .ctr | FLITPSCweak | f | FLITPSCGState → L → Nat |
| . .ctr:= . | FLITPSCweak | f | FLITPSCGState × (L → Nat) → FLITPSCGState |
| . .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 | FLITPSCweak | f | FLITPSCState → FLITPSCGState |
| . .gstate | FLIT | f | FLITState → FLITGState |
| . .gstate:= . | FLITPSCweak | f | FLITPSCState × FLITPSCGState → FLITPSCState |
| . .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 |
| . .invFLITPSCREADl | FLITPSCweak | pf | FLITPSCAction → L with λ a. ∃ tid, l. a = invFLITPSCREAD(tid, l) |
| . .invFLITPSCWRITEl | FLITPSCweak | pf | FLITPSCAction → L with λ a. ∃ tid, l, v. a = invFLITPSCWRITE(tid, l, v) |
| . .invFLITPSCWRITEv | FLITPSCweak | pf | FLITPSCAction → V with λ a. ∃ tid, l, v. a = invFLITPSCWRITE(tid, l, v) |
| . .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) |
| . .invPSCPERSIST_FOl | FLITPSCweak | pf | FLITPSCAction → L with λ a. ∃ l. a = globalPSCPERSIST_FO(l) |
| . .invPSCPERSIST_Wl | FLITPSCweak | pf | FLITPSCAction → L with λ a. ∃ l. a = globalPSCPERSIST_W(l) |
| . .l | FLITPSCweak | f | FLITPSCLState → L |
| . .l | FLITPSCweak | pf | FLITPSCAction → L with λ a.
(∃ tid, l. a = pwbPSC(tid, l)) ∨ (∃ tid, l, v. a = doWritePSC(tid, l, v))
∨ (∃ tid, l, v. a = doReadPSC(tid, l, v)) ∨ (∃ tid, l, n. a = ctrReadPSC(tid, l, n))
∨ (∃ tid, l. a = ctrIncPSC(tid, l)) ∨ (∃ tid, l. a = ctrDecPSC(tid, 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)) |
| . .l:= . | FLITPSCweak | f | FLITPSCLState × L → FLITPSCLState |
| . .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 | FLITPSCweak | f | FLITPSCState → T → FLITPSCLState |
| . .lsf | FLIT | f | FLITState → T → FLITLState |
| . .lsf:= . | FLITPSCweak | f | FLITPSCState × (T → FLITPSCLState) → FLITPSCState |
| . .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) |
| . .mem | FLITPSCweak | f | FLITPSCGState → L → V |
| . .mem:= . | FLITPSCweak | f | FLITPSCGState × (L → V) → FLITPSCGState |
| . .n | FLITPSCweak | pf | FLITPSCAction → Nat with λ a. ∃ tid, l, n. a = ctrReadPSC(tid, l, n) |
| . .n | FLIT | pf | FLITAction → Nat with λ a. ∃ tid, l, n. a = ctrRead(tid, l, n) |
| . .p | FLITPSCweak | f | FLITPSCGState → L → List(FOW) |
| . .p:= . | FLITPSCweak | f | FLITPSCGState × (L → List(FOW)) → FLITPSCGState |
| . .pcf | FLITPSCweak | f | FLITPSCState → T → FLITPSCPC |
| . .pcf | FLIT | f | FLITState → T → FLITPC |
| . .pcf:= . | FLITPSCweak | f | FLITPSCState × (T → FLITPSCPC) → FLITPSCState |
| . .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 |
| . .readers | FLITPSCweak | f | FLITPSCGState → L → Set(T) |
| . .readers:= . | FLITPSCweak | f | FLITPSCGState × (L → Set(T)) → FLITPSCGState |
| . .retFLITPSCREADv | FLITPSCweak | pf | FLITPSCAction → V with λ a. ∃ tid, v. a = retFLITPSCREAD(tid, v) |
| . .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 | FLITPSCweak | f | FLITPSCLState → T |
| . .t | FLIT | f | FLITLState → T |
| . .t | FLITPSCweak | pf | FLITPSCAction → T with λ a.
(∃ tid. a = retFLITPSCWRITE(tid)) ∨ (∃ tid, v. a = retFLITPSCREAD(tid, v))
∨ (∃ tid, l, v. a = invFLITPSCWRITE(tid, l, v)) ∨ (∃ tid, l. a = invFLITPSCREAD(tid, l))
∨ (∃ tid. a = callPSCRUN(tid)) ∨ (∃ tid. a = callPSCCOMPLETE(tid)) |
| . .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:= . | FLITPSCweak | f | FLITPSCLState × T → FLITPSCLState |
| . .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 | FLITPSCweak | pf | FLITPSCAction → T with λ a.
(∃ tid. a = sfencePSC(tid)) ∨ (∃ tid, l. a = pwbPSC(tid, l))
∨ (∃ tid, l, v. a = doWritePSC(tid, l, v)) ∨ (∃ tid, l, v. a = doReadPSC(tid, l, v))
∨ (∃ tid, l, n. a = ctrReadPSC(tid, l, n)) ∨ (∃ tid, l. a = ctrIncPSC(tid, l))
∨ (∃ tid, l. a = ctrDecPSC(tid, l)) |
| . .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 | FLITPSCweak | f | FLITPSCLState → V |
| . .v | FLITPSCweak | pf | FLITPSCAction → V with λ a. (∃ tid, l, v. a = doWritePSC(tid, l, v)) ∨ (∃ tid, l, v. a = doReadPSC(tid, l, v)) |
| . .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)) |
| . .v:= . | FLITPSCweak | f | FLITPSCLState × V → FLITPSCLState |
| . .val | FLIT | f | FLITLState → V |
| . .val | FOW | pf | FOW → V with λ fow. fow.W? |
| . .val:= . | FLIT | f | FLITLState × V → FLITLState |
| . .writers | FLITPSCweak | f | FLITPSCGState → L → Set(T) |
| . .writers:= . | FLITPSCweak | f | FLITPSCGState × (L → Set(T)) → FLITPSCGState |
| . < . | 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 . | FLITPSCweak-preds | p | List(FOW) × List(FOW) |
| . ⊒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) |
| τ | FLITPSCweak | c | FLITPSCAction |
| τ | 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 | |
| FLITPSCAction | FLITPSCweak | s | |
| FLITPSCGInv | FLITPSCweak | p | FLITPSCGState |
| FLITPSCGState | FLITPSCweak | s | |
| FLITPSCInv | FLITPSCweak | p | FLITPSCGState × (T → Type(FLITPSCLState)) × (T → Type(FLITPSCPC)) |
| FLITPSCLInv | FLITPSCweak | p | FLITPSCGState × FLITPSCLState × FLITPSCPC |
| FLITPSCLState | FLITPSCweak | s | |
| FLITPSCPC | FLITPSCweak | s | |
| FLITPSCREAD | FLITPSCweak | pr | L × T × (L → V) × (L → Nat) : (L → List(FOW)) × (L → Set(T)) : V |
| FLITPSCRely | FLITPSCweak | p | FLITPSCGState × T × FLITPSCGState |
| FLITPSCState | FLITPSCweak | s | |
| FLITPSCWRITE | FLITPSCweak | pr | L × V × T : (L → List(FOW)) × (L → Nat) × (L → Set(T)) |
| 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)) |
| PSCCOMPLETE | FLITPSCweak | pr | T × (L → List(FOW)) : |
| PSCCRASH | FLITPSCweak | pr | : (L → List(FOW)) × (L → Nat) × (L → Set(T)) × (L → Set(T)) × (T → FLITPSCPC) |
| PSCPERSIST_FO | FLITPSCweak | pr | L : (L → List(FOW)) (nondeterministic) |
| PSCPERSIST_W | FLITPSCweak | pr | L : (L → V) × (L → List(FOW)) |
| PSCRUN | FLITPSCweak | pr | : |
| R1 | FLITPSCweak | c | FLITPSCPC |
| R1 | FLIT | c | FLITPC |
| R2 | FLITPSCweak | c | FLITPSCPC |
| R2 | FLIT | c | FLITPC |
| R3 | FLITPSCweak | c | FLITPSCPC |
| R3 | FLIT | c | FLITPC |
| R4 | FLITPSCweak | c | FLITPSCPC |
| 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 | FLITPSCweak | c | FLITPSCPC |
| W1 | FLIT | c | FLITPC |
| W2 | FLITPSCweak | c | FLITPSCPC |
| W2 | FLIT | c | FLITPC |
| W3 | FLITPSCweak | c | FLITPSCPC |
| W3 | FLIT | c | FLITPC |
| W4 | FLITPSCweak | c | FLITPSCPC |
| W4 | FLIT | c | FLITPC |
| W5 | FLITPSCweak | c | FLITPSCPC |
| W5 | FLIT | c | FLITPC |
| W6 | FLITPSCweak | c | FLITPSCPC |
| W6 | FLIT | c | FLITPC |
| W7 | FLITPSCweak | c | FLITPSCPC |
| W7 | FLIT | c | FLITPC |
| a | FLIT-refines-FLITPSCweak | v | FLITAction |
| aa | FLIT-refines-FLITPSCweak | v | FLITPSCAction |
| abs | FLIT-refines-FLITPSCweak | p | FLITState × FLITPSCState |
| ags | FLIT-refines-FLITPSCweak | v | FLITPSCGState |
| als | FLIT-refines-FLITPSCweak | v | FLITPSCLState |
| alsf | FLIT-refines-FLITPSCweak | v | T → FLITPSCLState |
| apc | FLIT-refines-FLITPSCweak | v | FLITPSCPC |
| apcf | FLIT-refines-FLITPSCweak | v | T → FLITPSCPC |
| as | FLIT-refines-FLITPSCweak | v | FLITPSCState |
| atomicW1 | FLITPSCweak | c | FLITPSCAction |
| atomicW2 | FLIT | f | (L → Nat) × L × (L → Set(T)) × T × (L → Nat) × (L → Set(T)) → FLITAction |
| atomicW5 | FLITPSCweak | c | FLITPSCAction |
| atomicW6 | FLIT | f | (L → Nat) × L × (L → Set(T)) × T × (L → Nat) × (L → Set(T)) → FLITAction |
| b | FLIT-refines-FLITPSCweak | v | Bool |
| bel | FLIT-refines-FLITPSCweak | v | List(Bevent) |
| bq | FLIT-refines-FLITPSCweak | v | T → List(Bevent) |
| callFLITCOMPLETE | FLIT | f | T → FLITAction |
| callPSCCOMPLETE | FLITPSCweak | f | T → FLITPSCAction |
| callPSCRUN | FLITPSCweak | f | T → FLITPSCAction |
| callRUN | FLIT | f | T → FLITAction |
| crashed | FLITPSCweak | c | FLITPSCPC |
| crashed | FLIT | c | FLITPC |
| ctr | FLIT-refines-FLITPSCweak | v | L → Nat |
| ctrDec | FLIT | f | T × L → FLITAction |
| ctrDecPSC | FLITPSCweak | f | T × L → FLITPSCAction |
| ctrInc | FLIT | f | T × L → FLITAction |
| ctrIncPSC | FLITPSCweak | f | T × L → FLITPSCAction |
| ctrRead | FLIT | f | T × L × Nat → FLITAction |
| ctrReadPSC | FLITPSCweak | f | T × L × Nat → FLITPSCAction |
| 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 |
| doReadPSC | FLITPSCweak | f | T × L × V → FLITPSCAction |
| doWrite | FLIT | f | T × L × V → FLITAction |
| doWriteFO | FLIT | f | T × L → FLITAction |
| doWritePSC | FLITPSCweak | f | T × L × V → FLITPSCAction |
| dups | list-dup | p | List('a) |
| fctr | FLIT-refines-FLITPSCweak | v | L → Nat |
| fillfirst | list-last | f | Nat × 'a × List('a) → List('a) |
| firstPersistW | FLITPSCweak-preds | f | List(FOW) → Nat |
| flitInit | FLIT | p | FLITState |
| flitStep | FLIT | p | FLITState × FLITAction × FLITState |
| flitpscInit | FLITPSCweak | p | FLITPSCState |
| flitpscStep | FLITPSCweak | p | FLITPSCState × FLITPSCAction × FLITPSCState |
| fow | FLIT-refines-FLITPSCweak | v | FOW |
| fowl | FLIT-refines-FLITPSCweak | v | List(FOW) |
| frome | list-del | f | List('a) × 'a → List('a) |
| gabs | FLIT-refines-FLITPSCweak | p | FLITGState × (T → Type(FLITLState)) × (T → Type(FLITPC)) × FLITPSCGState × (T → Type(FLITPSCLState)) × (T → Type(FLITPSCPC)) |
| globalCRASH | FLIT | c | FLITAction |
| globalPERSIST_FO | FLIT | f | L → FLITAction |
| globalPERSIST_W | FLIT | f | L → FLITAction |
| globalPSCCRASH | FLITPSCweak | c | FLITPSCAction |
| globalPSCPERSIST_FO | FLITPSCweak | f | L → FLITPSCAction |
| globalPSCPERSIST_W | FLITPSCweak | f | L → FLITPSCAction |
| gs | FLIT-refines-FLITPSCweak | v | FLITGState |
| gstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCGState |
| gstepf | FLIT | f | FLITGState × FLITLState × FLITPC × FLITAction → FLITGState |
| idle | FLITPSCweak | c | FLITPSCPC |
| idle | FLIT | c | FLITPC |
| il | FLIT-refines-FLITPSCweak | v | L |
| invFLITPSCREAD | FLITPSCweak | f | T × L → FLITPSCAction |
| invFLITPSCWRITE | FLITPSCweak | f | T × L × V → FLITPSCAction |
| invFLITREAD | FLIT | f | T × L → FLITAction |
| invFLITWRITE | FLIT | f | T × L × V → FLITAction |
| isPersistFO | FLITPSCweak-preds | p | Nat × List(FOW) |
| isPropFO | FLIT-preds | p | Nat × L × List(Bevent) |
| iv | FLIT-refines-FLITPSCweak | v | V |
| l | FLIT-refines-FLITPSCweak | v | L |
| labs | FLIT-refines-FLITPSCweak | p | FLITGState × FLITLState × FLITPC × FLITPSCGState × FLITPSCLState × FLITPSCPC |
| loc | FLIT-refines-FLITPSCweak | v | L |
| ls | FLIT-refines-FLITPSCweak | v | FLITLState |
| lsf | FLIT-refines-FLITPSCweak | v | T → FLITLState |
| lstep | FLITPSCweak | p | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction × FLITPSCGState × FLITPSCLState × FLITPSCPC |
| lstep | FLIT | p | FLITGState × FLITLState × FLITPC × FLITAction × FLITGState × FLITLState × FLITPC |
| lstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCLState |
| lstepf | FLIT | f | FLITGState × FLITLState × FLITPC × FLITAction → FLITLState |
| m | FLIT-refines-FLITPSCweak | v | Nat |
| mem | FLIT-refines-FLITPSCweak | v | L → V |
| mkFLITPSCgs | FLITPSCweak | f | (L → V) × (L → List(FOW)) × (L → Nat) × (L → Set(T)) × (L → Set(T)) → FLITPSCGState |
| mkFLITPSCls | FLITPSCweak | f | T × L × V → FLITPSCLState |
| 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 | FLITPSCweak | f | FLITPSCGState × (T → FLITPSCLState) × (T → FLITPSCPC) → FLITPSCState |
| mkstate | FLIT | f | FLITGState × (T → FLITLState) × (T → FLITPC) → FLITState |
| n | FLIT-refines-FLITPSCweak | 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))) |
| ov | FLIT-refines-FLITPSCweak | v | V |
| p | FLIT-refines-FLITPSCweak | v | L → List(FOW) |
| pc | FLIT-refines-FLITPSCweak | v | FLITPC |
| pcf | FLIT-refines-FLITPSCweak | v | T → FLITPC |
| pcstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCPC |
| 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-refines-FLITPSCweak | v | L → V |
| pq | FLIT-refines-FLITPSCweak | v | L → List(FOW) |
| pre | FLITPSCweak | p | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction |
| pre | FLIT | p | FLITGState × FLITLState × FLITPC × FLITAction |
| propFO | FLIT | f | T × L → FLITAction |
| propFOs | abs-FLIT-FLITPSCweak | f | T × L × List(Bevent) → List(FOW) |
| propSF | FLIT | f | T → FLITAction |
| pwb | FLIT | f | T × L → FLITAction |
| pwbPSC | FLITPSCweak | f | T × L → FLITPSCAction |
| readFOsOk | FLIT-preds | p | (T → Type(List(Bevent))) × (L → Type(Set(T))) |
| ready | FLITPSCweak | c | FLITPSCPC |
| ready | FLIT | c | FLITPC |
| rely | FLITPSCweak-preds | p | T × List(FOW) × List(FOW) |
| rely | FLITPSCweak-preds | p | T × (L → Type(List(FOW))) × (L → Type(List(FOW))) |
| 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) |
| ren | FLIT-refines-FLITPSCweak | f | FLITAction × FLITPSCGState × (T → FLITPSCLState) → FLITPSCAction |
| reorder | abs-FLIT-FLITPSCweak | p | (L → Type(List(FOW))) × (L → Type(List(FOW))) × (T → Type(List(Bevent))) |
| reorder | abs-FLIT-FLITPSCweak | p | L × List(FOW) × List(FOW) × (T → Type(List(Bevent))) |
| retFLITPSCREAD | FLITPSCweak | f | T × V → FLITPSCAction |
| retFLITPSCWRITE | FLITPSCweak | f | T → FLITPSCAction |
| retFLITREAD | FLIT | f | T × V → FLITAction |
| retFLITWRITE | FLIT | f | T → FLITAction |
| rev | list-last | f | List('a) → List('a) |
| s | FLIT-refines-FLITPSCweak | v | FLITState |
| sfence | FLIT | f | T → FLITAction |
| sfencePSC | FLITPSCweak | f | T → FLITPSCAction |
| t | FLIT-refines-FLITPSCweak | v | T |
| v | FLIT-refines-FLITPSCweak | v | V |
| val | FLIT-refines-FLITPSCweak | v | V |
| writers | FLIT-refines-FLITPSCweak | v | L → Set(T) |
| 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))) |