Checking Parameterized Promela Models of Cache Coherence Protocols
This paper introduces a method for scalable verification of cache coherence protocols described in the Promela language. Scalability means that resources spent on verification (first of all, machine time and memory) do not depend on the number of processors in the system under verification. The meth...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/139 |
| _version_ | 1818824907225563136 |
|---|---|
| author | V. S. Burenkov A. S. Kamkin |
| author_facet | V. S. Burenkov A. S. Kamkin |
| author_sort | V. S. Burenkov |
| collection | DOAJ |
| description | This paper introduces a method for scalable verification of cache coherence protocols described in the Promela language. Scalability means that resources spent on verification (first of all, machine time and memory) do not depend on the number of processors in the system under verification. The method is comprised of three main steps. First, a Promela model written for a certain configuration of the system is generalized to the model being parameterized with the number of processors. To do it, some assumptions on the protocol are used as well as simple induction rules. Second, the parameterized model is abstracted from the number of processors. It is done by syntactical transformations of the model assignments, expressions, and communication actions. Finally, the abstract model is verified with the Spin model checker in a usual way. The method description is accompanied by the proof of its correctness. It is stated that the suggested abstraction is conservative in a sense that every invariant (a property that is true in all reachable states) of the abstract model is an invariant of the original model (invariant properties are the properties of interest during verification of cache coherence protocols). The method has been automated by a tool prototype that, given a Promela model, parses the code, builds the abstract syntax tree, transforms it according to the rules, and maps it back to Promela. The tool (and the method in general) has been successfully applied to verification of the MOSI protocols implemented in the Elbrus computer systems. |
| first_indexed | 2024-12-19T00:03:20Z |
| format | Article |
| id | doaj.art-07be596aa44c46e9b29bfc5c9403b61e |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-19T00:03:20Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-07be596aa44c46e9b29bfc5c9403b61e2022-12-21T20:46:20ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-01284577610.15514/ISPRAS-2016-28(4)-4139Checking Parameterized Promela Models of Cache Coherence ProtocolsV. S. Burenkov0A. S. Kamkin1АО «МЦСТ»Институт системного программирования РАНThis paper introduces a method for scalable verification of cache coherence protocols described in the Promela language. Scalability means that resources spent on verification (first of all, machine time and memory) do not depend on the number of processors in the system under verification. The method is comprised of three main steps. First, a Promela model written for a certain configuration of the system is generalized to the model being parameterized with the number of processors. To do it, some assumptions on the protocol are used as well as simple induction rules. Second, the parameterized model is abstracted from the number of processors. It is done by syntactical transformations of the model assignments, expressions, and communication actions. Finally, the abstract model is verified with the Spin model checker in a usual way. The method description is accompanied by the proof of its correctness. It is stated that the suggested abstraction is conservative in a sense that every invariant (a property that is true in all reachable states) of the abstract model is an invariant of the original model (invariant properties are the properties of interest during verification of cache coherence protocols). The method has been automated by a tool prototype that, given a Promela model, parses the code, builds the abstract syntax tree, transforms it according to the rules, and maps it back to Promela. The tool (and the method in general) has been successfully applied to verification of the MOSI protocols implemented in the Elbrus computer systems.https://ispranproceedings.elpub.ru/jour/article/view/139многоядерные микропроцессоры, мультипроцессоры с разделяемой памятью, протоколы когерентности памяти, проверка моделей, spin, promela |
| spellingShingle | V. S. Burenkov A. S. Kamkin Checking Parameterized Promela Models of Cache Coherence Protocols Труды Института системного программирования РАН многоядерные микропроцессоры, мультипроцессоры с разделяемой памятью, протоколы когерентности памяти, проверка моделей, spin, promela |
| title | Checking Parameterized Promela Models of Cache Coherence Protocols |
| title_full | Checking Parameterized Promela Models of Cache Coherence Protocols |
| title_fullStr | Checking Parameterized Promela Models of Cache Coherence Protocols |
| title_full_unstemmed | Checking Parameterized Promela Models of Cache Coherence Protocols |
| title_short | Checking Parameterized Promela Models of Cache Coherence Protocols |
| title_sort | checking parameterized promela models of cache coherence protocols |
| topic | многоядерные микропроцессоры, мультипроцессоры с разделяемой памятью, протоколы когерентности памяти, проверка моделей, spin, promela |
| url | https://ispranproceedings.elpub.ru/jour/article/view/139 |
| work_keys_str_mv | AT vsburenkov checkingparameterizedpromelamodelsofcachecoherenceprotocols AT askamkin checkingparameterizedpromelamodelsofcachecoherenceprotocols |