Chapter 45Optional

Concurrent Separation Logic and Higher-Order Ghost State

Prerequisites. Direct starred prerequisites: Chapter 43, Chapter 44. No later core chapter depends on this route.

Suppose two threads execute the following compare-and-swap loop on one heap cell. Each load is locally safe, and each successful compare-and-swap changes only that cell. $\begin{matrix} ({incr}_{phy}) & \begin{array}{l} rec incr l := \\ let oldv :=! l in \\ if CAS l oldv (oldv + 1) \\ then oldv else incr l . \end{array} \end{matrix}$ The sequential frame rule does not say which thread may temporarily own the shared cell, how the loser of a race recovers its precondition, or which physical instruction performs the abstract increment. These are three different obligations. We solve them in a fixed instance of Iris for HeapLang: invariants control shared physical state, ghost ownership records abstract state, and a logically atomic specification exposes one abstract transition to a client.

The physical race

A HeapLang state is a finite map $σ$ from locations to values. We need only allocation, load, fork, and integer compare-and-swap. Write $⟨ e, σ ⟩ ⟶_{p} ⟨ e^{'}, σ^{'} ⟩$ for one physical reduction. HeapLang’s surface $CAS$ projects the Boolean component of its primitive $CmpXchg$ . At a location $ℓ$ , the two primitive cases are $\begin{matrix} (C A S) & \begin{aligned} ⟨ CmpXchg ℓ v w, σ ⟩ & ⟶_{p} ⟨ (v, true), σ [ℓ \mapsto w] ⟩ & if σ (ℓ) = v, \\ ⟨ CmpXchg ℓ v w, σ ⟩ & ⟶_{p} ⟨ (σ (ℓ), false), σ ⟩ & if σ (ℓ) \neq v . \end{aligned} \end{matrix}$ The comparison and conditional write are one physical step. A preceding load is a different step.

Start with $σ (ℓ) = 5$ . Let both threads load before either executes CAS. Their local values are then both $5$ . The remaining calculation is $\begin{aligned} (5; {CAS}_{1} (5, 6); {CAS}_{2} (5, 6)) & ⟶_{p} (6; {return}_{1} (5); {CAS}_{2} (5, 6)) \\ ⟶_{p} (6; {return}_{1} (5); {retry}_{2}) . \end{aligned}$ The successful CAS changes the cell and returns the old value. The failed CAS changes neither the cell nor the abstract counter; it merely sends the second thread back to the loop. A load–store implementation would instead permit both stores of $6$ , losing one increment.

Exercise 45.1 — The retrying schedule ¶

★☆☆ Continue the displayed schedule until both calls return. Give the physical heap value and the multiset of return values after every successful CAS. Identify the only two physical steps that can represent abstract increments.

Referenced from 3 locations

Write $ℓ \mapsto_{h} v$ for full exclusive ownership of the physical cell $ℓ$ at value $v$ .

Proposition 45.1 — Disjoint parallel ownership is insufficient ¶

Suppose a parallel-composition rule gives each thread a disjoint assertion and both calls require full ownership of the same cell. Its combined precondition is unsatisfiable.

Referenced from 3 locations

Concurrent Separation Logic and Higher-Order Ghost State

Proof of Proposition 45.1 — Disjoint parallel ownership is insufficient

Proof. Full ownership for the two premises requires $(ℓ \mapsto_{h} v_{1}) * (ℓ \mapsto_{h} v_{2}) .$ The two factors would place the same location in disjoint heap fragments, contradicting the definition of separating conjunction. Framing private state around the premises does not change this shared-location contradiction. ◻

The disjoint-concurrency rule is useful when thread footprints are separate. For a shared counter, concurrent separation logic instead transfers the cell through a protected resource invariant. Iris makes the invariant itself a persistent assertion and controls each transfer by masks.

Assertions that may be forgotten or shared

The assertions below are Iris propositions. Separating conjunction retains its resource meaning from chapter 44; internal entailment is written $P ⊢_{I} Q$ , and mutual entailment is $P ⊣ ⊢_{I} Q$ . The assertion $ℓ \mapsto_{h} v$ owns the physical HeapLang cell $ℓ$ with value $v$ . It is exclusive: $\begin{matrix} (P t - e x c l u s i v e) & (ℓ \mapsto_{h} v) * (ℓ \mapsto_{h} w) ⊢_{I} False . \end{matrix}$

Definition 45.2 — Affine and persistent assertions ¶

