Proving non-interference

Our problem in verifying Tomasulo's algorithm with an arbitrary number of execution units is that we are forced consider only one execution unit at a time, in order to obtain a finite-state verification problem. Thus, we consider the correctness only of the results of one particular execution unit. When we perform this verification, the other execution units are abstracted to an undefined value Thus, although we are not concerned with the correctness of the data values they produce, they may still upset the control state in the given reservation station by returning spurious tags.

To rule out this possibility, we add a non-interference lemma. This states that while a reservation station is expecting a result from a given execution unit, no other unit returns a result for that particular RS. In general, such a lemma is needed whenever the state of one system component might be corrupted by a spurious message from other components that have been abstracted away.

In order to state the condition that a given reservation station does not receive an unexpected result, we first have to add some auxiliary state information to tell us which execution unit the reservation station is actually expecting a result from. To do this, we add an additional field to the auxiliary state array:

  forall (i in TAG)
    aux[i].eu : TAG;

Now, each time that a given reservation station issues an instruction to an execution unit, we record the index of that execution unit in the auxiliary state:

   if(exe_valid)next(aux[issue_choice].eu) := issue_eu;

We can now state the non-interference lemma as follows:

   lemma3 : assert G (pout.valid -> (complete_eu = aux[pout.tag].eu));

That is, lemma3 states that, at all times, if a result is returning on the pout bus, with a given tag pout.tag, then the unit returning the result (complete_eu) must be the unit that the indicated reservation station is waiting for (aux[pout.tag].eu).

Now, lets see if we can prove lemma3. The first thing we'll have to do is to break the lemma into cases, so we only have to consider one reservation station and one execution unit. So let's add the following case splitting declaration:

   forall(i in TAG) forall(j in EU)
     subcase lemma3[i][j] of lemma3 for pout.tag = i & complete_eu = j;

That is, we only consider the case where the returning result is for reservation station i and the execution unit returning the result is j. With the above additions, open the file, and select property lemma3[0][0]. If you look in the cone pane, you should see that SMV has automatically performed data type reductions, reducing TAG to just {0,NaN} and EU to 0,NaN. As a result, there are only 9 state variables (notice also that no data variables appear in the cone, because lemma3 is a control property, and does depend on any data variables. However, if you try to verify the property, you'll find that it's false. The counterexample shows a case where reservation station 0 is waiting for a result from execution unit 0, but instead, at state 3, a result returns from some other execution unit (that is complete_eu = NaN. In other words, in trying to prove non-interference, we've run into an interference problem. You might think that we are caught in an infinite regression here. However, in fact all is not lost. This is because when proving a particular case of lemma3 at time $t$, SMV will allow us to assume the full lemma holds up to time $t-1$. In other words, we only have to prove that execution unit 0 is not the em first execution unit to interfere. If this is true for all execution units, we can then safely infer that no execution unit interferes. To tell SMV to assume the full lemma up to time $t-1$, add the following declaration:

  forall(i in TAG) forall(j in EU)
    using (lemma3) prove lemma3[i][j];

The parentheses around lemma3 tell SMV to make the weaker assumption that lemma3 only holds up to $t-1$. If we leave them out, SMV will complain that the proof is circular. With this addition, open the file, and try to prove lemma3[0][0]. This time it should be true.

Now that we've proved that other executions can't interfere, let's return to the proof of lemma2 (correctness of returning results). We want to prove that a result coming back on the result bus is correct, assuming that no previous interference has occurred. To do this, add (lemma3) to the assumptions used to prove lemma2. You should get a declaration like the following:

  forall(i in TAG) forall(j in EU)
  forall(a in WORD) forall(b in WORD) forall(c in WORD)
    using opra//free, oprb//free, st[i]//lemma1,
      f//undefined, f[a][b], (lemma3)
    prove pout//lemma2[i][j][a][b][c];

Notice that we only assume the non-interference lemma up to time $t-1$ when proving lemma2 up to time $t$. In fact, SMV won't allow us to use lemma3 up to time $t$. This is because lemma2 is a refinement map. Thus, we might well choose to use it use it when proving lemma3, which would result in a circularity. Fortunately, the weaker assumption is sufficient to prove the lemma. To confirm this, open the new version, and choose ``Prop|Verify all''.

With the addition of a non-interference lemma, we have now proved that our implementation of Tomasulo's algorithm works for any word size, any ALU function, any number of registers, any number of reservation stations, and any number of execution units.