Диссертация (1149932), страница 5
Текст из файла (страница 5)
1. Сценарий программы MP-volatile, который не соответствует аксиомаммодели JMMдля версии программы MP, в которой локация y помечена как изменчивая:[x] := 0; [y] := 0;[x] := 1;a :=volatile [y]; //1[y] :=volatile 1 b := [x]//0(MP-volatile)Для того, чтобы проверить предыдущее утверждение, рассмотрим соответствующий сценарий поведения (см. рис. 1). В его графе имеется шесть событий.События p и q являются инициализирующим записям в локации x и y, а остальные — инструкциям из MP-volatile. Недописанные дуги — это дуги отношенияpo. На рис. 1 опущены дуги отношения hb, связывающие p и r (po ⊆ hb), а такжеr и u (т.к.
po(r, s), sw(s, t), po(t,u) и hb = (po ∪ sw)+ ). Таким образом, данныйграф противоречит приведенной выше аксиоме и не является корректным в JMM.Отметим, что если бы локация y не была бы помечена как изменчивая, тособытия s и t имели бы обычный тип и между ними бы не было ребра sw, следовательно аксиома бы выполнялась и результат [a = 1, b = 0] был бы возможен.Для того, чтобы запретить “значения из воздуха”, в JMM используется процесс валидации сценариев.
В рамках этого процесса строится серия сценариев,каждый из которых является корректным с точки зрения аксиом JMM, при этомпоследним в серии является валидируемый сценарий. Также каждому сценариюв серии присваивается множество добавленных (committed) событий. Эти множества монотонно растут, а последнее является множеством всех событий в графевалидируемого сценария.
При этом на каждом шаге трансформации в серии сохраняется подмножество отношения hb, заданное на добавленных событиях.В [44] показывается, что именно из-за процесса валидации упомянутые выше оптимизации некорректны в JMM.241.3.3Модель памяти C/C++В последние годы научное сообщество уделяет особое внимание моделипамяти C/C++, которая появилась в стандартах языков в 2011 году [30, 31]. Онане претерпела существенных изменений в последующих стандартах 2014 [82] и2017 [83] годов, и поэтому в литературе обычно не различают понятия “модельпамяти C/C++” и “модель памяти C/C++11”.
Далее в работе используется “модельпамяти C/C++11” или “C/C++11 MM”.Базовым результатом о свойствах этой модели является её формализация,представленная в [4]; далее под C/C++11 MM будет подразумеваться именноэта формализация. Существуют работы, посвященные корректности компиляциии оптимизаций [42, 84–87], логикам для формальных рассуждений о программах [65–67, 88, 89] и другим свойствам этой модели [71, 90–93]. Как следствие,C/C++11 MM является одной из самых проработанных моделей памяти для языков программирования. Тем не менее, она не лишена недостатков, в том числе“значений из воздуха”.Виды обращений к памятиВ C/C++11 MM локации бывают двух типов — неатомарные (non-atomic) иатомарные (atomic). В отличие от языка Java, разделение между ними менее строгое, т.к. языки C/C++ разрешают преобразование типов, следовательно на один итот же адрес в памяти может ссылаться две переменных в программе, одна из которых будет иметь атомарный тип, а другая — неатомарный.
Поэтому в C/C++11MM обращения к одной и той же локации могут быть как неатомарными, так иатомарными. Последние, в свою очередь, также подразделяются на несколько категорий в зависимости от типа обращения — чтение, запись или одновременноечтение-запись (RMW, read-modify-write). Описание RMW опущено для краткости.Событие чтения может быть неатомарным, расслабленным (relaxed,rlx), потребляющим (consume, con), приобретающим (acquire, acq) илипоследовательно-консистентным (sequentially-consistent, sc). Событие записиможет быть неатомарным, расслабленным, высвобождающим (release, rel) илипоследовательно-консистентным. В обоих случаях виды обращений упорядоченыпо величине предоставляемых гарантий.
Так, расслабленные обращения похожи25на обычные обращения в модели JMM, тогда как последовательно-консистентные— на синхронизирующие. Неатомарные обращения предоставляют наименьшиегарантии: если неатомарное обращение является частью гонки по данным, то вC/C++11 MM программа имеет неопределенное поведение. Приобретающее чтение и высвобождающая запись могут быть использованы для того, чтобы запретить результат [a = 1, b = 0] (аналогично синхронизирующим обращениям в случае JMM):[x] :=rlx 0; [y] :=rlx 0;[x] :=rlx 1; a :=acq [y]; //1[y] :=rel 1 b :=rlx [x] //0При этом в отличие от синхронизирующих обращений JMM и sc-обращенийC/C++11 MM на высвобождающих и приобретающих событиях не существуеттотального порядка, учитывающего программный порядок, и, как следствие, следующая программа, использующая высвобождающие записи, имеет сценарий поведения с результатом [a = 1, b = 1]:[x] :=rel 1;[y] :=rel 2a :=scb :=sc[y] :=rel 1;[x] :=rel 2[x]; //1[y] //1(2W-rel)В то же время эта программа с sc-записями такого сценария не имеет:[x] :=sc 1;[y] :=sc 2a :=scb :=sc[y] :=sc 1;[x] :=sc 2[x]; //1[y] //1(2W-sc)Инструкция высвобождающей записи не может быть переставлена инструкциями записями, предшествующими ей в программном порядке, ни на этапе компиляции, ни во время исполнения программ.
Как следствие, гарантируется, чтопоток, который с помощью инструкции приобретающего чтения прочитает из высвобождающей записи, будет осведомлён о предшествующих ей записях. Аналогично, инструкция приобретающего чтения не может быть переставлена с последующими чтениями.Инструкция потребляющего (consume, con) чтения является ослабленнойверсией инструкции приобретающего чтения и предоставляет те же гарантии, но26только для последующих чтений, которые зависят по данным от потребляющего. Так, потребляющего чтени будет недостаточно, чтобы гарантировать отсутствие сценария поведения [a = 1, b = 0] в версии программы MP-rel-acq, в которойacq-чтение заменено на con-чтение. Тем не менее, con-чтения будет достаточно,чтобы гарантировать отсутствие сценария поведения [a = y, b = 0] в следующейпрограмме:[x] := 0; [y] := 0; [z] := x;[y] :=rlx 1; a :=con [z]; //y[z] :=rel y b :=rlx [a] //0(MP-addr-con)Сценарии поведенияАналогично модели JMM, в C/C++11 MM сценарий поведения программыпредставляется в виде графа, вершинами которого являются события над памятью.
Также в сценариях поведения фигурируют отношения программного порядка po, “читает из” rf, “синхронизируется с” sw и “предшествует” hb. При этомsw и hb определяются по-другому. Так, в частности, sw включает в себя подмножество rf, связывающее высвобождающие записи с приобретающими чтениями,а hb является транзитивным замыканием объединения po и sw в отсутствии conчтений (с ними определение становится сложнее).
Дополнительно в модели используются два важных отношения — mo и sc. Отношение mo (порядок памяти,memory order, coherence order) для каждой локации является полным порядкомна событиях записи в неё. Отношение sc (sequential consistency order) являетсяполным порядком на всех sc-событиях в сценарии поведения.Также, как и в случае JMM, для C/C++11 MM определяются аксиомы, которые ограничивают пространство возможных сценариев поведения. Полный список аксиом представлен в [4, 65]. Отличием от JMM является то, что в C/C++11MM не используется процесс верификации исполнения. В итоге, с одной стороны, C/C++11 MM допускает поведения со “значениями из воздуха”, но, с другойстороны, поддерживает большее число компиляторных оптимизаций.Построение сценариев поведения по программеПостроение сценариев поведения в C/C++11 MM состоит из трёх следующих этапов.
На первом этапе для программы строится множество т.н. предзапусков (preexecutions) — частичных графов сценариев поведения, в которых присут-27p : Wrlx (x,0)q : Wrlx (y,0)r : Wrlx (x,1)t : Racq (y,5)s : Wrel (y,1)u : Rrlx (x,9)Рис. 2. Предзапуск программы MP-rel-acqp : Wrlx (x,0)moq : Wrlx (y,0)hbt : Racq (y,1)r : Wrlx (x,1)s : Wrel (y,1)swhbu : Rrlx (x,0)Рис.
3. Сценарий поведения программы MP-rel-acq, прошедший базовуюпроверку на корректностьствует только отношение po (аналогичный процесс для аксиоматической моделиARMv8.3 [10] представлен в приложении Г.2). При этом, поскольку события чтения не связываются с событиями записи, для каждого события чтения прочитанное значение выбирается недетерминировано.
В частности, среди предзапусковпрограммы MP-rel-acq присутствует граф, изображенный на рис. 2.На втором этапе в каждый предзапуск недетерминировано добавляются дуги отношений rf, sc и mo, по которым также вычисляются производные отношения, такие как sw и hb. Полученные графы проверяются на базовую корректность.В частности, проверяется, что если из события e идёт rf-дуга в f , то e являетсясобытием записи, f — чтения, они оперируют над одной и той же локацией, и прочитанное значение равняется записанному. После второго этапа во множестве полученных сценариев поведения для программы MP-rel-acq появляется сценарийповедения, изображенный на рис.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
