Algebraic models of behaviour and correctness of SMT and CMT processors

Superscalar microprocessors execute multiple instructions simultaneously by virtue of large amounts of (possibly duplicated) hardware. Much of this hardware is idle at least part of the time. Simultaneous multi-threaded (SMT) microprocessors utilize this idle hardware by interleaving multiple independent execution threads. In essence, a single physical processor appears to be multiple virtual processors. Multi-core, or chip-level multi-threaded (CMT) processors duplicate the execution pipeline, while sharing other resources. Both approaches increase processor hardware utilization (and hence speed) by introducing thread-level parallelism.The key question we consider in this paper is: how do we model SMT/CMT processors? In particular, how do we model multiple, parallel, intercommunicating threads of execution, whose behaviour is defined in terms of some lower level implementation? And, what does it mean for such SMT/CMT models to be correct? The model developed here focusses particularly on (a) the relationship between timing behaviour at different levels of abstraction; and (b) what it means for a representation of a processor at one level of abstraction (typically representing an implementation) to be correct with respect to another (typically representing a specification consisting of multiple interacting threads). An inevitable, and realistic, consequence of the model of SMT/CMT processors developed is a weakening of the long-established principle of separation between a processor implementation and specification.