TLA+ Notation Guide

TLA+ operators and syntax used in these slides

Basic Operators

Notation	Meaning	Example
`==`	Definition ("means")	`Init == ...` means "Init is defined as..."
`/\`	AND (logical conjunction)	`A /\ B` means "A and B"
`\/`	OR (logical disjunction)	`A \/ B` means "A or B"
`=>`	Implication ("if...then")	`A => B` means "if A then B"
`~`	NOT (negation)	`~A` means "not A"
`\in`	Element of set	`x \in S` means "x is in S"
`\notin`	Not element of set	`x \notin S`
`\cup`	Union	`S \cup T`
`\subseteq`	Subset	`S \subseteq T`
`\A`	Universal quantifier (∀, for all)	`\A t \in Threads : P(t)`
`\E`	Existential quantifier (∃, exists)	`\E o \in Objects : ...`

Variables and State Transitions

Notation	Meaning	Example
`VARIABLES x, y`	State variable declaration	Constitute the model state
`x'`	Value of `x` in the next state	`x' = x + 1` means "increment x by 1"
`UNCHANGED <<x, y>>`	x, y remain unchanged	No change in this action
`Init`	Initial state definition	Specifies initial values for all variables
`Next`	Next-state relation (transition)	Disjunction of possible actions
`[][Next]_vars`	Always Next or stuttering	Temporal formula of the specification
`WF_vars(Next)`	Weak fairness (enabled actions eventually execute)	Required for liveness

Functions and Records

Notation	Meaning	Example
`[x \in S \|-> e]`	Function definition (returns e for each x in S)	`[t \in Threads \|-> 0]` initializes all threads to 0
`f[x]`	Value of f at x	`global_rc[o]` is the RC of object o
`[f EXCEPT ![x] = e]`	New function with only f[x] changed to e	`[pc EXCEPT ![t] = "done"]`
`@`	Current value inside EXCEPT	`[f EXCEPT ![x] = @ + 1]` means +1
`[a \|-> 1, b \|-> 2]`	Record (struct)	`r.a` for field access

Conditionals and Choice

Notation	Meaning	Example
`IF P THEN A ELSE B`	Conditional expression	Standard if-then-else
`CASE p1 -> e1 [] p2 -> e2`	Pattern match	p1: if p1 is true then e1, if p2 then e2
`LET x == e IN ...`	Local definition	`auto x = e;` in C++equivalent
`CHOOSE x \in S : P(x)`	Pick one element of S satisfying P	Nondeterministic choice

Constants and Types

Notation	Meaning	Example
`CONSTANTS`	Model parameters	`Threads, Objects, MaxLocalRC`
`0..N`	0to N integer set	`0..MaxVal`
`Nat`	Natural numbers	For type checking
`BOOLEAN`	{TRUE, FALSE}	For type checking

CONSTANTS and .cfg Files

The CONSTANTS in a TLA+ spec define model parameters. Concrete values are specified in .cfg files (TLC configuration files).

Spec (.tla)	Config (.cfg)	Meaning
`CONSTANTS Threads, Objects`	`Threads = {t1, t2} Objects = {o1, o2}`	Set concrete values for model checking
`CONSTANTS EnableCAS, EnableRecycle`	`EnableCAS = TRUE EnableRecycle = TRUE`	Feature enable/disable flags

Increasing thread/object count causes exponential state space growth. Typically verified with 2-3 threads and 2 objects, with symmetry reduction.

StateConstraint vs INVARIANT

Notation	Location	Meaning
`CONSTRAINT StateConstraint`	.cfg file	When a state violating this condition is reached, exploration beyond it is pruned. Used to make the state space finite. Not a safety check.
`INVARIANT MemorySafety`	.cfg file	Checks that this condition holds in every reachable state. Violations are reported as bugs.

Important distinction: CONSTRAINT means "only explore within this range" (search restriction). INVARIANT means "does this always hold?" (safety verification).
e.g., global_rc[o] <= 5 in CONSTRAINT: states where global_rc exceeds 5 are not explored (potential misses). Same expression in INVARIANT: reported as an error if global_rc exceeds 5.

This model does not use StateConstraint. State space is made structurally finite via C++ scope destruction and modular arithmetic, exploring all reachable states without artificial pruning.

{a, b, c}Finite set{"scan", "cas", "idle"}

Reading tips: A TLA+ action (e.g., ReserveScanCAS(t)): is a declaration: "when these conditions hold, change variables as follows." /\: all conjuncts must be true for the action to be enabled. x'is the next state; UNCHANGED means no change.

Layer 1: atomic_shared_ptr

TLA+ Model Walkthrough — atomic_shared_ptr.tla (340 lines)

Role in the 2-layer architecture: This deck was previously titled "Layer 0" (now renamed to slides_layer1.html). It has been renamed to Layer 1 to match the paper's 2-layer model (Layer 1: atomic_shared_ptr / Layer 2: bundle/unbundle + commit). Content unchanged.

What is modeled

kame/atomic_smart_ptr.h : the entire reference counting protocol.
Exhaustive TLA+ verification of the lock-free C++ atomic_shared_ptr.

Model Components

Element	TLA+ Representation	C++ Counterpart
Shared pointer	`ptr` + `local_rc`	`m_ref` (uintptr_t)
Objects	`Objects` (Finite set)	Ref struct
Reference count	`global_rc[o]`	Inside Ref:`atomic<int>`
Freed state	`freed[o]`	delete call
Thread state	`pc[t]`, `thr_*`	Local variables in functions

Variables (12 total)

VARIABLES
    ptr,            \* Pointer (Object or NULL)
    local_rc,       \* Local reference counter (lower 3 bits)
    global_rc,      \* global_rc[o]: Global RC for each object
    freed,          \* freed[o]: Freed flag
    pc,             \* Per-thread program counter (22 states)
    thr_op,         \* "scan", "cas", "idle"
    thr_pref,       \* Pointer read by acquire_tag_ref_
    thr_rcnt,       \* Local RC read by acquire_tag_ref_
    thr_old,        \* CAS: Expected old object
    thr_new,        \* CAS: New object
    thr_holds,      \* Objects held via local_shared_ptr
    thr_ls_ctx      \* Return target for release_tag_ref_

acquire_tag_ref_: Atomic Read + CAS

C++ source: atomic_smart_ptr.h lines 462-488

m_ref.load() in C++is a single atomic operation; pointer and local RC are always derived from the same loaded value. TLA+ models this as a single step.

(* Atomic read: read ptr and local_rc simultaneously *)
ReserveScanRead(t) ==
    /\ pc[t] = "rs_read"
    /\ thr_pref' = [thr_pref EXCEPT ![t] = ptr]       \* ← read ptr
    /\ thr_rcnt' = [thr_rcnt EXCEPT ![t] = local_rc]  \* ← read local_rc (simultaneously)
    /\ pc' = [pc EXCEPT ![t] = "rs_cas"]

(* CAS — succeeds only if both ptr and RC match *)
ReserveScanCAS(t) ==
    /\ pc[t] = "rs_cas"
    /\ thr_pref[t] /= NULL
    /\ \/ (* CAS succeeds: both ptr AND local_rc match *)
          /\ ptr = thr_pref[t]
          /\ local_rc = thr_rcnt[t]
          /\ local_rc' = thr_rcnt[t] + 1  \* Pinned!
       \/ (* CAS fails: retry from read *)
          /\ ~(ptr = thr_pref[t] /\ local_rc = thr_rcnt[t])
          /\ pc' = [pc EXCEPT ![t] = "rs_read"]

Key point: Even if another thread changes ptr/local_rc between read and CAS, the CAS performs full-word comparison (both ptr + local_rc), so inconsistencies are always caught.

scan_: load_shared_(): 3 Steps

C++ source: lines 494-503

(* Step 1: acquire_tag_ref_ → Atomic Read + CAS to increment local RC [see previous slide] *)

(* Step 2: Increment global RC — safe with relaxed *)
ScanIncGlobal(t) ==
    /\ pc[t] = "scan_inc"
    /\ global_rc' = [global_rc EXCEPT ![thr_pref[t]] = @ + 1]
    /\ pc' = [pc EXCEPT ![t] = "scan_leave"]

(* Step 3: release_tag_ref_ → decrement local RC *)

acquire_tag_ref_ → global_rc++ → release_tag_ref_

release_tag_ref_: Fallback Branch

LeaveScanCAS(t) ==
    \/ (* CAS succeeds: ptr unchanged → decrement local RC *)
       /\ ptr = thr_pref[t] /\ local_rc = thr_rcnt[t]
       /\ local_rc' = thr_rcnt[t] - 1

    \/ (* CAS fails, ptr same → retry *)
       /\ ptr = thr_pref[t]
       /\ pc' = [pc EXCEPT ![t] = "ls_read"]

    \/ (* CAS fails, ptr changed → fallback: global_rc-- *)
       /\ ptr /= thr_pref[t]
       /\ pc' = [pc EXCEPT ![t] = "ls_global"]

(* Fallback: the swapping thread already transferred the local RC *)
LeaveScanGlobal(t) ==
    /\ global_rc' = [global_rc EXCEPT ![o] = @ - 1]
    /\ IF global_rc[o] = 1
       THEN freed' = [freed EXCEPT ![o] = TRUE]  \* → freed!

This fallback is essential: without it, refcount leak or use-after-free. Confirmed by TLA+ verification.

compareAndSwap_: 6 Phases

C++ source: lines 556-603

Phase	TLA+ Action	Operation
1	`CASPreInc`	Increment new object's `global_rc++`
2	`CASReserve`→`rs_*`	Pin via `acquire_tag_ref_`
3	`CASCheck`	`pref != oldr`then return failure
4	`CASTransfer`	Transfer local RC to `global_rc`
5	`CASSwap`	CAS (`acq_rel`): Swap pointer
6	`CASCleanup`	Decrement old object's `global_rc`

(* Phase 4: Transfer local RC to global *)
CASTransfer(t) ==
    /\ IF thr_pref[t] /= NULL /\ thr_rcnt[t] /= 1
       THEN global_rc' = [global_rc EXCEPT
                ![thr_pref[t]] = @ + thr_rcnt[t] - 1]

(* Phase 5: CAS — Full-word comparison *)
CASSwap(t) ==
    \/ /\ ptr = thr_pref[t] /\ local_rc = thr_rcnt[t]  \* match
       /\ ptr' = thr_new[t]
       /\ local_rc' = 0
    \/ /\ ~(...)  \* CAS fails → Undo → release_tag_ref_ → retry

Relation to ABA: Caller holds oldr via local_shared_ptr → global_rc > 0 → never freed → ABA is structurally impossible.
However, in load_shared_() the thread holds no reference, so TLA+ models ABA recycling as a sound over-approximation.

swap: Unconditional Exchange

Key difference from CAS: swap does not check the old pointer — it unconditionally replaces it. No PreInc phase needed (ownership is exchanged, not added).

Protocol

StartSwap(t) ==
    /\ EnableSwap
    /\ pc[t] = "idle"
    /\ \E newObj \in Objects \cup {NULL} :
       /\ (newObj /= NULL => thr_holds[t][newObj] > 0)
       /\ thr_new' = [thr_new EXCEPT ![t] = newObj]
    /\ pc' = [pc EXCEPT ![t] = "cas_acquire"]  \* skip PreInc
    /\ thr_op' = [thr_op EXCEPT ![t] = "swap"]

\* After acquire_tag_ref_ succeeds:
\*   CASTransfer: global_rc[pref] += local_rc  (tag→global transfer)
\*   CASSwap: CAS ptr from pref to newObj, local_rc → 0
\*   No CASCleanup needed (no PreInc to undo)

Reset: local_shared_ptr::reset()

Reset(t) ==
    /\ pc[t] \in {"idle", "done"}
    /\ \E o \in Objects :
       /\ thr_holds[t][o] > 0
       /\ thr_holds' = [thr_holds EXCEPT ![t][o] = @ - 1]
       /\ global_rc' = [global_rc EXCEPT ![o] = @ - 1]
       \* decAndTest: if global_rc reaches 0, mark as freed
       /\ freed' = [freed EXCEPT ![o] =
            IF global_rc[o] = 1 THEN TRUE ELSE @]

Why swap vs load is critical

When a swapper replaces the pointer while a loader has an in-flight acquire_tag_ref_, the loader's release_tag_ref_ detects the pointer change and falls back to global_rc decrement. The swapper's CASTransfer compensates by folding the outstanding local_rc into global_rc. This tag-to-global transfer path is the core of atomic_shared_ptr's correctness and is only exercised when swap and load run concurrently.

ABA Recycling

Recycle(t) ==
    /\ EnableRecycle             \* Controlled by enable/disable flag
    /\ pc[t] \in {"idle", "done"}
    /\ \E o \in Objects :
       /\ freed[o] = TRUE       \* freed object
       /\ global_rc[o] = 0
       /\ freed' = [freed EXCEPT ![o] = FALSE]   \* recycled!
       /\ global_rc' = [global_rc EXCEPT ![o] = 1]
       /\ thr_holds' = [thr_holds EXCEPT ![t] = @ \cup {o}]

Sound over-approximation: Recycling allowed for all operations (in practice impossible for compareAndSwap_). If safety is proven under over-approximation, it also holds for the actual program.

Background: Author judged safety as obvious. AI proposed over-approximation modeling; author agreed.

Verified Invariants (7)

#	Invariant	Meaning
1	`MemorySafety`	Pinned object is not freed
2	`NoUseAfterFree`	Objects in `thr_holds` are not freed
3	`GlobalRCNonNeg`	For live objects: `global_rc ≥ 0`
4	`FreedImpliesZeroRC`	If freed then `global_rc = 0`
5	`InstalledNotFreed`	Object pointed by `ptr` is not freed
6	`LocalRCBounded`	`local_rc ≤ number of threads`
7	`TypeOK`	Type invariant

MemorySafety ==
    \A t \in Threads :
        (pc[t] \in {"scan_inc", "scan_leave",
                     "ls_read", "ls_cas", "ls_global",
                     "cas_check", ..., "cas_cleanup"}
         /\ thr_pref[t] /= NULL)
        => freed[thr_pref[t]] = FALSE

Verification Results (no StateConstraint)

Config	Threads	States	Time	Result
scan only	3	40,934	1s	✅ Pass
scan+CAS (no ABA)	2	3,549,304	12s	✅ Pass (complete)
full (CAS+ABA)	2	8,719,367	28s	✅ Pass (complete)
swap+load (no ABA)	2	—	—	ohtaka running
swap+CAS+ABA	2	6.6×10⁹+	18h+	partial, no violation (I/O limited)

C++ ↔ TLA+ ↔ Generated C11 Correspondence

For author's C++ ↔ TLA+ cross-reference and C11 translation review (continues in Layer 2 slides / slides_layer2_en.html)

Variable Mapping

TLA+ Variable	C++ (atomic_smart_ptr.h)	Generated C11 (test_atomic_shared_ptr.c)
`ptr` + `local_rc`	`m_ref` (uintptr_t) upper=ptr, lower=tag	`_Atomic(uintptr_t) g_ref` `get_ptr()` / `get_tag()`
`global_rc[o]`	`o->refcnt` (intrusive atomic)	`_Atomic(uintptr_t) obj_refcnt[NUM_OBJECTS]`
`freed[o]`	delete call	`int obj_freed[NUM_OBJECTS]`
`thr_pref[t]`	`Ref* pref` (local)	`uintptr_t pref` (local)
`thr_rcnt[t]`	`Refcnt rcnt` (local)	`unsigned rcnt` (local)
`thr_holds[t][o]`	`local_shared_ptr`reference count	thread-local `hold` index

Action Mapping

TLA+ Action	C++ Function	Generated C11	memory_order
`AcquireTagRefRead` + `AcquireTagRefCAS`	`acquire_tag_ref_()`	`acquire_tag_ref()`	relaxed → acq_rel
`LoadSharedIncGlobal`	`load_shared_()` (inside)	`load_shared()` (inside) `fetch_add(refcnt, 1)`	relaxed
`ReleaseTagRefCAS` / `ReleaseTagRefGlobal`	`release_tag_ref_()`	`release_tag_ref()`	acq_rel / acq_rel
`CASPreInc` → `CASSwap` → `CASCleanup`	`compareAndSwap_()`	`compare_and_swap()`	relaxed / acq_rel
`StartSwap` → `CASTransfer` → `CASSwap`	`swap()`	`swap_exchange()`	acq_rel
`Reset`	`local_shared_ptr::reset()`	`local_reset()`	acq_rel (decAndTest)

Verification Triangle:
C++ implementation (written by author) ← author cross-references independently → TLA+ spec
TLA+ → generated C11 (produced in independent session without C++ access) → GenMC verification (RC11)
Closing this triangle confirms TLA+ model fidelity.