Use two different shared locations x and y, initially zero, and two CPU cores. The following are architectural memory operations, with each result kept in its own processor register:

Each CPU core can retire its write into its own store buffer. Before either write drains, Core 0's load instruction misses its own store buffer because it asks for y, while Core 1's asks for x. Both can read the old shared values. Afterwards the buffers drain and both locations become one. ThusThere is no contradiction with cache coherence: each location still has an agreed write order. The unusual observation concerns ordering across two different locations. This is the standard store-buffering example, also permitted by total store order.^[ref]

On a single CPU core executing the two logical participants in an ordinary thread interleaving, the same pair of zero observations is impossible under the usual shared-buffer and own-write-forwarding behavior. To read y=0, Core-0's logical read must precede the other participant's write of y; to read x=0, the other read must precede the write of x. Combining these requirements with each participant's program order gives the impossible cycleIf a write is still buffered across a context switch on that single CPU core, a later read of the same address sees it through store-to-load forwarding rather than returning an older value. Hence separate store buffers on different CPU cores enable the observation; the comparison assumes ordinary coherent cacheable computer memory and no device accesses or additional writes. A locally completed store need not yet be visible to another core.

A small memory cache close to the CPU can be accessed quickly, but cannot hold the entire useful data set. Increasing its capacity usually increases lookup, wiring and energy costs. A cache hierarchy combines a small fast first level with progressively larger levels that reduce the number of accesses reaching slow main computer memory.

In a simple serial two-level timing model, let $t_1$ be the first-level lookup time, $m_1$ its cache miss rate, $t_2$ the additional second-level lookup time, $m_2$ the second level's local cache miss rate conditional on a first-level miss, and $t_M$ the remaining main-memory cost. ThenThis average memory access time combines the common fast path with a rarer large-capacity path. Several levels balance hit latency, capacity, cost and traffic; making one cache very large does not preserve a tiny first-level hit time. Temporal locality and spatial locality make this arrangement useful.

Treat the condition as another instruction operand. At issue, capture the tag or value of the particular older processor condition flags that the instruction reads. Later flag writers must not redirect that dependence. A single unversioned “current flags” value would be wrong when flag-producing instructions finish out of order.

Without a reorder buffer. A conservative implementation keeps the conditional instruction in its reservation station until its predicate and required data operands are ready. If the predicate is true, send the instruction to its functional unit; if false, suppress its specified changes. Independent unconditional instructions in other reservation stations can execute meanwhile, which already gives the overlap in part (c). A conditional store instruction must not write computer memory while its predicate is unresolved, and a false condition must not raise an exception associated with executing the suppressed operation.

Register renaming makes the false case more subtle than simply throwing away an instruction. For a conditional update of destination r2, let $v_{\mathrm{old}}$ be its preceding logical value and let $v_{\mathrm{calc}}$ be the computed new value. The required result isIf issue has already assigned a producer tag to the conditional instruction's destination, younger consumers wait for that tag in either case. Record the old destination as an additional input before changing its register renaming map. When the predicate is false, broadcast $v_{\mathrm{old}}$ under the conditional instruction's new tag, or provide an equivalent correctly ordered mapping/merge mechanism. Merely failing to broadcast would leave those consumers waiting forever. Even a conditional move with an immediate source needs this old-destination input. A conditional instruction that sets processor condition flags needs the same preserve-or-replace treatment for the flags.

With a reorder buffer. Allocate a reorder buffer entry at issue and use its tag, or a corresponding physical register, as the persistent destination. The CPU may use the same wait-for-predicate policy. It may also execute a candidate result early, retaining it and any exception privately in the reorder buffer until the predicate is known. The functional unit and possibly the reservation station can then be released while the entry waits. A false predicate selects the old destination value and discards any exception belonging only to the suppressed operation; a true predicate selects the computed result and retains a genuine exception. Instruction retirement changes architectural state only when the entry reaches the head and its predicate and status are resolved. Store instructions similarly hold their writes until authorized instruction retirement.

A reorder buffer by itself does not remove the destination ambiguity. For instance, a younger addition consuming r2 must not irreversibly use $v_{\mathrm{calc}}$ if the predicate might be false. It can wait for the merged $v_{\mathrm{out}}$. A more aggressive design can predict the predicate, forward the predicted value and replay or squash dependent instructions if that prediction fails, using the reorder buffer and saved register renaming state for recovery.

