Исследовательская группа

Лаборатория языковых инструментов

Проверка моделей в слабых моделях памяти

April 13

Проверка моделей --- это метод автоматической формальной верификации программ. На сегодняшний день большинство инструментов для проверки моделей либо не учитывают эффекты, возникающие в слабых моделях памяти, либо работают только с некоторой фиксированной моделью. Среди этих инструментов выделяется GenMC, который не привязан к конкретной модели памяти. GenMC может работать с широким классом моделей (в который входят, например, модели RC11 и IMM). Тем не менее наиболее сложные и интересные модели (Promising, Weakestmo) не поддерживаются, так как эти в этих моделях не выполняются некоторые свойства, подразумеваемые GenMC. Кроме того, оказывается что и сами эти модели (Promising, Weakestmo), настолько "слабые", что какой-либо алгоритм их проверки может оказаться неприменимым на практике.

На семинаре мы рассмотрим алгоритм, лежащий в основе GenMC. Мы поговорим об ограничениях на входную модель памяти, которые накладывает GenMC и рассмотрим проблемы, возникающие при попытке осабить эти ограничения. Также будет предложена модифицированная версия модели Weakestmo, которая существенно упрощаёт алгоритм её проверки и в то же время сохраняет все желаемые свойства модели. В конце доклада будет приведён прототип усовершенствованного алгоритма GenMC, который добавляет поддержку модели Weakestmo.

Статьи к докладу:

Kokologiannakis, Michalis, Azalea Raad, and Viktor Vafeiadis. "Model checking for weakly consistent libraries." Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019.

Kokologiannakis, Michalis, and Viktor Vafeiadis. "HMC: Model Checking for Hardware Memory Models." Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems. 2020.