×

Algebraic models of simultaneous multithreaded and multi-core processors. (English) Zbl 1214.68230

Mossakowski, Till (ed.) et al., Algebra and coalgebra in computer science. Second international conference, CALCO 2007, Bergen, Norway, August 20–24, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73857-2/pbk). Lecture Notes in Computer Science 4624, 294-311 (2007).
Summary: 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 different 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 microprocessors and their correctness to SMT and CMT. We outline how the one-step theorems for simplifying verification are modified for SMT and CMT processors. The particular problems that are addressed are: how to map multiple (possibly interacting) user-level SMT/CMT models to a single implementation? And how to accommodate the (unavoidable) presence of implementation level components in the user-level model?
For the entire collection see [Zbl 1123.68007].

MSC:

68Q65 Abstract data types; algebraic specification
68M07 Mathematical problems of computer architecture
PDFBibTeX XMLCite
Full Text: DOI