Performance comparison. Let the predicate be available at time $L$, the candidate's ordinary source data at time $D$, and its functional unit take $F$ cycles. Ignoring issue and selection overhead, waiting before execution gives a selected result at about $\max (L,D)+F$. Early execution into a reorder buffer can give it at $\max (L,D+F)$, provided the old value is also ready when needed. For $D=0$, $L=50$ and $F=20$, that is $70$ versus $50$ cycles. Dependent instructions still wait for a correct selected value unless supported by prediction and recovery.

A reorder buffer can therefore overlap useful candidate work with predicate computation and release scarce scheduling resources earlier, at the cost of buffered results and possible wasted execution. Instruction retirement can still wait behind an older incomplete instruction. A design without a reorder buffer could also retain a harmless early arithmetic result in its reservation station until the predicate is ready, but it occupies that station longer and still must defer effects and exceptions. The fundamental requirements are versioned predicate dependence, preservation of false-case values, and controlled commitment; the reorder buffer makes speculative completion and recovery more systematic.

Consider a slow load instruction controlling one conditional addition, followed by independent work. The following is schematic A32 assembly language; the plain ADD and MUL forms shown do not update processor condition flags:Without branch prediction, the unresolved conditional branch prevents fetching beyond it until the load instruction, comparison and branch resolution complete. The multiplication does not depend on r0, yet the out-of-order execution machinery cannot execute it if it has not been fetched and issued.

Conditional execution removes that branch:ADDEQ adds one exactly when the zero flag from CMP is set; otherwise it preserves r2. The instruction stream has a known sequential continuation, so the CPU can fetch and issue the multiplication while the load instruction is outstanding. With available reservation stations and a free multiplier, independent multiplication overlaps the load instruction's latency.

Predication removes a control-flow obstacle to finding independent work; it does not resolve the slow load or its dependent condition earlier. The conditional addition must still select the correct result after the processor condition flags become known. The gain is especially useful for a short conditional region, since instructions whose predicates are false still occupy fetch and issue resources. On a strictly blocking in-order pipeline, a slow demand load instruction would still stop later work in MEM; the overlap here uses the question's out-of-order execution setting and a nonblocking memory path.

A reorder buffer records instructions in program order, including those with no destination processor register. Each entry needs a completion state before instruction retirement can pass it. Thus a store instruction must report that its memory address and data are ready and whether execution detected a fault, even though it has no ordinary register file result.

Suppose an older division occupies the head of the reorder buffer, followed by a store instruction and an addition. The latter two can finish first. The store instruction's completion message identifies its reorder buffer entry, carries or identifies the buffered memory address and data, and supplies its status. The entry is then ready, but its write remains private until it is the oldest instruction allowed to commit. When the division retires successfully, the store instruction can commit to the store buffer or memory system, and the addition can subsequently retire. If the division faults, the younger store instruction is discarded without changing visible computer memory.

If the store instruction never reported completion, its reorder buffer entry would remain unready and block instruction retirement indefinitely. Conversely, treating it as completed at issue could commit missing data or suppress its later fault. The common data bus carries tagged completion information as well as register values. A false-predicated instruction also needs a completion indication even when it changes no data.

This answer uses the diagram's shared result/completion path. An architecture can instead provide a dedicated store queue completion path to the reorder buffer; there is no universal requirement to send store data over the same physical wires as arithmetic results. What is essential is delivery of the tagged completion and exception status before instruction retirement.

In the illustrated out-of-order execution scheme without a reorder buffer, a reservation station identifier acts as the producer tag for an outstanding result. A register renaming map and waiting operands in other reservation stations can refer to that tag. The tag must remain unique until the result has been broadcast and the required register file update has occurred.

For example, issue a slow multiplication producing r1 into reservation station S, then an addition r4 := r1 + r5 into another reservation station. The addition records S as the unresolved source of r1. Even after the multiplier has accepted its operands, the multiplication can take many cycles; S cannot be reassigned merely because its operands have left the reservation station. If an independent short instruction is assigned S and broadcasts first, the addition would mistake that unrelated value for the multiplication's result. A later multiplication result could likewise corrupt the new instruction's register renaming mapping.

Finishing execution is also insufficient if the result is waiting for common data bus access: consumers and the register file still name S until writeback. Keep the producer tag allocated through broadcast/writeback, so no younger result can masquerade as the outstanding producer. With a separate persistent producer tag, such as a reorder buffer entry or a physical register, a design can release the scheduling slot earlier; this changes the tag-ownership arrangement in the question.

Speculative execution allows younger instructions to proceed while some condition on an older instruction is unresolved. Here the prediction is that a store instruction will pass its memory management unit's protection and translation checks. Successful prediction avoids waiting; failure requires discarding younger work and taking the older instruction's synchronous processor exception. A result computed speculatively must not become an irreversible architectural change before it is safe.

