Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Models of Timing Abstraction in Simultaneous Multithreaded and Multi-Core Processors

Speaker: Neal Harman
Slot: Array, 14:30-14:50, col. 5


This paper builds on a series examing algebraic models of
microprocessors and their correctness. Current models can accommodate
pipelined and superscalar processors. However, these are no longer
state-of-the-art: Simultaneous Multithreaded (SMT) and Multi-core
microprocessors enable a single microprocessor implementation to
present itself to the programmer as multiple (virtual in the case of
SMT) processors with shared state.
We extend the existing algebraic
tools for modeling microprocessors and their correctness to SMT and
Multi-Core systems. We outline how the one-step theorems for
simplifying verification are modified for SMT and Multi-Core

websites: Arnold Beckmann 2006-04-19