Chapter 87Optional

Compositional Linearizability and Modular Concurrent Objects

Prerequisites. Direct starred prerequisites: Chapter 86. No later core chapter depends on this route.

Two exchanger calls overlap. Thread $0$ offers $2$ and returns $4$ ; thread $1$ offers $4$ and returns $2$ . No ordering of two independent deterministic atomic exchanges explains both results: the first ordered operation would have to return before the second offer was available. A paired specification can perform the two calls and the two returns as one concurrency class. The problem is to expose that behavior as a black box without losing composition.

Finite traces make the obstruction calculable

Fix a finite number $T : N$ of threads and put $Name (T) : = {i : N ∣ i < T} .$ An effect signature $E$ assigns to each result type $A$ a type $E (A)$ of operations returning values of type $A$ . A thread event is $i : call (m) or i : ret (m, v), i : Name (T), m : E (A), v : A .$

Definition 87.1 — Sequentially consistent traces ¶

An active map $a$ assigns to each thread either no operation or one package $⟨ A, m : E (A) ⟩$ . The judgment $SeqCons (a, p)$ is generated from the end of a finite trace by

SeqCons (a, [])

CL-Seq-nil

a (i) = none

a^{'} (i) = some ⟨ A, m ⟩

\forall j \neq i . a (j) = a^{'} (j)

SeqCons (a^{'}, p)

SeqCons (a, i : call (m) :: p)

CL-Seq-call

a (i) = some ⟨ A, m ⟩

a^{'} (i) = none

\forall j \neq i . a (j) = a^{'} (j)

SeqCons (a^{'}, p)

SeqCons (a, i : ret (m, v) :: p)

CL-Seq-ret

A complete history begins under the everywhere-empty active map and ends under the everywhere-empty active map. A pending history may instead be completed by appending matching returns or by deleting pending calls. Every comparison in this chapter applies the same completion choice to its two sides.

Referenced from 3 locations

Compositional Linearizability and Modular Concurrent Objects

The trace $0 : call (inc); 0 : ret (inc, 1); 1 : call (get); 1 : ret (get, 1)$ satisfies CL-Seq-call, CL-Seq-ret, CL-Seq-call, and CL-Seq-ret in that order. A return by thread $1$ before its call fails the first premise of CL-Seq-ret.

Definition 87.2 — The frozen LTS specification ¶

A specification is an element $V : {Spec}_{T} (E)$ . Its data are a state type $S_{V}$ , an initial state $s_{V}$ , and a labelled relation $s {Step}_{V} (e) s^{'} (e : Name (T) \times Event (E)) .$ It also contains a proof that every trace from $s_{V}$ satisfies $SeqCons$ under the empty active map. Write $Tr (V)$ for its finite traces from $s_{V}$ .

Referenced from 3 locations

The sequential-consistency proof is data in the card because later linking must not manufacture a return for a call that never occurred. An arbitrary labelled graph is therefore not a ${Spec}_{T} (E)$ .

Programs, modules, and linking

The LHL artifact defines its own program tree. It does not import the interaction-tree library of chapter 86.

Definition 87.3 — The artifact-local program and module interface ¶

For an underlay signature $E$ , programs are given by ${Prog}_{E} (A) ::= Return (a) ∣ Tau (p) ∣ Vis (m, k),$ where $a : A$ , $m : E (B)$ , and $k : B \to {Prog}_{E} (A)$ . An implementation $M : Impl (E, F)$ maps each $m : F (A)$ to a program $M (m) : {Prog}_{E} (A)$ . The displayed grammar denotes the greatest fixed point of the operator $F (X) : = A + X + \sum_{B : Type} E (B) \times (B \to X) .$ Consequently its constructors are observations, not a finite syntax induction principle. For example, guarded corecursion defines $spin : {Prog}_{E} (A)$ by $spin = Tau (spin)$ .

The bridge from definition 86.1 is the constructor-preserving map $Return \mapsto Ret, Tau \mapsto Tau, Vis \mapsto Vis .$ It preserves finite traces by induction on the observer budget. It does not identify the two libraries or transfer a Rocq theorem between them.

For a relation $S$ on programs, the artifact-local one-layer relation $EuttF (S)$ matches equal returns, matches equal visible operations with $S$ -related continuations, and has the three silent clauses

S (p, q)

EuttF (S, Tau (p), Tau (q))

EuttF (S, p, q)

EuttF (S, Tau (p), q)

EuttF (S, p, q)

EuttF (S, p, Tau (q))

Write $p \approx_{P} q$ for the greatest fixed point of this monotone operator. It is termination sensitive: the two asymmetric clauses remove a finite silent prefix inside one inductive layer, but do not equate $spin$ with a return. For modules $M, N : Impl (E, F)$ , the displayed notation $M \approx_{P} N$ below denotes its pointwise lifting: $M (m) \approx_{P} N (m)$ for every result type $A$ and operation $m : F (A)$ .

The artifact makes substitution productive by defining it mutually with a continuation operation. For $k : B \to {Prog}_{F} (A)$ and $p : {Prog}_{E} (B)$ , the complete observation equations are $\begin{aligned} {subst}_{M} (Return (a)) & : = Return (a), \\ {subst}_{M} (Tau (p)) & : = Tau ({subst}_{M} (p)), \\ {subst}_{M} (Vis (m, k)) & : = Tau ({bindSubst}_{M} (k, M (m))), \\ {bindSubst}_{M} (k, Return (b)) & : = Tau ({subst}_{M} (k (b))), \\ {bindSubst}_{M} (k, Tau (p)) & : = Tau ({bindSubst}_{M} (k, p)), \\ {bindSubst}_{M} (k, Vis (u, h)) & : = Vis (u, λ x . {bindSubst}_{M} (k, h (x))) . \end{aligned}$ Every recursive call is guarded by $Tau$ or lies in a visible continuation. The administrative silent steps are why the module laws below hold at $\approx_{P}$ rather than by constructor equality. These operations are local to the artifact and do not use $interp$ from chapter 86.

Referenced from 5 locations

Running $M : Impl (E, F)$ above $V : {Spec}_{T} (E)$ produces the linked specification $V ▹ M : {Spec}_{T} (F)$ . An overlay call starts $M (m)$ for the selected thread. A visible operation of $M (m)$ becomes an underlay call and return in $V$ . A program $Tau$ changes only the thread state. The next four rules exhibit the thread-local cases.

q (i) = Idle

q i : call (m) q [i \mapsto Cont (m, M (m))]

CL-Overlay-call

q (i) = Cont (m, Return (v))

q i : ret (m, v) q [i \mapsto Idle]

CL-Overlay-ret

q (i) = Cont (m, Vis (u, k))

s {Step}_{V} (i : call (u)) s^{'}

(q, s) ⟶_{CL} (q [i \mapsto UCall (m, u, k)], s^{'})

CL-Underlay-call

q (i) = UCall (m, u, k)

s {Step}_{V} (i : ret (u, v)) s^{'}

(q, s) ⟶_{CL} (q [i \mapsto Cont (m, k (v))], s^{'})

CL-Underlay-ret

The silent case sends $Cont (m, Tau (p))$ to $Cont (m, p)$ without changing $s$ . Thus no scheduler object is part of the signature: one transition chooses one thread name and applies its matching rule.

Definition 87.4 — Vertical and horizontal composition ¶

Let $M : Impl (E, F)$ and $N : Impl (F, G)$ . Vertical module composition substitutes $M$ into the upper program $N (g)$ : $\begin{aligned} (M; N) (g) & : = {subst}_{M} (N (g)), \\ (M; N) (g) & : {Prog}_{E} (A) (g : G (A)) . \end{aligned}$ The identity module is $idM (m) : = Vis (m, Return)$ .

For tagged signatures $E_{1} + E_{2}$ and specifications $V_{i} : {Spec}_{T} (E_{i})$ over the same finite thread set, the horizontal tensor $V_{1} \otimes V_{2} : {Spec}_{T} (E_{1} + E_{2})$ has state ${Active}_{T} (E_{1} + E_{2}) \times S_{V_{1}} \times S_{V_{2}} .$ On a left call by $i$ , the active entry for $i$ must be empty, becomes the left-tagged operation, and the first component specification takes the corresponding call step; the right state is unchanged. A left return requires that same left-tagged active operation and clears the entry. The two right-tagged clauses exchange the component roles. All active entries for $j \neq i$ are preserved. This shared active map rules out a call in one component followed by a return through the other, even though a thread may use either component at different times. The tensor $M_{1} \otimes M_{2}$ dispatches on operation tags and maps every event generated by the chosen module through the same tag.

Referenced from 2 locations

Compositional Linearizability and Modular Concurrent Objects

Lemma 87.5 — Module and linking algebra ¶

Let the data have types $V : {Spec}_{T} (E), M : Impl (E, F), N : Impl (F, G), L : Impl (G, H) .$ The local weak equivalence satisfies $\begin{aligned} idM; M & \approx_{P} M, & M; idM & \approx_{P} M, \\ (M; N); L & \approx_{P} M; (N; L), \\ (V ▹ M) ▹ N & ≅ V ▹ (M; N), \\ (V_{1} \otimes V_{2}) ▹ (M_{1} \otimes M_{2}) & = (V_{1} ▹ M_{1}) \otimes (V_{2} ▹ M_{2}) \end{aligned}$ where the tensor equation additionally quantifies over $V_{i} : {Spec}_{T} (E_{i})$ and $M_{i} : Impl (E_{i}, F_{i})$ ; the signature sums are tagged. The relation $≅$ is linked-LTS isomorphism up to renaming the nested thread and product states. There is deliberately no law $V ▹ idM = V$ : the left side is the identity saturation $K (V)$ and exposes linearization brackets absent from $V$ .

Referenced from 6 locations

Compositional Linearizability and Modular Concurrent Objects

Proof of Lemma 87.5 — Module and linking algebra

Proof. For the module unit and associativity laws, coinduct on the local program. Return and silent forms are immediate. At a visible form, substitution expands one local bind; its return, silent, and visible cases establish the two unit equations and reassociate the nested substitutions. This produces $\approx_{P}$ because only a finite administrative silent prefix can differ.

For linking compatibility, relate the nested linked state containing the outer continuation to the single linked state containing its substituted program. The overlay rules match directly. An underlay call/return pair in the nested state corresponds to the visible substitution clause in the single state. This establishes the displayed $≅$ without erasing an overlay bracket.

For tensor, induct on a finite execution. A left-tagged event changes only the first component on both sides; a right-tagged event changes only the second. The shared active-map premise preserves the selected tagged operation until its matching return, and every unselected entry is unchanged. These facts exhaust the transition relation and preserve global $SeqCons$ . ◻

Exercise 87.2 ¶

★★☆ Prove the two module unit laws of lemma 87.5 for one visible program $Vis (m, k)$ . Expand local substitution and bind, then match the returned continuation pointwise. Finally exhibit a two-thread trace of $K (V) = V ▹ idM$ whose two overlay calls occur before either underlay return, explaining why this does not prove $V ▹ idM = V$ .

Referenced from 3 locations

Identity saturation determines linearizability

The direction of $Ref$ is fixed by the trace inclusion: the concrete $V^{'}$ occurs first. Reversing the arguments would allow a concrete object to add behaviors not admitted by its specification.

Theorem 87.7 — Observational refinement and locality ¶

Let $V_{E}^{'}, V_{E} : {Spec}_{T} (E), M : Impl (E, G) .$ If $Lin (V_{E}^{'}, V_{E})$ , then $Ref (V_{E}^{'} ▹ M, V_{E} ▹ M) .$ For tagged signatures over the same finite thread set, with $V_{i}^{'}, V_{i} : {Spec}_{T} (E_{i})$ , $Lin (V_{1}^{'} \otimes V_{2}^{'}, V_{1} \otimes V_{2}) ⟺ Lin (V_{1}^{'}, V_{1}) \land Lin (V_{2}^{'}, V_{2}) .$

Referenced from 4 locations

Proof of Theorem 87.7 — Observational refinement and locality

Proof. For observational refinement, take a trace of $V_{E}^{'} ▹ M$ . Projecting away the program states yields a trace of $V_{E}^{'}$ . The hypothesis places that trace in $K (V_{E}) = V_{E} ▹ idM$ . Reinsert the same $M$ transitions. Linking compatibility gives $(V_{E} ▹ idM) ▹ M ≅ V_{E} ▹ (idM; M) ≅ V_{E} ▹ M,$ where the last step is the module unit law. Thus the reinserted execution is an execution of $V_{E} ▹ M$ ; no equation $K (V_{E}) = V_{E}$ is used.

For locality from right to left, project a tensor trace to its left and right tags. The two hypotheses linearize the projections independently. Their shuffle preserves per-thread order because the shared active map permits at most one tagged operation of a thread at a time. The tensor clause of lemma 87.5 reconstructs a trace of $K (V_{1} \otimes V_{2})$ .

For the reverse implication, take a trace of $V_{1}^{'}$ and tensor it with the empty trace of $V_{2}^{'}$ . Tensor linearizability and left projection give $Lin (V_{1}^{'}, V_{1})$ . The right result follows by exchanging the two product projections; this exchange preserves the trace, completion, and thread-order hypotheses. ◻

Theorem 87.8 — Horizontal and vertical composition ¶

For $i \in {1, 2}$ , let $V_{E_{i}}^{'} : {Spec}_{T_{i}} (E_{i})$ , $M_{i} : Impl (E_{i}, F_{i})$ , and $V_{F_{i}} : {Spec}_{T_{i}} (F_{i})$ , where $T_{1} = T_{2} = T$ and both signature sums are tagged. Write $V_{i}^{'} : = V_{E_{i}}^{'}$ and $V_{i} : = V_{F_{i}}$ . If $Lin (V_{1}^{'} ▹ M_{1}, V_{1})$ and $Lin (V_{2}^{'} ▹ M_{2}, V_{2})$ , then $Lin ((V_{1}^{'} \otimes V_{2}^{'}) ▹ (M_{1} \otimes M_{2}), V_{1} \otimes V_{2}) .$ For the vertical statement, let $\begin{aligned} V_{E} & : {Spec}_{T} (E), & M_{E} & : Impl (E, F), \\ V_{F} & : {Spec}_{T} (F), & M_{F} & : Impl (F, G), \\ V_{G} & : {Spec}_{T} (G) . \end{aligned}$ If $Lin (V_{E} ▹ M_{E}, V_{F})$ and $Lin (V_{F} ▹ M_{F}, V_{G})$ , then $Lin (V_{E} ▹ (M_{E}; M_{F}), V_{G}) .$

Referenced from 5 locations

Proof of Theorem 87.8 — Horizontal and vertical composition

Proof. The tensor equation in lemma 87.5, followed by the two directions of theorem 87.7, gives the horizontal claim. For the vertical claim, apply observational refinement to the first hypothesis with client $M_{F}$ . Compose the resulting trace inclusion with the second hypothesis, then reassociate linking by lemma 87.5. The right-hand specification is $K (V_{G})$ , as required by the definition of the displayed linearizability judgment. ◻

Atomic, set, and interval boundaries

For an atomic specification, each call is immediately followed by its return. Then an execution of $K (V)$ chooses one point between the overlay call and return at which the atomic transition occurs. Hence $Lin (-, V)$ specializes to Herlihy–Wing linearizability, with the completion convention of definition 87.1.

The exchanger trace $\begin{aligned} 0 : & call (exch (2)); 1 : call (exch (4)); \\ 0 : & ret (exch (2), 4); 1 : ret (exch (4), 2) \end{aligned}$ has no atomic linearization. If thread $0$ is first, its return $4$ depends on thread $1$ ’s later offer. If thread $1$ is first, its return $2$ depends on thread $0$ ’s later offer. A paired set step sees both offers and returns the crossed pair.

Exercise 87.3 ¶

★★☆ Enumerate the two total orders of the exchanger operations. For each order, write the first return required by a deterministic atomic specification and show why the required offered value is unavailable at that point.

Referenced from 4 locations

Theorem 87.9 — Restricted set specialization ¶

Fix a finite history $H$ and a particular partition $π = (C_{1}, \dots, C_{n})$ into nonempty concurrency classes. Suppose each class contains at most one operation per thread, the class order respects real-time and per-thread order, and both the set-sequential and linked-LTS readings use the same pending-call completion. Let $V_{set}$ be the ordinary event-labelled LTS whose traces are exactly the invocation-then-response sequentializations admitted by those classes. Then $(H, π)$ is accepted by the set-sequential specification if and only if the event trace of $H$ lies in $K (V_{set})$ through a linked execution whose underlay trace is one of the sequentializations determined by $π$ .

Referenced from 6 locations

Proof of Theorem 87.9 — Restricted set specialization

Proof. From left to right, choose the invocation and response orders supplied by the set-sequential witness for each $C_{q} = {o_{q, 1}, \dots, o_{q, r_{q}}}$ . In $K (V_{set})$ , emit the overlay calls in their history order, take the individual event-labelled underlay call/return steps in the chosen class sequentialization, and then emit the corresponding overlay returns in their history order. Nonemptiness and the at-most-one-operation condition keep every thread state single-valued. Real-time and per-thread order show that concatenating these segments preserves $SeqCons$ .

From right to left, use the stipulated underlay witness belonging to $π$ . Its successive class sequentializations are traces of $V_{set}$ ; erase the identity-module brackets and read each segment back as $C_{q}$ . The thread-state invariant and the hypotheses on $π$ give single-valued thread states, real-time order, and per-thread order. Apply the shared completion convention to pending final calls. This reconstructs an accepted set-sequential execution for the same fixed partition, rather than silently replacing $π$ by an existentially chosen grouping. ◻

Deleting the at-most-one-operation condition invalidates the reverse construction: one thread state cannot contain two active operations. Allowing an empty class invalidates the forward construction because it contributes no event-labelled underlay segment.

Exercise 87.4 ¶

★★★ Apply theorem 87.9 to the two-operation exchanger class. Construct both directions explicitly. Then put two operations of thread $0$ in the same class and identify the exact thread-state invariant that fails.

Referenced from 3 locations

Interval-sequential specifications are different. An operation may influence several alternating invocation and response classes. A one-shot write-snapshot can therefore return a set reflecting an interval of overlap rather than one atomic or set transition. This chapter uses that example only under its one-shot and blocking assumptions; the restricted set theorem does not imply the interval result.

Suggested first pass.

None of these problems is a prerequisite. Begin with exercise 87.1 and exercise 87.3; for the practical sequence, complete stages 1–3 before the two composition checks.

Exercise 87.5 ¶

★★★ Reconstruct both directions of locality for two one-bit registers over the same two-thread set and tagged operation signatures. Give the two trace projections, show that each preserves completion and per-thread order, and interleave the two linearized projections into a tensor trace. Use the shared active map to exclude overlapping left and right operations by one thread.

Referenced from 3 locations

Exercise 87.6 ¶

★★☆ Give a one-shot write-snapshot history in which one operation overlaps two others. Show that no atomic point yields its returned set, then write the three interval classes that do. Do not apply theorem 87.9: explain which single-class premise is absent.

Referenced from 3 locations

Exercise 87.7 ¶

★★★ Practical project.compositional-lts-checker Implement in Kappa a parser for the supplied finite LTS fixtures and a breadth-first trace-inclusion checker. Maintain the invariant that the queue is ordered first by depth and then by thread, tag, and value. Stage 1 checks the atomic counter through depth $6$ ; stage 2 reports the first four-event atomic-exchanger counterexample; stage 3 accepts the paired-set exchanger through depth $4$ ; stage 4 implements horizontal composition; stage 5 checks two counters through depth $6$ . The exact summary lines are atomic-counter: PASS depth=6 (bounded), the four-event exchanger failure, exchanger-vs-paired-set: PASS depth=4 (bounded), and two-counter-horizontal: PASS depth=6 (bounded). Reversing the thread tie order must change the reported first counterexample and fail the canonical-trace test.

Referenced from 4 locations

Sources. The identity-saturation definition and Theorems 4–6 are frozen to the LTS presentation of Hatti, Oliveira Vale, Wang, Feng, and Shao. The more general game-semantic account of Oliveira Vale, Shao, and Chen supplies provenance and the Karoubi construction, but no game-semantic theorem is silently transferred to the displayed LTS. Herlihy and Wing own the atomic history definition; Castañeda, Rajsbaum, and Raynal own the interval-sequential comparison. The restricted set theorem above is book-owned and has exactly the hypotheses stated in theorem 87.9. The theorem owners and comparison sources are [HOVW^+26, OVSC24, HW90, CRR15].

Compositional Linearizability and Modular Concurrent Objects

Finite traces make the obstruction calculable

Definition 87.1 — Sequentially consistent traces ¶

Definition 87.2 — The frozen LTS specification ¶

Exercise 87.1 ¶

Programs, modules, and linking

Definition 87.3 — The artifact-local program and module interface ¶

Definition 87.4 — Vertical and horizontal composition ¶

Lemma 87.5 — Module and linking algebra ¶

Exercise 87.2 ¶

Identity saturation determines linearizability

Definition 87.6 — Refinement and identity saturation ¶

Theorem 87.7 — Observational refinement and locality ¶

Theorem 87.8 — Horizontal and vertical composition ¶

Atomic, set, and interval boundaries

Exercise 87.3 ¶

Theorem 87.9 — Restricted set specialization ¶

Exercise 87.4 ¶

Suggested first pass.

Exercise 87.5 ¶

Exercise 87.6 ¶

Exercise 87.7 ¶

Search the book