Chapter 6 Correctness

The correctness proof of the Tomasulo scheduling algorithm with reorder buffer itself is already in [Ger98]. It is based on a proof for the Tomasulo scheduler without reorder buffer in [Mül97a]. The proof presented here uses a slightly different notation. The correctness proof has two parts: The first part shows that data consistency is maintained. The second part proves that the algorithm terminates, i.e., the hardware is deadlock-free.

6.1 Data Consistency

6.1.1 Definitions

Let I₁ to I_n be a sequence of n instructions. Data consistency intuitively means that the results generated by any given instruction I_i in the program conform to the semantics of an abstract DLX machine. These semantics are defined as transition rules on an abstract configuration set C(i) of the machine. This configuration includes all DLX registers, which are R₀(i) to R₃₁(i), SPR, FPR, and PC(i), and the rest of the program to be executed. A shorthand for all register files is RF[](i). The start configuration C(0) is the configuration after the reset.

This abstract DLX machine processes one instruction with each transition. Let the source registers of instruction I_i be S₁(i) to S_s(i)(i) with values s₁(i) to s_s(i)(i) and the destination registers D₁(i) to D_d(i)(i) with values d₁(i) to d_d(i)(i). We use s(i) source and d(i) destination registers to handle double precision floating point instructions without disturbing distinction of cases. For example, the instruction

FPR₀:=FPR₂+FPR₄

has six source operands (FGR₂ to FGR₅ and RM and MASK) and three destination operands (FGR₀, FGR₁, and IEEEf). Let op_i be the operation of instruction I_i, this is a double precision floating point addition in the example.

Now, I_i can be specified as

I_i: (D₁(i),..,D_d(i)(i)) = op_i(S₁(i),..,S_s(i)(i))

with values

I_i: (d₁(i),..,d_d(i)(i)) = op_i(s₁(i),..,s_s(i)(i))

As mentioned above, the abstract DLX machine processes instruction I_i in transition i, which results in configuration C(i). Registers not written by instruction I_i are passed unmodified from configuration C(i-1). Let last(r,i) be index of the last instruction prior I_i which modified register r:

last(r,i) = max{j<i | I_j has destination register r }

This allows an easy criterion for data consistency for any given (non-abstract) machine.

Criterion 1 For any given source register, the value of this register must be the result of the last instruction writing it:

s_x(i) = d_y(last(S_x(i),i)) " x Î {1,..,s(i)}, D_y(i)=S_x(i)

There are some exceptions from this rule, e.g., the register R₀, which are left out for sake of simplicity. Furthermore, if there is no such instruction, this value is undefined, therefore, it is assumed that all registers, which are used as source register, are initialized with proper values by the program.

The rest of the section will prove that this condition holds for the machine presented in chapter 3. The denominators of the abstract DLX machine for the registers and the values are now used for the Tomasulo DLX configuration. This is done in analogy to the proof in [Mül97a] with the help of four invariants.

Invariant 1 During the issue of instruction I_i, source operand S_x(i) is in the register file, as indicated by RF[r].valid=1. In this case, the data item of the register holds the desired value, i.e., it holds the result of the last instruction writing RF[r].

Invariant 2 During the issue of instruction I_i, source operand r:=S_x(i) is, as indicated by RF[r].valid=0, the result of an previous instruction I_j, which has not yet retired. In this case, the tag item of the register holds I_j.tag, i.e., the tag of the instruction I_j. This instruction is the last instruction writing RF[r].

Invariant 3 Let instruction I_i be an instruction in reservation station RS_l. If there is an operand x in this reservation station which is not yet valid (RS_l.opx.valid=0), there must be a previous instruction I_j, which produces the value for the operand and has not yet completed. The tag of this instruction is the tag in RS_l.opx.tag.

Invariant 4 Let invariant 2 or 3 apply for I_i and source operand r:=S_x(i) with tag S_x(i).tag. If the CDB is valid and if the CDB tag is equal to the tag of the operand, the result of the last instruction writing the operand is on the CDB. If the ROB entry pointed to by the tag of the operand is valid, the result of the last instruction writing the operand is in this ROB entry.

