Proceedings of the Institute for System Programming of the RAS
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Proceedings of ISP RAS:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Proceedings of the Institute for System Programming of the RAS, 2017, Volume 29, Issue 4, Pages 231–246
DOI: https://doi.org/10.15514/ISPRAS-2017-29(4)-15
(Mi tisp246)
 

A technique for parameterized verification of cache coherence protocols

V. S. Burenkov

JSC MCST
References:
Abstract: This paper introduces a technique for scalable functional verification of cache coherence protocols that is based on the verification method, which was previously developed by the author. Scalability means that verification efforts do not depend on the model size (that is, the number of processors in the system under verification). The article presents an approach to the development of formal Promela models of cache coherence protocols and shows examples taken from the Elbrus-4C protocol model. The resulting formal models consist of language constructs that directly reflect the way protocol designers describe their developments. The paper describes the development of the tool, which is written in the C++ language with the Boost.Spirit library as parser generator. The tool automatically performs the syntactical transformations of Promela models. These transformations are part of the verification method. The procedure for refinement of the transformed models is presented. The refinement procedure is supposed to be used to eliminate spurious error messages. Finally, the overall verification technique is described. The technique has been successfully applied to verification of the MOSI protocol implemented in the Elbrus computer systems. Experimental results show that computer memory requirements for parameterized verification are negligible and the amount of manual work needed is acceptable.
Keywords: multicore microprocessors, shared memory multiprocessors, cache coherence protocols, model checking, Spin, Promela.
Bibliographic databases:
Document Type: Article
Language: English
Citation: V. S. Burenkov, “A technique for parameterized verification of cache coherence protocols”, Proceedings of ISP RAS, 29:4 (2017), 231–246
Citation in format AMSBIB
\Bibitem{Bur17}
\by V.~S.~Burenkov
\paper A technique for parameterized verification of cache coherence protocols
\jour Proceedings of ISP RAS
\yr 2017
\vol 29
\issue 4
\pages 231--246
\mathnet{http://mi.mathnet.ru/tisp246}
\crossref{https://doi.org/10.15514/ISPRAS-2017-29(4)-15}
\elib{https://elibrary.ru/item.asp?id=29968654}
Linking options:
  • https://www.mathnet.ru/eng/tisp246
  • https://www.mathnet.ru/eng/tisp/v29/i4/p231
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Proceedings of the Institute for System Programming of the RAS
    Statistics & downloads:
    Abstract page:152
    Full-text PDF :153
    References:30
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024