ch:compositional-linearizability: ch:compositional-linearizability

After $0:\mathsf{call}(\mathsf{inc})$, the active map records thread $0$’s operation. Since the frozen counter has one thread and no internal visible operation, the only visible length-two prefix is $$0:\mathsf{call}(\mathsf{inc});0:\mathsf{ret}(\mathsf{inc},1).$$ The proposed return-$2$ prefix passes CL-Seq-ret’s active-map premises but fails the counter state relation: from state $0$, the increment response is $1$, not $2$. Thus the rejecting premise is $0{\mathsf{Step}}_{V_{\mathsf{ctr}}}(0:\mathsf{ret}(\mathsf{inc},2))s^{\prime }$.

For the left unit, expand ${\mathsf{subst}}_{\mathsf{idM}}(\mathsf{Vis}(m,k))$. The visible substitution clause and local bind equations give $$\mathsf{bind}(\mathsf{Vis}(m,\mathsf{Return}),\lambda x.{\mathsf{subst}}_{\mathsf{idM}}(k(x))){\approx }_{\mathsf{P}}\mathsf{Vis}(m,\lambda x.{\mathsf{subst}}_{\mathsf{idM}}(k(x))).$$ Pointwise coinduction on $k(x)$ identifies this with $\mathsf{Vis}(m,k)$. For the right unit, ${\mathsf{subst}}_M(\mathsf{Vis}(m,\mathsf{Return}))$ expands to $\mathsf{bind}(M(m),\mathsf{Return})$, and coinduction on $M(m)$ proves the right-unit law.

These module laws do not imply $V▹\mathsf{idM}=V$. With two threads, $\mathsf{K}(V)$ may expose overlay calls $0:\mathsf{call}(m_0);1:\mathsf{call}(m_1)$ before either underlay return is reflected to the overlay. Those open brackets are precisely the additional states used by linearizability; an atomic $V$ need not contain that overlay trace.

There are two total orders. If thread $0$’s operation comes first, a deterministic atomic exchange must choose thread $0$’s return before thread $1$’s offer is present, so it cannot return $4$. If thread $1$ comes first, its operation must choose its return before thread $0$’s offer is present, so it cannot return $2$. Both orders contradict the four-event history. The paired set class containing both operations sees offers $2$ and $4$ together and returns $(4,2)$, so the obstruction is atomic ordering rather than sequential consistency of either thread.

The exchanger class $C=\{0:\mathsf{exch}(2)/4,1:\mathsf{exch}(4)/2\}$ becomes two overlay calls, one underlay transition labelled by $C$, and two overlay returns. Each thread state holds one active operation, and the paired transition fixes both return values. Conversely, grouping the identity-module brackets around that one underlay transition recovers exactly $C$.

If $C$ also contains a second operation of thread $0$, the forward construction would have to store two active operations at $q(0)$. The thread state grammar in definition 87.3 stores at most one $\mathsf{Cont}$ or $\mathsf{UCall}$ package. Hence the at-most-one-operation premise of theorem 87.9 is necessary for this construction.

Project a tensor trace twice. Retain left-tagged events in one projection and right-tagged events in the other. Each projection deletes only events carrying the other register tag. It therefore preserves retained call/return order and the completion decision for pending calls. The shared active map supplies the missing cross-tag fact: one thread cannot have simultaneous left and right operations.

Linearize the two projections in $\mathsf{K}(V_1)$ and $\mathsf{K}(V_2)$. Shuffle those traces subject to the original cross-tag order of every thread. The component orders and the cross-tag per-thread orders are compatible because each linearization preserves the corresponding projected thread order. Left events change only the first state, and right events only the second, so the shuffle lies in $\mathsf{K}(V_1\otimes V_2)$.

Conversely, tensor an arbitrary left trace with the empty right trace over the same thread set and project its assumed tensor linearization. Exchanging the tagged projections gives the right result.

Let thread $0$ invoke $\mathsf{ws}(3)$, then let threads $1$ and $2$ invoke $\mathsf{ws}(5)$ and $\mathsf{ws}(2)$ while thread $0$ remains active. Let thread $0$ return $\{3,5\}$ before thread $2$ returns $\{3,5,2\}$. No single atomic point for thread $0$ sees exactly its reported overlap while also ordering all three complete operations. An interval presentation uses the classes Thread $0$ spans $I_0$ and $I_1$; the exercise therefore lacks the premise that each operation is represented by one set class. The restricted set theorem does not apply.