Диссертация (1149932), страница 6
Текст из файла (страница 6)
3 (некоторые ребра в нём опущены).На третьем этапе полученные сценарии поведения проверяются на соответствие аксиомам C/C++11 MM. Одна из таких аксиом аналогична приведённой выше для JMM:∀r, w. rf(w, r) ∧ hb(w, r) ⇏ ∃w′ . mo(w,w′ ) ∧ hb(w, w′ ) ∧ hb(w′ , r).28p : Wrlx (x,0)q : Wrlx (y,0)morfr : Wrlx (x,1)p : Wrlx (x,0)q : Wrlx (y,0)mot : Racq (y,0)r : Wrlx (x,1)u : Rrlx (x,0)s : Wrel (y,1)rfp : Wrlx (x,0)q : Wrlx (y,0)mot : Racq (y,0)r : Wrlx (x,1)u : Rrlx (x,1)s : Wrel (y,1)t : Racq (y,1)rfrfs : Wrel (y,1)rfu : Rrlx (x,1)Рис. 4. Сценарии поведения программы MP-rel-acq в C/C++11 MMp : Wrlx (x,0)q : Wrlx (y,0)r : Rrlx (x,1)t : Rrlx (y,1)s : Wrlx (y,1)rfu : Wrlx (x,1)Рис.
5. Сценарий поведения программы IF-OOTA-rlxДанная аксиома не выполняется для последнего приведенного сценария, и, какследствие, программа MP-rel-acq имеет только три корректных сценария поведения в рамках C/C++11 MM (см. рис. 4), соответствующих результатам [a = 0, b =0], [a = 0, b = 1] и [a = 1, b = 1].Проблема “значений из воздуха”Для того, чтобы понять, откуда берется проблема “значений из воздуха” вC/C++11 MM, рассмотрим программу, которая уже была обсуждена ранее:[x] :=rlx 0; [y] :=rlx 0;b :=rlx [y];a :=rlx [x];if aif bthen [y] :=rlx 1then [x] :=rlx 1else skipelse skipfifi(IF-OOTA-rlx)Одним из корректных сценариев поведения этой программы в C/C++ MMявляется граф, изображённый на рис.
5. Он обладает “значениями из воздуха”,т.к. соответствует результату [a = 1, b = 1]. В данном случае очевидно, что у события r есть циклическая зависимость от себя самого — для того, чтобы событие29r прочитало 1, событие u должно записать 1, и это возможно только если событиеt прочитало значение 1, которое должно была быть записано событием s, котороеслучается только если r прочитало 1!Мы могли бы попробовать решить данную проблему, добавив в граф отношение зависимости по управлению ctrl с рёбрами (r, s) и (t, u), а также дополнительную аксиому, которая требовала бы ацикличности объединения отношений ctrl и rf. Тогда в приведенном графе был бы цикл [r, s, t, u, r], и сценарийсчитался бы некорректным с точки зрения модифицированной модели.К сожалению, такое решение является неудовлетворительным с точки зрения задач C/C++11 MM.
Рассмотрим следующую программу:[x] :=rlx 0; [y] :=rlx 0;b :=rlx [y];a :=rlx [x];if aif bthen [y] :=rlx 1then [x] :=rlx 1else [y] :=rlx 1else skipfifi(IF-notOOTA-rlx)Она отличается от IF-OOTA-rlx тем, что ветка else в первом потоке содержитинструкцию записи [y] :=rlx 1. Наличие этой инструкции позволяет компилятору сделать вывод о том, что инструкция [y] :=rlx 1 не зависит от условияконструкции if, следовательно может быть вынесена из этой конструкции.
Далее вынесенная операция может быть переупорядочена с независимым чтениемa :=rlx [x]:[x] :=rlx 0; [y] :=rlx 0;[y] :=rlx 1; b :=rlx [y];if bthen [x] :=rlx 1a :=rlx [x]else skipfi(IF-notOOTA-optimized)Для получившейся программы результат [a = 1, b = 1] возможен также и в моделиSC.Таким образом для того, чтобы разрешить использованные трансформации, C/C++11 MM должна разрешать результат [a = 1, b = 1] для программыIF-notOOTA-rlx. Это означает, что предложенное ранее “исправление” модели не30может быть напрямую использовано, т.к. добавление зависимостей по управлению в граф и дополнительной аксиомы в модель сделает результат [a = 1, b = 1]некорректным для IF-notOOTA-rlx.Рассмотрим, в чём заключается разница между зависимостями по управлению в левых потоках программ IF-OOTA-rlx и IF-notOOTA-rlx.
В обоих случаяхприсутствует синтаксическая зависимость инструкции [y] :=rlx 1 от a :=rlx [x],но семантическая зависимость имеется только в программе IF-OOTA-rlx. Соответственно, проблема могла бы быть решена, если бы в граф сценария поведениябыла добавлена семантическая зависимость по управлению [94]. В следующемразделе рассмотрены существующие на данный момент способы представлениясемантической зависимости.Стоит отметить, что в стандартах C [30] и C++ [31, 82] упомянутую проблему пытаются решить путём прямого запрета сценариев поведения со “значениямииз воздуха”. Данный запрет является неформальным, поскольку в стандарте отсутствует формальное определение “значений из воздуха”. Но в [5] отмечается,что такое решение проблемы является неудовлетворительным, поскольку не даётвозможности строго рассуждать о программах.1.3.4Теоретические модели памятиВ этом разделе коротко рассматриваются альтернативные теоретическиемодели памяти для языков программирования.В [40] определяется операционная семантика на базе C/C++11 MM.
Эта семантика по предзапуску программы инкрементально строит полный сценарий поведения. Данный подход решает проблему интеграции C/C++11 MM c остальнойчастью стандарта [79], однако оставляет проблему “значений из воздуха”, а такжене предоставляет операционной интуиции о поведении программы.В [35] предлагается альтернативный подход к аннотированию инструкцийобращений к памяти: вместо того, чтобы помечать часть инструкций “строгими”модификаторами, такими как acq, rel и sc, и значит неявно запрещать переупорядочивание инструкций вокруг них, авторы [35] предлагают явно указыватьто, порядок между какими инструкциями должен быть сохранён. Такой подходпозволяет эффективнее компилировать программы в целевую платформу.
Самамодель памяти в данной работе представлена в операционном виде. К её недостат-31кам стоит отнести то, что в ней позволяются сценарии поведения со “значениямииз воздуха”.В [38] представлена модели памяти на основе структур событий (eventstructures) [95,96]. Семантика программы представляется не как множество несвязанных графов, а как один общий граф, в котором присутствует отношение конфликта.
Последнее позволяет разделять вершины, относящиеся к разным сценарием поведения — каждый максимальный подграф, в котором нет конфликтующих событий, является одним сценарием поведения в аксиоматическом смысле. Поскольку в структуре событий все сценарии представляются согласованно,данная семантика может проверять наличие семантической зависимости междусобытиями.
В частности, для программы IF-notOOTA-rlx семантика может проверить, что вне зависимости от того, какое значение читается в регистр a левымпотоком, он исполняет запись [y] :=rlx 1, следовательно между соответствующими чтением и записью нет зависимости. Аналогично, для программы IF-OOTA-rlxсемантика может определить наличие зависимости. Данная модель обладает следующими недостатками. Во-первых, она поддерживает только фиксированноемножество компиляторных оптимизаций, которые явным образом представленыкак переходы в модели. Во-вторых, модель определена для подмножества языка C/C++, содержащего только неатомарные и расслабленные операции чтения изаписи, а также захват и высвобождение замков.
И, в-третьих, модель не поддерживает эффективную компиляцию в модель ARMv8 POP [9]5 .Близкий подход к заданию модели памяти без “значений из воздуха” представлен в [39]. В этой модели, в отличие от использования явных переписыванийструктуры событий с помощью фиксированного набора оптимизаций, задан процесс валидации корректных сценариев поведения, похожий на аналогичный механизм в JMM. Процесс валидации основан на идее игры двух игроков. Первый игрок пытается обойти подграф структуры событий, соответствующий проверяемому сценарию; второй игрок вмешивается в этот обход, добавляя в конфигурациюобхода произвольные вершины и пытаясь помешать первому. При наличии выигрышной стратегии у первого игрока считается, что сценарий поведения корректенс точки зрения модели.
Эта игра является представлением недетерминированногопереключения контекстов со стороны процессора. Для модели формально доказано утверждение, косвенно подтверждающие отсутствие проблемы “значений из5Вглаве 3 рассматривается программа ARM-weak. Эта программа обладает слабым поведением, которое не проявляется в модели [38].32воздуха”. К недостаткам подхода стоит отнести то, что он не поддерживает некоторые базовые оптимизации, в частности, перестановку независимых чтений.1.4ВыводыНа основе проделанного обзора сделаны следующие выводы.– Модель памяти промышленного языка программирования должна удовлетворять, как минимум, трём критериям. Во-первых, должна существовать корректная схема компиляции в модель целевой процессорной архитектуры.
Во-вторых, основные компиляторные оптимизации должныбыть корректны в рамках модели. В-третьих, у модели должна отсутствовать проблема “значений из воздуха”.– При разработке новой модели памяти языка программирования нужно доказывать корректность эффективной компиляции в модели памяти целевых процессорных архитектур.– Существующие модели памяти промышленных языков программирования не удовлетворяют приведённым выше критериям.– Требуется разработать операционную модель памяти с синтаксисомC/C++11 MM, которая не имеет проблемы “значений из воздуха”.33Глава 2. Операционная модель памяти C/C++11В данной главе описана предложенная в диссертации операционная модельпамяти OpC11 для языков C/C++11, и представлен реализующий её интерпретатор.
Материал главы покрывает результат статьи [25].Модель OpC11 (далее OpC11 MM) представлена как семейство аспектов,каждый из которых описывает некоторую особенность C/C++11 MM [4]. Это позволяет упростить использование модели для задач, в которых рассматриваетсятолько подмножество языка C/C++11 MM. Также, поскольку некоторые особенности С/C++11 MM, такие как поддержка секвенциализации (см. раздел 2.1.8),неоднозначны, то аспектное представление позволяет легко настраивать интерпретатор на интересующий вариант семантики.Описание модели организовано следующим образом. В начале рассматриваются ряд примеров, мотивирующих введение различных аспектов OpC11 MM,и неформально описываются сами аспекты (раздел 2.1). Далее приводится математическое определение упомянутых аспектов (раздел 2.2).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