In the displayed five-stage in-order pipeline, the store instruction's memory address is computed in EX and its memory operation is in MEM. Take the permission check to finish at the end of MEM, with a one-cycle cache hit, no data hazards and sufficient store buffer capacity. A concrete conservative implementation without speculative execution fetches no younger instruction until this check has passed. Compare the start of a stream of independent, nonfaulting store instructions:

The conservative version inserts three otherwise unnecessary cycles after each such store instruction, whereas the speculative version can start one instruction per cycle. For $N$ stores, counting through WB, the times are $4N+1$ and $N+4$ cycles. ThusMore generally, with a fraction $f$ of such store instructions and no other delays, this particular interlock gives an asymptotic comparison $S=1+3f$. The maximum is four, not five: the permission check is resolved in MEM, so waiting for the empty store WB stage is unnecessary.

The baseline's interlock position matters. If it allows younger IF and ID work but prohibits younger EX until the end of the store's MEM stage, only one EX cycle is lost per store: successive stores reach EX in cycles $3,5,7,\dots$, compared with $3,4,5,\dots$ under speculative execution, giving a limiting factor of two for that baseline. Holding at ID instead gives two lost cycles per store and a factor of three. The fourfold figure compares against a pipeline that stops younger fetch; an implementation that already permits younger front-end work has a smaller remaining benefit. The source specifies the five stages but does not prescribe this alternative's interlock position.^[ref]

On a protection failure detected at the end of MEM, younger instructions occupy EX, ID and IF and can be invalidated before their normal WB. Younger store instructions must also be prevented from draining from a store buffer before validation. Earlier updates to processor condition flags, if any, need delayed commitment or restoration too. This is what makes the prediction compatible with a precise exception; merely continuing to execute is insufficient.

A store buffer holds the memory address and value of a store instruction while the memory cache or backing computer memory completes the write. The in-order pipeline can continue after enqueueing the write, rather than waiting for a possibly long memory access latency. A full store buffer eventually causes a pipeline stall; buffering hides finite delays, not an indefinitely inadequate service rate.

Without a memory management unit, the comparison can use the actual physical addresses; there is no address translation or synonym problem to solve. Suppose x initially contains zero and these operations execute in order:If the write is still in the store buffer, reading only computer memory could incorrectly return zero. The load instruction searches older buffered store instructions for an overlapping memory address. If the newest matching write covers the requested bytes and its data are ready, store-to-load forwarding returns seven directly. With several pending writes to x, the youngest older matching write wins. If the relevant data are not ready, the load instruction waits; partial overlaps require merging the covered bytes or conservatively waiting for the writes to drain.

A load instruction from an unrelated address y can bypass those buffered writes, subject to the architecture's memory model. Buffer writes to overlap them with useful execution, but preserve each load's dependence on older writes to the same bytes. Device accesses through memory-mapped input-output need their specified ordering and should not be treated as ordinary cacheable computer memory.

Register forwarding supplies a later instruction with a computed value before that value has reached the register file. It removes some read-after-write hazards without changing the program's meaning. Consider these symbolic machine instructions, with the destination first:In the five-stage in-order pipeline, the addition produces its result at the end of EX. In the next cycle the subtraction is in EX, although the addition has not yet reached WB. A bypass from the addition's EX/MEM pipeline register to the subtraction's arithmetic logic unit input supplies the new r1; the old value read in ID must be overridden.

The bypass control compares source and destination processor register identifiers and selects the youngest applicable older producer. It must also check that the producer actually writes that processor register. Forward the newest available result instead of waiting for its writeback. A load instruction is different: its value is normally available only at the end of MEM, so an immediately following dependent instruction still needs a pipeline stall in this five-stage arrangement.

Yes: the procedure always terminates after finitely many steps. If an iteration does not return, then $X_{i+1}⊊X_i$. Thus at least one state is permanently removed. A finite set of $|S|$ states can suffer at most $|S|$ such strict decreases, after which the next equality test must return. Therefore the procedure makes at mostwhen started from $X_0=S$, counting the final evaluation that detects equality. The bound also covers $S=\varnothing$, where the first evaluation already returns. Each evaluation inspects finitely many states and successors, so every individual step terminates as well. Finiteness, rather than monotonicity alone, supplies this finite termination bound.

Start with every state, and repeatedly discard a state that is outside $A=\mathrm{Sat}(\Phi )$ or has any successor outside the current candidate set. Use a fresh set on each iteration so that the displayed procedure computes exactly $H(X)$:This is fixed-point iteration $X_0=S$, $X_{i+1}=H(X_i)$. The first step gives $X_1=A$, because every successor is a state of $S$. Thus $X_1\subseteq X_0$. If $X_i\subseteq X_{i-1}$, the order-preserving function property givesThe candidate sets therefore form a descending chain under set inclusion.

