Preview

Труды Института системного программирования РАН

Расширенный поиск

Проверка параметризованных Promela-моделей протоколов когерентности памяти

https://doi.org/10.15514/ISPRAS-2016-28(4)-4

Аннотация

В статье представлен метод масштабируемой верификации Promela-моделей протоколов обеспечения когерентности памяти. Под масштабируемостью понимается независимость затрат на верификацию (прежде всего, машинного времени и памяти) от числа процессоров в системе. Метод состоит из трех основных шагов. На первом шаге в модель протокола, созданную для определенной конфигурации системы (для конкретного числа процессоров), вводится параметр, представляющий число процессоров в системе. Для этого используются простые индуктивные правила, что возможно только при определенных допущениях на вид протокола. На втором шаге построенная параметризованная модель абстрагируется от числа процессоров. Для этого над присваиваниями, выражениями и коммуникационными действиями модели совершается ряд синтаксических преобразований. На третьем шаге полученная абстрактная модель верифицируется с помощью инструмента Spin обычным образом. Помимо описания метода, в статье приводится доказательство его корректности: утверждается, что предложенная схема абстракции является консервативной в том смысле, что любой инвариант (свойство истинное во всех достижимых состояниях) абстрактной модели является инвариантом исходной модели (свойства-инварианты - это именно те свойства, которые представляют интерес при верификации протоколов обеспечения когерентности памяти). Предложенный метод был воплощен в прототипе инструмента, который разбирает код на языке Promela, строит дерево абстрактного синтаксиса, преобразует его по заданным правилам и отображает обратно в Promela код. Инструмент (и метод в целом) был успешно использован при верификации протоколов семейства MOSI, разработанных в АО «МЦСТ» и реализованных в вычислительных комплексах «Эльбрус».

Об авторах

В. С. Буренков
АО «МЦСТ»
Россия


А. С. Камкин
Институт системного программирования РАН
Россия


Список литературы

1. Patterson D.A., Hennessy J.L. Computer Organization and Design: The Hardware/Software Interface. Morgan Kaufmann, 2013. 800 p.

2. Ким A.K., Перекатов В.И., Ермаков С.Г. Микропроцессоры и вычислительные комплексы семейства «Эльбрус». Спб.: Питер, 2013. 272 с.

3. Sorin D.J., Hill M.D., Wood D.A. A Primer on Memory Consistency and Cache Coherence. Morgan and Claypool, 2011, 195 p.

4. Камкин А.С., Петроченков М.В. Система поддержки верификации реализаций протоколов когерентности с использованием формальных методов. Вопросы радиоэлектроники. Серия ЭВТ, 2014, вып. 3, стр. 27-38.

5. Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT Press, 1999, 314 p.

6. Буренков В.С. Анализ применимости инструмента SPIN к верификации протоколов когерентности памяти. Вопросы радиоэлектроники. Серия ЭВТ, 2014. вып. 3, стр. 126-134.

7. Emerson E.A., Kahlon V. Exact and Efficient Verification of Parameterized Cache Coherence Protocols. Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, 2003, pp. 247-262.

8. Holzmann, G.J. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003, 608 p.

9. Park S., Dill D.L. Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. Annual ACM Symposium on Parallel Algorithms and Architectures, 1996, pp. 288-296.

10. Ip C.N., Dill D.L. Verifying Systems with Replicated Components in Murphi. International Conference on Computer Aided Verification, 1996, pp. 147-158.

11. Pnueli A., Xu J., Zuck L. Liveness with (0, 1, )-Counter Abstraction. International Conference on Computer Aided Verification, 2002, pp. 107-122.

12. Clarke E., Talupur M., Veith H. Environment Abstraction for Parameterized Verification. Verification, Model Checking, and Abstract Interpretation, 2006. LNCS, vol. 3855, pp. 126-141.

13. Clarke E., Talupur M., Veith H. Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 33-47.

14. McMillan K. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. Conference on Correct Hardware Design and Verification Methods, 2001, pp. 179-195.

15. Chou C.-T., Mannava P.K., Park S. A Simple Method for Parameterized Verification of Cache Coherence Protocols. Formal Methods in Computer-Aided Design, 2004. LNCS, vol. 3312, pp. 382-398.

16. Krstic S. Parameterized System Verification with Guard Strengthening and Parameter Abstraction. International Workshop on Automated Verification of Infinite-State Systems, 2005.

17. Talupur M., Tuttle M.R. Going with the Flow: , pp. 1-8.

18. O'Leary J., Talupur M., Tuttle M.R. Protocol Verification Using Flows: An Industrial Experience. Formal Methods in Computer-Aided Design, 2009, pp. 172-179.


Рецензия

Для цитирования:


Буренков В.С., Камкин А.С. Проверка параметризованных Promela-моделей протоколов когерентности памяти. Труды Института системного программирования РАН. 2016;28(4):57-76. https://doi.org/10.15514/ISPRAS-2016-28(4)-4

For citation:


Burenkov V.S., Kamkin A.S. Checking Parameterized Promela Models of Cache Coherence Protocols. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(4):57-76. https://doi.org/10.15514/ISPRAS-2016-28(4)-4



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)