Engineering Journal: Science and InnovationELECTRONIC SCIENCE AND ENGINEERING PUBLICATION
Certificate of Registration Media number Эл #ФС77-53688 of 17 April 2013. ISSN 2308-6033. DOI 10.18698/2308-6033
  • Русский
  • Английский
Article

Issues of parameterized verification of cache coherence protocols

Published: 18.11.2013

Authors: Burenkov V.S., Ivanov S.R.

Published in issue: #11(23)/2013

DOI: 10.18698/2308-6033-2013-11-1013

Category: Information technology

The article deals with parameterized cache coherence verification. Cache coherence protocols are mechanisms used in multiprocessors. Substantial amount of processor cores leads to the state explosion problem. Two approaches to combat this problem are model checking-based methods, aimed at automation, and theorem proving style methods, aimed at scalability. Information sources show that the most promising methods combine the advantages of both groups. The most successful method is probably the CMP method representing a combined approach. Authors propose a sequence of steps for verification of the industrial-strength Elbrus microprocessors cache coherence protocol.