An assertion $P$ is affine when $P ⊢_{I} ⟨ aff ⟩ P$ , and it is persistent when $P ⊢_{I} ◻ P$ . The affinely modality asserts its body together with an empty owned resource. The persistently modality asserts that its body can be duplicated. Their characteristic laws include $⟨ aff ⟩ P ⊢_{I} emp, ◻ P ⊢_{I} ◻ P * ◻ P, ◻ P ⊣ ⊢_{I} ◻ ◻ P .$ This HeapLang Iris instance is affine: owned resources may be discarded. Affineness does not imply persistence.

Referenced from 2 locations

Concurrent Separation Logic and Higher-Order Ghost State

For example, $ℓ \mapsto_{h} 5$ is affine but not persistent. If it were persistent, duplication followed by (Pt-exclusive) would derive $False$ from a valid one-cell state. A named invariant, by contrast, is persistent. It can be used by both threads because opening the invariant supplies its body only under a mask discipline; it does not duplicate the body.

Exercise 45.2 — Classifying assertions ¶

★☆☆ Classify $True$ , $ℓ \mapsto_{h} v$ , $◻ P$ , and ${inv}_{N} (P)$ as affine, persistent, both, or neither in this affine Iris instance. For every rejected persistence claim, name the resource that duplication would copy.

Referenced from 3 locations

Invariants and the selected update modality

An invariant is allocated in a namespace $N$ , whose set of names is written $↑ N$ . A mask $E$ is a set of enabled invariant names. The assertion ${inv}_{N} (P)$ says that the shared resource satisfies $P$ whenever the invariant is closed. We use only the following fragment of the fancy-update interface.

Definition 45.3 — Fancy updates and invariant access ¶

The fancy update from $E_{1}$ to $E_{2}$ , with postcondition $P$ , is written $| = E_{1}, E_{2} = > P$ . It may perform a frame-preserving ghost update and finishes with mask $E_{2}$ satisfying $P$ . Put $\begin{matrix} (C l o s e) & {close}_{N, E} (P) : = ▹ P - * | = E ∖ ↑ N, E = > True . \end{matrix}$ The selected rules are $P ⊢_{I} | = E, E = > P .$ $\begin{aligned} | = E_{1}, E_{2} = > P * (P - * | = E_{2}, E_{3} = > Q) & ⊢_{I} \\ | = E_{1}, E_{3} = > Q . \end{aligned}$ Invariant allocation satisfies $▹ P ⊢_{I} | = E, E = > {inv}_{N} (P) .$ If $↑ N \subseteq E$ , invariant opening satisfies $\begin{matrix} (I n v) & \begin{aligned} {inv}_{N} (P) & ⊢_{I} | = E, E ∖ ↑ N = > ▹ P * {close}_{N, E} (P) . \end{aligned} \end{matrix}$ Allocation chooses an internal invariant name under $N$ . In the opening line, the second conjunct is the closing obligation. It returns $▹ P$ and re-enables $↑ N$ .

Referenced from 2 locations

Concurrent Separation Logic and Higher-Order Ghost State

The missing namespace in the intermediate mask records that the invariant is open. Consequently the same invariant cannot be opened twice before its closing obligation is discharged. This side condition prevents the invalid calculation ${inv}_{N} (ℓ \mapsto_{h} 5) from yielding (ℓ \mapsto_{h} 5) * (ℓ \mapsto_{h} 5),$ which would contradict exclusivity.

Weakest preconditions connect the resource logic to HeapLang. The assertion ${WP}_{E} e {v . Φ (v)}$ means: if $e$ returns $v$ , then $Φ (v)$ holds, and every reachable non-value state has a physical step. For an expression $e$ that is physically atomic, the mask-changing rule is $\begin{matrix} (W P - A t o m i c) & | = E_{1}, E_{2} = > {WP}_{E_{2}} e {v . | = E_{2}, E_{1} = > Φ (v)} ⊢_{I} {WP}_{E_{1}} e {v . Φ (v)} . \end{matrix}$ This is why the invariant body may be borrowed around one load or CAS, but not around the whole retry loop.

Exercise 45.3 — Why the mask shrinks ¶

★★☆ Let $P : = ℓ \mapsto_{h} 5$ . Attempt to use the invariant-opening rule twice without closing the first access. State the mask required by the second opening and the mask actually available. Then show how closing the first access makes a later second opening admissible.

Referenced from 3 locations

Ghost authority records an abstract counter

