Algebraic Models of Simultaneous Multithreaded and Multi-core Processors

13 years 10 months ago
Algebraic Models of Simultaneous Multithreaded and Multi-core Processors
Much current work on modelling and verifying microprocessors can accommodate pipelined and superscalar processors. However, superscalar and pipelined processors are no longer state-of-the-art: Simultaneous Multithreaded (SMT) and Multi-core, or Chip-Level Multithreaded (CMT) microprocessors enable a single microprocessor implementation to present itself to the programmer as multiple (virtual in the case of SMT) processors with shared state. This paper builds on a series which has developed a hierarchy of many-sorted algebraic models, able to model a variety of processor types, at nt levels of temporal and data abstraction. These models address both the behavioural definition of microprocessors, and also the question: what does it mean for a microprocessor implemenation to be correct? They also consider how the process of formal verification can be simplified by indentifying some easily-checked preconditions (the one-step theorems). We extend the existing algebraic tools for modeling...
Neal A. Harman
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Authors Neal A. Harman
Comments (0)