The verification of the on-chip COMA cache coherence protocol

Open Access
Authors
Publication date 2008
Host editors
  • J. Meseguer
  • G. Roşu
Book title Algebraic Methodology and Software Technology
Book subtitle 12th International Conference, AMAST 2008 Urbana, IL, USA, July 28-31, 2008 : proceedings
ISBN
  • 9783540799795
ISBN (electronic)
  • 9783540799801
Series Lecture Notes in Computer Science
Event 12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008), Urbana, IL, USA
Pages (from-to) 413-429
Publisher Berlin: Springer
Organisations
  • Faculty of Science (FNWI) - Informatics Institute (IVI)
Abstract 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.
Document type Conference contribution
Language English
Published at https://doi.org/10.1007/978-3-540-79980-1_31
Downloads
293367.pdf (Submitted manuscript)
Permalink to this page
Back