The verification of the on-chip COMA cache coherence protocol. (English) Zbl 1170.68301
Meseguer, José (ed.) et al., Algebraic methodology and software technology. 12th international conference, AMAST 2008, Urbana, IL, USA, July 28–31, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79979-5/pbk). Lecture Notes in Computer Science 5140, 413-429 (2008).
Summary: This paper gives a correctness proof for the on-chip COMA cache coherence protocol that supports the Microgrid of microthreaded architecture, a multi-core architecture capable of integrating hundreds to hundreds of thousands of processors on single silicon chip. We use the Abstract State Machine (ASM) as a theoretical framework for the specification of the on-chip COMA cache coherence protocol. We show that the protocol obeys the Location Consistency model proposed by Gao and Sakar.
For the entire collection see [Zbl 1154.68019].
For the entire collection see [Zbl 1154.68019].
MSC:
| 68M07 | Mathematical problems of computer architecture |
