Mechanized theory of event structures: a case of parallel register machine

Модели истинной конкурентности и, в частности, структуры событий были представлены в 1980-ых как альтернатива операционным семантикам с чередованием, и на сегодняшний день эти модели вновь обретают популярность. Структуры событий позволяют явно выразить отношения причинно-следственной связи и конфликта между атомарными событиями системы, что приводит к более компактному и лаконичному представлению семантики. В данной отчете о текущей работе мы представляем теорию структур событий, механизированную в системе интерактивного доказательства теорем COQ и демонстрируем пример применения этой теории к проблеме задания сертифицированной исполняемой семантики простой параллельной регистровой машины с разделяемой памятью.