An invariant can hide the physical cell, but a client may need a stable fact about an abstract state. Ghost state supplies such facts without adding a runtime cell. We use a single authoritative-counter resource.

Definition 45.4 — Authoritative counter resource ¶

Let $M = N_{⊥, ⊤} \times N$ . The first component is either no authority $⊥$ , a natural number, or the invalid collision $⊤$ . Combining two elements takes the unique non-bottom authority when there is one, yields $⊤$ when there are two, and takes the maximum of the second components. An element $(a, n)$ is valid exactly when $a = ⊥$ , or $a = m \in N$ and $n \leq m$ . Its duplicable core is $(⊥, n)$ . We abbreviate $∙ m = (m, 0), \circ n = (⊥, n) .$ At ghost name $γ$ , ownership is written ${own}_{γ} (a)$ .

Referenced from 3 locations

Two calculations do the work. First, $\begin{matrix} (A u t h - a g r e e) & ∙ m \cdot \circ n = (m, n) is valid ⟹ n \leq m . \end{matrix}$ Second, for $n \leq m$ , the simultaneous increment is a frame-preserving update: $\begin{matrix} (A u t h - i n c) & ∙ m \cdot \circ n ⇝_{fp} ∙ (m + 1) \cdot \circ (n + 1) . \end{matrix}$ Indeed, any compatible frame has no authority and has fragment index $k \leq m$ . After the update, $k \leq m + 1$ still holds; the displayed new fragment also satisfies $n + 1 \leq m + 1$ . Thus every compatible frame remains compatible. Updating only the fragment to $n + 1$ would fail when $m = n$ .

A shared-counter invariant may now tie the physical and abstract states: $\begin{matrix} (C o u n t e r - i n v) & I (ℓ, γ) : = \exists m \in Z_{\geq 0} . (ℓ \mapsto_{h} m) * {own}_{γ} (∙ m) . \end{matrix}$ A client holding ${own}_{γ} (\circ n)$ knows, after the invariant is opened, that the physical counter is at least $n$ . The fragment is persistent because its core is itself; the authority remains exclusive inside the invariant.

Proposition 45.5 — Fragment lower bound and successful update ¶

Suppose an admissible atomic opening of ${inv}_{N} (I (ℓ, γ))$ reveals witness $m$ , while the client holds ${own}_{γ} (\circ n)$ . Then $n \leq m$ . If the physical CAS changes $m$ to $m + 1$ , the invariant can be closed at witness $m + 1$ , and the client can retain ${own}_{γ} (\circ (n + 1))$ .

Referenced from 2 locations

Concurrent Separation Logic and Higher-Order Ghost State

Proof of Proposition 45.5 — Fragment lower bound and successful update

Proof. The opened invariant supplies $ℓ \mapsto_{h} m * {own}_{γ} (∙ m)$ . Compatibility with the client fragment gives $n \leq m$ by (Auth-agree). The physical CAS produces $ℓ \mapsto_{h} (m + 1)$ . Apply (Auth-inc) to the two ghost components, return $∙ (m + 1)$ with the new points-to assertion to $I (ℓ, γ)$ , and retain $\circ (n + 1)$ outside. ◻

Exercise 45.4 — Simultaneous authority update ¶

★★☆ Prove (Auth-inc) from the compatibility definition. Then take $m = n$ and give the frame that refutes $\begin{aligned} ∙ m \cdot \circ n & ⇝_{fp} \\ ∙ m \cdot \circ (n + 1) . \end{aligned}$

Referenced from 3 locations

Saving a proposition as ghost data

The counter algebra stores natural numbers. Higher-order protocols also need ghost names whose payload is itself an Iris proposition.

Definition 45.6 — Saved proposition ¶

The assertion ${saved}_{γ}^{d} (P)$ owns share $d$ of ghost name $γ$ , whose payload is the Iris proposition $P$ . A discarded share, written ${saved}_{γ}^{◻} (P)$ , is persistent. The payload is stored under one logical later step.

Referenced from 2 locations

Concurrent Separation Logic and Higher-Order Ghost State

The later is not decorative. Without it, a proposition could inspect an unguarded ghost copy of itself and recreate the circularity that guarded recursion was introduced to prevent.

Proposition 45.7 — Saved-proposition agreement ¶

${saved}_{γ}^{d_{1}} (P) * {saved}_{γ}^{d_{2}} (Q) ⊢_{I} ▹ (P ⊣ ⊢_{I} Q) .$ Full ownership may be frame-preservingly updated to save any new proposition; the update rule requires that full share. A discarded persistent share alone does not satisfy the update premise, although saved_prop_unpersist can recover a fractional share from it.

