Terminology

Basic domains

• $r ∈ Reg$ – Registers (local variables)
• $x ∈ Loc$ – Locations
• $v ∈ Val$ – Values including 0
• $i ∈ Tid = \{1, ... ,N\}$ – Thread identifiers

Expressions and commands

• e ::= r | v | e + e | ...
  • Not including Locations
• c ::= skip | if e then c else c | while e do c | c ; c | r := e | r := x | x := e | r := FAA(x, e) | r := $\bold{CAS}(x, e_r, e_w)$ | fence
  • FAA - Fetch and Add
  • CAS - Compare and Set / Swap
  • Fence can guarantee that all writes before are written to memory

Programs

P : Tid → Cmd, written as $P = c_1 ∥ ... ∥ c_N$

Subsystems

1. Thread subsystem

• Thread-local steps: $c, s →^l c' , s'$ .
• Interpret sequential programs.
• Lift them to program steps: $P, S →^{i:l} P' , S'$.