A Rigorous Correctness Proof of a Tomasulo Scheduler Supporting Precise Interrupts
Daniel Kroening, Silvia Melitta Mueller, Wolfgang J. Paul · 1999
The Tomasulo Algorithm is the classical scheduler supporting out-of-order execution; it is widely used in current high performance micro processors. In this paper, we combine the Tomasulo Scheduler with a reorder buffer which implements precise interrupts, and we give a mathematical correctness proof for this enhanced scheduling algorithm. We show that data consistency is maintained, and that the scheduling is deadlock free and fair.