CMP.14:4 - Solution

Local mantra: choose the observations; expose the interactions; construct compatible steps; find the failing order or invariant; repair the protocol; establish progress under its actual assumptions.

CMP.14:4.1 - Specify what the combined computation must make observable

State the allowed inputs and required results. Include the observations a receiving component can make while work is in progress: returned values, shared-state reads, messages, failures or completed operations. Distinguish a request from each attempt to transmit or execute it when retries are possible.

Choose the required ordering. For a concurrent object, linearizability compares a history of calls and responses with legal sequential behavior. A finite history can contain pending calls. Append responses to any selected pending calls, then omit those still pending. Keep every originally completed operation, including its arguments and returned value. Seek a legal sequential order of the retained operations that respects every case where one operation returned before another was called. Each retained operation appears to take effect between its call and response in this extended history.

The appended responses belong to this comparison; they do not establish that the pending operations will actually return. Section :5.4 shows a pending call whose effect another operation has already observed. Other applications may accept weaker order, duplicate-tolerant combination or eventual agreement; use the property the receiving computation needs.

Also state required eventual events, such as a pending operation returning. An acceptable state or finite history does not alone settle that question. In concurrency theory, a safety property excludes a violation detectable in a finite execution prefix; a liveness property requires progress that no finite delay alone disproves. These meanings describe execution properties here.

CMP.14:4.2 - Expose steps, shared state and the environment

Give each component its local state and point of execution. Identify shared variables, owned data, channels and the operations that connect them. For each elementary action, specify when it is enabled, what it reads and changes, and which other values remain unchanged.

Choose the granularity supported by the computational model. A source statement that reads and then writes a value may allow another component’s step in between. If a compare-and-swap or transaction is assumed atomic, its availability and scope are part of the construction.

Under an interleaving shared-memory model, form the combined state from the components and shared store, and let an enabled component take one step at a time. Message passing adds channel states and send/receive transitions; rendezvous requires the participating steps together. Include the admitted environment transitions, such as message loss, duplication, restart or input arrival, where the required claim depends on them.

A real language or memory model may permit observations absent from simple interleaving. Recover its ordering and visibility rules before transferring the argument. The method can then change the synchronization or the model instead of concealing the missing premise.

CMP.14:4.3 - Derive a compatible invariant or interaction rule

Construct the relation that must survive composition. For example, the shared counter must equal the number of committed increments, a request identifier must have at most one committed effect, or a waiting computation must request only a resource later in an acquisition order.

Establish that relation initially and inspect each allowed transition that can affect it. Local predicates must survive permitted environment steps. Rely/guarantee reasoning makes this explicit: a component assumes a stated interference relation from its environment and establishes a stated relation for its own steps. Its neighbors’ possible steps must fit that assumption. Check the step-level conditions and their initial basis; mutually assuming that the other component eventually succeeds supplies no initial progress.

For a finite construction, explore enabled interleavings until a failure or the relevant closed state set is obtained. CMP.4 supplies search and CMP.13 supplies a qualified abstraction when the state space is too large. A counterexample should retain enough state and ordering to reproduce the offending interaction.

When operations commute under the observations of interest, exploit that property: some orders can be combined or avoided in exploration. Include intermediate observations in the comparison. Equality of the final store is insufficient if a neighboring read distinguishes the swapped operations.

CMP.14:4.4 - Change the interaction that causes the failure

Construct a repair from the failed premise. Common choices have different costs:

Execute the original failing trace against the repair, then inspect the transition family that caused it. This both explains the changed behavior and identifies what a more general argument must cover.

CMP.14:4.5 - Establish the progress actually promised

Identify what can enable and execute each required next step. A component may wait for another component, a message or a resource. A finite dependency with an available first move differs from a cycle in which every participant waits.

Choose only scheduling and delivery assumptions the intended use can support. Weak fairness excludes postponing an action forever once it remains continuously enabled. Strong fairness also excludes postponing an action forever when it becomes enabled infinitely often. Name the action or action family: fairness for an entire process does not make every branch of its code fair.

Use those assumptions with a progress measure or a dependency argument. Show why a required response eventually becomes possible and occurs. A bound on elapsed time additionally needs timing and resource bounds. A retry limit provides a finite failure return, not a guarantee that the requested effect happened or that it did not happen.

Test the relevant lost-progress case: an unavailable participant, an indefinitely lost reply, a stopped lock holder or an unfair scheduler. Return the supported result or the unresolved execution status. Do not preserve an eventual-response claim after removing its delivery or scheduling premise.

CMP.14:4.6 - Compare replacements through the composed observation

Relate the detailed execution to the promised higher-level operation. Some implementation steps may leave the chosen observation unchanged. That permits a coarser description, but hiding indefinitely many such steps can conceal lost progress; qualify the correspondence accordingly.

For replacement, ask whether the new component introduces an observation the allowed context could not obtain before. Include context interactions, failure and progress when they are part of the required behavior. A final-value comparison is sufficient only for a receiving use governed by that value.

Return the constructed coordination procedure, the result it supports and the assumptions the next user must retain. If a supplier changes its operation, memory rule, failure behavior or response promise, reopen the dependent composition. Use the common result-cost comparison and C.11.DUA when deciding whether another experiment, formal argument or alternative implementation would change the next move.