Простой подход к рассуждениям о параллельно выполняемых программах состоит в том, чтобы определить их поведение как набор всех возможных чередований неделимых действий в отдельных потоках. Однако обоснование с точки зрения чередования оказывается слишком сложным и для людей, и для компьютеров, потому что число возможных чередований быстро растет.

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

Цель этого проекта — разработать формализованную теорию моделей параллелизма без чередования в системе Coq. Такая библиотека поможет исследователям, занимающимся этой темой, формально доказать свойства этих моделей и разработать новые варианты применения этой теории.

Репозиторий проекта