In this section we discuss the workings of ROO in practice and present some experimental results.
At first glance one's intuition might suggest that the ability of ROO to deliver the expected performance would be hobbled by the restriction that only one process can be carrying out Task B at a time. If Task B falls behind (the K list grows continually, and never emptied), there will be two bad effects. The first is that the use of an important generated clause may be delayed by a long residence in the K list, thus postponing the proof. The second is that, particularly for large numbers of processes, Task B may not be able to keep the pool of work units filled by adding new, fully processed clauses to the set of support. In this situation, idle processes will await work in the askfor monitor, wasting potential processing power.
In practice, however, this situation does not arise as often as one might think. (It does indeed arise however; see Section ?? below). To understand just what does happen as ROO proceeds, it is useful to study its behavior with a general purpose tool developed at Argonne called Atrace [1].
In Figure ![[*]](http://www-fp.mcs.anl.gov/~lusk/images/papers/cross_ref_motif.gif){kind=small}
we see the situation at the beginning of the run of Sam's
Lemma on ROO with sixteen processes on a Sequent Symmetry. (Describe
start up, set of support size, task B, etc.) But later in the run (3 / 4sec. later) the situation has changed, and the restriction that only one
process can do B at a time is not a restriction. All processes are busy.
(upshot picture of Sam at 750 millisecs.)
What has happened is that although the instances of A are generating new candidate clauses, after a while the existing clause space has expanded to the point where most new clauses are subsumed by Task A and never make it into the K list. When K does become non-empty, it quickly emptied by the next process to become available.