Referenced from 2 locations

Concurrent Separation Logic and Higher-Order Ghost State

Proof of Proposition 45.7 — Saved-proposition agreement

Proof. The saved-proposition construction places $Next (P)$ in an agreement resource. Separating conjunction requires compatible shares, and compatibility yields agreement of their $Next$ payloads, which is exactly the displayed later equivalence. A full share has no compatible external share, so replacement preserves every frame. A discarded share is itself a compatible external witness and blocks such replacement. This reconstructs the artifact lemmas saved_prop_agree, saved_prop_update, and persistence of discarded ownership. The exact source is iris/base_logic/lib/saved_prop.v:148–226 at the pinned artifact revision. ◻

One abstract increment inside a retry loop

The loop in (incr_ phy) is not one physical step. Its useful client interface is instead logically atomic. The quantifier in the precondition below binds $v$ across the postcondition and lets the client choose that current abstract state when it opens its own invariant.

Definition 45.8 — Logically atomic increment contract ¶

For a location $ℓ$ , the contract is $\begin{matrix} (I n c r - A U) & ⟨ ⟨ \forall v \in Z . ℓ \mapsto_{h} v ⟩ ⟩ {incr}_{phy} ℓ @ \emptyset ⟨ ⟨ ℓ \mapsto_{h} (v + 1) ∣ RET v ⟩ ⟩ . \end{matrix}$ Operationally, using the contract means supplying a continuation that may either abort with the original $ℓ \mapsto_{h} v$ , or commit with $ℓ \mapsto_{h} (v + 1)$ and return $v$ . The empty mask is part of this exact physical-heap statement.

Referenced from 2 locations

Concurrent Separation Logic and Higher-Order Ghost State

Theorem 45.9 — The physical increment is logically atomic ¶

For every HeapLang location $ℓ$ , the recursive value ${incr}_{phy}$ of (incr_ phy) satisfies (Incr-AU).

Referenced from 4 locations

Proof of Theorem 45.9 — The physical increment is logically atomic

Proof. This reconstructs incr_phy_spec from iris_heap_lang/lib/increment.v:22–41 at the pinned artifact revision. The proof uses Löb induction for the recursive retry. At each load it opens the client’s atomic update, obtains $ℓ \mapsto_{h} v$ , performs the load, and uses the abort continuation to restore the same atomic update. No abstract step has occurred.

After the pure arithmetic, bind the CAS as the next atomic expression and open the atomic update again at some current value $w$ . There are two cases.

If the loaded value equals $w$ , the success rule in (CAS) changes the physical cell from $w$ to $w + 1$ . Use the commit continuation with $ℓ \mapsto_{h} (w + 1)$ ; it supplies the requested postcondition at return value $w$ . This CAS is the abstract transition $w ⟶_{a} w + 1$ .
If the loaded value differs from $w$ , the failure rule leaves $ℓ \mapsto_{h} w$ unchanged. Use the abort continuation to reconstruct the atomic update, then apply the Löb hypothesis to the recursive call. This branch performs no abstract transition.

Every opening is closed around one physically atomic instruction. The two branches exhaust integer equality, so the contract is restored or committed at every CAS. ◻

The proof separates three clocks:

level	event	established fact
physical	load or CAS in HeapLang	one reduction $⟶_{p}$
abstract	successful CAS selected by the proof	exactly one transition $v ⟶_{a} v + 1$ and return of $v$
client	invariant allocation, two calls, parallel composition	a weakest precondition and, by adequacy, safety

Logical atomicity therefore does not say that the entire call is one physical instruction. It says that a client may reason as if one abstract update occurred at the successful CAS.

Exercise 45.5 — Abort or commit ¶

★★☆ For each of load, successful CAS, and failed CAS, state the points-to assertion obtained when the atomic update is opened, the closing continuation used, and the atomic update returned to the proof. Explain why committing at the load would give the wrong return value after interference.

Referenced from 3 locations

The concrete client theorem

The pinned artifact next introduces an atomic-heap interface with an abstract load and CAS, defines a second value $incr$ over that interface, and proves its logically atomic specification. Its client is exactly $\begin{matrix} (C l i e n t) & incr_client x : = let ℓ := ref x in incr ℓ ∥ incr ℓ . \end{matrix}$ The calls here are $incr$ , not ${incr}_{phy}$ . Conflating those names would import a client theorem at the wrong program.

