| 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 |
| . .R? | RWevent | p | RWevent |
| . .W? | RWevent | p | RWevent |
| . .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 | PLIB | f | PLIBState → PLIBGState |
| . .gstate | FLITPSCweak | f | FLITPSCState → FLITPSCGState |
| . .gstate:= . | PLIB | f | PLIBState × PLIBGState → PLIBState |
| . .gstate:= . | FLITPSCweak | f | FLITPSCState × FLITPSCGState → FLITPSCState |
| . .h | PLIB | f | PLIBGState → List((RWevent, Bool)) |
| . .h:= . | PLIB | f | PLIBGState × List((RWevent, Bool)) → PLIBGState |
| . .head | list-data | pf | List('a) → 'a with λ x. x ≠ [] |
| . .il | PLIB | f | PLIBLState → L |
| . .il:= . | PLIB | f | PLIBLState × L → PLIBLState |
| . .indexOf ( . ) | list-del | f | List('a) × 'a → Nat |
| . .indexWhere ( . ) | forall-indexWhere | f | List('a) × ('a → Bool) → Nat |
| . .invAPersistl | PLIB | pf | PLIBAction → L with λ a. ∃ l. a = globalAPersist(l) |
| . .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) |
| . .iv | PLIB | f | PLIBLState → V |
| . .iv:= . | PLIB | f | PLIBLState × V → PLIBLState |
| . .l | RWevent | f | RWevent → L |
| . .l | FLITPSCweak | f | FLITPSCLState → L |
| . .l | PLIB | pf | PLIBAction → L with λ a. ∃ t, l. a = AInvRead(t, 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 ≠ [] |
| . .lastPersistedOrElse ( . ) | PLIB-preds | p | List((RWevent, Bool)) × L × Bool |
| . .loc | PLIB | pf | PLIBAction → L with λ a. ∃ t, l, v. a = AInvWrite(t, l, v) |
| . .lsf | PLIB | f | PLIBState → T → PLIBLState |
| . .lsf | FLITPSCweak | f | FLITPSCState → T → FLITPSCLState |
| . .lsf:= . | PLIB | f | PLIBState × (T → PLIBLState) → PLIBState |
| . .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) |
| . .ov | PLIB | f | PLIBLState → V |
| . .ov:= . | PLIB | f | PLIBLState × V → PLIBLState |
| . .p | FLITPSCweak | f | FLITPSCGState → L → List(FOW) |
| . .p:= . | FLITPSCweak | f | FLITPSCGState × (L → List(FOW)) → FLITPSCGState |
| . .pcf | PLIB | f | PLIBState → T → PLIBPC |
| . .pcf | FLITPSCweak | f | FLITPSCState → T → FLITPSCPC |
| . .pcf:= . | PLIB | f | PLIBState × (T → PLIBPC) → PLIBState |
| . .pcf:= . | FLITPSCweak | f | FLITPSCState × (T → FLITPSCPC) → FLITPSCState |
| . .pm | PLIB | f | PLIBGState → L → V |
| . .pm:= . | PLIB | f | PLIBGState × (L → V) → PLIBGState |
| . .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 | RWevent | f | RWevent → T |
| . .t | PLIB | f | PLIBLState → T |
| . .t | FLITPSCweak | f | FLITPSCLState → T |
| . .t | PLIB | pf | PLIBAction → T with λ a.
(∃ t. a = callTSync(t)) ∨ (∃ t. a = callARun(t)) ∨ (∃ t. a = ARetWrite(t))
∨ (∃ t, v. a = ARetRead(t, v)) ∨ (∃ t, l, v. a = AInvWrite(t, l, v))
∨ (∃ t, l. a = AInvRead(t, l)) ∨ (∃ t. a = ADoWrite(t)) ∨ (∃ t. a = ADoRead(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:= . | PLIB | f | PLIBLState × T → PLIBLState |
| . .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 | RWevent | f | RWevent → V |
| . .v | FLITPSCweak | f | FLITPSCLState → V |
| . .v | PLIB | pf | PLIBAction → V with λ a. ∃ t, v. a = ARetRead(t, 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 | PLIB | pf | PLIBAction → V with λ a. ∃ t, l, v. a = AInvWrite(t, l, v) |
| . .val | FOW | pf | FOW → V with λ fow. fow.W? |
| . .vm | PLIB | f | PLIBGState → L → V |
| . .vm:= . | PLIB | f | PLIBGState × (L → V) → PLIBGState |
| . .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) |
| . | . | PLIB-preds | f | List((RWevent, Bool)) × T → List((RWevent, Bool)) |
| . | . | PLIB-preds | f | List((RWevent, Bool)) × Bool → List((RWevent, Bool)) |
| . | . | PLIB-preds | f | List((RWevent, Bool)) × L → List((RWevent, Bool)) |
| . | . | FLITPSC-preds | f | List(FOW) × T → List(FOW) |
| . |FO | FLITPSC-preds | f | List(FOW) → List(FOW) |
| . |R | PLIB-preds | f | List((RWevent, Bool)) → List((RWevent, Bool)) |
| . |W | PLIB-preds | f | List((RWevent, Bool)) → List((RWevent, Bool)) |
| . |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) |
| . ⊑p . | PLIB-preds | p | List((RWevent, Bool)) × List((RWevent, Bool)) |
| . ⊒ . | list-last | p | List('a) × List('a) |
| . ⊒W . | FLITPSCweak-preds | p | List(FOW) × List(FOW) |
| . ⊕ . | PLIB-preds | f | (L → V) × List((RWevent, Bool)) → L → V |
| . ⊕ . | 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) |
| τ | PLIB | c | PLIBAction |
| τ | FLITPSCweak | c | FLITPSCAction |
| ∅ | set-basic | c | Set('a) |
| ∅ | memory | f | L → V |
| ACrash | PLIB | pr | (L → V) : (L → V) × List((RWevent, Bool)) × (T → PLIBPC) |
| ADOREAD | PLIB | pr | T × L × (L → V) : V × List((RWevent, Bool)) |
| ADoRead | PLIB | f | T → PLIBAction |
| ADoWrite | PLIB | f | T → PLIBAction |
| AInvRead | PLIB | f | T × L → PLIBAction |
| AInvWrite | PLIB | f | T × L × V → PLIBAction |
| APersist | PLIB | pr | L : (L → V) × List((RWevent, Bool)) |
| ARETREAD | PLIB | pr | V : : V |
| ARetRead | PLIB | f | T × V → PLIBAction |
| ARetWrite | PLIB | f | T → PLIBAction |
| ARun | PLIB | pr | : |
| DOWRITE | PLIB | pr | T × L × V : (L → V) × List((RWevent, Bool)) |
| 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 | |
| INVREAD | PLIB | pr | L : L |
| INVWRITE | PLIB | pr | L × V : L × V |
| L | memory | s | |
| List | list-data | s | |
| Nat | nat-basic | s | |
| O | memory | c | V |
| PLIBAction | PLIB | s | |
| PLIBGInv | PLIB | p | PLIBGState |
| PLIBGState | PLIB | s | |
| PLIBInv | PLIB | p | PLIBGState × (T → Type(PLIBLState)) × (T → Type(PLIBPC)) |
| PLIBLInv | PLIB | p | PLIBGState × PLIBLState × PLIBPC |
| PLIBLState | PLIB | s | |
| PLIBPC | PLIB | s | |
| PLIBRely | PLIB | p | PLIBGState × T × PLIBGState |
| PLIBState | PLIB | s | |
| 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 | : |
| R | RWevent | f | T × L × V → RWevent |
| R1 | FLITPSCweak | c | FLITPSCPC |
| R2 | FLITPSCweak | c | FLITPSCPC |
| R3 | FLITPSCweak | c | FLITPSCPC |
| R4 | FLITPSCweak | c | FLITPSCPC |
| RETWRITE | PLIB | pr | : |
| RWevent | RWevent | s | |
| Set | set-basic | s | |
| T | memory | s | |
| TSync | PLIB | pr | T × List((RWevent, Bool)) : |
| V | memory | s | |
| W | RWevent | f | T × L × V → RWevent |
| 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-refines-PLIB | v | FLITPSCAction |
| aa | FLITPSCweak-refines-PLIB | v | PLIBAction |
| abs | abs-FLITPSCweak-PLIB | p | List((RWevent, Bool)) × (L → Type(Set(T))) × (L → Type(List(FOW))) |
| abs | FLITPSCweak-refines-PLIB | p | FLITPSCState × PLIBState |
| absloc | abs-FLITPSCweak-PLIB | p | List(RWevent) × Set(T) × List(FOW) |
| ags | FLITPSCweak-refines-PLIB | v | PLIBGState |
| allReadsOK | PLIB-preds | p | List((RWevent, Bool)) |
| allReadsOKInd | PLIB-preds | p | (L → Type(V)) × (L → Type(Bool)) × List((RWevent, Bool)) |
| allWritesOK | PLIB-preds | p | List((RWevent, Bool)) |
| allWritesOKInd | PLIB-preds | p | (T → Type(Bool)) × (L → Type(Bool)) × List((RWevent, Bool)) |
| als | FLITPSCweak-refines-PLIB | v | PLIBLState |
| alsf | FLITPSCweak-refines-PLIB | v | T → PLIBLState |
| apc | FLITPSCweak-refines-PLIB | v | PLIBPC |
| apcf | FLITPSCweak-refines-PLIB | v | T → PLIBPC |
| as | FLITPSCweak-refines-PLIB | v | PLIBState |
| atomicW1 | FLITPSCweak | c | FLITPSCAction |
| atomicW5 | FLITPSCweak | c | FLITPSCAction |
| b | FLITPSCweak-refines-PLIB | v | Bool |
| callARun | PLIB | f | T → PLIBAction |
| callPSCCOMPLETE | FLITPSCweak | f | T → FLITPSCAction |
| callPSCRUN | FLITPSCweak | f | T → FLITPSCAction |
| callTSync | PLIB | f | T → PLIBAction |
| crashed | PLIB | c | PLIBPC |
| crashed | FLITPSCweak | c | FLITPSCPC |
| ctr | FLITPSCweak-refines-PLIB | 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) |
| e | FLITPSCweak-refines-PLIB | v | RWevent |
| events | PLIB-preds | f | List((RWevent, Bool)) → List(RWevent) |
| fillfirst | list-last | f | Nat × 'a × List('a) → List('a) |
| firstPersistW | FLITPSCweak-preds | f | List(FOW) → Nat |
| firstVolWrite | PLIB-preds | f | L × List((RWevent, Bool)) → Nat |
| flitpscInit | FLITPSCweak | p | FLITPSCState |
| flitpscStep | FLITPSCweak | p | FLITPSCState × FLITPSCAction × FLITPSCState |
| fow | FLITPSCweak-refines-PLIB | v | FOW |
| fowl | FLITPSCweak-refines-PLIB | v | List(FOW) |
| frome | list-del | f | List('a) × 'a → List('a) |
| gabs | FLITPSCweak-refines-PLIB | p | FLITPSCGState × (T → Type(FLITPSCLState)) × (T → Type(FLITPSCPC)) × PLIBGState × (T → Type(PLIBLState)) × (T → Type(PLIBPC)) |
| globalACrash | PLIB | c | PLIBAction |
| globalAPersist | PLIB | f | L → PLIBAction |
| globalPSCCRASH | FLITPSCweak | c | FLITPSCAction |
| globalPSCPERSIST_FO | FLITPSCweak | f | L → FLITPSCAction |
| globalPSCPERSIST_W | FLITPSCweak | f | L → FLITPSCAction |
| gs | FLITPSCweak-refines-PLIB | v | FLITPSCGState |
| gstepf | PLIB | f | PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBGState |
| gstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCGState |
| h | FLITPSCweak-refines-PLIB | v | List((RWevent, Bool)) |
| idle | PLIB | c | PLIBPC |
| idle | FLITPSCweak | c | FLITPSCPC |
| il | FLITPSCweak-refines-PLIB | v | L |
| invFLITPSCREAD | FLITPSCweak | f | T × L → FLITPSCAction |
| invFLITPSCWRITE | FLITPSCweak | f | T × L × V → FLITPSCAction |
| invRead | PLIB | c | PLIBPC |
| invWrite | PLIB | c | PLIBPC |
| isPersistFO | FLITPSCweak-preds | p | Nat × List(FOW) |
| iv | FLITPSCweak-refines-PLIB | v | V |
| l | FLITPSCweak-refines-PLIB | v | L |
| labs | FLITPSCweak-refines-PLIB | p | FLITPSCGState × FLITPSCLState × FLITPSCPC × PLIBGState × PLIBLState × PLIBPC |
| ls | FLITPSCweak-refines-PLIB | v | FLITPSCLState |
| lsf | FLITPSCweak-refines-PLIB | v | T → FLITPSCLState |
| lstep | PLIB | p | PLIBGState × PLIBLState × PLIBPC × PLIBAction × PLIBGState × PLIBLState × PLIBPC |
| lstep | FLITPSCweak | p | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction × FLITPSCGState × FLITPSCLState × FLITPSCPC |
| lstepf | PLIB | f | PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBLState |
| lstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCLState |
| mem | FLITPSCweak-refines-PLIB | 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 |
| mkPLIBgs | PLIB | f | (L → V) × (L → V) × List((RWevent, Bool)) → PLIBGState |
| mkPLIBls | PLIB | f | T × L × V × V → PLIBLState |
| mklist | list-last | f | 'a × Nat → List('a) |
| mkstate | PLIB | f | PLIBGState × (T → PLIBLState) × (T → PLIBPC) → PLIBState |
| mkstate | FLITPSCweak | f | FLITPSCGState × (T → FLITPSCLState) × (T → FLITPSCPC) → FLITPSCState |
| 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))) |
| ov | FLITPSCweak-refines-PLIB | v | V |
| p | FLITPSCweak-refines-PLIB | v | L → List(FOW) |
| pc | FLITPSCweak-refines-PLIB | v | FLITPSCPC |
| pcf | FLITPSCweak-refines-PLIB | v | T → FLITPSCPC |
| pcstepf | PLIB | f | PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBPC |
| pcstepf | FLITPSCweak | f | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCPC |
| pendingOk | FLITPSC-preds | p | (L → Type(List(FOW))) |
| perm | list-perm | p | List('a) × List('a) |
| persistDependentReads | PLIB-preds | f | L × List((RWevent, Bool)) → List((RWevent, Bool)) |
| plibInit | PLIB | p | PLIBState |
| plibStep | PLIB | p | PLIBState × PLIBAction × PLIBState |
| pre | PLIB | p | PLIBGState × PLIBLState × PLIBPC × PLIBAction |
| pre | FLITPSCweak | p | FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction |
| pwbPSC | FLITPSCweak | f | T × L → FLITPSCAction |
| ready | PLIB | c | PLIBPC |
| ready | FLITPSCweak | c | FLITPSCPC |
| rely | PLIB-preds | p | T × List((RWevent, Bool)) × List((RWevent, Bool)) |
| 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) |
| ren | FLITPSCweak-refines-PLIB | f | FLITPSCAction × PLIBGState × (T → PLIBLState) → PLIBAction |
| resRead | PLIB | c | PLIBPC |
| resWrite | PLIB | c | PLIBPC |
| retFLITPSCREAD | FLITPSCweak | f | T × V → FLITPSCAction |
| retFLITPSCWRITE | FLITPSCweak | f | T → FLITPSCAction |
| rev | list-last | f | List('a) → List('a) |
| s | FLITPSCweak-refines-PLIB | v | FLITPSCState |
| sfencePSC | FLITPSCweak | f | T → FLITPSCAction |
| t | FLITPSCweak-refines-PLIB | v | T |
| v | FLITPSCweak-refines-PLIB | v | V |
| vpe | FLITPSCweak-refines-PLIB | v | (RWevent, Bool) |
| writers | FLITPSCweak-refines-PLIB | v | L → Set(T) |
| writersOk | FLITPSC-preds | p | (L → Type(List(FOW))) × (L → Type(Set(T))) |