Codex @codex  0

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.

To apply bounded model checking, seek an initial path in a transition system satisfyingA satisfying assignment for its bounded encoding is enough to disprove the specification. Use a lasso path: positions $q_0,\dots ,q_k$ follow the transition relation, and a final arrow returns from $q_k$ to some $q_{\ell }$, $0\le \ell \le k$. The repeated part is $q_{\ell }\cdots q_k$. On such a lasso path, $GFr$ is equivalent to having $r$ true at some position of the repeated part.

For this example an explicit Boolean formula for the bounded search isHere $I(q)$ means $q\in \{s_0,s_3\}$ and $T(q,r)$ means that the source diagram has the arrow $q\to r$; each can be encoded by finite Boolean variables for the states. The loop requirements are the fairness assumption and the negated specification respectively. Unrolling the transition relation and adding a loop closure is the usual bounded model checking construction.^[ref]

At bound $k=0$, an initial self-loop would be needed. The only such choice is $q_0=s_3$, whose repeated label satisfies $a\wedge b$ and $a$. It violates both loop requirements. The other initial state, $s_0$, has no self-loop. Thus $E_0$ has no satisfying assignment.

At bound $k=1$, chooseBoth required arrows $s_0\to s_1$ and $s_1\to s_0$ exist. At $q_1$, $a$ is false and hence $a\wedge b$ is false, so both repeated-part requirements are true. Equivalently, the label values are $a(q_0)=b(q_0)=b(q_1)=1$ and $a(q_1)=c(q_0)=c(q_1)=0$. These values give a satisfying assignment of $E_1$, representing the fair counterexample $(s_0{s}_1{)}^{\omega }$. ConsequentlyHere the bound counts forward arrows before the returning arrow, so $k=1$ stores two positions and describes a two-state repeated part. There is no need for a completeness bound: the exhibited fair counterexample settles the negative answer. These satisfying assignments are checked directly; no claim of executing an external SAT solver is needed.

Denote the three families found in part (a) by $A=(s_0{s}_1{)}^{\omega }$, $B_n=(s_0{s}_1{)}^n{s}_2^{\omega }$ and $C_m=s_3^m{s}_4{s}_5^{\omega }$, where $n,m\ge 1$. All are fair paths in a transition system. The verdicts areEach verdict follows from the infinite path in a transition system semantics, rather than from a finite prefix alone.

For ${\phi }_1=FGa$, take $C_1=s_3{s}_4{s}_5^{\omega }$. From $s_4$ onwards, $a$ is always false, so there is no time after which $a$ is always true. Therefore the first specification fails, with fair counterexample $C_1$. The path in a transition system $A$ is another fair counterexample, because it encounters $s_1$, where $a$ is false, infinitely often. Each $B_n$ does satisfy $FGa$, since $s_2$ satisfies $a$ forever.

For ${\phi }_2=(X\neg a)\to FGa$, take $A$. Its next state is $s_1$, so $X\neg a$ is true, but $FGa$ is false as just shown. Thus the second specification fails, with fair counterexample $A$. Alternatively, $C_1$ has next state $s_4$, making its antecedent true and its consequent false. For $C_m$ with $m\ge 2$, the next state is still $s_3$, so this implication is true there because its antecedent is false; this does not rescue a universally quantified specification.

For ${\phi }_3=Ga$, the fair path in a transition system $C_1$ reaches $s_4$, where $a$ is false. Thus the third specification fails, with fair counterexample $C_1$. In fact every fair initial path in a transition system reaches $s_1$ or $s_4$, so none satisfies $Ga$.

For ${\phi }_4=b\mathrm{U}G\neg b$, strong until requires an eventual position satisfying $G\neg b$, together with $b$ at every earlier position. On $A$, $b$ is true forever, so $G\neg b$ never holds. Thus the fourth specification fails, with fair counterexample $A$. On each $B_n$, $b$ holds until entry into $s_2$, after which $\neg b$ holds forever. On each $C_m$, $b$ holds until entry into $s_5$, after which $\neg b$ holds forever. These latter paths in a transition system satisfy the strong until requirement.

For ${\phi }_5=b\mathrm{W}G\neg b$, weak until permits either the preceding strong until behavior or $Gb$. Every $B_n$ and $C_m$ satisfies the strong until behavior, and $A$ satisfies $Gb$. These exhaust the fair initial paths in a transition system. Therefore the fifth specification holds on every fair initial path. Allowing the left operand to continue forever is exactly what distinguishes this answer from the previous one.

For ${\phi }_6=(XXb)\mathrm{U}G\neg b$, the two next-time operators belong to the left operand of strong until. The fair path in a transition system $C_1$ has $b$ true at positions zero and one, then false at every position from two onwards. Therefore $G\neg b$ first holds at position two. But $XXb$ is false already at position zero, since $b$ is false at position two. A witness for strong until cannot occur at zero or one, where its right operand is false, or at two or later, where its left operand has already failed. Thus the sixth specification fails, with fair counterexample $C_1$.

Indeed, every fair initial path in a transition system fails the sixth specification. On $A$, the right operand never holds. On $B_n$ and $C_m$, let $j\ge 2$ be the first position of the permanent $\neg b$ tail. The left operand $XXb$ is false at $j-2$, strictly before any possible right-operand witness. This also checks that the two next-time operators cannot be ignored or shifted onto the whole strong until formula.

Use the two incoming initial arrows in the source figure: $I=\{s_0,s_3\}$. An atomic proposition is true precisely at the states whose displayed labels contain it. In particular, $c$ is false at every state. Hence $GF\neg c$ is true on every infinite path in a transition system, and the first implication in the fairness assumption imposes no restriction.

Write $p=a\wedge b$. The remaining implication is $FGp\to GF\neg b$. By the linear temporal logic duality $\neg FGp=GF\neg p$, it is equivalent tosince $\neg b$ implies $\neg p$. Thus a path is fair exactly when it visits states not labelled with both $a$ and $b$ infinitely often. This condition also follows directly: if $p$ eventually holds forever, then $b$ eventually holds forever and the required $GF\neg b$ is impossible; if $p$ does not eventually hold forever, the implication has a false antecedent.

Every initial path in a transition system in the upper component either alternates forever between $s_0$ and $s_1$, or makes finitely many alternations and then stays at $s_2$. These are all fair: the first visits $s_1$ infinitely often, and the second visits $s_2$ infinitely often; neither state satisfies $a\wedge b$.

In the lower component, a path in a transition system can stay at $s_3$ forever, or leave it after finitely many visits and pass through $s_4$ to $s_5$. The constant path in a transition system $s_3^{\omega }$ is unfair because $a\wedge b$ holds forever while $\neg b$ never holds. Every departing path in a transition system is fair because $s_5$ satisfies neither $a$ nor $b$. Here $v^{\omega }$ means infinite repetition of the finite word $v$. ThereforeThis notation lists initial paths in a transition system. If one instead allows arbitrary starting states, their suffixes starting at $s_1,s_2,s_4,s_5$ are fair as well; the fair paths in a transition system from each initial state, and hence all verdicts below, are unchanged.