Theorem 45.10 — Concrete two-call client safety ¶

For every integer $x$ , the pinned HeapLang development proves $\begin{matrix} (C l i e n t - s a f e) & heap_inv - * {WP}_{⊤} incr_client x {u . True} . \end{matrix}$ Here $heap_inv$ is the persistent invariant required by the artifact’s atomic-heap instance, and $⊤$ denotes the ambient mask used by the unannotated artifact weakest precondition.

Referenced from 5 locations

Proof of Theorem 45.10 — Concrete two-call client safety

Proof. The artifact proof is iris_heap_lang/lib/increment.v:178–196. It proceeds as follows. Consume $heap_inv$ as a persistent assumption and allocate $ℓ$ with $ℓ \mapsto_{h} x$ . Allocate the client invariant ${inv}_{N_{client}} (\exists z \in Z . ℓ \mapsto_{h} z) .$ From the atomic-heap theorem incr_spec, establish the persistent assertion $◻ {WP}_{⊤} incr ℓ {u . True} .$ To discharge its atomic precondition, open the client invariant, choose its current integer $z$ , and supply $ℓ \mapsto_{h} z$ . Whether the call aborts or commits, close the invariant with the returned points-to assertion; the postcondition $True$ requires no retained result.

The parallel-composition rule duplicates the persistent weakest precondition and assigns one copy to each thread. After both threads return, discard their results and prove $True$ . ◻

Corollary 45.11 — Adequacy boundary ¶

In the pinned HeapLang instance, every thread in every reachable pool of the closed client is either a value or has a physical reduction. If the main thread returns, its return value satisfies $True$ .

Referenced from 5 locations

Proof of Corollary 45.11 — Adequacy boundary

Proof. Apply heap_adequacy from iris_heap_lang/adequacy.v:25–49 to theorem 45.10. For $primitive_atomic_heap$ , the interface’s $heap_inv$ is $True$ ; weakening turns its client proof into the $inv_heap_inv - *$ premise required by heap_adequacy. The resulting adequacy record supplies the postcondition for a completed main expression and the not-stuck clause for every thread in every reachable pool. ◻

The corollary is a safety statement. It does not prove that either retry loop terminates, that the scheduler is fair, that the final counter is $x + 2$ , or that the program remains correct under a weak-memory semantics. Its postcondition intentionally forgets both return values and the allocated cell.

Exercise 45.6 — Read the exact client guarantee ¶

★☆☆ For each of termination, absence of stuck reachable threads, final counter value $x + 2$ , fairness, and returned pair $(x, x + 1)$ in some order, say whether it follows from theorem 45.10 and corollary 45.11. Quote the exact clause that supports every positive answer.

Referenced from 3 locations

A paired operation is a different shape

An exchanger waits for two offers and gives each caller the other’s value. A single matched pair has the abstract transition $\begin{matrix} (E x c h a n g e) & (offer (a), offer (b)) ⟶_{a} (return (b), return (a)) . \end{matrix}$ This small example marks a boundary of per-call deterministic atomic operations.

Proposition 45.12 — No independent deterministic exchanger steps ¶

Assume an offer has no hidden partner parameter and that each call is modeled by an independent deterministic unary function $f$ on its own argument. No such $f$ implements (Exchange) for all distinct values.

Referenced from 3 locations

Concurrent Separation Logic and Higher-Order Ghost State

Proof of Proposition 45.12 — No independent deterministic exchanger steps

Proof. Fix $a$ and choose distinct partners $b \neq c$ . The first exchange requires $f (a) = b$ , while the second requires $f (a) = c$ . Determinism gives $b = c$ , a contradiction. A sound abstract specification must therefore represent the shared matching protocol or a paired transition; it cannot split the behavior into two partner-free unary functions. ◻

This contrast does not import a generalized linearizability theorem. The chapter has established the pinned Iris logically atomic specifications and their client-safety consequence only. It has not introduced module saturation, possibility sets, liveness, fairness, or a weak-memory model.

Exact source and evidence boundary

