| 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 |
| . .W? | FOW | p | FOW |
| . .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)) |
| . .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)) |
| . .gstate | FLITPSCweak | f | FLITPSCState → FLITPSCGState |
| . .gstate:= . | FLITPSCweak | f | FLITPSCState × FLITPSCGState → FLITPSCState |
| . .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) |
| . .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:= . | FLITPSCweak | f | FLITPSCLState × L → FLITPSCLState |
| . .last | list-last | pf | List('a) → 'a with λ x. x ≠ [] |
| . .lsf | FLITPSCweak | f | FLITPSCState → T → FLITPSCLState |
| . .lsf:= . | FLITPSCweak | f | FLITPSCState × (T → FLITPSCLState) → FLITPSCState |
| . .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) |
| . .p | FLITPSCweak | f | FLITPSCGState → L → List(FOW) |
| . .p:= . | FLITPSCweak | f | FLITPSCGState × (L → List(FOW)) → FLITPSCGState |
| . .pcf | FLITPSCweak | f | FLITPSCState → T → FLITPSCPC |
| . .pcf:= . | FLITPSCweak | f | FLITPSCState × (T → FLITPSCPC) → FLITPSCState |
| . .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) |
| . .sublist ( . ) | list-del | pf | List('a) × Nat × Nat → List('a) with λ x, n, m. n + m ≤ # x |
| . .t | FLITPSCweak | f | FLITPSCLState → 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:= . | FLITPSCweak | f | FLITPSCLState × T → FLITPSCLState |
| . .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)) |
| . .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:= . | FLITPSCweak | f | FLITPSCLState × V → FLITPSCLState |
| . .val | FOW | pf | FOW → V with λ fow. fow.W? |
| . .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) |
| . |W | FLITPSC-preds | f | List(FOW) → List(FOW) |
| . ∈ . | 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) |
| . ⊕ . | FLITPSC-preds | f | V × List(FOW) → V |
| . ⊕ . | FLITPSC-preds | f | (L → V) × (L → List(FOW)) → 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 |
| ∅ | set-basic | c | Set('a) |
| ∅ | memory | f | L → V |
| 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)) |
| FO | FOW | f | T → FOW |
| FOFollowsW | FLITPSC-preds | p | T × List(FOW) |
| FOW | FOW | s | |
| L | memory | s | |
| List | list-data | s | |
| Nat | nat-basic | s | |
| O | memory | c | V |
| 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 |
| R2 | FLITPSCweak | c | FLITPSCPC |
| R3 | FLITPSCweak | c | FLITPSCPC |
| R4 | FLITPSCweak | c | FLITPSCPC |
| Set | set-basic | s | |
| T | memory | s | |
| V | memory | s | |
| W | FOW | f | V × T → FOW |
| W1 | FLITPSCweak | c | FLITPSCPC |
| W2 | FLITPSCweak | c | FLITPSCPC |
| W3 | FLITPSCweak | c | FLITPSCPC |
| W4 | FLITPSCweak | c | FLITPSCPC |
| W5 | FLITPSCweak | c | FLITPSCPC |
| W6 | FLITPSCweak | c | FLITPSCPC |
| W7 | FLITPSCweak | c | FLITPSCPC |
| a | FLITPSCweak-proofs | v | FLITPSCAction |
| atomicW1 | FLITPSCweak | c | FLITPSCAction |
| atomicW5 | FLITPSCweak | c | FLITPSCAction |
| callPSCCOMPLETE | FLITPSCweak | f | T → FLITPSCAction |
| callPSCRUN | FLITPSCweak | f | T → FLITPSCAction |
| crashed | FLITPSCweak | c | FLITPSCPC |
| ctr | FLITPSCweak-proofs | v | L → Nat |
| ctrDecPSC | FLITPSCweak | f | T × L → FLITPSCAction |
| ctrIncPSC | FLITPSCweak | f | T × L → FLITPSCAction |
| 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) |
| doReadPSC | FLITPSCweak | f | T × L × V → FLITPSCAction |
| doWritePSC | FLITPSCweak | f | T × L × V → FLITPSCAction |
| dups | list-dup | p | List('a) |
| fillfirst | list-last | f | Nat × 'a × List('a) → List('a) |
| firstPersistW | FLITPSCweak-preds | f | List(FOW) → Nat |
| flitpscInit | FLITPSCweak | p | FLITPSCState |
| flitpscStep | FLITPSCweak | p | FLITPSCState × FLITPSCAction × FLITPSCState |
| fow | FLITPSCweak-proofs | v | FOW |
| fowl | FLITPSCweak-proofs | v | List(FOW) |
| frome | list-del | f | List('a) × 'a → List('a) |
| glb | FLITPSCweak-proofs | v | Nat |
| globalPSCCRASH | FLITPSCweak | c | FLITPSCAction |
| globalPSCPERSIST_FO | FLITPSCweak | f | L → FLITPSCAction |
| globalPSCPERSIST_W | FLITPSCweak | f | L → FLITPSCAction |
| gs | FLITPSCweak-proofs | v | FLITPSCGState |
| gstate | FLITPSCweak-proofs | v | FLITPSCGState |
| gstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCGState |
| idle | FLITPSCweak | c | FLITPSCPC |
| invFLITPSCREAD | FLITPSCweak | f | T × L → FLITPSCAction |
| invFLITPSCREADl | FLITPSCweak-proofs | v | L |
| invFLITPSCWRITE | FLITPSCweak | f | T × L × V → FLITPSCAction |
| invFLITPSCWRITEl | FLITPSCweak-proofs | v | L |
| invFLITPSCWRITEv | FLITPSCweak-proofs | v | V |
| invPSCPERSIST_FOl | FLITPSCweak-proofs | v | L |
| invPSCPERSIST_Wl | FLITPSCweak-proofs | v | L |
| isPersistFO | FLITPSCweak-preds | p | Nat × List(FOW) |
| l | FLITPSCweak-proofs | v | L |
| loc | FLITPSCweak-proofs | v | Nat |
| ls | FLITPSCweak-proofs | v | FLITPSCLState |
| lsf | FLITPSCweak-proofs | v | T → FLITPSCLState |
| lstep | FLITPSCweak | p | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction × FLITPSCGState × FLITPSCLState × FLITPSCPC |
| lstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCLState |
| mem | FLITPSCweak-proofs | 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 |
| mklist | list-last | f | 'a × Nat → List('a) |
| mkstate | FLITPSCweak | f | FLITPSCGState × (T → FLITPSCLState) × (T → FLITPSCPC) → FLITPSCState |
| n | FLITPSCweak-proofs | v | Nat |
| noPending | FLITPSC-preds | p | T × (L → Type(List(FOW))) |
| noPendingW | FLITPSC-preds | p | T × (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))) |
| p | FLITPSCweak-proofs | v | L → List(FOW) |
| pc | FLITPSCweak-proofs | v | FLITPSCPC |
| pcf | FLITPSCweak-proofs | v | T → FLITPSCPC |
| pcstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCPC |
| pendingOk | FLITPSC-preds | p | (L → Type(List(FOW))) |
| perm | list-perm | p | List('a) × List('a) |
| plin | FLITPSCweak-proofs | v | L → List(FOW) |
| pre | FLITPSCweak | p | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction |
| pwbPSC | FLITPSCweak | f | T × L → FLITPSCAction |
| readers | FLITPSCweak-proofs | v | L → Set(T) |
| ready | FLITPSCweak | c | FLITPSCPC |
| rely | FLITPSCweak-preds | p | T × List(FOW) × List(FOW) |
| rely | FLITPSCweak-preds | p | T × (L → Type(List(FOW))) × (L → Type(List(FOW))) |
| 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) |
| retFLITPSCREAD | FLITPSCweak | f | T × V → FLITPSCAction |
| retFLITPSCREADv | FLITPSCweak-proofs | v | V |
| retFLITPSCWRITE | FLITPSCweak | f | T → FLITPSCAction |
| rev | list-last | f | List('a) → List('a) |
| s | FLITPSCweak-proofs | v | FLITPSCState |
| sfencePSC | FLITPSCweak | f | T → FLITPSCAction |
| t | FLITPSCweak-proofs | v | T |
| tid | FLITPSCweak-proofs | v | T |
| ts | FLITPSCweak-proofs | v | Set(T) |
| v | FLITPSCweak-proofs | v | V |
| wl | FLITPSCweak-proofs | v | L |
| writers | FLITPSCweak-proofs | v | L → Set(T) |
| writersOk | FLITPSC-preds | p | (L → Type(List(FOW))) × (L → Type(Set(T))) |