With the help of these invariants, the proof of the data consistency is done by induction over n. For n=0, the claim is obvious. The induction for n>0 requires a distinction of two cases. Let instruction I_i read source operand S_x(i). This is possible in two different phases.

Let instruction I_i read register r:=S_x(i) during issue. In dependence of the value of RF[r].valid, either invariant 1 or invariant 2 applies. If RF[S_x(i)].valid is set, the claim is an implication of invariant 1, since the operand is in the register file.

If not so, invariant 2 states that RF[r] contains the tag of the instruction I_j which produces the result. As the operand of the instruction is already available during issue, it must be either in the ROB or on the CDB. In both cases, invariant 4 applies. Thus, the result in the ROB or on the CDB is d(last(r,i)). The instruction I_j had correct operands because of j<i.
Let instruction I_i read register r:=S_x(i) while in reservation station RS_l. This only happens if RS_l.opx.valid is not set. In this case, invariant 3 states that the tag in RS_l.opx.tag is the tag of the instruction I_j which produces d(last(r,i)). This tag must be equal to the tag on the CDB, thus invariant four applies. I_i therefore reads the result of I_j. This is the correct result because of j<i.

6.2 Termination

6.2.1 Definitions

The termination proof will show that an instruction sequence I₁ to I_n is processed in a finite amount of clock cycles. The following shorthands are used: fetch(i), issue(i), disp(i), compl(i) and term(i) denote the cycles in with instruction I_i is fetched, issued, dispatched, completed and terminated, respectively.

6.2.2 Termination

Lemma 1 All instructions are issued in program order and terminate in program order, i.e., issue(i)<issue(j) and term(i)<term(j) for any i<j.

In-order termination is a conclusion of the fact that an instruction terminates when leaving the ROB. The ROB is a fifo queue and is filled in program order. Consequently, to prove termination, it is sufficient to prove that a finite a exists with term(i)+a ³ term(j) for any i<j, i.e., to find an upper bound for the number of cycles of an instruction. A weak upper bound for a can be determined by summing up the maximum time which an instruction spends in each stage after all previous instructions terminated:

a £ a₀ + ... + a₄

This bound is proved by induction over n. The induction hypothesis is that instruction I_i obeys to this bound.

Fetch After all previous instructions terminated, instruction I_i can be fetched if there is no stall from the instruction memory. If lmem<¥ is the maximum latency of the memory, a₀ = lmem.

Issue Instruction I_i can be issued iff there is no issue stall (the conditions for an issue stall are in section 3.5.6, page ??). This is obviously true one cycle after all previous instructions terminated and if there is no stall from the instruction memory. Since lmem is the maximum latency of the memory, a₁ = lmem+1.

Dispatch Instruction I_i can be dispatched iff all its operands are valid and if the function unit is able to accept data. Obviously, the operands are valid after all previous instructions terminated. However, the function unit still might be blocked by instructions after I_i, i.e, instructions I_j with j>i. Let imax be the maximum number of instructions the function unit can hold (including the producer pipeline stage), and l the maximum latency of the function unit. For iterative function units, imax · l is a weak bound for the number of cycles until the function unit is empty. This bound is valid for pipelined function units, too. However, before an instruction can leave the function unit, it is necessary to wait for the CDB. Since the CDB is allocated round robin, this takes n cycles at most, with n being the number of function units. Thus, it takes a₂=imax · l · n cycles at most until the function unit is empty. As I_i is the oldest valid instruction in the reservation stations (all previous already terminated), I_i is dispatched afterwards.

Completion As shown above, an instruction I_i in a function unit leaves it (completes) after at most a₃=imax · l · n cycles.

Termination A valid (completed) instruction in the ROB terminates one cycle after all previous instructions terminated. Thus, a₄ is one cycle.