The invariant, fancy-update, weakest-precondition, and authoritative-counter rules used above follow the official Iris lecture notes: persistently in Section 7; invariants and the double-opening obstruction in Sections 8.1–8.2; the authoritative counter construction in Section 8.7; and weakest preconditions and fancy updates in Sections 14.1–14.3 [BB23]. The resource-algebra and invariant construction is proved semantically in Sections 3–8 of [JKJ^+18]; the earlier monoids-and-invariants paper gives the concurrent-separation-logic origin of the same separation of resources and protocols [JSS^+15]. O’Hearn’s Section 3 isolates disjoint concurrency and Sections 4–5 introduce resource-mediated interaction and its proof rules [O'H07]. Brookes gives the dynamic trace semantics in Section 4 and semantic equivalence in Section 5, presents the proof system in Section 8, proves soundness in Section 12, and derives absence of races in Section 13 [Bro07]. Those results explain proposition 45.1; their command language and trace-validity theorem are not substituted for HeapLang or Iris adequacy.

The program theorems are checked against the pinned Iris artifact at commit 832a5cd28048a8af53a7eddb1f4d4bb5c002efe0. The exact ledger is:

${incr}_{phy}$ .: Declaration incr_phy is at iris_heap_lang/lib/increment.v:15–20.
Physical atomic contract.: Declaration incr_phy_spec and its complete proof are in the same file at lines 22–41.
Atomic-heap bridge.: Declarations incr and incr_spec are in the same file at lines 51–57 and 104–127.
Concrete client.: Declaration incr_client is in the same file at lines 170–173; incr_client_safe and its proof are at lines 175–196.
Invariant interface.: Persistence, allocation, allocation-and-opening, and access are in iris/base_logic/lib/invariants.v:97–133; the displayed access rule is inv_acc at lines 129–133.
Higher-order ghost payload.: Definition saved_prop_own, persistence, allocation, agreement, and update are in iris/base_logic/lib/saved_prop.v:148–226; agreement is at lines 201–203 and full update at lines 216–218.
Adequacy.: Declarations adequate and adequate_tp_safe are in iris/program_logic/, file adequacy.v, lines 181–215. HeapLang’s heap_adequacy is in iris_heap_lang/adequacy.v:25–49.

The file iris_heap_lang/lib/increment.v has SHA-256 digest 6d18f23c064d67b8ceaf6241516f43287db3c6a181ae856d2b787003920d3276. The proof reconstructions preserve the exact program names, masks, preconditions, postconditions, and theorem boundaries. The Kappa supplement checks a finite operational abstraction of their branch structure; it is not a replacement for the Rocq proof.

Suggested first pass.

Begin with exercise 45.7, exercise 45.8, exercise 45.9; then use the exchanger problem and executable project to test the boundary. No problem in this optional seminar is a prerequisite for a later chapter.

Exercise 45.7 — Reconstructing the atomic proof ¶

★★☆ Write the proof state of theorem 45.9 immediately before the load, immediately after closing the load, and in both CAS branches. At each state record the current mask, the points-to assertion, the abort continuation, the commit continuation, and whether an abstract transition has occurred.

Referenced from 4 locations

Exercise 45.8 — A lower-bound client ¶

★★☆ Put (Counter-inv) under a namespace and give a client a fragment ${own}_{γ} (\circ n)$ . Derive the lower bound on the physical cell when the invariant is open. Show the simultaneous physical and ghost update for one successful increment, then close the invariant and state the client’s new fragment.

Referenced from 4 locations

Exercise 45.9 — Checking the pinned boundary ¶

★☆☆ Use the exact ledger to locate incr_phy_spec, incr_spec, and incr_client_safe. Record the program, mask, precondition, return value, and postcondition of each theorem. Explain why replacing incr by incr_phy in the client theorem is not justified by textual similarity of the two recursive values.

Referenced from 4 locations

Exercise 45.10 — The exchanger boundary ¶

★★☆ Extend proposition 45.12 to nondeterministic independent relations. Give a relation broad enough to contain every possible partner, then explain why membership alone no longer guarantees that two simultaneous returns are paired with one another. State the extra shared-state relation that a useful atomic specification must retain.

Referenced from 3 locations

Exercise 45.11 — Increment trace checker ¶

★★★ Practical project.iris-increment-trace-checker Implement the finite physical machine from section 45.1 in Kappa. A thread is ready, has loaded an integer, or has returned an integer. A successful CAS must increment both the physical counter and an abstract commit count; a failed CAS must change neither and must return the thread to ready. Check an uncontended call, the two possible winning orders, a failed CAS followed by retry, a load without commit, rejection of an inconsistent authority fragment, rejection of a double-opened namespace, and the paired exchanger transition. Print the eight case results followed by

All 8 Chapter 45 corpus cases passed.

Referenced from 4 locations