Формализация семантики и верификация многопоточных программ на основе структур событий тема диссертации и автореферата по ВАК РФ 00.00.00, кандидат наук Моисеенко Евгений Александрович
Моисеенко Евгений Александрович
кандидат наук
2023
- Специальность ВАК РФ00.00.00
- Количество страниц 275
Оглавление диссертации кандидат наук Моисеенко Евгений Александрович
Введение
Глава 1. Обзор
1.1 Слабые модели памяти
1.1.1 Программные примитивы
1.1.2 Требования к моделям памяти
1.1.3 Классы моделей памяти
1.1.4 Сравнение моделей памяти и открытые проблемы
1.2 Семантика параллельных программ и моделей памяти
1.2.1 Системы помеченных переходов
1.2.2 Языки помсетов и простые структуры событий
1.2.3 Графы сценариев исполнения
1.2.4 Структуры событий в модели Weakestmo
Глава 2. Модель Weakestmo и корректность компиляции
2.1 Схема доказательства теоремы о корректности компиляции
2.2 Модель IMM и обход графа сценария исполнения
2.3 Операционная семантика построения структуры событий
2.4 Симуляция обхода графа IMM
2.5 Кодирование доказательства в системе Coq
2.6 Выводы
Глава 3. Модель Weakestmo2: свобода от буферизации операций
чтения и локальность сертификации
3.1 Свобода от буферизации операций чтения
3.2 Локальность сертификации
3.3 Оптимизация алгоритма проверки моделей
3.4 Формализация модели Weakestmo2
3.4.1 Свобода от гонок и буферизации операций чтения
3.4.2 Корректность компиляции
3.4.3 Корректность локальных трансформаций
3.5 Выводы
Стр.
Глава 4. Верификация методом проверки модели для Weakestmo2
4.1 Метод проверки моделей для слабых моделей памяти
4.2 Инструмент GenMC
4.3 Инструмент WMC
4.4 Экспериментальное исследование
4.5 Выводы
Глава 5. Модель Weakestmo и классическая теория структур событий
5.1 Теория простых структур событий для моделей памяти
5.2 Сравнение структур событий в модели Weakestmo и простых структур событий
5.3 Кодирование теории простых структур событий в Coq
5.4 Выводы
Заключение
Список литературы
Список рисунков
Список таблиц
Рекомендованный список диссертаций по специальности «Другие cпециальности», 00.00.00 шифр ВАК
Операционные методы в приложении к слабым моделям памяти2018 год, кандидат наук Подкопаев Антон Викторович
Методы и средства верификации протоколов когерентности памяти2017 год, кандидат наук Буренков, Владимир Сергеевич
Автоматический поиск ошибок в компьютерных программах с применением динамического анализа2013 год, кандидат наук Исходжанов, Тимур Равилевич
Методы автоматизации построения поведенческой модели программного продукта на основе UCM-спецификаций2013 год, кандидат наук Никифоров, Игорь Валерьевич
Расчетная модель для нахождения состояния гонки в многопоточных алгоритмах2011 год, кандидат физико-математических наук Заборовский, Никита Владимирович
Введение диссертации (часть автореферата) на тему «Формализация семантики и верификация многопоточных программ на основе структур событий»
Введение
Актуальность темы. На сегодняшний день многопоточность широко применяется в самом разнообразном программном обеспечении — банковских системах, системах реального времени, ядрах операционных систем, системах управления базами данных и пр. Многопоточность позволяет эффективно задействовать современные многоядерные процессоры и значительно повысить скорость выполнения и отзывчивость программ. При этом семантика многопоточных программ принципиально сложнее, чем семантика последовательных программ. Данное обстоятельство является следствием недетерминированности переключения потоков при исполнении программы и отсутствием единой линейной последовательности выполнения ее инструкций. В итоге затруднена не только разработка, но и тестирование многопоточных программ — многие ошибки многопоточного программирования проявляются только в малом проценте сценариев и не воспроизводятся при повторных запусках программы. По этой причине актуальна верификация многопоточных программ, а решение этой задачи, в свою очередь, требует построения для них строгой математической семантики.
Формальная семантика многопоточной системы, оперирующей с общей разделяемой памятью, называется моделью памяти (memory model). Основной задачей модели памяти является определение множества допустимых сценариев исполнения программы.
Наиболее известной и интуитивно понятной моделью памяти является модель последовательной согласованности (sequential consistency), предложенная Лесли Лампортом в 1979 году [1]. Эта модель предполагает, что любой результат исполнения многопоточной программы может быть получен с помощью последовательного исполнения некоторого чередования инструкций потоков программы единственным вычислителем (например, ядром процессора): вычислитель делает один или несколько шагов вычисления в одном потоке, потом переключается на другой поток, выполняет несколько инструкций там, затем переключается на следующий поток, и так далее, пока все потоки не будут полностью исполнены. Во время исполнения каждый поток может иметь свой собственный локальный контекст (счетчик команд и состояние регистров), который переключается в вычислителе при смене текущего потока, но глобальное состояние разделяемой памяти является общим для всех потоков.
К сожалению, простая и интуитивная модель последовательной согласованности не может описать все возможные сценарии исполнения многопоточных программ, которые наблюдаются на современных системах. Это является следствием того, что компиляторы и процессоры применяют различные оптимизации при трансляции и выполнении программ. Данные оптимизации не меняют семантику однопоточной, последовательной, программы, однако эффекты от их применения могут наблюдаться при исполнении потоков на многопоточной системе. Например, компилятор может переставлять инструкции программы, а процессор — исполнять инструкции не по порядку (out of order).
Сценарии исполнения многопоточных программ, которые выходят за пределы модели последовательной согласованности, называются слабыми (weak behaviours), а допускающие их модели памяти — слабыми моделями памяти (weak memory models).
Вопрос о том, какие именно слабые сценарии поведения следует допускать, а какие нет, не является однозначным — ответ зависит от языка программирования и целевой процессорной архитектуры. По этой причине в последние годы появилось множество различных моделей памяти как для мультипроцессоров, x86 [2], ARM [3], POWER [4], так и для языков программирования, C/C++ [5], Java [6], JavaScript [7], OCaml [8], а также для распределенных систем [9; 10].
В связи с этим актуальна задача по формализации существующих моделей памяти и созданию теоретического инструментария для разработки будущих моделей памяти. В частности, открытой остается проблема разработки моделей памяти для высокопроизводительных языков программирования, таких как C/C++ и Java. К этим моделям предъявляется набор противоречивых требований. C одной стороны, они должны поддерживать оптимальные схемы компиляции в целевой код современных мультипроцессоров и допускать применение широкого спектра оптимизаций исходного кода — эти требования влекут к необходимости ослабления модели памяти. С другой стороны, данные модели должны предоставлять набор гарантий о поведении программ, что необходимо, в частности, для разработки инструментов формальной верификации.
Первоначальные версии моделей памяти языков C/C++ [5] и Java [6] не удовлетворяли приведенным выше требованиям [11—13]. В качестве возможных кандидатов им на замену были предложено множество различных моделей, в частности модели Weakestmo [14], Promising [15], MRD [16], PwT [17; 18] и другие [16; 19; 20]. Тем не менее, данные модели тоже подвергаются критике. Во-
первых, в доказательствах ключевых свойств некоторых из этих моделей были выявлены ошибки [19; 21; 22]. Во-вторых, в рамках вышеупомянутых моделей даже для небольших программ вычислительно затратно перечисление возможных слабых сценариев поведения, что препятствует разработке эффективных средств верификации многопоточных программ. Наконец, еще одним пунктом критики является чрезмерная концептуальная сложность данных моделей, а также обнаружение новых контруинтуитивных слабых сценариев поведения, допустимых этими моделями [16; 17; 23; 24].
Для того, чтобы исключить ошибки в доказательстве свойств моделей можно использовать автоматические системы доказательств — Coq [25], Agda [26], Lean [27], Arend [28]. Фактический, формализация математических выкладок в системах доказательства теорем уже стала стандартом не только в области слабых моделей памяти, но и в целом в области теории языков программирования, а также в ряде других областей. Практика использования таких систем получила название инженерии доказательств (proof engineering) и является отдельной активно развивающейся областью исследований [29].
Наличие строго определенной формальной семантики является необходимым предусловием для разработки инструментов верификации программ, в частности, инструментов проверки моделей [30] (model checking). Такие инструменты выполняют систематическое исследование различных трасс программы, выполняя поиск различных ошибок: состояний гонок (data races), взаимных блокировок (deadlocks), выхода за пределы выделенной памяти (out-of-bounds accesses), и других. Например, инструменты вроде GenMC [31] или CDSChecker [32] способны выполнять верификацию многопоточных программ, написанных на языках C/C++. Однако, подобные инструменты поддерживают либо только фрагмент модели памяти языков C/C++ [22], не учитывающий все возможные слабые сценарии поведения, либо демонстрируют низкую эффективность даже для небольших программ. Дело в том что, как уже было упомянуто, предложенные на сегодняшний день модели памяти для языков программирования C/C++ и Java допускают слишком большое количество слабых сценариев исполнения, что затрудняет процесс построения эффективных инструментов верификации. Это, в свою очередь, ставит вопрос о необходимости уточнения данных моделей с целью упрощения процесса верификации программ в этих моделях.
Перспективным способом решения проблемы концептуальной сложности слабых моделей памяти является теория структур событий [33]. Эта теория
позволяет декларативно описать семантику многопоточной системы. В наиболее простом варианте структура событий состоит из следующий элементов: множества атомарных событий; функции, присваивающей каждому событию семантическую метку; отношения причинно-следственной связи; отношения конфликта между событиями. Заметим, однако, что слабые модели памяти, использующие структуры событий, вводят новые виды таких структур, которые оказываются несовместимыми с классической теорией [33—37]. А это, в свою очередь, делает невозможным использование известных теоретических результатов о структурах событий [38—41]. В связи с этим возникает вопрос о том, могут ли данные модели или какие-то их содержательные подмножества быть выражены в рамках классической теории структур событий?
Таким образом, актуальной является задача построения и уточнения моделей памяти для языков программирования C/C++ и Java, формализации этих моделей в системах доказательства теорем и разработки на основе этих исследований инструментов верификации многопоточных программ.
Степень разработанности темы.
Теория слабых моделей памяти активно развивается, начиная с 1990-х годов — создано множество моделей памяти, описывающих поведение мультипроцессоров, многопоточных языков программирования и распределенных систем (см. обзор [42]). Эти модели, в свою очередь, можно разделить на несколько классов.
Модели, сохраняющие программный порядок, образуют широкий класс, включая модель TSO процессоров семейства x86 [2], модели последовательной согласованности (sequential consistency) [1], причинной согласованности (causal consistency) [10] и согласованности в конечном счёте (eventual consistency) [9]. В этот же класс входят модели памяти некоторых языков программирования, например, языка OCaml [8]. Общим недостатком всех этих моделей является то, что они не поддерживают оптимальные схемы компиляции в целевой код для широко распространённых мультипроцессоров ARM и POWER. Это означает, что реализация данных моделей на этих мультипроцессорах влечет дополнительные накладные расходы и может приводить к увеличению времени исполнения программ [43].
Модели памяти мультипроцессоров, в частности, ARM [3] и POWER [4], как правило, принадлежат к классу моделей, сохраняющих синтаксические зависимости. Основное ограничение этих моделей заключается в том, что они не поддерживают некоторые значимые трансформации программ, применяемые оптимизи-
рующими компиляторами, например, свертку констант. По этой причине модели данного класса, как правило, не применяются для языков программирования.
Таким образом, модели памяти двух вышеупомянутых классов не отвечают требованиям, предъявляемым к моделям памяти для таких языков как C/C++ и Java. С целью преодоления этих ограничений исследователями были предложены модели Promising [15], Weakestmo [14], MRD [16], PwT [17; 18], модель A.Jeffrey и J.Riely [19] и модель J.Pichon-Pharabod и P. Sewell [20]. Все эти модели обычно относят к классу моделей, сохраняющих семантические зависимости. Они, как правило, поддерживают оптимальные схемы компиляции для современных мультипроцессоров и широкий спектр оптимизаций программ.
Модели, сохраняющие программный порядок и синтаксические зависимости, в настоящее время хорошо изучены. Напротив, модели, сохраняющие семантические зависимости, по-прежнему активно исследуются. В частности, для них, фактически, не изучены вопросы построения эффективных инструментов автоматической и интерактивной верификации.
Рассмотрим в качестве примера язык C/C++. Для описания модели памяти данного языка исследовательским было предложено несколько подходов. Модель RC11 [22] относится к классу моделей, сохраняющих программный порядок. Данная модель является относительно простой и предоставляет ряд полезных на практике свойств. Для неё также были разработаны эффективные средства верификации, например, инструмент проверки моделей GenMC [44]. Однако эта модель не поддерживает оптимальную схему компиляции в мультипроцессоры ARM и POWER. С другой стороны, модели Promising и Weakestmo, относящиеся к классу моделей, сохраняющих семантические зависимости, хоть и поддерживают оптимальную схему компиляции и широкий набор оптимизаций программ, но оказываются существенно более сложными, а их свойства слабо изучены. Наконец, для этих моделей отсутствуют эффективные методы верификации программ.
В контексте данной работы была выбрана модель Weakestmo [14], которую её авторы предложили в качестве модели памяти для языков C/C++ и LLVM [45]. Модель Weakestmo основана на теории структур событий [33; 46]. Преимуществом использования данного формализма является декларативность, что позволяет упростить модификацию этой модели с целью добавления в нее новых свойств.
Ранее было доказано, что модель Weakestmo обладает рядом важных для практики свойств [14]. Однако у данной модели имеется ряд недостатков: для нее
ранее не была доказана корректность оптимальной схемы компиляции в модели современных мультипроцессоров, для данной модели отсутствуют средства верификации программ, а также эта модель не укладывается в классическую теорию структур событий [33].
Целью данной работы является исследование и модификация известной модели Weakestmo для разработки на ее основе инструментов верификации многопоточных программ.
Для достижения данной цели были сформулированы следующие задачи.
1. Формализовать в системе интерактивного доказательства теорем Coq модель памяти Weakestmo и доказательство корректности оптимальной схемы компиляции из модели Weakestmo в модели памяти современных мультипроцессоров.
2. Разработать строгую версию модели Weakestmo, допускающую реализацию эффективных инструментов автоматической верификации и доказать, что для неё сохраняются основные свойства Weakestmo (в частности, корректность компиляции, корректность локальных трансформаций программ, теорема о свободе от гонок).
3. Разработать инструмент проверки моделей (model checking) для предложенной модели.
4. Исследовать применимость классической теории структур в контексте слабых моделей памяти.
Методология и методы исследования. Диссертационное исследование базируется на теории формальных семантик для математически строгого описания сценариев поведения программ.
В работе используются классические формализмы, в частности, системы помеченных переходов, языки помеченных частично упорядоченных мультимножеств и структуры событий. Для формализации некоторых теорем и доказательств, представленных в данной работе, использовалась система интерактивного доказательства теорем Coq и библиотека формализованных математических теорий MathComp. Представленные в работе программные средства верификации реализованы на языке C и используют инструмент GenMC.
Основные положения, выносимые на защиту.
1. Доказана корректность оптимальной схемы компиляции из модели Weakestmo в модели современных мультипроцессоров TSO, ARM и
POWER; выполнена формализация модели Weakestmo, а также предложенного доказательства в системе Coq.
2. Предложена модель Weakestmo2, расширяющая модель Weakestmo новыми свойствами свободы от буферизации операций чтения и локальности сертификации, предназначенными для верификации; для Weakestmo2 доказано сохранение основных свойств модели Weakestmo: корректность компиляции, корректность локальных трансформаций программ, теорема о свободе от гонок.
3. Разработан инструмент WMC, выполняющий верификацию многопоточных программ, написанных на языке C, методом проверки моделей относительно модели памяти Weakestmo2; экспериментально показана эффективность данного инструмента по сравнению с аналогами.
4. Предложен метод кодирования слабых моделей памяти с помощью классических простых структур событий с предикатом консистентности. Теория данного класса структур событий формализована в системе Coq. Выделен фрагмент модели памяти Weakestmo, укладывающийся в эту теорию.
Научная новизна.
1. Впервые доказана корректность оптимальной схемы компиляции из модели памяти, основанной на структурах событий (Weakestmo), в модели памяти современных мультипроцессоров.
2. Впервые предложена модель памяти (Weakestmo2), принадлежащая к классу моделей, сохраняющих семантические зависимости, и при этом допускающая реализацию эффективных методов автоматической верификации программ.
3. Разработан инструмент проверки моделей WMC для модели памяти Weakestmo2, который является существенно более эффективным по сравнению с аналогами поддерживающими класс моделей памяти, сохраняющих синтаксические или семантические зависимости (HMC [47], rmem [48], Nidhugg [49; 50], CDSChecker [32]).
4. Впервые выполнена формализация классической теории простых структур событий в системе Coq.
Теоретическая и практическая значимость. Формализация модели памяти Weakestmo в системе Coq открывает путь к дальнейшей разработке инструмен-
тов для интерактивной верификации многопоточных программ с учетом слабых сценариев исполнения.
Предложенные в рамках модели Weakestmo2 новые свойства — свобода от буферизации операций чтения (load buffering race freedom) и локальности сертификации (certification locality), — также могут быть добавлены в другие модели памяти с целью разработки методов автоматической верификации программ в этих моделях. Наличие данных свойств позволяет оптимизировать алгоритм проверки моделей и таким образом существенно увеличить его эффективность.
Предложенный инструмент проверки моделей может быть использован на практике для отладки и верификации многопоточных программ, написанных на языке C, с учетом слабых сценариев исполнения, допустимых стандартом этого языка.
Исследование фрагмента модели памяти Weakestmo, укладывающегося в классическую теорию структур событий, закладывает основы для разработки обобщенной теории структур событий для описания слабых сценариев исполнения.
Достоверность полученных результатов обеспечивается математическими доказательствами, разработанными в том числе с использованием систем интерактивного доказательства теорем, а также экспериментами. Результаты находятся в соответствии с другими исследованиями в данной области.
Апробация работы. Основные результаты работы докладывались на следующих научных конференциях и семинарах: Surrey Concurrency Workshop (2324 июля 2019, Университет Суррея, Великобритания), внутренние семинары JetBrains Research (18 ноября 2018, 13 апреля 2020, Санкт-Петербург, Россия), The European Conference on Object-Oriented Programming (ECOOP, 15-17 ноября 2020, Берлин, Германия), Spring/Summer Young Researchers' Colloquium on Software Engineering (27-28 мая 2021, Москва, Россия), conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA, 5-10 декабря 2022, Окленд, Новая Зеландия).
Публикации. Основные результаты по теме диссертации изложены в 5 печатных изданиях, 1 из которых изданы в журналах, рекомендованных ВАК, 4 — в периодических научных журналах, индексируемых Web of Science и Scopus.
Личный вклад автора в публикациях, выполненных с соавторами, распределён следующим образом. В работе [51] автор предложил метод кодирования семантики параллельной регистровой машины с моделью памяти, сохраняющей
программный порядок, в терминах простых структур событий; соавторы участвовали в формализации данного метода в системе Coq. В работе [52] автор предложил метод кодирования семантического домена языков частично упорядоченных мультимножеств с использованием фактор-типов, соавторы участвовали в обсуждении данного метода и его формализации в системе Coq. В работе [42] автор выполнил сбор и анализ данных о существующих моделях памяти языков программирования; соавторы участвовали в создании структуры статьи и анализе результатов исследования. В работе [53] автор выполнил формализацию доказательства корректности компиляции из модели Weakestmo в модели современных мультипроцессоров; соавторы участвовали в обсуждении данного доказательства и выполнили его формализацию в системе Coq. В работе [54] автор формализовал новые свойства модели Weakestmo2, а именно, свойства свободы от буферизации операций чтения и локальности сертификации, доказал сохранение полезных свойств модели Weakestmo в Weakestmo2, а также разработал прототип инструмента проверки моделей WMC для модели Weakestmo2; соавторы участвовали в обсуждении формализации модели Weakestmo2, оказывали помощь при реализации нового инструмента, а также провели эксперименты.
Объем и структура работы. Диссертация состоит из введения, 5 глав, и заключения. Полный объём диссертации составляет 146 страниц, включая 39 рисунков и 5 таблиц. Список литературы содержит 96 наименований.
Благодарности. Я хочу поблагодарить своего научного руководителя Дмитрия Владимировича Кознова за его проницательность, отзывчивость и терпение на протяжении всего процесса написания этой диссертации. Также хочу выразить благодарность Антону Подкопаеву, который направлял мои исследования в области слабых моделей памяти и стал моим вторым научным руководителем.
Я благодарен своим коллегам и соавторам, с которыми имел удовольствие работать на протяжении многих лет, в том числе Михалису Кокологианнакису, Виктору Вафеядису, Ори Лахаву, Сохаму Чакраборти, Антону Трунову, Владимиру Гладштейну, Дмитрию Михайловскому, Дмитрию Мордвинову, Екатерине Вербицкой, Семену Григорьеву, Даниилу Березуну, Дмитрию Косареву, Петру Лозову, Рустаму Азимову.
Я также благодарен Дмитрию Булычеву, который познакомил меня с теорией языков программирования. Кроме того, хочу поблагодарить кафедру системного программирования Санкт-Петербургского государственного университета, ее
профессорско-преподавательский состав и руководителя — профессора Андрея Николаевича Терехова.
Я благодарен своей жене Анастасии Бирилло за ее поддержку и готовность всегда помочь мне. Я глубоко признателен своим родителям, Ирине Геннадьевне Моисеенко и Александру Николаевичу Моисеенко, которые воспитали во мне тягу к знаниям и поощряли мое стремление к образованию.
Глава 1. Обзор
В данной главе приводится введение в предметную область диссертационного исследования — семантику многопоточных программ и слабые модели памяти. Рассматриваются требования, предъявляемые к моделям памяти, обсуждаются существующие модели памяти, приводится их классификация. Рассматриваются недостатки существующих моделей памяти и открытые вопросы. Также вводятся необходимые математические формализмы, используемые для описания семантики многопоточных программ и слабых моделей памяти.
1.1 Слабые модели памяти
Напомним, что в контексте данного исследования моделью памяти называется формальная семантика многопоточных программ, оперирующих с разделяемой памятью. В данной работе будут рассмотрены модели памяти языков программирования — C/C++, Java и другие.
Как уже обсуждалось выше, одной из наиболее простых моделей памяти является модель последовательной согласованности (sequential consistency) [1]. В рамках данной модели каждый допустимый сценарий поведения многопоточной программы является результатом поочередного исполнения атомарных обращений к разделяемой памяти из параллельных потоков.
Рассмотрим в качестве примера программу, представленную ниже.
x := 1 rl ::= y if ri =0 {
//критическая секция
}
y :=1
r2 := x if Г2 = 0 {
//критическая секция
}
(Dekker's Lock)
Данная программа является упрощенной версией алгоритма блокировки Деккера [55]. В ней два потока соревнуются за доступ к критической секции. Для того, чтобы обозначить свое намерение войти в критическую секцию, каждый поток устанавливает значение переменной х или у соответственно 1. Право войти в
ХВ данной работе разделяемые переменные будем обозначать как х, у, г..., а локальные переменные как п, г2, г3...
критическую секцию получает тот поток, который успеет прочитать значение переменной до его установки другим потоком.
В рамках модели последовательной согласованности в результате выполнения данной программы либо один из потоков прочитает значение 1, а другой 0, либо оба прочитают значение 1, и в этом последнем случае ни один из потоков не войдет в критическую секцию. В результате имеем один из следующих допустимых результатов: [r1 = 0,r2 = 1], [r1 = 1,r2 = 0] или [r1 = 1,r2 = 1]. Соответствующие сценарии будем называть последовательно согласованными.
Алгоритм Деккера полагается на тот факт, что оба потока не могут одновременно прочитать значение 0. В противном случае не гарантируется свойство взаимного исключения, то есть два потока могут одновременно войти в критическую секцию. Тем не менее, если написать эту программу на языке C, скомпилировать её с помощью GCC и запустить на процессоре семейства x86/x64, то можно получить следующий результат: [ri = 0,r2 = 0]. Подобные сценарии, не укладывающиеся в модель последовательной согласованности, принято называть слабыми сценариями. Они могут появляться в результате выполнения различных оптимизаций компилятором при сборке программы или процессором при ее исполнении. Например, в случае программы Dekker's Lock, оптимизатор может выполнить переупорядочивание независимых инструкций записи в переменную x и чтения из переменной y в левом потоке. Для оптимизированной версии программы сценарий поведения, ведущий к результату [r1 = 0, r2 = 0], уже является последовательно согласованным. Таким образом, разработчик, использующий мно-гопоточноть, должен знать о возможных контринтуитивных сценариях поведения его программы. Для этого современные многопоточные языки программирования предоставляют слабые модели памяти, то есть формальную спецификацию поведения многопоточных программ, допускающую слабые сценарии поведения, поскольку более строгая модель последовательной согласованности запрещает применение широкого спектра оптимизаций и, следовательно, реализация данной модели на практике приводит к значительным накладным расходам [56—59].
Таким образом, разработчикам важно понимать, насколько слабую модель памяти предоставляет используемый ими язык программирования, какие оптимизации допускаются этой моделью и какие гарантии она предлагает программисту.
Далее в разделе 1.1.1 вводятся программные примитивы для работы с разделяемой памятью. В разделе 1.1.2 более подробно обсуждаются различные требования, предъявляемые к моделям памяти, а в разделе 1.1.3 обсуждаются существу-
Похожие диссертационные работы по специальности «Другие cпециальности», 00.00.00 шифр ВАК
Анализ корректности синхронизации компонентов ядра операционных систем2021 год, кандидат наук Андрианов Павел Сергеевич
Методы комплексного подхода к автоматизации дедуктивной верификации программ с финитными итерациями2022 год, кандидат наук Кондратьев Дмитрий Александрович
Методы и инструментальные средства формальной верификации функционально-потоковых параллельных программ2022 год, кандидат наук Ушакова Мария Сергеевна
Поиск ошибок переполнения буфера в исходном коде программ с помощью символьного выполнения2019 год, кандидат наук Дудина Ирина Александровна
Формальная семантика C-LIGHT программ и их верификация методом Хоара2004 год, кандидат физико-математических наук Промский, Алексей Владимирович
Список литературы диссертационного исследования кандидат наук Моисеенко Евгений Александрович, 2023 год
Список литературы
1. Lamport L. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs // IEEE Trans. Computers. — 1979. — T. 28, № 9. — C. 690—691.
2. Sewell P., Sarkar S., Owens S., Nardelli F. Z., Myreen M. O. x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors // Commun. ACM. — 2010. — T. 53, № 7. — C. 89—97.
3. Pulte C., Flur S., Deacon W., French J., Sarkar S., Sewell P. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8 // Proceedings of the ACM on Programming Languages. — 2018. — T. 2, POPL. — C. 1—29.
4. Sarkar S., Sewell P., Alglave J., Maranget L., Williams D. Understanding POWER Multiprocessors // PLDI 2011. — ACM, 2011. — C. 175—186.
5. Batty M., Owens S., Sarkar S., Sewell P., Weber T. Mathematizing C++ Concurrency // POPL 2011. — ACM, 2011. — C. 55—66.
6. Manson J., Pugh W., Adve S. V. The Java Memory Model // POPL 2005. — ACM, 2005. — C. 378—391.
7. Watt C., Pulte C., Podkopaev A., Barbier G., Dolan S., Flur S., Pichon-Pharabod J., Guo S.-y. Repairing and mechanising the JavaScript relaxed memory model // Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. — 2020. — C. 346—361.
8. Dolan S., Sivaramakrishnan K., Madhavapeddy A. Bounding data races in space and time // ACM SIGPLAN Notices. — 2018. — T. 53, № 4. — C. 242—255.
9. Jagadeesan R., Riely J. Eventual consistency for CRDTs // European Symposium on Programming. — Springer. 2018. — C. 968—995.
10. Lahav O., Boker U. Decidable verification under a causally consistent shared memory // Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. — 2020. — C. 211—226.
11. Sevcik J., Aspinall D. On validity of program transformations in the Java memory model // European Conference on Object-Oriented Programming. — Springer. 2008. — C. 27—51.
12. Vafeiadis V., Balabonski T., Chakraborty S., Morisset R., Zappa Nardelli F. Common compiler optimisations are invalid in the C11 memory model and what we can do about it // Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. — 2015. — C. 209—220.
13. Batty M., Memarian K., Nienhuis K., Pichon-Pharabod J., Sewell P. The Problem of Programming Language Concurrency Semantics // ESOP. T. 9032. — Springer, 2015. — C. 283—307. — (LNCS).
14. Chakraborty S., Vafeiadis V. Grounding thin-air reads with event structures // Proceedings of the ACM on Programming Languages. — 2019. — T. 3, POPL. — C. 1—28.
15. Kang J., Hur C.-K., Lahav O., Vafeiadis V., Dreyer D. A Promising Semantics for Relaxed-Memory Concurrency // POPL 2017. — ACM, 2017.
16. Paviotti M., Cooksey S., Paradis A., Wright D., Owens S., Batty M. Modular Relaxed Dependencies in Weak Memory Concurrency // European Symposium on Programming. — Springer, Cham. 2020. — C. 599—625.
17. Jagadeesan R., Jeffrey A., Riely J. Pomsets with preconditions: a simple model of relaxed memory // Proceedings of the ACM on Programming Languages. — 2020. — T. 4, OOPSLA. — C. 1—30.
18. Jeffrey A., Riely J., Batty M., Cooksey S., Kaysin I., Podkopaev A The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency // Proceedings of the ACM on Programming Languages. — 2022. — T. 6, POPL. —C. 1—30.
19. Jeffrey A., Riely J. On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory // LICS 2016. — IEEE, 2016.
20. Pichon-Pharabod J., Sewell P. A Concurrency Semantics for Relaxed Atomics that Permits Optimisation and Avoids Thin-Air Executions // POPL 2016. — ACM, 2016. — C. 622—633.
21. Pichon-Pharabod J. Y. A. A no-thin-air memory model for programming languages : дис. ... канд. / Pichon-Pharabod Jean Yves Alexis. — University of Cambridge, 2018.
22. Lahav O., Vafeiadis V., Kang J., Hur C.-K., Dreyer D. Repairing Sequential Consistency in C/C++11 // PLDI 2017. — ACM, 2017.
23. Lee S.-H., Cho M., Podkopaev A., Chakraborty S., Hur C.-K., Lahav O., Vafeiadis V. Promising 2.0: global optimizations in relaxed memory concurrency // Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. — 2020. — С. 362—376.
24. Cho M., Lee S.-H., Hur C.-K., Lahav O. Modular Data-Race-Freedom Guarantees in the Promising Semantics // Proceedings of the 42st ACM SIGPLAN Conference on Programming Language Design and Implementation. — 2021.
25. The Coq Development Team. The Coq Proof Assistant. — Вер. 8.13. — 01.2021. — URL: https://doi.org/10.5281/zenodo.4501022.
26. Agda language reference. — Available at https://agda.readthedocs.io/ [Online; accessed 7-May-2021].
27. Moura L. d., Ullrich S. The lean 4 theorem prover and programming language // International Conference on Automated Deduction. — Springer. 2021. — С. 625—635.
28. Arend theorem prover. — Available at https://arend-lang.github.io/ [Online; accessed 7-May-2021].
29. Ringer T., Palmskog K., Sergey I., Gligoric M., Tatlock Z. [и др.]. QED at large: A survey of engineering of formally verified software // Foundations and Trends® in Programming Languages. — 2019. — Т. 5, № 2/3. — С. 102—281.
30. Baier C., Katoen J.-P. Principles of model checking. — MIT Press, 2008.
31. Kokologiannakis M., Vafeiadis V. GenMC: A model checker for weak memory models // International Conference on Computer Aided Verification. — Springer. 2021. — С. 427—440.
32. Norris B., Demsky B. CDSchecker: checking concurrent data structures written with C/C++ atomics // Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications. — 2013. — С. 131—150.
33. Winskel G. Event structures // Advanced Course on Petri Nets. — Springer. 1986. — С. 325—392.
34. Nielsen M., Plotkin G., Winskel G. Petri nets, event structures and domains, part I // Theoretical Computer Science. — 1981. — Т. 13, № 1. — С. 85—108.
35. Boudol G., Castellani I. Flow models of distributed computations: event structures and nets : дис. ... канд. / Boudol Gérard, Castellani Ilaria. — INRIA, 1991.
36. Langerak R. Bundle event structures: a non-interleaving semantics for LOTOS // 5th International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols, FORTE 1992. — North-Holland Publishing Company. 1991. — С. 331—346.
37. Baldan P., Corradini A., Montanari U. Contextual Petri nets, asymmetric event structures, and processes // Information and Computation. — 2001. — Т. 171, № 1. — С. 1—49.
38. Vaandrager F. W. Determinism^(event structure isomorphism= step sequence equivalence) // Theoretical Computer Science. —1991. — Т. 79, № 2. — С. 275— 294.
39. Sassone V., Nielsen M., Winskel G. Deterministic behavioural models for concurrency // International Symposium on Mathematical Foundations of Computer Science. — Springer. 1993. — С. 682—692.
40. Nielsen M., Sassone V., Winskel G. Relationships between models of concurrency // Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems). — Springer. 1993. — С. 425—476.
41. Winskel G. Prime algebraicity // Theoretical Computer Science. — 2009. — Т. 410, № 41. — С. 4160—4168.
42. Moiseenko E., Podkopaev A., Koznov D. A Survey of Programming Language Memory Models // Programming and Computer Software. — 2021. — Vol. 47, no. 6. — P. 439—456.
43. Ou P., Demsky B. Towards understanding the costs of avoiding out-of-thin-air results // Proceedings of the ACM on Programming Languages. — 2018. — Т. 2, OOPSLA. — С. 1—29.
44. Kokologiannakis M., Raad A., Vafeiadis V. Model checking for weakly consistent libraries // Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. — 2019. — С. 96—110.
45. Chakraborty S., Vafeiadis V. Formalizing the concurrency semantics of an LLVM fragment //2017 IEEE/ACM International Symposium on Code Generation and Optimization (CGO). — IEEE. 2017. — С. 100—110.
46. Winskel G. Event structure semantics for CCS and related languages // International Colloquium on Automata, Languages, and Programming. — Springer. 1982. — С. 561—576.
47. Kokologiannakis M., Vafeiadis V. HMC: Model checking for hardware memory models // Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems. — 2020. — С. 1157—1171.
48. Pulte C., Pichon-Pharabod J., Kang J., Lee S.-H., Hur C.-K. Promising-ARM/RISC-V: a simpler and faster operational concurrency model // Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. — 2019. — С. 1—15.
49. Abdulla P. A., Aronis S., Atig M. F., Jonsson B., Leonardsson C., Sagonas K. Stateless Model Checking for TSO and PSO // Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS
2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. Т. 9035. — Springer. 2015. — С. 353.
50. Abdulla P. A., Atig M. F., Jonsson B., Leonardsson C. Stateless model checking for POWER // International Conference on Computer Aided Verification. — Springer.
2016. — С. 134—156.
51. Gladstein V., Mikhailovskii D., Moiseenko E., Trunov A. Mechanized Theory of Event Structures: A Case of Parallel Register Machine // Труды Института системного программирования РАН. — 2021. — Т. 33, № 3. — С. 143—154.
52. Moiseenko E., Gladstein V., Podkopaev A., Koznov D. Mechanization of pomset languages in the Coq proof assistant for the specification of weak memory models // Scientific and Technical Journal of Information Technologies, Mechanics and Optics. — 2022.
53. Moiseenko E., Podkopaev A., Lahav O., Melkonian O., Vafeiadis V. Reconciling Event Structures with Modern Multiprocessors // European Conference on Object-Oriented Programming, ECOOP 2020. Vol. 166. — Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020. — 5:1—5:26. — (Leibniz International Proceedings in Informatics (LIPIcs)). —URL: https://drops.dagstuhl. de/opus/volltexte/2020/13162.
54. Moiseenko E., Kokologiannakis M., Vafeiadis V. Model checking for a Multi-Execution Memory Model // Proceedings of the ACM on Programming Languages. — 2022. — T. 6, OOPSLA.
55. Dijkstra E. W. Cooperating sequential processes // The origin of concurrent programming. — Springer, 1968. — C. 65—138.
56. Marino D., Singh A., Millstein T., Musuvathi M., Narayanasamy S. A case for an SC-preserving compiler // ACM SIGPLAN Notices. — 2011. — T. 46, № 6. — C. 199—210.
57. Singh A., Narayanasamy S., Marino D., Millstein T., Musuvathi M. End-to-end sequential consistency // 2012 39th Annual International Symposium on Computer Architecture (ISCA). — IEEE. 2012. — C. 524—535.
58. Liu L., Millstein T., Musuvathi M. A Volatile-by-default JVM for Server Applications // Proceedings of the ACM on Programming Languages. — 2017. — T. 1, OOPSLA. — C. 1—25.
59. Liu L., Millstein T., Musuvathi M. Accelerating sequential consistency for Java with speculative compilation // Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. — 2019. — C. 16—30.
60. Flur S., Sarkar S., Pulte C., Nienhuis K., Maranget L., Gray K. E., Sezgin A., Batty M., Sewell P. Mixed-size concurrency: ARM, Power, C/C++ 11, and SC // ACM SIGPLAN Notices. — 2017. — T. 52, № 1. — C. 429—442.
61. Vollmer M., Scott R. G., Musuvathi M., Newton R. R. SC-Haskell: Sequential consistency in languages that minimize mutable shared heap // ACM SIGPLAN Notices. — 2017. — T. 52, № 8. — C. 283—298.
62. Klabnik S., Nichols C. The Rust Programming Language (Covers Rust 2018). — No Starch Press, 2019.
63. Alglave J., Maranget L., Tautschnig M. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory // ACM Trans. Program. Lang. Syst. — 2014. — T. 36, № 2. — 7:1—7:74.
64. Lahav O., Giannarakis N., Vafeiadis V. Taming release-acquire consistency // ACM SIGPLAN Notices. — 2016. — T. 51, № 1. — C. 649—662.
65. Boehm H.-J., Adve S. V. Foundations of the C++ concurrency memory model // ACM SIGPLAN Notices. — 2008. — T. 43, № 6. — C. 68—78.
66. Boudol G., Petri G. A theory of speculative computation // European Symposium on Programming. — Springer. 2010. — C. 165—184.
67. Boehm H.-J., Demsky B. Outlawing Ghosts: Avoiding Out-of-thin-air Results // MSPC 2014. — ACM, 2014. — 7:1—7:6.
68. Kokologiannakis M., Lahav O., Sagonas K., Vafeiadis V. Effective stateless model checking for C/C++ concurrency // Proceedings of the ACM on Programming Languages. — 2017. — T. 2, POPL. — C. 1—32.
69. Muchnick S. Advanced compiler design and implementation. — Morgan Kaufmann, 1997.
70. Alglave J., Maranget L., McKenney P. E., Parri A., Stern A. Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel // Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems. — 2018. — C. 405—418.
71. Pratt V. The pomset model of parallel processes: Unifying the temporal and the spatial // International Conference on Concurrency. — Springer. 1984. — C. 180—196.
72. Gischer J. L. The equational theory of pomsets // Theoretical Computer Science. — 1988. — T. 61, № 2/3. — C. 199—224.
73. Weakestmo Memory Model and compilation correctness proofs for it. — Available at https : / / github . com / weakmemory / weakestmoToImm/ [Online; accessed 12-August-2022].
74. Podkopaev A., Lahav O., Vafeiadis V. Bridging the gap between programming languages and hardware weak memory models // Proceedings of the ACM on Programming Languages. — 2019. — T. 3, POPL. — C. 1—31.
75. Milner R. An Algebraic Definition of Simulation Between Programs. // IJCAI: Proceedings of the 2nd International Joint Conference on Artificial Intelligence. London, UK, September 1971. — William Kaufmann Inc. 1971. — С. 481—489.
76. Hahn : A Coq library for lists and relations. — Available at https://github.com/ vafeiadis/hahn [Online; accessed 16-December-2022].
77. Intermediate Memory Model (IMM) and compilation correctness proofs for it. — Available at https : / / github . com / weakmemory / imm [Online; accessed 16-December-2022].
78. Chalupa M., Chatterjee K., Pavlogiannis A., Sinha N., Vaidya K. Data-centric dynamic partial order reduction // Proceedings of the ACM on Programming Languages. — 2017. — Т. 2, POPL. — С. 1—30.
79. Abdulla P. A., Atig M. F., Jonsson B., Ngo T. P. Optimal stateless model checking under the release-acquire semantics // Proceedings of the ACM on Programming Languages. — 2018. — Т. 2, OOPSLA. — С. 1—29.
80. Abdulla P. A., Atig M. F., Jonsson B., Lâng M., Ngo T. P., Sagonas K. Optimal stateless model checking for reads-from equivalence under sequential consistency // Proceedings of the ACM on Programming Languages. — 2019. — Т. 3, OOPSLA. — С. 1—29.
81. rmem. rmem: Executable concurrency models for ARMv8, RISC-V, Power, and x86. — 2009. — URL: https://github.com/rems-project/rmem (дата обр. 15.08.2022).
82. Alglave J., Maranget L., Sarkar S., Sewell P. Litmus: Running tests against hardware // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2011. — С. 41—44.
83. SV-COMP. Competition on Software Verification (SV-COMP). — 2019. — URL: https://sv-comp.sosy-lab.org/2019/ (дата обр. 16.08.2022).
84. Varacca D., Yoshida N. Typed event structures and the linear n-calculus // Theoretical Computer Science. — 2010. — Т. 411, № 19. — С. 1949—1973.
85. Crafa S., Varacca D., Yoshida N. Event structure semantics of parallel extrusion in the pi-calculus // International Conference on Foundations of Software Science and Computational Structures. — Springer. 2012. — С. 225—239.
86. Hildebrandt T. T., Johansen C., Normann H. A stable non-interleaving early operational semantics for the pi-calculus // International Conference on Language and Automata Theory and Applications. — Springer. 2017. — C. 51—63.
87. Castellan S., Yoshida N. Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side // Proceedings of the ACM on Programming Languages. — 2019. — T. 3, POPL. — C. 1—29.
88. MahboubiA., Tassi E. Mathematical components. — 2017. — URL: https://math-comp.github.io/mcb/.
89. Gonthier G., Mahboubi A. An introduction to small scale reflection in Coq // Journal of formalized reasoning. — 2010. — T. 3, № 2. — C. 95—152.
90. Gonthier G., Mahboubi A., Tassi E. A small scale reflection extension for the Coq system. — 2016.
91. Garillot F., Gonthier G., Mahboubi A., Rideau L. Packaging mathematical structures // International Conference on Theorem Proving in Higher Order Logics. — Springer. 2009. — C. 327—342.
92. Cohen C., Sakaguchi K., Tassi E. Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi // FSCD 2020-5th International Conference on Formal Structures for Computation and Deduction. — 2020. — C. 34—1.
93. Mechanized Theory of Event Structures. — Available at https://github.com/ Event-Structures/event-struct [Online; accessed 12-August-2022].
94. Perrin M., Mostéfaoui A., Jard C. Causal consistency: beyond memory // Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. — 2016. — C. 1—12.
95. Bartoletti M., Cimoli T., Pinna G. M., Zunino R. Contracts as games on event structures // Journal of logical and algebraic methods in programming. — 2016. — T. 85, № 3. — C. 399—424.
96. Fellner A., Tarrach T., Weissenbacher G. Language inclusion for finite prime event structures // International Conference on Verification, Model Checking, and Abstract Interpretation. — Springer. 2020. — C. 314—336.
Список рисунков
1.3 Пример системы помеченных переходов и принимаемого ей языка. . . 30
1.4 Пример кодирования языка системы переходов как языка помеченных частично упорядоченных мультимножеств и как
простой структуры событий.........................32
1.5 Графы сценариев исполнения программы LB-nodep............36
1.6 Графы сценариев исполнения, обосновывающие результат а = Ь = 1. . 40
1.7 Пример некогерентного графа сценария исполнения...........42
1.8 Пример неатомарного графа сценария исполнения............43
1.9 Пример графа сценария исполнения, который не является последовательно согласованным.....................45
1.10 Weakestmo-консистентная структура событий программы LB-nodep и извлеченный из нее граф сценария исполнения..............47
2.1 Операционная семантика обхода 1ММ графа................54
2.2 Операционная семантика построения структуры событий Weakestmo. . 56
2.3 Вспомогательные определения для операционной семантики построения структуры событий Weakestmo................57
2.4 Пример программы и соответствующий ей 1ММ граф...........58
2.5 Граф сценария исполнения конфигурация обхода ТСа и соответствующая этой конфигурации структура событий Sa вместе с конфигурацией Ха. Покрытые события помечены как □, а выпущенные — как О. События, принадлежащие конфигурации Ха, помечены как' I1................................61
2.6 Граф сценария исполнения конфигурация обхода ТСЬ и соответствующая этой конфигурации структура событий Sь вместе с конфигурацией Хь..............................62
2.7 Граф сценария исполнения конфигурация обхода ТСс и соответствующая этой конфигурации структура событий Sc вместе с конфигурацией Хс..............................65
3.1 Пример гонки с буферизацией операции чтения..............72
3.2 Пример свободной от буферизации операций чтения программы и соответствующих ей Weakestmo консистентных графов сценариев исполнения..................................73
3.3 Weakestmo (но не Weakestmo2) консистентная структура событий для программы 1_БРР-сех.............................73
3.4 Программа, содержащая гонку с буферизацией операции чтения и дополнительную операцию записи.....................74
3.5 Программа, содержащая гонку с буферизацией операции чтения и цикл. 74
3.6 Программа LB+Rdep и ее граф сценария исполнения, содержащий
гонку с буферизацией операции чтения................... 77
3.7 Иллюстрация к доказательству теоремы 1_БРР...............81
3.8 Частично построенная Weakestmo2 консистентная структура
событий программы LB-IMM........................83
3.9 Список трансформаций переупорядочивания независимых инструкций. 85
3.10 Список трансформаций элиминации избыточных инструкций......85
3.11 Фрагмент построения структур событий для доказательства корректности переупорядочивания инструкции чтения после инструкции записи..............................86
4.1 Программа и один из ее Weakestmo2-консистентных графов
сценариев исполнения............................99
5.1 Пример программы и соответствующей ей разделимой на потоки простой структуры событий.........................116
5.2 Пример построения по программе соответствующей ей, разделимой
на потоки, простой структуры событий................... 120
5.3 Пример программы для которой полная структура события не
является Weakestmo консистентной.....................127
5.4 Пример программы для которой множество Weakestmo консистентных графов сценариев исполнения не является префикс-замкнутым. ............................ 128
5.5 Вариант программы LB+CAS после переупорядочивания инструкций в первом потоке, а также соответствующая ей структура событий Weakestmo...................................130
Список таблиц
1.1 Список примитивов модели памяти.....................17
1.2 Классы моделей памяти и их свойства...................27
4.2 Отсутствие (—) или наличие (+) гонок с буферизацией операций
чтения в тестовых программах........................105
4.3 Время работы на тестовом наборе GenMC.................106
4.4 Время работы на тестовом наборе SV-COMP [83].............107
4.5 Время работы на тестовом наборе CDSChecker [32]............108
4.6 Количество исследуемых WMC сценариев исполнения для синтетических программ........................... 109
SAINT-PETERSBURG STATE UNIVERSITY
On the rights of the manuscript
Evgenii Moiseenko
Formalization of Semantics and Verification of Concurrent Programs Based on Event Structures
Scientific specialty
2.3.5.Mathematical and software support for computers, complexes and computer
networks
DISSERTATION for the degree of Candidate of Physico-Mathematical Sciences
Translation from Russian
Scientific supervisor: Doctor of Science, Associate Professor
Dmitry Koznov
Saint Petersburg— 2023
Contents
Стр.
Introduction........................................................................4
Chapter 1. Background .............................12
1.1 Weak Memory Models..........................12
1.1.1 Programming Primitives.....................13
1.1.2 Memory Model Requirements..................16
1.1.3 Classes of Memory Models ...................20
1.1.4 Comparison of Memory Models and Open Problems......23
1.2 Formal Semantics of Concurrent Programs and Memory Models .... 24
1.2.1 Labelled Transition Systems...................24
1.2.2 Pomset Languages and Prime Event Structures.........26
1.2.3 Execution Graphs.........................29
1.2.4 Weakestmo Event Structures...................38
Chapter 2. Weakestmo and Soundness of Compilation Schemes.......43
2.1 Proof Sketch of the Soundness Theorem.................43
2.2 IMM and Execution Graph Traversal...................45
2.3 Operational Semantics of Event Structure Construction ..................48
2.4 Simulation of IMM Graph Traversal...................48
2.5 Encoding Proof in Coq ....................................................58
2.6 Conclusions ................................................................60
Chapter 3. Weakestmo2, Load Buffering Race Freedom and Certification
Locality................................61
3.1 Load Buffering Race Freedom......................61
3.2 Certification Locality ......................................................64
3.3 Optimizations of Model Checking....................66
3.4 Formalization of Weakestmo2......................68
3.4.1 Load Buffering and Data Race Freedom.............69
3.4.2 Soundness of Compilation Schemes...............72
3.4.3 Soundness of Local Program Transformations..........73
CTp.
3.5 Conclusions................................76
Chapter 4. Model Checking for Weakestmo2..................78
4.1 Model Checking for Weak Memory Models...............78
4.2 GenMCTool...............................79
4.3 WMC ................................... 84
4.4 Experimental Evaluation of WMC....................88
4.5 Conclusions ................................ 95
Chapter 5. Weakestmo and Classical Theory of Event Structures ......97
5.1 Prime Event Structures Theory for Memory Models...........99
5.2 Comparison of Weakestmo and Prime Event Structures.........110
5.3 Encoding Prime Event Structures in Coq.................114
5.4 Conclusions ................................ 115
Conclusion ..................................... 117
References.....................................118
List of Figures...................................127
List of Tables....................................129
Introduction
Actuality.
Nowadays multithreading is used in a wide variety of software, such as banking systems, real-time systems, operating system kernels, database management systems, and numerous others. Multithreading enables effective use of modern multi-core processors, substantially enhancing the execution speed and responsiveness of programs. However, the semantics of multithreaded programs is fundamentally more complicated than the semantics of sequential programs. This is due to non-deterministic thread switching during program execution and the absence of a single linear instruction execution order. As a result, it is difficult not only to develop, but also to test multithreaded programs—many errors of multithreaded programming manifest themselves only in a small percentage of scenarios and are hardly reproducible. For this reason, verification of multithreaded programs is a relevant problem, and its solution requires the construction of a rigorous mathematical semantics.
Formal semantics of a multithreaded system operating with shared memory is called a memory model. The main purpose of a memory model is to determine the set of valid execution scenarios of a program.
The most well-known and intuitive memory model is the sequential consistency model proposed by Leslie Lamport in 1979 [1]. This model assumes that any result of executing a multithreaded program can be obtained by sequentially executing some sequence of instructions from the program's threads by a single computer (for example, a processor core): it performs one or more computation steps in one thread, then switches to another thread, executes a few instructions there, then switches to the next thread, and so on until all threads are fully executed. During execution, each thread can have its own local context (instruction counter and state of registers), which switches in the computer when the current thread is changed, but the global state of memory is shared between all threads.
Unfortunately, the simple and intuitive sequential consistency model cannot describe all possible execution scenarios of multithreaded programs that are observed in modern systems. This is a consequence of compilers and processors applying various optimizations when translating and executing programs. These optimizations do not change the semantics of a single-threaded, sequential program, but the effects of their application can be observed when executing threads on a multithreaded system. For
example, a compiler can rearrange program instructions, and a processor can execute instructions out of order.
Execution scenarios of multithreaded programs that go beyond the sequential consistency model are called weak behaviors, and the memory models that allow them are called weak memory models.
The question of which weak behavior scenarios should be allowed and which should not is ambiguous: its answer depends on the programming language and the target processor architecture. For this reason, many different memory models have appeared in recent years, both for multiprocessors such as x86 [2], ARM [3], POWER [4], and for programming languages such as C/C++ [5], Java [6], JavaScript [7], OCaml [8], as well as distributed systems [9; 10].
Hence, the task of formalizing existing memory models and creating a theoretical framework for the development of future memory models is very relevant. In particular, the problem of developing memory models for high-performance programming languages such as C/C++ and Java remains unsolved. These models have to meet contradictory requirements. On the one hand, they must support optimal compilation to target code of modern multiprocessors and permit a wide range of source code optimizations— these requirements entail the need to weaken the memory model. On the other hand, these models should provide a set of guarantees about the behavior of programs, which is necessary, in particular, for the development of formal verification tools.
Initial versions of memory models of C/C++ [5] and Java [6] did not meet the above requirements [11—13]. Many different models have been proposed as possible replacements, in particular, Weakestmo [14], Promising [15], MRD [16], PwT [17; 18] and others [16; 19; 20]. However, these models have also faced criticism. First, errors were identified in the proofs of key properties of some of them [19; 21; 22]. Second, in these models, even for small programs, it is computationally expensive to enumerate possible weak behavior scenarios, which hinders the development of effective verification tools for multithreaded programs. Finally, another problematic point is the excessive conceptual complexity of these models, as well as the discovery of new counter-intuitive weak behavior scenarios that they permit [16; 17; 23; 24].
In order to eliminate mistakes in the proofs of models' properties, researchers can use interactive proof assistants, such as Coq [25], Agda [26], Lean [27], and Arend [28]. In fact, formalization of proofs in such systems has already become a standard not only in the field of weak memory models, but also in programming language theory in gen-
eral, as well as in several other areas. The practice of using such systems has been named proof engineering, and it is a separate, actively growing field of research [29].
The presence of strictly defined formal semantics is a necessary precondition for the development of program verification tools, in particular, tools for model checking [30]. Such tools systematically examine program traces searching for various errors, such as: data races, deadlocks, out-of-bounds accesses and others. For example, tools like GenMC [31] or CDSChecker [32] are able to perform verification of multithreaded programs written in C/C++. However, such tools either support only a fragment of the C/C++ memory model [22] that does not take into account all possible weak behavior scenarios, or they demonstrate low efficiency even for small programs. The fact is that, as noted previously, the memory models proposed today for C/C++ and Java allow for an excessive number of weak execution scenarios, which complicates the process of building effective verification tools. This, in turn, raises the question of the need to refine these models in order to simplify the program verification process.
A promising approach to solving the problem of conceptual complexity of weak memory models is the theory of event structures [33]. This theory makes it possible to declaratively describe the semantics of a multithreaded system. The simplest version of an event structure consists of the following: a set of atomic events; a function that assigns a semantic label to each event; causality and conflict relations between events. Note, however, that existing weak memory models based on event structures introduce new types of such structures that turn out to be incompatible with classical theory [33— 37]. And this, in turn, makes it impossible to use known theoretical results on event structures [38—41]. In this regard, the question arises whether these models or some of their meaningful subsets can be expressed within the framework of the classical theory of event structures.
Thus, this proves the relevance of the tasks of constructing and refining memory models for C/C++ and Java, formalizing these models in automated proof systems, and development of verification tools for multithreaded programs based on these studies.
Background.
The theory of weak memory models has been under active development starting in the 1990s. Since then, many memory models that describe behavior of multiprocessors, multithreaded programming languages, and distributed systems have been created (see review [42]). These models, in turn, can be divided into several classes.
Models that preserve program order constitute a large class, which includes the TSO model of x86 processors [2], sequential consistency models [1], causal consis-
tency [10] and eventual consistency [9]. It also includes memory models of some programming languages, for example, OCaml [8]. The common disadvantage of all listed models is that they do not support optimal compilation to target code of modern multiprocessor architectures such as ARM and POWER. This means that the implementation of these models for these multiprocessors incurs additional overhead and may degrade program performance [43].
The memory models of multiprocessors, in particular ARM [3] and POWER [4], as a rule, belong to the class of models that preserve syntactic dependencies. The main limitation of these models is that they do not support some important program transformations used by optimizing compilers, for example, constant folding. For this reason, models of this class are generally not used for programming languages.
Thus, the memory models of the two aforementioned classes do not meet the requirements for memory models for languages such as C/C++ and Java. In order to overcome these limitations, researchers have proposed the following models: Promising [15], Weakestmo [14], MRD [16], PwT [17; 18], the model by A.Jeffrey and J.Riely [19] and the model by J.Pichon-Pharabod and P. Sewell [20]. All listed models are usually classified as semantic dependency preserving models. They usually support optimal compilation for modern multiprocessors and a broad range of program optimizations.
Models that preserve program order and syntactic dependencies are well studied. In contrast, models that preserve semantic dependencies are still being actively investigated. In fact, development of effective tools for automatic and interactive verification for these models has not been studied in depth.
Consider the C/C++ language as an example. To describe the memory model of this language, researchers have proposed several approaches. The RC11 [22] model belongs to the class of models that preserve program order. This model is relatively simple and provides a number of properties useful in practice. Effective verification tools such as GenMC [44] have been developed for this model. However, it does not support optimal compilation schemes in ARM and POWER multiprocessors. On the other hand, consider the Promising and Weakestmo models that preserve semantic dependencies: although they support an optimal compilation scheme and a wide range of program optimizations, they are significantly more complex, and their properties are poorly studied. Finally, there are no effective methods of program verification for these models.
For this work, we chose the Weakestmo [14] model, that was proposed as a memory model for C/C++ and LLVM [45]. The Weakestmo model is based on the theory of event structures [33; 46]. The advantage of using this formalism is its declarative nature, which makes it easier to modify this model in order to add new properties to it.
Earlier it was proved that the Weakestmo model has a number of important properties for practical use [14]. However, this model has a number of disadvantages: the soundness of optimal compilation to the model of modern multiprocessors has not been proven yet, there are no software verification tools for this model, and it does not fit into the classical theory of event structures [33].
The aim of this work is to study and modify the well-known Weakestmo model for the development of multithreaded program verification tools based on it.
To achieve this goal, the following tasks were formulated.
a) Formalize the Weakestmo memory model and the proof of soundness of the optimal compilation scheme from Weakestmo to the memory models of modern multiprocessors using the Coq interactive theorem prover.
b) Develop a stronger version of the Weakestmo model, enabling implementation of effective automatic verification tools, and prove that it preserves the properties of the original Weakestmo model (in particular, soundness of compilation, soundness of local transformations of programs, the data race freedom theorem).
c) Develop a model checking tool for the proposed model.
d) Investigate the applicability of the classical theory of event structures in the context of weak memory models.
Methodology and research methods. This dissertation is based on the theory of formal semantics for mathematically rigorous description of program behavior.
The paper uses classical formalisms, in particular, labeled transition systems, languages of labeled partially ordered multisets, and event structures. To formalize some of the theorems and proofs presented in this paper, we used the Coq proof assistant and the MathComp library which provides access to formalized mathematical theories. The software verification tool presented in the dissertation is implemented in C on top of GenMC tool.
The main results submitted for defense.
a) We prove the soundness of optimal compilation schemes from Weakestmo to the models of modern multiprocessors TSO, ARM and POWER; we formalize Weakestmo, as well as the proposed proof, in Coq.
b) We propose the Weakestmo2 model, which extends Weakestmo with new properties of load buffering race freedom and certification locality required for verification; we prove the preservation of the basic properties of Weakestmo for Weakestmo2: soundness of compilation, soundness of local transformations of programs, and the data race freedom theorem.
c) We develop the WMC tool, which performs verification of multithreaded programs written in C using the model checking with regards to the Weakestmo2 memory model; we show the effectiveness of this tool in comparison with its counterparts.
d) We propose a method for encoding weak memory models using classical prime event structures with a consistency predicate. The theory of this class of event structures is formalized in Coq. The fragment of the Weakestmo memory model that fits into this theory is identified.
Scientific novelty.
a) For the first time, we prove the soundness of optimal compilation from the memory model based on event structures (Weakestmo) to the memory models of modern multiprocessors.
b) For the first time, we propose a memory model (Weakestmo2) which preserves semantic dependencies, and at the same time allows the implementation of effective methods for automatic verification of programs.
c) The WMC model checking tool for the Weakestmo2 memory model has been developed, which is significantly more efficient compared to its counterparts that support a class of memory models preserving syntactic or semantic dependencies
d) For the first time, we formalize the classical prime event structure theory in Coq.
Theoretical and practical influence. The formalization of the Weakestmo memory model in Coq opens the path to further development of tools for interactive verification of multithreaded programs that take into account weak execution scenarios.
New properties proposed within the Weakestmo2 model—load buffering race freedom and certification locality—can also be added to other memory models in order to develop methods for automatic verification of programs in these models. These properties make it possible to optimize the model checking algorithm and thus significantly increase its efficiency.
The proposed model checking tool can be used in practice for debugging and verification of multithreaded programs written in C, taking into account weak execution scenarios allowed by the language standard.
The presented study of a fragment of the Weakestmo memory model that fits into the classical theory of event structures lays the foundations for the development of a generalized theory of event structures for describing weak execution scenarios.
The reliability of the obtained results is ensured by the presented mathematical proofs, developed both with and without interactive theorem provers, as well as conducted experiments. The results are in line with other studies in the field.
Approbation. The main results of the work were reported at the following scientific conferences and seminars: Surrey Concurrency Workshop (July 23-24, 2019, University of Surrey, UK), JetBrains Research Internal Seminars (November 18, 2018, April 13, 2020, St. Petersburg, Russia), The European Conference on Object-Oriented Programming (ECOOP, November 15-17, 2020, Berlin, Germany), Spring/Summer Young Researchers' Colloquium on Software Engineering (May 27-28, 2021, Moscow, Russia), conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA, December 5-10, 2022, Auckland, New Zealand).
Publications. The main results on the topic of the thesis are presented in 5 scientific papers, 1 of the publications in a journal recommended by the Higher Attestation Commission, 4 — in periodic scientific journals indexed by Web of Science and Scopus.
Scope and structure of work. The dissertation consists of an introduction, 5 chapters, and a conclusion. The full scope of the thesis is 129 pages, including 39 figures h 5 tables. The list of references contains 96 titles.
Acknowledgments. I would like to thank my supervisor, Dmitry Koznov, for his insight, responsiveness, and patience throughout the process of writing this dissertation. I also want to express my gratitude to Anton Podkopaev, who helped me to navigate in the field of weak memory models and who became my second scientific supervisor.
I am grateful to my colleagues and co-authors with whom I had pleasure to work through the years, including Michalis Kokologiannakis, Viktor Vafeiadis, Ori Lahav, Soham Chakraborty, Anton Trunov, Vladimir Gladstein, Dmitry Mikhailovskii, Dmitry Mordvinov, Ekaterina Verbitskaia, Semyon Grigorev, Daniil Berezun, Dmitry Kosarev, Peter Lozov, Rustam Azimov.
I am thankful to Dmitry Boulytchev, who introduced me to the theory of programming languages. I also want to thank Software Engineering Department at Saint Petersburg State University, its faculty members and its head—professor Andrey Terekhov.
I am grateful to my wife, Anastasiia Birillo, for her support and her willingness to always help me. I am deeply appreciative of my parents, Irina Moiseenko and Alexander Moiseenko, who cultivated within me a passion for learning and encouraged my pursuit of education.
Chapter 1. Background
This chapter serves as an introduction to the domain of the dissertation research: the semantics of multithreaded programs and weak memory models. In this chapter, we consider existing memory models and their classification, as well as the requirements posed for a memory model. Furthermore, we also discuss shortcomings of the existing memory models and open questions of the domain. Finally, in this chapter we introduce the necessary mathematical formalisms used to describe the semantics of multithreaded programs and weak memory models.
1.1 Weak Memory Models
Recall that in the context of this study, a memory model is the formal semantics of multithreaded programs operating with shared memory. Further on, we will consider memory models of programming languages, such as C/C++, Java and others.
As discussed above, one of the simplest memory models is the sequential consistency [1] memory model. Within its framework, each admissible behavior of a multithreaded program is the result of sequential execution of atomic operations on shared memory from parallel threads.
Consider the program below as an example.
x := 1
ri := y if ri = 0 {
//critical section
}
y :=1
r2 := x
if r2 = 0 { (Dekker's Lock)
//critical section
}
This program is a simplified version of Dekker's algorithm [47]. Two threads compete for access to the critical section. To indicate its intention to enter the critical section, each thread sets the value of x or y respectively. 1 The right to enter the critical section is given to the thread that manages to read the value of the variable before it is set by another thread.
Under the sequential consistency model, as a result of executing this program, either one of the threads will read the value 1 and the other 0, or both will read the
1In this thesis, shared variables are denoted as x, y, z..., and local variables—as ri, r2, rs..
value 1, in which case neither thread will enter the critical section. As a result, we have one of the following valid results: [n = 0, r2 = 1], [r\ = 1,r2 = 0], or [n = 1,r2 = 1]. The corresponding behaviors are called sequentially consistent.
Dekker's algorithm relies on the fact that both threads cannot read the value 0 at the same time. Otherwise, the mutual exclusion property is not guaranteed, i.e. two threads can enter the critical section at the same time. However, if one writes this program in C, compile it with GCC, and run it on an x86/x64 family processor, one can get the following result: [n = 0,r2 = 0]. Such behaviors that do not fit into the sequential consistency model are called weak behaviors. They can appear as a result of various optimizations performed by the compiler when compiling the program or by the processor when it is executed. For example, in the case of Dekker's Lock, the optimizer can reorder independent instructions, that is, reorder the write to x and the read from y in the left thread. For the optimized version of the program, the behavior leading to outcome [n = 0,r2 = 0] is sequentially consistent. Thus, a developer must be aware of possible counter-intuitive behaviors of his program. To do this, modern multithreaded programming languages provide weak memory models, that is, formal specifications of the behavior of multithreaded programs that allows for weak behaviors, since a stronger sequential consistency model prohibits the use of a wide range of optimizations and, therefore, the implementation of this model in practice leads to significant overhead [48—51].
Thus, it is important for developers to understand how weak is the memory model provided by the programming language, what optimizations are allowed by this model, and what guarantees it offers.
Further in Section 1.1.1, programming primitives for working with shared memory are introduced. Section 1.1.2 discusses the various requirements for memory models in more detail, while Section 1.1.3 discusses existing models and their classification. Finally, Section 1.1.4 compares different classes of memory models and identifies open research problems, some of which have been solved in this thesis.
1.1.1 Programming Primitives
For the purposes of this study, we will assume that the shared memory of a multithreaded program is a mapping of variable addresses2 into their values. Thus, we will
2We will also refer to the address of a variable as its location.
assume that shared memory consists of mutually disjoint, typed addressable memory cells.3
The main operations that shared memory provides are writes and reads to and from shared variables. In addition, we will assume that the following atomic read-modify-write operations are available: , compare-and-swap, CAS; atomic exchange, EXCHG; atomic fetch-and-add, FADD. Compare-and-swap atomically compares the current and expected values of a variable and, if they match, replaces the value of the variable with the desired value. The exchange operation atomically replaces the value of a variable and returns its previous value. Finally, fetch-and-add adds given value to a variable and returns its value before modification.
Another important primitive provided by memory models is the memory barrier or memory fence—a special instruction that can be inserted into code to prevent reordering of instructions and thus the occurrence of weak behaviors.
The above description of memory model primitives is summarized in Table 1.
Memory models generally distinguish between several kinds of accesses to shared memory and allow the programmer to annotate these accesses with an access mode. Access modes differ by the guarantees they provide. The following access modes are identified: non-atomic mode, relaxed mode (or opaque in Java), acquire mode, release mode, combined acquire-release mode, and the sequentially consistent mode (or volatile in Java). These modes are denoted as na, rlx, acq, rel, acqrel, and sc respectively. The acq mode is applicable only to reads, and the rel is applicable only to writes. Access modes are ordered by guarantees they provide, as shown in the following diagram.
Non-atomic accesses annotated with the na mode are not intended for concurrent access to a shared variable from parallel program threads. Depending on the particular programming language, concurrent non-atomic accesses are either completely prohibited (for example, in Haskell [53] and Rust [54]) or may lead to undefined behavior (for example, in C/C++ [5]) or provide no guarantee on the order in which threads can observe these accesses (for example, in Java [6]).
3Memory model theory also sometimes defines shared memory as an untyped sequence of bytes that allows mixed-size accesses [52]. In this work, mixed-size accesses are not considered.
na C rlx
acqrel C sc
acq ^
Instruction syntax
Instruction semantics
x0 := v Write value v to shared variable x with access mode o.
r := xo Read value from shared variable x to local variable r with access mode o.
r := x. CAS0s0f (ve,vd) Atomic comparison of shared variable x with expected value ve and swap to a desired value vd; read value is assigned to local variable r; if comparison succeeds, the os access mode is applied, otherwise of.
r := x. EXCHG0(v) Atomic exchange of the value of shared variable x to value v, annotated with the o access mode; read value is assigned to local variable r.
r := x. FADD0(v) Atomic fetch-and-add of value v to shared variable x, annotated with access mode o; read value is assigned to local variable r.
fence0 Memory barrier instruction annotated with access mode o.
Table 1 — List of used programming primitives.
Usually, only coherence [55] is guaranteed for relaxed accesses annotated with the rlx mode. This property provides sequential consistency for each individual mem-
ory location. It follows from this that a program consisting of relaxed accesses to a single variable allows only sequentially consistent behaviors.
Accesses annotated with acq acquire and rel release modes are used to support the message passing idiom [56]. The thread sending the message must annotate the corresponding shared memory write operation with the rel access mode. The thread waiting for this message must have a read annotated with the acq access mode.
Finally, sequentially consistent accesses (annotated with the sc mode), when used correctly, guarantee the semantics of sequential consistency [22; 57].
1.1.2 Memory Model Requirements
As shown above, in the discussion of the Dekker algorithm, the development of multithreaded programs requires to take into account the memory model provided by the corresponding programming language. It should be kept in mind that conflicting requirements are imposed on memory models. On the one hand, a stronger model allows for fewer behaviors and provides more guarantees to the developer. On the other hand, a weaker model allows for more optimizations, thus better program performance. Thus, when creating a memory model, it is necessary to find a trade-off between these conflicting requests.
In this section, a set of typical requirements for memory models of programming languages will be described in detail.
Optimality and Soundness of Compilation Schemes
A compilation scheme is a mapping of programming primitives into assembly language instructions of a specific processor family. We will assume that both the highlevel programming language and the assembly language in this case provide the same set of programming primitives, described in the section 1.1.1.
An optimal compilation scheme compiles shared memory instructions from the programming language into instructions of the target processor without inserting memory barriers and strengthening the access mode. In other words, if a programming language has an optimal compilation scheme, it is possible to compile programs in this language into efficient code of the corresponding target processor. On the contrary, the use of non-optimal compilation schemes can lead to a decrease in the performance of the code due to the insertion of memory barriers. At the same time, barriers can prevent weak behaviors allowed by the processor architecture.
V := 1 (SB)
r2 := x
The soundness of a compilation scheme ensures that the set of behaviors allowed by the processor's memory model for the compiled program is a subset of the source program's behaviors allowed by the programming language's memory model.
Consider the following example. The SB program is a simplified version of Dekker's algorithm:
x := 1
ri := V
Assume that the programming language must provide a sequentially consistent memory model and support compilation into assembler code for processors of the x86/x64 family.
Consider a compilation scheme that compiles shared variable read and write instructions into a MOV instruction.4 This compilation scheme is optimal because it does not introduce additional memory barriers and does not strengthen memory access modes. However, this scheme is unsound, since the specification of the x86/x64 memory model allow for SB a behavior with outcome [r1 = 0, r2 = 0], which is not sequentially consistent. This result may be due to write buffering, as x := 1 can be executed by the processor after all other program instructions have been executed.
Consider another compilation scheme that inserts the mfence instruction after each write operation [2; 5]. The mfence instruction is a special memory barrier in the x86/x64 processor instruction set, and its execution flushes the write buffer to the main memory. For the program SB compiled in this manner, the result [r1 = 0, r2 = 0] is not possible in x86/x64. Thus, the alternative compilation scheme is sound, but not optimal.5
Unfortunately, the sequential consistency model does not have an optimal and sound compilation scheme for modern multiprocessors of the x86/x64, ARM, and POWER families. This is one of the reasons for the weakening of memory models in high-performance programming languages.
Soundness of Program Transformations
Another important requirement for memory models is the soundness of source code transformations, that is, the source code transformation rules used by the compiler during program optimization phase. Soundness of transformation guarantees that the
4In the x86/x64 architecture, MOV is also used for regular loads and stores from/to shared memory.
5In practice, using this compilation scheme can lead to a slowdown of 10-30% [48; 50].
set of behaviors of the transformed program is a subset of the allowed behaviors of the original program.
Returning to the SB program, let us revisit the sequential consistency model and the transformation of independent instruction reordering. Assume that this transformation is applied to the left thread and swaps write and read operations, as shown below.
x := 1
n := y
y := 1 n := y
r2 := x x := 1
y := 1
r2 := x
For the original version of the program on the left, the result [ri = 0, r2 = 0] is not sequentially consistent, but for the transformed version of the program, this result is sequentially consistent. Thus, we can conclude that the reordering of independent instructions is not a sound transformation from the point of view of the sequential consistency model.
Theory of memory models considers the soundness of a wide set of basic transformations. A detailed list of these transformations with explanations can be found in [42]. This dissertation will discuss only some specific transformations, which will be introduced as needed.
Data Race Freedom Guarantees
The basic guarantee expected from a memory model is that only sequentially consistent behaviors are allowed for programs that do not contain data races6. This property is also called data race freedom, DRF [6].
More formally, a weak memory model M is said to satisfy the DRF property if, for any program P that does not contain data races in any sequentially consistent behavior, M allows only a sequentially consistent behaviors. 7
Thus, DRF makes it possible to reduce reasoning about the behavior of a multithreaded program under a weak model to reasoning about the behavior of the same program under a simpler sequential consistency model. To do this, it suffices to show that the program has no races in the sequential consistency model.
6A data race is a pair of concurrent (from different threads) accesses of the same shared variable, such as at least one of these accesses is a write.
7Data race freedom in the above formulation is also called DRF-SC, after the sequential consistency memory model. One can also consider DRF with respect to another arbitrary model M, in which case it is called DRF-M.
Speculative Execution
Another important property of the memory model is the presence or absence of the speculative execution. Consider another example:
ri := x
y :=1
r2 := y ,
, (LB)
x := 1
Some memory models, in particular, models of the ARM and POWER multiprocessor families, allow a behavior that leads to the result [r1 = 1,r2 = 1], although this result cannot be obtained by executing the instructions in-order. To get this result, speculative execution [58; 59] is required: for example, this result can be obtained by buffering the r1 := x load in the left thread and executing the write y := 1 out of order.8 It is important to note that unrestricted use of speculative execution can lead to undesirable consequences. Consider the following example:
r1 := x
y := ri
r2 : y (LB+dep)
x := r2
Behavior that first speculatively performs a write operation to the variable y of the value 1 in the left thread, then reads this value and writes it to the variable x in the right thread, and then reads it again back in the left thread, leads to a causal loop and an unexpected out-of-thin-air result [r1 = 1, r2 = 1] [13]. In order to prohibit behaviors that result in out-of-thin-air values, the memory model must restrict the use of speculative execution. Possible solutions to this problem are discussed in more detail in Sections 1.1.3, 1.2.3, and 1.2.4.
Automated Formal Verification
Multithreaded programs are sources of non-trivial bugs that are difficult to reproduce. Testing of multithreaded programs is in general insufficiently effective due to their non-deterministic behavior. In the context of weak memory models, this problem is even more acute due to weak behaviors.
For this reason, it is extremely important to develop tools for automatic program verification, for example, via model checking [30], which would take into account weak
8This is where the name of the above program, load buffering, LB, comes from.
behaviors. However, for some memory models, the verification problem is computationally difficult due to the very large space of possible states. In particular, the verification process can be significantly hampered if the memory model allows speculative execution. This issue is discussed in more detail in the section 1.1.3.
1.1.3 Classes of Memory Models
Programming languages weak memory models can be divided into several classes based on their properties: the existence of a sound and optimal compilation scheme, supported transformations, and provided guarantees.
According to the classification presented in [42], we will consider four classes of memory models:
- program order preserving models;
- syntactic dependency preserving models;
- semantic dependency preserving models;
- out-of-thin-air models.
Let us demonstrate the difference between these classes using the following variations of the load buffering program:
a := x //1
y := 1
b := y //1
x := b
(LB-nodep)
a := x // 1
y := 1 + a * 0
b := y //1
x := b
(LB-fakedep)
a := x // 1
y := a
b := y //1
x := b
(LB-dep)
Program Order Preserving Memory Models
In such models, the effects of accessing shared memory in threads occur according to their program order, that is, in the linear order in which the corresponding instructions are placed in the program.9 In other words, speculative execution is prohibited within these models. The memory models of this class prohibit the weak behavior with the result [n = 1,r2 = 1] for LB-nodep, LB-fakedep, and LB-dep.
Memory models that preserve program order provide strong guarantees for program behavior. In particular, they provide DRF property, prohibit speculative execution, and therefore do not allow out-of-thin-air values [22]. Effective algorithms for
9Note that in this case, this class of models still lets the read operations observe the "outdated" values, that is not the last written values, as opposed to the sequential consistency model.
automatic verification via model checking have been developed for this class of models [44; 60]. On the other hand, this class does not support the optimal compilation scheme for ARM and POWER multiprocessor models, nor does it support load/store reordering.
The following models belong to this class: the RC11 model [22], which covers the subset of behaviors allowed by the memory model of the C language; TSO model of the x86 family processors [2]; sequential consistency model [1]; causal consistency model [10]; eventual consistency model [9]; and the memory model of OCaml [8].
Syntactic Dependency Preserving Models
These models relax the total program order and introduce a partial order relation, called preserved program order. Shared memory access operations from the same thread are in preserved program order if there are syntactic dependencies between their corresponding instructions, such as data dependency or control dependency.
For example, in the LB-nodep program, there is no syntactic dependency between the instructions in the left thread, so these instructions can be executed in any order. Therefore, a memory model that preserves syntactic dependencies allows a behavior with the outcome [r1 = 1,r2 = 1]. However, this result is not allowed for the LB-dep and LB-fakedep programs because there is an instruction dependency in both threads in these programs.
Models of this class support optimal compilation schemes to modern multiprocessor models. Unlike models that preserve program order, this class of models permits load/store reordering. But at the same time, this class prohibits many other transformations that can remove syntactic dependencies between instructions. An example of such a transformation is constant folding [61]. For example, in the case of LB-fakedep, constant folding can convert y := 1 + a * 0 into y := 1, removing the dependency on the previous read instruction a := x. After applying this transformation, the behavior with the result [r1 = 1,r2 = 1] becomes valid, although it was invalid for the source program.
Memory models that preserve syntactic dependencies provide weaker guarantees than models that preserve program order. These models still provide DRF property, but unlike the latter, they allow speculative execution of syntactically independent instructions. Nevertheless, for this class of models, there are effective algorithms for automatic verification via model checking [62—64].
Models that preserve syntactic dependencies are not used for programming languages because they prohibit the use of a wide class of transformations (for example, constant folding). At the same time, most models of modern multiprocessors, for example, ARM [3] and POWER [4], fall into this class. This class also includes the Linux kernel memory model [65]
Обратите внимание, представленные выше научные тексты размещены для ознакомления и получены посредством распознавания оригинальных текстов диссертаций (OCR). В связи с чем, в них могут содержаться ошибки, связанные с несовершенством алгоритмов распознавания. В PDF файлах диссертаций и авторефератов, которые мы доставляем, подобных ошибок нет.