Every fixed point $Z$ is contained in every $X_i$: initially $Z\subseteq S$, and $Z\subseteq X_i$ implies $Z=H(Z)\subseteq H(X_i)=X_{i+1}$. At return, $X=H(X)$, and $X$ contains every fixed point. The returned set is consequently the greatest fixed point, so $\boxed{X=\mathrm{Sat}(\forall \square \Phi )}$ by part (d).

The iteration also has a direct interpretation. $X_1$ contains precisely the states satisfying $\Phi$ now; $X_2$ retains those satisfying it now and at all immediate successors; later rounds extend the checked horizon one step at a time. The stable set enforces the condition at every future position.

Let $X$ be any fixed point of $H$. Thenso $X\subseteq A$ and every successor of every member of $X$ belongs to $X$. Take $s_0\in X$ and an arbitrary infinite path in a transition system $s_0{s}_1{s}_2\cdots$ from $s_0$. By mathematical induction, every $s_i$ belongs to $X$: the base case is the choice of $s_0$, and $s_i\in X$ implies $s_{i+1}\in \mathrm{Post}(s_i)\subseteq X$.

Since $X\subseteq A$, the whole path in a transition system stays in $A$. The path in a transition system was arbitrary, so $s_0\models \forall \square \Phi$. Thus $s_0\in G_{\Phi }$, and since $s_0$ was arbitrary in $X$,Part (b) proves that $G_{\Phi }$ itself is a fixed point. Thereforethe greatest fixed point with respect to set inclusion. In fact the same induction works for every $X\subseteq H(X)$, showing why a successor-closed set of good states certifies this universal property.

Every state has at least one successor, so $\mathrm{Post}(s)⊈\varnothing$ for every $s\in S$. ThereforeThe empty set is always a fixed point. Whenever $G_{\Phi }$ is nonempty, it is therefore an additional, distinct fixed point.

For an explicit example, take a one-state transition system with $S=\{s\}$, the self-loop $s\to s$, and $A=S$. Then $G_{\Phi }=S$ and $H$ has the two distinct fixed points $\varnothing$ and $\{s\}$. This example meets the requirement of no terminal states.

The wording does not guarantee distinct additional fixed points for every instance. For example, if $A=\varnothing$, then $H(X)=\varnothing$ for every $X$ and its only fixed point is $G_{\Phi }=\varnothing$. Thus additional fixed points can occur, but need not occur. The universal example $\varnothing$ is distinct precisely when the desired satisfaction set is nonempty, as also follows from the greatest fixed point argument below.

Let $G_{\Phi }=\mathrm{Sat}(\forall \square \Phi )$. By computation tree logic semantics, a state belongs to $G_{\Phi }$ exactly when every infinite path in a transition system starting there stays in $A=\mathrm{Sat}(\Phi )$ at every position, including position zero. There are no terminal states, so every state lies at the start of an infinite path in a transition system.

If $s\in G_{\Phi }$, then $s\in A$. For any successor $t$ of $s$, every infinite path in a transition system from $t$ can be prefixed with $s$. Hence every such continuation stays in $A$, so $t\in G_{\Phi }$. Thus $\mathrm{Post}(s)\subseteq G_{\Phi }$ and $s\in H(G_{\Phi })$.

Conversely, if $s\in H(G_{\Phi })$, then $s\in A$ and every successor belongs to $G_{\Phi }$. Every infinite path in a transition system from $s$ therefore has its first state in $A$ and its entire remaining tail in $A$. Consequently $s\in G_{\Phi }$. Both inclusions giveso the desired satisfaction set is a fixed point of $H$.

Write $A=\mathrm{Sat}(\Phi )\subseteq S$. All arguments depend only on this given satisfaction set; they do not require an additional convention for the printed notation $\Phi \in 2^{AP}$. For a state $s$, let $\mathrm{Post}(s)=\{t:s\to t\}$. The power set $2^S$ is ordered by set inclusion.

Take $X\subseteq Y\subseteq S$ and any $s\in H(X)$. By the definition of $H$, we have both $s\in A$ and $\mathrm{Post}(s)\subseteq X$. By transitivity of set inclusion, $\mathrm{Post}(s)\subseteq Y$, so $s\in H(Y)$. Since this applies to every member of $H(X)$,Thus $H$ is an order-preserving function, which is the meaning of monotonicity here. This proof does not need either finiteness or the absence of terminal states.