| symbol | specification | entry |
|---|
| # | list-data | function,
List('a) → Nat |
| # | set-basic | function,
Set('a) → Nat |
| #oc | list-perm | function,
'a × List('a) → Nat |
| ' | list | function,
'a → List('a) |
| + | list | function,
List('a) × 'a → List('a) |
| + | list | function,
List('a) × List('a) → List('a) |
| + | list-data | function,
'a × List('a) → List('a) |
| + | nat-basic | function,
Nat × Nat → Nat |
| ++ | list-dup | function,
List('a) × 'a → List('a) |
| ++ | set-basic | function,
Set('a) × 'a → Set('a) |
| +1 | nat-basic | function,
Nat → Nat |
| +2 | list | function,
'a × 'a → List('a) |
| - | nat | partial function,
Nat × Nat → Nat |
| -- | set-union | function,
Set('a) × 'a → Set('a) |
| -1 | nat-basic | partial function,
Nat → Nat |
| -1l | list-del | function,
List('a) × 'a → List('a) |
| -l | list-del | function,
List('a) × 'a → List('a) |
| -p | list-del | function,
List('a) × Nat → List('a) |
| .FO? | Bevent | predicate,
Bevent |
| .FO? | FOW | predicate,
FOW |
| .FOWs | FLIT-preds | function,
List(Bevent) × T × L → List(FOW) |
| .FOs? | FLIT-preds | predicate,
T → List(Bevent) |
| .R? | RWevent | predicate,
RWevent |
| .W? | RWevent | predicate,
RWevent |
| .W? | Bevent | predicate,
Bevent |
| .W? | FOW | predicate,
FOW |
| .bq | FLIT | function,
FLITGState → T → List(Bevent) |
| .bq:= | FLIT | function,
FLITGState × T → List(Bevent) → FLITGState |
| .butlast | list-last | partial function,
List('a) → List('a) |
| .count | filter-count | partial function,
List('a) × Nat × Nat × 'a → Bool → Nat |
| .count | filter-count | function,
List('a) × 'a → Bool → Nat |
| .ctr | FLITPSCweak | function,
FLITPSCGState → L → Nat |
| .ctr:= | FLITPSCweak | function,
FLITPSCGState × L → Nat → FLITPSCGState |
| .distinct | list-dup | function,
List('a) → List('a) |
| .drop | list-del | partial function,
List('a) × Nat → List('a) |
| .dropRight | list-last | partial function,
List('a) × Nat → List('a) |
| .exists | forall-indexWhere | predicate,
List('a) × 'a → Bool |
| .fctr | FLIT | partial function,
FLITAction → L → Nat |
| .fctr | FLIT | function,
FLITGState → L → Nat |
| .fctr0 | FLIT | partial function,
FLITAction → L → Nat |
| .fctr:= | FLIT | function,
FLITGState × L → Nat → FLITGState |
| .filter | filter-count | function,
List('a) × 'a → Bool → List('a) |
| .filter | set-union | function,
Set('a) × 'a → Bool → Set('a) |
| .foldLeft | list | function,
List('a) × 'b × 'b × 'a → 'b → 'b |
| .forall | forall-indexWhere | predicate,
List('a) × 'a → Bool |
| .freaders | FLIT | function,
FLITGState → L → Set(T) |
| .freaders:= | FLIT | function,
FLITGState × L → Set(T) → FLITGState |
| .fwriters | FLIT | partial function,
FLITAction → L → Set(T) |
| .fwriters | FLIT | function,
FLITGState → L → Set(T) |
| .fwriters0 | FLIT | partial function,
FLITAction → L → Set(T) |
| .fwriters:= | FLIT | function,
FLITGState × L → Set(T) → FLITGState |
| .gstate | FLIT | function,
FLITState → FLITGState |
| .gstate | FLITPSCweak | function,
FLITPSCState → FLITPSCGState |
| .gstate | PLIB | function,
PLIBState → PLIBGState |
| .gstate:= | FLIT | function,
FLITState × FLITGState → FLITState |
| .gstate:= | FLITPSCweak | function,
FLITPSCState × FLITPSCGState → FLITPSCState |
| .gstate:= | PLIB | function,
PLIBState × PLIBGState → PLIBState |
| .h | PLIB | function,
PLIBGState → List((RWevent, Bool)) |
| .h:= | PLIB | function,
PLIBGState × List((RWevent, Bool)) → PLIBGState |
| .head | list-data | partial function,
List('a) → 'a |
| .il | PLIB | function,
PLIBLState → L |
| .il:= | PLIB | function,
PLIBLState × L → PLIBLState |
| .indexOf | list-del | function,
List('a) × 'a → Nat |
| .indexWhere | forall-indexWhere | function,
List('a) × 'a → Bool → Nat |
| .invAPersistl | PLIB | partial function,
PLIBAction → L |
| .invFLITPSCREADl | FLITPSCweak | partial function,
FLITPSCAction → L |
| .invFLITPSCWRITEl | FLITPSCweak | partial function,
FLITPSCAction → L |
| .invFLITPSCWRITEv | FLITPSCweak | partial function,
FLITPSCAction → V |
| .invFLITREADloc | FLIT | partial function,
FLITAction → L |
| .invFLITWRITEloc | FLIT | partial function,
FLITAction → L |
| .invFLITWRITEval | FLIT | partial function,
FLITAction → V |
| .invPERSIST_FOloc | FLIT | partial function,
FLITAction → L |
| .invPERSIST_Wloc | FLIT | partial function,
FLITAction → L |
| .invPSCPERSIST_FOl | FLITPSCweak | partial function,
FLITPSCAction → L |
| .invPSCPERSIST_Wl | FLITPSCweak | partial function,
FLITPSCAction → L |
| .iv | PLIB | function,
PLIBLState → V |
| .iv:= | PLIB | function,
PLIBLState × V → PLIBLState |
| .l | RWevent | function,
RWevent → L |
| .l | FLIT | partial function,
FLITAction → L |
| .l | FLITPSCweak | partial function,
FLITPSCAction → L |
| .l | FLITPSCweak | function,
FLITPSCLState → L |
| .l | PLIB | partial function,
PLIBAction → L |
| .l | Bevent | partial function,
Bevent → L |
| .l:= | FLITPSCweak | function,
FLITPSCLState × L → FLITPSCLState |
| .last | list-last | partial function,
List('a) → 'a |
| .lastPersistedOrElse | PLIB-preds | predicate,
List((RWevent, Bool)) × L × Bool |
| .loc | FLIT | partial function,
FLITAction → L |
| .loc | FLIT | function,
FLITLState → L |
| .loc | PLIB | partial function,
PLIBAction → L |
| .loc:= | FLIT | function,
FLITLState × L → FLITLState |
| .lsf | FLIT | function,
FLITState → T → FLITLState |
| .lsf | FLITPSCweak | function,
FLITPSCState → T → FLITPSCLState |
| .lsf | PLIB | function,
PLIBState → T → PLIBLState |
| .lsf:= | FLIT | function,
FLITState × T → FLITLState → FLITState |
| .lsf:= | FLITPSCweak | function,
FLITPSCState × T → FLITPSCLState → FLITPSCState |
| .lsf:= | PLIB | function,
PLIBState × T → PLIBLState → PLIBState |
| .map | list | function,
List('a) × 'a → 'b → List('b) |
| .map | set-union | function,
Set('a) × 'a → 'b → Set('b) |
| .mem | FLITPSCweak | function,
FLITPSCGState → L → V |
| .mem:= | FLITPSCweak | function,
FLITPSCGState × L → V → FLITPSCGState |
| .n | FLIT | partial function,
FLITAction → Nat |
| .n | FLITPSCweak | partial function,
FLITPSCAction → Nat |
| .ov | PLIB | function,
PLIBLState → V |
| .ov:= | PLIB | function,
PLIBLState × V → PLIBLState |
| .p | FLITPSCweak | function,
FLITPSCGState → L → List(FOW) |
| .p:= | FLITPSCweak | function,
FLITPSCGState × L → List(FOW) → FLITPSCGState |
| .pcf | FLIT | function,
FLITState → T → FLITPC |
| .pcf | FLITPSCweak | function,
FLITPSCState → T → FLITPSCPC |
| .pcf | PLIB | function,
PLIBState → T → PLIBPC |
| .pcf:= | FLIT | function,
FLITState × T → FLITPC → FLITState |
| .pcf:= | FLITPSCweak | function,
FLITPSCState × T → FLITPSCPC → FLITPSCState |
| .pcf:= | PLIB | function,
PLIBState × T → PLIBPC → PLIBState |
| .pm | PLIB | function,
PLIBGState → L → V |
| .pm:= | PLIB | function,
PLIBGState × L → V → PLIBGState |
| .pmem | FLIT | function,
FLITGState → L → V |
| .pmem:= | FLIT | function,
FLITGState × L → V → FLITGState |
| .pq | FLIT | function,
FLITGState → L → List(FOW) |
| .pq:= | FLIT | function,
FLITGState × L → List(FOW) → FLITGState |
| .readers | FLITPSCweak | function,
FLITPSCGState → L → Set(T) |
| .readers:= | FLITPSCweak | function,
FLITPSCGState × L → Set(T) → FLITPSCGState |
| .retFLITPSCREADv | FLITPSCweak | partial function,
FLITPSCAction → V |
| .retFLITREADval | FLIT | partial function,
FLITAction → V |
| .rfo | FLIT | function,
FLITGState → T → List(Bevent) |
| .rfo:= | FLIT | function,
FLITGState × T → List(Bevent) → FLITGState |
| .sublist | list-del | partial function,
List('a) × Nat × Nat → List('a) |
| .t | RWevent | function,
RWevent → T |
| .t | FLIT | partial function,
FLITAction → T |
| .t | FLIT | function,
FLITLState → T |
| .t | FLITPSCweak | partial function,
FLITPSCAction → T |
| .t | FLITPSCweak | function,
FLITPSCLState → T |
| .t | PLIB | partial function,
PLIBAction → T |
| .t | PLIB | function,
PLIBLState → T |
| .t:= | FLIT | function,
FLITLState × T → FLITLState |
| .t:= | FLITPSCweak | function,
FLITPSCLState × T → FLITPSCLState |
| .t:= | PLIB | function,
PLIBLState × T → PLIBLState |
| .tail | list-data | partial function,
List('a) → List('a) |
| .take | list-del | partial function,
List('a) × Nat → List('a) |
| .takeRight | list-del | partial function,
List('a) × Nat → List('a) |
| .tid | FLIT | partial function,
FLITAction → T |
| .tid | FLITPSCweak | partial function,
FLITPSCAction → T |
| .tid | FOW | function,
FOW → T |
| .v | RWevent | function,
RWevent → V |
| .v | FLIT | partial function,
FLITAction → V |
| .v | FLITPSCweak | partial function,
FLITPSCAction → V |
| .v | FLITPSCweak | function,
FLITPSCLState → V |
| .v | PLIB | partial function,
PLIBAction → V |
| .v | Bevent | partial function,
Bevent → V |
| .v:= | FLITPSCweak | function,
FLITPSCLState × V → FLITPSCLState |
| .val | FLIT | function,
FLITLState → V |
| .val | PLIB | partial function,
PLIBAction → V |
| .val | FOW | partial function,
FOW → V |
| .val:= | FLIT | function,
FLITLState × V → FLITLState |
| .vm | PLIB | function,
PLIBGState → L → V |
| .vm:= | PLIB | function,
PLIBGState × L → V → PLIBGState |
| .writers | FLITPSCweak | function,
FLITPSCGState → L → Set(T) |
| .writers:= | FLITPSCweak | function,
FLITPSCGState × L → Set(T) → FLITPSCGState |
| < | list-data | predicate,
List('a) × List('a) |
| < | nat-basic | predicate,
Nat × Nat |
| > | nat | predicate,
Nat × Nat |
| ACrash | PLIB | procedure,
(L → V) : (L → V) × List((RWevent, Bool)) × (T → PLIBPC) |
| ADOREAD | PLIB | procedure,
T × L × (L → V) : V × List((RWevent, Bool)) |
| ADoRead | PLIB | function,
T → PLIBAction |
| ADoWrite | PLIB | function,
T → PLIBAction |
| AInvRead | PLIB | function,
T × L → PLIBAction |
| AInvWrite | PLIB | function,
T × L × V → PLIBAction |
| APersist | PLIB | procedure,
L : (L → V) × List((RWevent, Bool)) |
| ARETREAD | PLIB | procedure,
V : : V |
| ARetRead | PLIB | function,
T × V → PLIBAction |
| ARetWrite | PLIB | function,
T → PLIBAction |
| ARun | PLIB | procedure,
: |
| Bevent | Bevent | sort,
|
| CRASH | FLIT | procedure,
: (L → List(FOW)) × (L → Nat) × (T → List(Bevent)) × (L → Set(T)) × (L → Set(T)) ×
(T → List(Bevent)) × (T → FLITPC) |
| DOWRITE | PLIB | procedure,
T × L × V : (L → V) × List((RWevent, Bool)) |
| FLITAction | FLIT | sort,
|
| FLITCOMPLETE | FLIT | procedure,
T × (L → List(FOW)) × (T → List(Bevent)) : |
| FLITGInv | FLIT | predicate,
FLITGState |
| FLITGState | FLIT | sort,
|
| FLITInv | FLIT | predicate,
FLITGState × T → FLITLState × T → FLITPC |
| FLITLInv | FLIT | predicate,
FLITGState × FLITLState × FLITPC |
| FLITLState | FLIT | sort,
|
| FLITPC | FLIT | sort,
|
| FLITPSCAction | FLITPSCweak | sort,
|
| FLITPSCGInv | FLITPSCweak | predicate,
FLITPSCGState |
| FLITPSCGState | FLITPSCweak | sort,
|
| FLITPSCInv | FLITPSCweak | predicate,
FLITPSCGState × T → FLITPSCLState × T → FLITPSCPC |
| FLITPSCLInv | FLITPSCweak | predicate,
FLITPSCGState × FLITPSCLState × FLITPSCPC |
| FLITPSCLState | FLITPSCweak | sort,
|
| FLITPSCPC | FLITPSCweak | sort,
|
| FLITPSCREAD | FLITPSCweak | procedure,
L × T × (L → V) × (L → Nat) : (L → List(FOW)) × (L → Set(T)) : V |
| FLITPSCRely | FLITPSCweak | predicate,
FLITPSCGState × T × FLITPSCGState |
| FLITPSCState | FLITPSCweak | sort,
|
| FLITPSCWRITE | FLITPSCweak | procedure,
L × V × T : (L → List(FOW)) × (L → Nat) × (L → Set(T)) |
| FLITREAD | FLIT | procedure,
L × T × (L → V) × (L → List(FOW)) × (L → Nat)
: (T → List(Bevent)) × (L → Set(T)) × (T → List(Bevent))
: V |
| FLITRely | FLIT | predicate,
FLITGState × T × FLITGState |
| FLITState | FLIT | sort,
|
| FLITWRITE | FLIT | procedure,
L × V × T × (L → List(FOW)) : (L → Nat) × (T → List(Bevent)) × (L → Set(T)) |
| FO | Bevent | function,
L → Bevent |
| FO | FOW | function,
T → FOW |
| FOFollowsW | FLITPSC-preds | predicate,
T × List(FOW) |
| FOFollowsW | FLIT-preds | predicate,
T × List(Bevent) × List(FOW) × L |
| FOFollowsW | FLIT-preds | predicate,
T × List(Bevent) × L → List(FOW) × L |
| FOW | FOW | sort,
|
| INVREAD | PLIB | procedure,
L : L |
| INVWRITE | PLIB | procedure,
L × V : L × V |
| L | memory | sort,
|
| List | list-data | sort,
|
| Nat | nat-basic | sort,
|
| O | memory | constant,
V |
| PERSIST_FO | FLIT | procedure,
L : (L → List(FOW)) |
| PERSIST_W | FLIT | procedure,
L : (L → V) × (L → List(FOW)) |
| PLIBAction | PLIB | sort,
|
| PLIBGInv | PLIB | predicate,
PLIBGState |
| PLIBGState | PLIB | sort,
|
| PLIBInv | PLIB | predicate,
PLIBGState × T → PLIBLState × T → PLIBPC |
| PLIBLInv | PLIB | predicate,
PLIBGState × PLIBLState × PLIBPC |
| PLIBLState | PLIB | sort,
|
| PLIBPC | PLIB | sort,
|
| PLIBRely | PLIB | predicate,
PLIBGState × T × PLIBGState |
| PLIBState | PLIB | sort,
|
| PROP_FO | FLIT | procedure,
T × L × (L → Set(T)) : (L → List(FOW)) × (T → List(Bevent)) × (T → List(Bevent)) |
| PROP_SF | FLIT | procedure,
T × (L → List(FOW)) : (T → List(Bevent)) |
| PROP_W | FLIT | procedure,
T : (L → List(FOW)) × (T → List(Bevent)) |
| PSCCOMPLETE | FLITPSCweak | procedure,
T × (L → List(FOW)) : |
| PSCCRASH | FLITPSCweak | procedure,
: (L → List(FOW)) × (L → Nat) × (L → Set(T)) × (L → Set(T)) × (T → FLITPSCPC) |
| PSCPERSIST_FO | FLITPSCweak | procedure,
L : (L → List(FOW)) |
| PSCPERSIST_W | FLITPSCweak | procedure,
L : (L → V) × (L → List(FOW)) |
| PSCRUN | FLITPSCweak | procedure,
: |
| R | RWevent | function,
T × L × V → RWevent |
| R1 | FLIT | constant,
FLITPC |
| R1 | FLITPSCweak | constant,
FLITPSCPC |
| R2 | FLIT | constant,
FLITPC |
| R2 | FLITPSCweak | constant,
FLITPSCPC |
| R3 | FLIT | constant,
FLITPC |
| R3 | FLITPSCweak | constant,
FLITPSCPC |
| R4 | FLIT | constant,
FLITPC |
| R4 | FLITPSCweak | constant,
FLITPSCPC |
| RETWRITE | PLIB | procedure,
: |
| RUN | FLIT | procedure,
: |
| RWevent | RWevent | sort,
|
| SF | Bevent | constant,
Bevent |
| SFTrailing | FLIT-preds | predicate,
T → List(Bevent) |
| Set | set-basic | sort,
|
| T | memory | sort,
|
| TSync | PLIB | procedure,
T × List((RWevent, Bool)) : |
| V | memory | sort,
|
| W | RWevent | function,
T × L × V → RWevent |
| W | Bevent | function,
L × V → Bevent |
| W | FOW | function,
V × T → FOW |
| W1 | FLIT | constant,
FLITPC |
| W1 | FLITPSCweak | constant,
FLITPSCPC |
| W2 | FLIT | constant,
FLITPC |
| W2 | FLITPSCweak | constant,
FLITPSCPC |
| W3 | FLIT | constant,
FLITPC |
| W3 | FLITPSCweak | constant,
FLITPSCPC |
| W4 | FLIT | constant,
FLITPC |
| W4 | FLITPSCweak | constant,
FLITPSCPC |
| W5 | FLIT | constant,
FLITPC |
| W5 | FLITPSCweak | constant,
FLITPSCPC |
| W6 | FLIT | constant,
FLITPC |
| W6 | FLITPSCweak | constant,
FLITPSCPC |
| W7 | FLIT | constant,
FLITPC |
| W7 | FLITPSCweak | constant,
FLITPSCPC |
| [] | list-data | constant,
List('a) |
| \ | set-union | function,
Set('a) × Set('a) → Set('a) |
| \ | list-set | function,
List('a) × List('a) → List('a) |
| ] | list-getput | partial function,
List('a) × Nat × 'a → List('a) |
| ] | list-getput | partial function,
List('a) × Nat → 'a |
| a | list-getput | variable,
'a |
| a | list-del | variable,
'a |
| a | FLIT | variable,
FLITAction |
| a | list-perm | variable,
'a |
| a | filter-count | variable,
'a |
| a | FLITPSCweak | variable,
FLITPSCAction |
| a | FLITPSCweak-proofs | variable,
FLITPSCAction |
| a | forall-indexWhere | variable,
'a |
| a | list-dup | variable,
'a |
| a | FLITPSCweak-refines-PLIB | variable,
FLITPSCAction |
| a | list | variable,
'a |
| a | PLIB | variable,
PLIBAction |
| a | list-data | variable,
'a |
| a | list-last | variable,
'a |
| a | set-basic | variable,
'a |
| a | FLIT-refines-FLITPSCweak | variable,
FLITAction |
| a | set-union | variable,
'a |
| a | PLIB-proofs | variable,
PLIBAction |
| a | list-set | variable,
'a |
| a | FLIT-proofs | variable,
FLITAction |
| aa | FLITPSCweak-refines-PLIB | variable,
PLIBAction |
| aa | FLIT-refines-FLITPSCweak | variable,
FLITPSCAction |
| abs | FLITPSCweak-refines-PLIB | predicate,
FLITPSCState × PLIBState |
| abs | abs-FLITPSCweak-PLIB | predicate,
List((RWevent, Bool)) × L → Set(T) × L → List(FOW) |
| abs | FLIT-refines-FLITPSCweak | predicate,
FLITState × FLITPSCState |
| absloc | abs-FLITPSCweak-PLIB | predicate,
List(RWevent) × Set(T) × List(FOW) |
| ags | FLITPSCweak-refines-PLIB | variable,
PLIBGState |
| ags | abs-FLITPSCweak-PLIB | variable,
PLIBGState |
| ags | FLIT-refines-FLITPSCweak | variable,
FLITPSCGState |
| allReadsOK | PLIB-preds | predicate,
List((RWevent, Bool)) |
| allReadsOKInd | PLIB-preds | predicate,
L → V × L → Bool × List((RWevent, Bool)) |
| allWritesOK | PLIB-preds | predicate,
List((RWevent, Bool)) |
| allWritesOKInd | PLIB-preds | predicate,
T → Bool × L → Bool × List((RWevent, Bool)) |
| als | FLITPSCweak-refines-PLIB | variable,
PLIBLState |
| als | FLIT-refines-FLITPSCweak | variable,
FLITPSCLState |
| alsf | FLITPSCweak-refines-PLIB | variable,
T → PLIBLState |
| alsf | FLIT-refines-FLITPSCweak | variable,
T → FLITPSCLState |
| apc | FLITPSCweak-refines-PLIB | variable,
PLIBPC |
| apc | FLIT-refines-FLITPSCweak | variable,
FLITPSCPC |
| apcf | FLITPSCweak-refines-PLIB | variable,
T → PLIBPC |
| apcf | FLIT-refines-FLITPSCweak | variable,
T → FLITPSCPC |
| as | FLITPSCweak-refines-PLIB | variable,
PLIBState |
| as | FLIT-refines-FLITPSCweak | variable,
FLITPSCState |
| atomicW1 | FLITPSCweak | constant,
FLITPSCAction |
| atomicW2 | FLIT | function,
L → Nat × L × L → Set(T) × T × L → Nat × L → Set(T) → FLITAction |
| atomicW5 | FLITPSCweak | constant,
FLITPSCAction |
| atomicW6 | FLIT | function,
L → Nat × L × L → Set(T) × T × L → Nat × L → Set(T) → FLITAction |
| b | list-getput | variable,
'a |
| b | list-del | variable,
'a |
| b | list-perm | variable,
'a |
| b | filter-count | variable,
'b |
| b | PLIB-preds | variable,
Bool |
| b | list-dup | variable,
'a |
| b | FLITPSCweak-refines-PLIB | variable,
Bool |
| b | abs-FLITPSCweak-PLIB | variable,
Bool |
| b | list | variable,
'b |
| b | PLIB | variable,
Bool |
| b | list-last | variable,
'a |
| b | FLIT-refines-FLITPSCweak | variable,
Bool |
| b | set-union | variable,
'b |
| b | PLIB-proofs | variable,
Bool |
| b | list-set | variable,
'a |
| be | abs-FLIT-FLITPSCweak | variable,
Bevent |
| be | FLIT | variable,
Bevent |
| be | Bevent | variable,
Bevent |
| be | FLIT-preds | variable,
Bevent |
| be | FLIT-proofs | variable,
Bevent |
| bel | abs-FLIT-FLITPSCweak | variable,
List(Bevent) |
| bel | FLIT | variable,
List(Bevent) |
| bel | FLIT-refines-FLITPSCweak | variable,
List(Bevent) |
| bel | FLIT-preds | variable,
List(Bevent) |
| bel | FLIT-proofs | variable,
List(Bevent) |
| bq | abs-FLIT-FLITPSCweak | variable,
T → List(Bevent) |
| bq | FLIT | variable,
T → List(Bevent) |
| bq | FLIT-refines-FLITPSCweak | variable,
T → List(Bevent) |
| bq | FLIT-preds | variable,
T → List(Bevent) |
| bq | FLIT-proofs | variable,
T → List(Bevent) |
| bv | abs-FLIT-FLITPSCweak | variable,
Bool |
| bv | FLIT | variable,
Bool |
| bv | FLIT-proofs | variable,
Bool |
| c | list-getput | variable,
'a |
| c | list-perm | variable,
'a |
| c | list-dup | variable,
'a |
| c | list-last | variable,
'a |
| c | list-set | variable,
'a |
| callARun | PLIB | function,
T → PLIBAction |
| callFLITCOMPLETE | FLIT | function,
T → FLITAction |
| callPSCCOMPLETE | FLITPSCweak | function,
T → FLITPSCAction |
| callPSCRUN | FLITPSCweak | function,
T → FLITPSCAction |
| callRUN | FLIT | function,
T → FLITAction |
| callTSync | PLIB | function,
T → PLIBAction |
| crashed | FLIT | constant,
FLITPC |
| crashed | FLITPSCweak | constant,
FLITPSCPC |
| crashed | PLIB | constant,
PLIBPC |
| ctr | FLITPSCweak | variable,
L → Nat |
| ctr | FLITPSCweak-proofs | variable,
L → Nat |
| ctr | FLITPSCweak-refines-PLIB | variable,
L → Nat |
| ctr | abs-FLITPSCweak-PLIB | variable,
L → Nat |
| ctr | FLITPSCweak-preds | variable,
L → Nat |
| ctr | FLIT-refines-FLITPSCweak | variable,
L → Nat |
| ctr | FLITPSC-preds | variable,
L → Nat |
| ctrDec | FLIT | function,
T × L → FLITAction |
| ctrDecPSC | FLITPSCweak | function,
T × L → FLITPSCAction |
| ctrInc | FLIT | function,
T × L → FLITAction |
| ctrIncPSC | FLITPSCweak | function,
T × L → FLITPSCAction |
| ctrRead | FLIT | function,
T × L × Nat → FLITAction |
| ctrReadPSC | FLITPSCweak | function,
T × L × Nat → FLITPSCAction |
| ctrok | FLITPSC-preds | predicate,
L → Nat × L → Set(T) |
| disj | list-dup | predicate,
List('a) × List('a) |
| disjoint | set-union | predicate,
Set('a) × Set('a) |
| doRead | FLIT | function,
T × L × V → FLITAction |
| doReadPSC | FLITPSCweak | function,
T × L × V → FLITPSCAction |
| doWrite | FLIT | function,
T × L × V → FLITAction |
| doWriteFO | FLIT | function,
T × L → FLITAction |
| doWritePSC | FLITPSCweak | function,
T × L × V → FLITPSCAction |
| dups | list-dup | predicate,
List('a) |
| e | RWevent | variable,
RWevent |
| e | PLIB-preds | variable,
RWevent |
| e | FLITPSCweak-refines-PLIB | variable,
RWevent |
| e | abs-FLITPSCweak-PLIB | variable,
RWevent |
| e | PLIB | variable,
RWevent |
| e | PLIB-proofs | variable,
RWevent |
| el | PLIB-preds | variable,
List(RWevent) |
| el | abs-FLITPSCweak-PLIB | variable,
List(RWevent) |
| events | PLIB-preds | function,
List((RWevent, Bool)) → List(RWevent) |
| f | list-del | variable,
'a → 'b |
| f | list | variable,
'a → 'b |
| f | set-union | variable,
'a → 'b |
| fctr | FLIT | variable,
L → Nat |
| fctr | FLIT-refines-FLITPSCweak | variable,
L → Nat |
| fctr | FLIT-proofs | variable,
L → Nat |
| fillfirst | list-last | function,
Nat × 'a × List('a) → List('a) |
| firstPersistW | FLITPSCweak-preds | function,
List(FOW) → Nat |
| firstVolWrite | PLIB-preds | function,
L × List((RWevent, Bool)) → Nat |
| fl | FLIT | variable,
L |
| fl | FLIT-proofs | variable,
L |
| flitInit | FLIT | predicate,
FLITState |
| flitStep | FLIT | predicate,
FLITState × FLITAction × FLITState |
| flitpscInit | FLITPSCweak | predicate,
FLITPSCState |
| flitpscStep | FLITPSCweak | predicate,
FLITPSCState × FLITPSCAction × FLITPSCState |
| fow | abs-FLIT-FLITPSCweak | variable,
FOW |
| fow | FLIT | variable,
FOW |
| fow | FLITPSCweak | variable,
FOW |
| fow | FLITPSCweak-proofs | variable,
FOW |
| fow | FLITPSCweak-refines-PLIB | variable,
FOW |
| fow | abs-FLITPSCweak-PLIB | variable,
FOW |
| fow | FLITPSCweak-preds | variable,
FOW |
| fow | FLIT-refines-FLITPSCweak | variable,
FOW |
| fow | FLITPSC-preds | variable,
FOW |
| fow | FOW | variable,
FOW |
| fow | FLIT-preds | variable,
FOW |
| fow | FLIT-proofs | variable,
FOW |
| fowl | abs-FLIT-FLITPSCweak | variable,
List(FOW) |
| fowl | FLIT | variable,
List(FOW) |
| fowl | FLITPSCweak | variable,
List(FOW) |
| fowl | FLITPSCweak-proofs | variable,
List(FOW) |
| fowl | FLITPSCweak-refines-PLIB | variable,
List(FOW) |
| fowl | abs-FLITPSCweak-PLIB | variable,
List(FOW) |
| fowl | FLITPSCweak-preds | variable,
List(FOW) |
| fowl | FLIT-refines-FLITPSCweak | variable,
List(FOW) |
| fowl | FLITPSC-preds | variable,
List(FOW) |
| fowl | FLIT-preds | variable,
List(FOW) |
| fowl | FLIT-proofs | variable,
List(FOW) |
| freaders | FLIT | variable,
L → Set(T) |
| freaders | FLIT-proofs | variable,
L → Set(T) |
| frome | list-del | function,
List('a) × 'a → List('a) |
| fv | FLIT | variable,
V |
| fv | FLIT-proofs | variable,
V |
| fwriters | FLIT | variable,
L → Set(T) |
| fwriters | FLIT-proofs | variable,
L → Set(T) |
| gabs | FLITPSCweak-refines-PLIB | predicate,
FLITPSCGState × T → FLITPSCLState × T → FLITPSCPC × PLIBGState × T → PLIBLState × T → PLIBPC |
| gabs | FLIT-refines-FLITPSCweak | predicate,
FLITGState × T → FLITLState × T → FLITPC × FLITPSCGState × T → FLITPSCLState × T → FLITPSCPC |
| glb | FLIT | variable,
Nat |
| glb | FLITPSCweak | variable,
Nat |
| glb | FLITPSCweak-proofs | variable,
Nat |
| glb | abs-FLITPSCweak-PLIB | variable,
Nat |
| glb | FLIT-proofs | variable,
Nat |
| globalACrash | PLIB | constant,
PLIBAction |
| globalAPersist | PLIB | function,
L → PLIBAction |
| globalCRASH | FLIT | constant,
FLITAction |
| globalPERSIST_FO | FLIT | function,
L → FLITAction |
| globalPERSIST_W | FLIT | function,
L → FLITAction |
| globalPSCCRASH | FLITPSCweak | constant,
FLITPSCAction |
| globalPSCPERSIST_FO | FLITPSCweak | function,
L → FLITPSCAction |
| globalPSCPERSIST_W | FLITPSCweak | function,
L → FLITPSCAction |
| gs | FLIT | variable,
FLITGState |
| gs | FLITPSCweak | variable,
FLITPSCGState |
| gs | FLITPSCweak-proofs | variable,
FLITPSCGState |
| gs | FLITPSCweak-refines-PLIB | variable,
FLITPSCGState |
| gs | abs-FLITPSCweak-PLIB | variable,
FLITPSCGState |
| gs | PLIB | variable,
PLIBGState |
| gs | FLIT-refines-FLITPSCweak | variable,
FLITGState |
| gs | PLIB-proofs | variable,
PLIBGState |
| gs | FLIT-proofs | variable,
FLITGState |
| gstate | FLIT | variable,
FLITGState |
| gstate | FLITPSCweak | variable,
FLITPSCGState |
| gstate | FLITPSCweak-proofs | variable,
FLITPSCGState |
| gstate | PLIB | variable,
PLIBGState |
| gstate | PLIB-proofs | variable,
PLIBGState |
| gstate | FLIT-proofs | variable,
FLITGState |
| gstepf | FLIT | function,
FLITGState × FLITLState × FLITPC × FLITAction → FLITGState |
| gstepf | FLITPSCweak | function,
FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCGState |
| gstepf | PLIB | function,
PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBGState |
| h | PLIB-preds | variable,
List((RWevent, Bool)) |
| h | FLITPSCweak-refines-PLIB | variable,
List((RWevent, Bool)) |
| h | abs-FLITPSCweak-PLIB | variable,
List((RWevent, Bool)) |
| h | PLIB | variable,
List((RWevent, Bool)) |
| h | PLIB-proofs | variable,
List((RWevent, Bool)) |
| hPred | PLIB-preds | variable,
List((RWevent, Bool)) → Bool |
| head | list-data | variable,
'a |
| idle | FLIT | constant,
FLITPC |
| idle | FLITPSCweak | constant,
FLITPSCPC |
| idle | PLIB | constant,
PLIBPC |
| il | FLITPSCweak-refines-PLIB | variable,
L |
| il | abs-FLITPSCweak-PLIB | variable,
L |
| il | PLIB | variable,
L |
| il | FLIT-refines-FLITPSCweak | variable,
L |
| il | PLIB-proofs | variable,
L |
| intersect | list-set | function,
List('a) × List('a) → List('a) |
| invAPersistl | PLIB | variable,
L |
| invAPersistl | PLIB-proofs | variable,
L |
| invFLITPSCREAD | FLITPSCweak | function,
T × L → FLITPSCAction |
| invFLITPSCREADl | FLITPSCweak | variable,
L |
| invFLITPSCREADl | FLITPSCweak-proofs | variable,
L |
| invFLITPSCWRITE | FLITPSCweak | function,
T × L × V → FLITPSCAction |
| invFLITPSCWRITEl | FLITPSCweak | variable,
L |
| invFLITPSCWRITEl | FLITPSCweak-proofs | variable,
L |
| invFLITPSCWRITEv | FLITPSCweak | variable,
V |
| invFLITPSCWRITEv | FLITPSCweak-proofs | variable,
V |
| invFLITREAD | FLIT | function,
T × L → FLITAction |
| invFLITREADloc | FLIT | variable,
L |
| invFLITREADloc | FLIT-proofs | variable,
L |
| invFLITWRITE | FLIT | function,
T × L × V → FLITAction |
| invFLITWRITEloc | FLIT | variable,
L |
| invFLITWRITEloc | FLIT-proofs | variable,
L |
| invFLITWRITEval | FLIT | variable,
V |
| invFLITWRITEval | FLIT-proofs | variable,
V |
| invPERSIST_FOloc | FLIT | variable,
L |
| invPERSIST_FOloc | FLIT-proofs | variable,
L |
| invPERSIST_Wloc | FLIT | variable,
L |
| invPERSIST_Wloc | FLIT-proofs | variable,
L |
| invPSCPERSIST_FOl | FLITPSCweak | variable,
L |
| invPSCPERSIST_FOl | FLITPSCweak-proofs | variable,
L |
| invPSCPERSIST_Wl | FLITPSCweak | variable,
L |
| invPSCPERSIST_Wl | FLITPSCweak-proofs | variable,
L |
| invRead | PLIB | constant,
PLIBPC |
| invWrite | PLIB | constant,
PLIBPC |
| isPersistFO | FLITPSCweak-preds | predicate,
Nat × List(FOW) |
| isPropFO | FLIT-preds | predicate,
Nat × L × List(Bevent) |
| iv | FLITPSCweak-refines-PLIB | variable,
V |
| iv | abs-FLITPSCweak-PLIB | variable,
V |
| iv | PLIB | variable,
V |
| iv | FLIT-refines-FLITPSCweak | variable,
V |
| iv | PLIB-proofs | variable,
V |
| l | RWevent | variable,
L |
| l | abs-FLIT-FLITPSCweak | variable,
L |
| l | FLIT | variable,
L |
| l | FLITPSCweak | variable,
L |
| l | FLITPSCweak-proofs | variable,
L |
| l | PLIB-preds | variable,
L |
| l | FLITPSCweak-refines-PLIB | variable,
L |
| l | abs-FLITPSCweak-PLIB | variable,
L |
| l | FLITPSCweak-preds | variable,
L |
| l | PLIB | variable,
L |
| l | Bevent | variable,
L |
| l | memory | variable,
L |
| l | FLIT-refines-FLITPSCweak | variable,
L |
| l | PLIB-proofs | variable,
L |
| l | FLITPSC-preds | variable,
L |
| l | FOW | variable,
L |
| l | FLIT-preds | variable,
L |
| l | FLIT-proofs | variable,
L |
| labs | FLITPSCweak-refines-PLIB | predicate,
FLITPSCGState × FLITPSCLState × FLITPSCPC × PLIBGState × PLIBLState × PLIBPC |
| labs | FLIT-refines-FLITPSCweak | predicate,
FLITGState × FLITLState × FLITPC × FLITPSCGState × FLITPSCLState × FLITPSCPC |
| loc | FLIT | variable,
L |
| loc | FLITPSCweak | variable,
Nat |
| loc | FLITPSCweak-proofs | variable,
Nat |
| loc | abs-FLITPSCweak-PLIB | variable,
Nat |
| loc | PLIB | variable,
L |
| loc | FLIT-refines-FLITPSCweak | variable,
L |
| loc | PLIB-proofs | variable,
L |
| loc | FLIT-proofs | variable,
L |
| ls | FLIT | variable,
FLITLState |
| ls | FLITPSCweak | variable,
FLITPSCLState |
| ls | FLITPSCweak-proofs | variable,
FLITPSCLState |
| ls | FLITPSCweak-refines-PLIB | variable,
FLITPSCLState |
| ls | PLIB | variable,
PLIBLState |
| ls | FLIT-refines-FLITPSCweak | variable,
FLITLState |
| ls | PLIB-proofs | variable,
PLIBLState |
| ls | FLIT-proofs | variable,
FLITLState |
| lsf | FLIT | variable,
T → FLITLState |
| lsf | FLITPSCweak | variable,
T → FLITPSCLState |
| lsf | FLITPSCweak-proofs | variable,
T → FLITPSCLState |
| lsf | FLITPSCweak-refines-PLIB | variable,
T → FLITPSCLState |
| lsf | PLIB | variable,
T → PLIBLState |
| lsf | FLIT-refines-FLITPSCweak | variable,
T → FLITLState |
| lsf | PLIB-proofs | variable,
T → PLIBLState |
| lsf | FLIT-proofs | variable,
T → FLITLState |
| lstep | FLIT | predicate,
FLITGState × FLITLState × FLITPC × FLITAction × FLITGState × FLITLState × FLITPC |
| lstep | FLITPSCweak | predicate,
FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction × FLITPSCGState × FLITPSCLState × FLITPSCPC |
| lstep | PLIB | predicate,
PLIBGState × PLIBLState × PLIBPC × PLIBAction × PLIBGState × PLIBLState × PLIBPC |
| lstepf | FLIT | function,
FLITGState × FLITLState × FLITPC × FLITAction → FLITLState |
| lstepf | FLITPSCweak | function,
FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCLState |
| lstepf | PLIB | function,
PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBLState |
| m | list-getput | variable,
Nat |
| m | list-del | variable,
Nat |
| m | abs-FLIT-FLITPSCweak | variable,
Nat |
| m | list-perm | variable,
Nat |
| m | filter-count | variable,
Nat |
| m | abs-FLITPSCweak-PLIB | variable,
Nat |
| m | FLITPSCweak-preds | variable,
Nat |
| m | PLIB | variable,
Nat |
| m | list-last | variable,
Nat |
| m | FLIT-refines-FLITPSCweak | variable,
Nat |
| m | set-union | variable,
Nat |
| m | PLIB-proofs | variable,
Nat |
| m | FLITPSC-preds | variable,
Nat |
| m | list-set | variable,
Nat |
| m | FLIT-preds | variable,
Nat |
| mem | abs-FLIT-FLITPSCweak | variable,
L → V |
| mem | FLITPSCweak | variable,
L → V |
| mem | FLITPSCweak-proofs | variable,
L → V |
| mem | PLIB-preds | variable,
L → V |
| mem | FLITPSCweak-refines-PLIB | variable,
L → V |
| mem | abs-FLITPSCweak-PLIB | variable,
L → V |
| mem | FLITPSCweak-preds | variable,
L → V |
| mem | memory | variable,
L → V |
| mem | FLIT-refines-FLITPSCweak | variable,
L → V |
| mem | FLITPSC-preds | variable,
L → V |
| mem | FLIT-preds | variable,
L → V |
| mkFLITPSCgs | FLITPSCweak | function,
L → V × L → List(FOW) × L → Nat × L → Set(T) × L → Set(T) → FLITPSCGState |
| mkFLITPSCls | FLITPSCweak | function,
T × L × V → FLITPSCLState |
| mkFLITgs | FLIT | function,
L → V × L → List(FOW) × L → Nat × T → List(Bevent) × L → Set(T) × L → Set(T) × T → List(Bevent) → FLITGState |
| mkFLITls | FLIT | function,
T × L × V → FLITLState |
| mkPLIBgs | PLIB | function,
L → V × L → V × List((RWevent, Bool)) → PLIBGState |
| mkPLIBls | PLIB | function,
T × L × V × V → PLIBLState |
| mklist | list-last | function,
'a × Nat → List('a) |
| mkstate | FLIT | function,
FLITGState × T → FLITLState × T → FLITPC → FLITState |
| mkstate | FLITPSCweak | function,
FLITPSCGState × T → FLITPSCLState × T → FLITPSCPC → FLITPSCState |
| mkstate | PLIB | function,
PLIBGState × T → PLIBLState × T → PLIBPC → PLIBState |
| n | list-getput | variable,
Nat |
| n | list-del | variable,
Nat |
| n | abs-FLIT-FLITPSCweak | variable,
Nat |
| n | FLIT | variable,
Nat |
| n | list-perm | variable,
Nat |
| n | filter-count | variable,
Nat |
| n | FLITPSCweak | variable,
Nat |
| n | FLITPSCweak-proofs | variable,
Nat |
| n | PLIB-preds | variable,
Nat |
| n | abs-FLITPSCweak-PLIB | variable,
Nat |
| n | FLITPSCweak-preds | variable,
Nat |
| n | PLIB | variable,
Nat |
| n | list-data | variable,
Nat |
| n | list-last | variable,
Nat |
| n | FLIT-refines-FLITPSCweak | variable,
Nat |
| n | set-union | variable,
Nat |
| n | PLIB-proofs | variable,
Nat |
| n | FLITPSC-preds | variable,
Nat |
| n | list-set | variable,
Nat |
| n | FLIT-preds | variable,
Nat |
| n | FLIT-proofs | variable,
Nat |
| noPending | FLITPSC-preds | predicate,
T × L → List(FOW) |
| noPending | FLIT-preds | predicate,
T × T → List(Bevent) × L → List(FOW) |
| noPendingW | FLITPSC-preds | predicate,
T × L → List(FOW) |
| noPendingW | FLIT-preds | predicate,
T × T → List(Bevent) × L → List(FOW) |
| notMember | FLITPSC-preds | predicate,
T × L → Set(T) |
| oneMember | FLITPSC-preds | predicate,
T × L × L → Set(T) |
| onePendingW | FLITPSC-preds | predicate,
T × L × L → List(FOW) |
| ov | FLITPSCweak-refines-PLIB | variable,
V |
| ov | abs-FLITPSCweak-PLIB | variable,
V |
| ov | PLIB | variable,
V |
| ov | FLIT-refines-FLITPSCweak | variable,
V |
| ov | PLIB-proofs | variable,
V |
| p | abs-FLIT-FLITPSCweak | variable,
L → List(FOW) |
| p | filter-count | variable,
'a → Bool |
| p | FLITPSCweak | variable,
L → List(FOW) |
| p | FLITPSCweak-proofs | variable,
L → List(FOW) |
| p | forall-indexWhere | variable,
'a → Bool |
| p | FLITPSCweak-refines-PLIB | variable,
L → List(FOW) |
| p | abs-FLITPSCweak-PLIB | variable,
L → List(FOW) |
| p | FLITPSCweak-preds | variable,
L → List(FOW) |
| p | FLIT-refines-FLITPSCweak | variable,
L → List(FOW) |
| p | set-union | variable,
'a → Bool |
| p | FLITPSC-preds | variable,
L → List(FOW) |
| p | FLIT-preds | variable,
L → List(FOW) |
| pc | FLIT | variable,
FLITPC |
| pc | FLITPSCweak | variable,
FLITPSCPC |
| pc | FLITPSCweak-proofs | variable,
FLITPSCPC |
| pc | FLITPSCweak-refines-PLIB | variable,
FLITPSCPC |
| pc | PLIB | variable,
PLIBPC |
| pc | FLIT-refines-FLITPSCweak | variable,
FLITPC |
| pc | PLIB-proofs | variable,
PLIBPC |
| pc | FLIT-proofs | variable,
FLITPC |
| pcf | FLIT | variable,
T → FLITPC |
| pcf | FLITPSCweak | variable,
T → FLITPSCPC |
| pcf | FLITPSCweak-proofs | variable,
T → FLITPSCPC |
| pcf | FLITPSCweak-refines-PLIB | variable,
T → FLITPSCPC |
| pcf | PLIB | variable,
T → PLIBPC |
| pcf | FLIT-refines-FLITPSCweak | variable,
T → FLITPC |
| pcf | PLIB-proofs | variable,
T → PLIBPC |
| pcf | FLIT-proofs | variable,
T → FLITPC |
| pcstepf | FLIT | function,
FLITGState × FLITLState × FLITPC × FLITAction → FLITPC |
| pcstepf | FLITPSCweak | function,
FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCPC |
| pcstepf | PLIB | function,
PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBPC |
| pending | PLIB-preds | variable,
T → Bool |
| pendingOk | FLITPSC-preds | predicate,
L → List(FOW) |
| pendingOk | FLIT-preds | predicate,
T → List(Bevent) × L → List(FOW) |
| perm | list-perm | predicate,
List('a) × List('a) |
| persistDependentReads | PLIB-preds | function,
L × List((RWevent, Bool)) → List((RWevent, Bool)) |
| persisted | PLIB-preds | variable,
L → Bool |
| persisted | abs-FLITPSCweak-PLIB | variable,
L → Bool |
| plibInit | PLIB | predicate,
PLIBState |
| plibStep | PLIB | predicate,
PLIBState × PLIBAction × PLIBState |
| plin | FLITPSCweak | variable,
L → List(FOW) |
| plin | FLITPSCweak-proofs | variable,
L → List(FOW) |
| pm | abs-FLITPSCweak-PLIB | variable,
L → V |
| pm | PLIB | variable,
L → V |
| pm | PLIB-proofs | variable,
L → V |
| pmem | abs-FLIT-FLITPSCweak | variable,
L → V |
| pmem | FLIT | variable,
L → V |
| pmem | FLIT-refines-FLITPSCweak | variable,
L → V |
| pmem | FLIT-proofs | variable,
L → V |
| pq | abs-FLIT-FLITPSCweak | variable,
L → List(FOW) |
| pq | FLIT | variable,
L → List(FOW) |
| pq | FLIT-refines-FLITPSCweak | variable,
L → List(FOW) |
| pq | FLIT-preds | variable,
L → List(FOW) |
| pq | FLIT-proofs | variable,
L → List(FOW) |
| pre | FLIT | predicate,
FLITGState × FLITLState × FLITPC × FLITAction |
| pre | FLITPSCweak | predicate,
FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction |
| pre | PLIB | predicate,
PLIBGState × PLIBLState × PLIBPC × PLIBAction |
| propFO | FLIT | function,
T × L → FLITAction |
| propFOs | abs-FLIT-FLITPSCweak | function,
T × L × List(Bevent) → List(FOW) |
| propSF | FLIT | function,
T → FLITAction |
| pwb | FLIT | function,
T × L → FLITAction |
| pwbPSC | FLITPSCweak | function,
T × L → FLITPSCAction |
| readFOsOk | FLIT-preds | predicate,
T → List(Bevent) × L → Set(T) |
| readers | FLITPSCweak | variable,
L → Set(T) |
| readers | FLITPSCweak-proofs | variable,
L → Set(T) |
| readers | FLITPSCweak-preds | variable,
L → Set(T) |
| readers | FLITPSC-preds | variable,
L → Set(T) |
| ready | FLIT | constant,
FLITPC |
| ready | FLITPSCweak | constant,
FLITPSCPC |
| ready | PLIB | constant,
PLIBPC |
| rely | PLIB-preds | predicate,
T × List((RWevent, Bool)) × List((RWevent, Bool)) |
| rely | FLITPSCweak-preds | predicate,
T × L → List(FOW) × L → List(FOW) |
| rely | FLITPSCweak-preds | predicate,
T × List(FOW) × List(FOW) |
| rely | FLIT-preds | predicate,
T × L × List(FOW) × List(Bevent) × List(FOW) × List(Bevent) |
| rely | FLIT-preds | predicate,
T × L → List(FOW) × T → List(Bevent) × L → List(FOW) × T → List(Bevent) |
| relyp | FLITPSC-preds | predicate,
T × L → List(FOW) × L → List(FOW) |
| relyp | FLITPSC-preds | predicate,
T × List(FOW) × List(FOW) |
| relyws | FLITPSC-preds | predicate,
T × Set(T) × Set(T) |
| relyws | FLITPSC-preds | predicate,
T × L → Set(T) × L → Set(T) |
| ren | FLITPSCweak-refines-PLIB | function,
FLITPSCAction × PLIBGState × T → PLIBLState → PLIBAction |
| ren | FLIT-refines-FLITPSCweak | function,
FLITAction × FLITPSCGState × T → FLITPSCLState → FLITPSCAction |
| reorder | abs-FLIT-FLITPSCweak | predicate,
L × List(FOW) × List(FOW) × T → List(Bevent) |
| reorder | abs-FLIT-FLITPSCweak | predicate,
L → List(FOW) × L → List(FOW) × T → List(Bevent) |
| resRead | PLIB | constant,
PLIBPC |
| resWrite | PLIB | constant,
PLIBPC |
| retFLITPSCREAD | FLITPSCweak | function,
T × V → FLITPSCAction |
| retFLITPSCREADv | FLITPSCweak | variable,
V |
| retFLITPSCREADv | FLITPSCweak-proofs | variable,
V |
| retFLITPSCWRITE | FLITPSCweak | function,
T → FLITPSCAction |
| retFLITREAD | FLIT | function,
T × V → FLITAction |
| retFLITREADval | FLIT | variable,
V |
| retFLITREADval | FLIT-proofs | variable,
V |
| retFLITWRITE | FLIT | function,
T → FLITAction |
| rev | list-last | function,
List('a) → List('a) |
| rfo | abs-FLIT-FLITPSCweak | variable,
T → List(Bevent) |
| rfo | FLIT | variable,
T → List(Bevent) |
| rfo | FLIT-preds | variable,
T → List(Bevent) |
| rfo | FLIT-proofs | variable,
T → List(Bevent) |
| rs | abs-FLITPSCweak-PLIB | variable,
L → Set(T) |
| rset | abs-FLITPSCweak-PLIB | variable,
Set(T) |
| s | FLIT | variable,
FLITState |
| s | FLITPSCweak | variable,
FLITPSCState |
| s | FLITPSCweak-proofs | variable,
FLITPSCState |
| s | FLITPSCweak-refines-PLIB | variable,
FLITPSCState |
| s | PLIB | variable,
PLIBState |
| s | set-basic | variable,
Set('a) |
| s | FLIT-refines-FLITPSCweak | variable,
FLITState |
| s | set-union | variable,
Set('a) |
| s | PLIB-proofs | variable,
PLIBState |
| s | FLIT-proofs | variable,
FLITState |
| sfence | FLIT | function,
T → FLITAction |
| sfencePSC | FLITPSCweak | function,
T → FLITPSCAction |
| t | RWevent | variable,
T |
| t | abs-FLIT-FLITPSCweak | variable,
T |
| t | FLIT | variable,
T |
| t | FLITPSCweak | variable,
T |
| t | FLITPSCweak-proofs | variable,
T |
| t | PLIB-preds | variable,
T |
| t | FLITPSCweak-refines-PLIB | variable,
T |
| t | abs-FLITPSCweak-PLIB | variable,
T |
| t | FLITPSCweak-preds | variable,
T |
| t | PLIB | variable,
T |
| t | FLIT-refines-FLITPSCweak | variable,
T |
| t | PLIB-proofs | variable,
T |
| t | FLITPSC-preds | variable,
T |
| t | FLIT-preds | variable,
T |
| t | FLIT-proofs | variable,
T |
| tail | list-data | variable,
List('a) |
| tid | FLIT | variable,
T |
| tid | FLITPSCweak | variable,
T |
| tid | FLITPSCweak-proofs | variable,
T |
| tid | abs-FLITPSCweak-PLIB | variable,
T |
| tid | PLIB | variable,
T |
| tid | memory | variable,
T |
| tid | PLIB-proofs | variable,
T |
| tid | FOW | variable,
T |
| tid | FLIT-proofs | variable,
T |
| ts | FLIT | variable,
Set(T) |
| ts | FLITPSCweak | variable,
Set(T) |
| ts | FLITPSCweak-proofs | variable,
Set(T) |
| ts | FLITPSCweak-preds | variable,
Set(T) |
| ts | FLITPSC-preds | variable,
Set(T) |
| ts | FLIT-proofs | variable,
Set(T) |
| tsf | FLITPSCweak-preds | variable,
L → Set(T) |
| tsf | FLITPSC-preds | variable,
L → Set(T) |
| v | RWevent | variable,
V |
| v | abs-FLIT-FLITPSCweak | variable,
V |
| v | FLIT | variable,
V |
| v | FLITPSCweak | variable,
V |
| v | FLITPSCweak-proofs | variable,
V |
| v | PLIB-preds | variable,
V |
| v | FLITPSCweak-refines-PLIB | variable,
V |
| v | abs-FLITPSCweak-PLIB | variable,
V |
| v | FLITPSCweak-preds | variable,
V |
| v | PLIB | variable,
V |
| v | Bevent | variable,
V |
| v | memory | variable,
V |
| v | FLIT-refines-FLITPSCweak | variable,
V |
| v | PLIB-proofs | variable,
V |
| v | FLITPSC-preds | variable,
V |
| v | FOW | variable,
V |
| v | FLIT-preds | variable,
V |
| v | FLIT-proofs | variable,
V |
| val | FLIT | variable,
V |
| val | PLIB | variable,
V |
| val | FLIT-refines-FLITPSCweak | variable,
V |
| val | PLIB-proofs | variable,
V |
| val | FOW | variable,
V |
| val | FLIT-proofs | variable,
V |
| vm | abs-FLITPSCweak-PLIB | variable,
L → V |
| vm | PLIB | variable,
L → V |
| vm | PLIB-proofs | variable,
L → V |
| vpe | PLIB-preds | variable,
(RWevent, Bool) |
| vpe | FLITPSCweak-refines-PLIB | variable,
(RWevent, Bool) |
| vpe | abs-FLITPSCweak-PLIB | variable,
(RWevent, Bool) |
| vpe | PLIB | variable,
(RWevent, Bool) |
| vpe | PLIB-proofs | variable,
(RWevent, Bool) |
| wl | FLIT | variable,
L |
| wl | FLITPSCweak | variable,
L |
| wl | FLITPSCweak-proofs | variable,
L |
| wl | abs-FLITPSCweak-PLIB | variable,
L |
| wl | FLIT-proofs | variable,
L |
| writers | abs-FLIT-FLITPSCweak | variable,
L → Set(T) |
| writers | FLITPSCweak | variable,
L → Set(T) |
| writers | FLITPSCweak-proofs | variable,
L → Set(T) |
| writers | FLITPSCweak-refines-PLIB | variable,
L → Set(T) |
| writers | FLITPSCweak-preds | variable,
L → Set(T) |
| writers | FLIT-refines-FLITPSCweak | variable,
L → Set(T) |
| writers | FLITPSC-preds | variable,
L → Set(T) |
| writers | FLIT-preds | variable,
L → Set(T) |
| writersOk | FLITPSC-preds | predicate,
L → List(FOW) × L → Set(T) |
| writersOk | FLIT-preds | predicate,
T → List(Bevent) × L → List(FOW) × L → Set(T) |
| ws | abs-FLIT-FLITPSCweak | variable,
Set(T) |
| ws | abs-FLITPSCweak-PLIB | variable,
L → Set(T) |
| x | list-getput | variable,
List('a) |
| x | list-del | variable,
List('a) |
| x | list-perm | variable,
List('a) |
| x | filter-count | variable,
List('a) |
| x | forall-indexWhere | variable,
List('a) |
| x | list-dup | variable,
List('a) |
| x | list | variable,
List('a) |
| x | list-data | variable,
List('a) |
| x | list-last | variable,
List('a) |
| x | list-set | variable,
List('a) |
| y | list-getput | variable,
List('a) |
| y | list-del | variable,
List('a) |
| y | list-perm | variable,
List('a) |
| y | filter-count | variable,
List('a) |
| y | list-dup | variable,
List('a) |
| y | list | variable,
List('a) |
| y | list-data | variable,
List('a) |
| y | list-last | variable,
List('a) |
| y | list-set | variable,
List('a) |
| z | list-getput | variable,
List('a) |
| z | list-del | variable,
List('a) |
| z | list-perm | variable,
List('a) |
| z | filter-count | variable,
List('b) |
| z | list-dup | variable,
List('a) |
| z | list | variable,
List('a) |
| z | list-data | variable,
List('a) |
| z | list-last | variable,
List('a) |
| z | list-set | variable,
List('a) |
| zip | filter-count | function,
List('a) × List('b) → List(('a, 'b)) |
| | | PLIB-preds | function,
List((RWevent, Bool)) × L → List((RWevent, Bool)) |
| | | PLIB-preds | function,
List((RWevent, Bool)) × Bool → List((RWevent, Bool)) |
| | | PLIB-preds | function,
List((RWevent, Bool)) × T → List((RWevent, Bool)) |
| | | FLITPSC-preds | function,
List(FOW) × T → List(FOW) |
| |FO | FLITPSC-preds | function,
List(FOW) → List(FOW) |
| |R | PLIB-preds | function,
List((RWevent, Bool)) → List((RWevent, Bool)) |
| |SF | FLIT-preds | function,
List(Bevent) × L → List(Bevent) |
| |W | PLIB-preds | function,
List((RWevent, Bool)) → List((RWevent, Bool)) |
| |W | FLITPSC-preds | function,
List(FOW) → List(FOW) |
| |WL | FLIT-preds | function,
List(Bevent) × L → List(Bevent) |
| } | set-union | function,
'a → Set('a) |
| τ | FLIT | constant,
FLITAction |
| τ | FLITPSCweak | constant,
FLITPSCAction |
| τ | PLIB | constant,
PLIBAction |
| ∅ | memory | function,
L → V |
| ∅ | set-basic | constant,
Set('a) |
| ∈ | list | predicate,
'a × List('a) |
| ∈ | set-basic | predicate,
'a × Set('a) |
| ∩ | set-union | function,
Set('a) × Set('a) → Set('a) |
| ∪ | set-union | function,
Set('a) × Set('a) → Set('a) |
| ∪ | list-set | function,
List('a) × List('a) → List('a) |
| ≤ | nat | predicate,
Nat × Nat |
| ≥ | nat | predicate,
Nat × Nat |
| ⊆ | set-basic | predicate,
Set('a) × Set('a) |
| ⊆ | list-set | predicate,
List('a) × List('a) |
| ⊆m | list-perm | predicate,
List('a) × List('a) |
| ⊑ | list-last | predicate,
List('a) × List('a) |
| ⊑p | PLIB-preds | predicate,
List((RWevent, Bool)) × List((RWevent, Bool)) |
| ⊒ | list-last | predicate,
List('a) × List('a) |
| ⊒W | FLITPSCweak-preds | predicate,
List(FOW) × List(FOW) |
| ⊒w | FLIT-preds | predicate,
List(Bevent) × List(Bevent) |
| ⊕ | PLIB-preds | function,
L → V × List((RWevent, Bool)) → L → V |
| ⊕ | FLITPSC-preds | function,
L → V × L → List(FOW) → L → V |
| ⊕ | FLITPSC-preds | function,
V × List(FOW) → V |
| ⊕ | FLIT-preds | function,
L → V × List(Bevent) → L → V |
| ⊕ | FLIT-preds | function,
V × List(Bevent) → V |