Программирование, 2021, № 6, стр. 30-50

4.1. Схема компиляции

Будем понимать под схемой компиляции отображение примитивов языка программирования в инструкции конкретного семейства процессоров. Мы будем рассматривать примитивы, представленные в разделе § 4. Процессоры обычно предоставляют инструкции для выполнения обычных операций чтения и записи⁹⁹, операции чтения-модификации-записи, а также различные типы барьеров памяти.

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

Рассмотрим пример. Программа SB, представленная ниже, является фрагментом алгоритма Деккера, обсуждавшегося в § 1.

Предположим, что язык программирования предоставляет модель последовательной согласованности, а программа должна быть скомпилирована для x86. Если компилировать операции чтения и записи обычным образом x86 ¹⁰¹⁰, тогда, следуя спецификации модели памяти x86, допустимым будет следующий результат работы программы (он также будет наблюдаться и на практике): $[{{r}_{1}} = 0,{{r}_{2}} = 0]$. Данный результат может появиться вследствие буферизации операций записи – операция записи x := 1 может быть исполнена после выполнения всех остальных инструкций программы.

Отметим, что результат $[{{r}_{1}} = 0,{{r}_{2}} = 0]$ не является результатом последовательно согласованного сценария, и, следовательно, рассмотренная схема компиляции не является корректной. Как было продемонстрировано в разделе § 1, некорректность схемы компиляции может иметь негативные последствия и нарушать корректность программы.

Корректная схема компиляции для модели последовательной согласованности под архитектуру x86 может компилировать операцию записи как обычную инструкцию записи, за которой следует инструкция mfence [5, 9], как продемонстрировано ниже:

Инструкция mfence является специальным барьером памяти в системе команд процессоров x86, который выполняет сброс буфера записей в основную память. Для программы SB+MFENCE результат $[{{r}_{1}} = 0,{{r}_{2}} = 0]$ запрещен моделью памяти x86.

Несмотря на то, что модифицированная схема компиляции является корректной, она не оптимальна [31] в том смысле, что она использует барьеры памяти, которые обычно являются причиной замедления программы на 10–30% на процессорах семейства x86 [32, 33]. К сожалению, современные процессоры не могут иметь одновременно корректную и оптимальную схему компиляции в рамках модели последовательной согласованности. Этот факт затрудняет использование модели SC для высокопроизводительных языков программирования и служит одним из стимулов к ослаблению моделей памяти.

В рамках этой статьи при обсуждении схем компиляции мы будем рассматривать процессоры семейств x86, Armv7, Armv8 и POWER по следующим причинам. Во-первых, эти архитектуры наиболее распространены на сегодняшний день. Во-вторых, модели памяти для этих процессоров всесторонне изучены исследовательским сообществом, что привело к созданию строгих формальных спецификаций [9, 11, 14, 15].

4.2. Трансформации кода

Следующим критерием является C.2 – корректность трансформаций, то есть правил переписывания исходного кода, применяемых в компиляторных оптимизациях.

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

Возвращаясь к примеру SB, снова рассмотрим модель последовательной согласованности и возьмем трансформацию, которая переставляет местами операции записи и чтения в левом потоке, предполагая, что они оперируют различными локациями в памяти:

Для преобразованной версии программы (справа), результат $[{{r}_{1}} = 0,{{r}_{2}} = 0]$ является последовательно согласованным. Тем не менее, для оригинальной версии программы (слева) это неверно. Следовательно, вышеупомянутая трансформация является некорректной для модели SC.

В следующих разделах мы рассмотрим некоторые трансформации, обсуждаемые в различных исследованиях. Заметим, что этот список далеко не полон и не включает многие трансформации, выполняемые существующими оптимизирующими компиляторами [34]. Например, он не включает трансформации над циклами, так как в теории моделей памяти еще недостаточно проработаны темы гарантий прогресса (liveness properties) [35], которые необходимы для формального изучения этих трансформаций.

Трансформации, которые мы рассматриваем, разделены на два подкласса: локальные и глобальные. Локальные трансформации модифицируют небольшой участок кода в пределах одного потока; глобальные трансформации задействуют всю программу или ее большую часть, захватывая несколько потоков.

4.2.1. Локальные трансформации

Переупорядочивание независимых инструкций (Reordering of Independent Instructions). Эта трансформация переставляет местами две смежные инструкции, выполняющие обращение к различным адресам памяти. Выделяют четыре типа переупорядочивания: запись/чтение, запись/запись, чтение/чтение и чтение/запись.

Элиминация избыточного обращения (Elimination of Redundant Access). В паре двух смежных обращений к памяти одно из них может быть удалено, если его эффект покрывается другим. Например, две операции записи в одну и ту же переменную одного и того же значения могут быть заменены на одну операцию записи. Аналогично переупорядочиванию инструкций, выделяют четыре класса трансформации этого вида.

Элиминация нерелевантной операции чтения (Irrelevant Load Elimination, ILE). Эта трансформация удаляет инструкцию чтения, если ее результат не используется в программе.

Введение спекулятивной операции чтения (Speculative Load Introduction, SLI). Эта трансформация является обратной к предыдущей и вставляет инструкцию чтения в произвольное место программы.

В комбинации с элиминацей типа чтение/чтение эта трансформация может быть использована для того, чтобы вынести чтение из ветки условного оператора:

if (e) then {r := x} $ \rightsquigarrow $ s := x; if (e) then {r := s}

|s is never used  

Переупорядочивание с увеличением синхронизации (Roach Motel Reordering, RM). Этот класс трансформаций позволяет вносить дополнительные инструкции в блоки синхронизации. Например, инструкция записи может быть перенесена в критическую секцию, то есть переставлена за следующую операцию захвата блокировки. Интуитивно, такие перестановки могут только увеличить степень синхронизации в программе, то есть преобразованная программа должна обладать меньшим недетерминизмом и иметь меньшее количество допустимых сценариев поведения.

Неатомарные обращения могут быть внесены в критическую секцию без дополнительных предусловий. Кроме того, инструкция записи может быть перемещена после операции захвата блокировки, а инструкция чтения может быть перемещена до операции освобождения блокировки. Похожие правила применяются к перестановке операций вокруг захватывающих (acquire) и освобождающих (release) обращений к памяти.

Усиление обращений к памяти (Strengthening, S). Данная трансформация, подобно предыдущей, увеличивает степень синхронизации в программе путем усиления режима обращения к памяти. Например, неатомарное обращение к переменной может быть заменено на последовательно согласованное:

Трансформации, сохраняющие трассы (Trace Preserving Transformations, TP). Этот широкий класс трансформаций, который включает трансформации, не меняющие множество трасс потока [36]. Трассой называется последовательность видимых побочных эффектов, возникающих во время исполнения кода потока, при этом операции чтения и записи в разделяемую память тоже считаются эффектами. Классическим примером подобной трансформации является распространение констант [34, 37]. Ниже приведен пример применения данной трансформации.

Удаление общих подвыражений (Common Subexpression Elimination, CSE). CSE является еще одной классической трансформацией [34], которая выполняет поиск и удаление идентичных подвыражений. Вот пример выполнения этой трансформации:

4.2.2. Глобальные трансформации

Продвижение регистров (Register Promotion, RP). Если компилятор может определить, что обращения к разделяемой переменной происходят только из одного потока, тогда он может заменить все обращения к этой переменной на обращения к регистру.

| x is not accessed from other threads

| s is a fresh register

Слияние потоков (Thread Inlining, TI). Эта трансформация объединяет два потока в один. Оказывается, что эта на первый взгляд простая и очевидная трансформация не является корректной в некоторых моделях памяти.

Трансформации, основанные на анализе диапазона значений (Value Range Based Transformations, VR). Трансформации этого класса могут быть применены в случае, если программа удовлетворяет некоторому инварианту, выведенному с помощью глобального анализа диапазона возможных значений переменных. Например, в программе ниже условный оператор может быть удален, так как статический анализ может вывести инвариант $x \geqslant 0$.

4.3. Гарантии

Далее мы обсуждаем третий критерий C.3 – гарантии о поведении программ, предоставляемые моделью памяти.

4.3.1. DRF-свойство

При рассуждении о многопоточных программах большинство программистов подразумевают модель последовательной согласованности. Действительно, было бы неправильно ожидать от программистов знания всех деталей слабых моделей, так как это только усложнило бы и без того непростую задачу проектирования и разработки многопоточных программ. Для того чтобы решить эту проблему, было предложено свойство свободы от гонок (data-race freedom, DRF) [3]. Это свойство гарантирует, что при наличии достаточной степени синхронизации программа будет иметь только последовательно согласованные сценарии поведения в слабой модели памяти. Другими словами, если слабая модель памяти обладает DRF-свойством, то при условии правильного использования примитивов синхронизации программист может не задумываться о слабых сценариях поведения и подразумевать модель последовательной согласованности.

Рассмотрим пример. Вернемся к программе SB из § 4.1. Как было продемонстрировано ранее, в слабой модели эта программа может допускать результат $[{{r}_{1}} = 0,{{r}_{2}} = 0]$. Тем не менее, семантика последовательной согласованности может быть восстановлена, например, при помощи блокировок, как показано в примере ниже:

Совместимая с DRF-свойством слабая модель памяти должна гарантировать, что для программы выше допустимы только последовательно согласованные сценарии поведения с результатами $[{{r}_{1}} = 0,{{r}_{2}} = 1]$, $[{{r}_{1}} = 1,{{r}_{2}} = 0]$ или $[{{r}_{1}} = 1,{{r}_{2}} = 1]$.

Если модель предоставляет последовательно согласованный режим доступа, тогда программист также может аннотировать все обращения к переменным как последовательно согласованные и таким образом восстановить семантику SC:

Более формально, DRF-свойство для слабой модели M утверждает, что если программа не содержит гонок в модели последовательной согласованности, тогда модель M допускает только последовательно согласованные сценарии поведения для этой программы.

Итак, свойство DRF позволяет свести рассуждения о поведении программы в слабой модели к рассуждениям в модели последовательной согласованности. Достаточно лишь показать, что программа не имеет гонок в модели SC, чтобы иметь факт, что она будет иметь только SC сценарии поведения в слабой модели.

Свойство DRF в приведенной выше формулировке иногда также называется внешней свободой от гонок (eDRF), чтобы отличать его от внутренней свободы от гонок (iDRF). iDRF-свойство гарантирует для программы семантику SC в слабой модели M только в случае, если программа не имеет гонок в самой модели M. Это свойство предоставляет более слабую гарантию по сравнению с внешней свободой от гонок. Оно не позволяет полностью избежать рассуждений в терминах слабой модели, так как сначала необходимо показать, что программа не имеет гонок именно в слабой модели. Как будет продемонстрировано далее (см. § 6.3), внутренняя свобода от гонок является компромиссом для определенного класса моделей, которые не могут предоставить внешнюю свободу от гонок.

4.3.2. Когерентность (COH)

Как было показано раньше, современные процессоры не гарантируют выполнимость модели последовательной согласованности. Тем не менее, обычно они предоставляют более слабую гарантию последовательной согласованности по каждой локации в памяти, именуемую также когерентностью [12]. Соответственно, модели памяти для языков программирования также зачастую предоставляют эту гарантию.

Когерентность гарантирует, что все операции записи по определенному адресу памяти будут полностью упорядочены, и что получающийся в результате порядок когерентности (coherence order) отражает порядок, в котором эффекты от операций записи, выполненных некоторым потоком, отражаются в основной памяти, и их результаты становятся видимыми для других потоков. В частности, из свойства когерентности следует, что программа, состоящая из обращений только к одной локации в памяти, должна обладать семантикой последовательной согласованности. Например, рассмотрим следующую программу:

Наличие свойства когерентности предписывает модели памяти допускать для этой программы только последовательно согласованные сценарии поведения с результатами $[{{r}_{1}} = 1,{{r}_{2}} = 2]$, $[{{r}_{1}} = 1$, r₂ = 1] или $[{{r}_{1}} = 2,{{r}_{2}} = 2]$. Для модели, не удовлетворяющей свойству когерентности, допустимым также является результат $[{{r}_{1}} = 2,{{r}_{2}} = 1]$. Например, модель памяти Java допускает подобный сценарий поведения [3].

4.3.3. Неопределенное поведение (no-UB)

Как мы уже кратко упоминали, некоторые модели памяти, например, С/С++, рассматривают программы с гонками на неатомарных обращениях как имеющие неопределенное поведение [28]. Другими словами, для таких программ любой сценарий поведения считается допустимым. Это свойство также иногда называется возгорающейся семантикой (catch-fire semantics).

Практическая польза такого подхода заключается в том, что он допускает оптимальную схему компиляции для неатомарных обращений и позволяет применять к ним любые оптимизации, корректные для последовательных программ. Дело в том, что эффекты от оптимизаций, осуществляемых процессором или компилятором, могут наблюдаться только при обращении к переменным из параллельных потоков. Если таким обращениям предписывается неопределенное поведение и на них не распространяются никакие гарантии, то тогда эффекты этих оптимизаций становятся неразличимы с точки зрения семантики программы.

4.3.4. Спекулятивное исполнение (In-Order) и значения из воздуха (no-OOTA)

Чтобы представить последние два свойства, а именно, наличие спекулятивного исполнения и значений из воздуха, мы рассмотрим еще один пример:

Предположим, что модель памяти допускает результат $[{{r}_{1}} = 1,{{r}_{2}} = 1]$ для этой программы. Например, модели семейств процессоров Armv7, Armv8 и POWER допускают сценарий поведения, ведущий к такому результату, и этот сценарий может наблюдаться на некоторых процессорах семейства Armv7 [38].

Результат $[{{r}_{1}} = 1,{{r}_{2}} = 1]$ не может быть получен путем исполнения инструкции согласно их порядку внутри потоков. Чтобы получить подобное поведение, модель памяти должна использовать некоторую форму спекулятивного исполнения [16, 39]. Это означает, что операция чтения ${{r}_{1}}: = x$ должна быть буферизована, а операция записи y := 1 должна выполниться вне очереди (отсюда и название программы выше – буферизация операции чтения load buffering).

Однако неограниченные спекуляции могут привести к нежелательным последствиям. Операция записи, исполненная вне очереди, может обернуться самоисполняющимся пророчеством (self-fulfilling prophecy) [16]. Рассмотрим следующий вариант программы с буферизацией операции чтения:

Здесь гипотетическая абстрактная машина может спекулятивно исполнить операцию записи в переменную y значения 1 в левом потоке, затем прочитать это значение в правом потоке, записать его в переменную x и прочитать обратно из первого потока, таким образом сформировав парадоксальный цикл причинно-следственных связей. Значение 1 в примере выше появляется из воздуха (out of thin-air) и приводит к неожиданному результату $[{{r}_{1}} = 1,{{r}_{2}} = 1]$.

Как будет показано в § 6, возможность спекулятивного исполнение необходима для того, чтобы поддержать в модели памяти некоторый класс трансформаций программ. Тем не менее, спекулятивное исполнения необходимо ограничить должным образом, чтобы избежать появления значений из воздуха. В § 6.4–§ 6.6 мы рассмотрим то, как эта проблема решается в различных моделях памяти.

6.1. Модель последовательной согласованности

Данная модель является наиболее интуитивной моделью многопоточности. В рамках этой модели состояние памяти может быть представлено как отображение из адресов переменных в хранящиеся значения. Тогда каждый допустимый сценарий поведения программы может быть получен в результате поочередного последовательного исполнения инструкций потоков.

Многие распространенные трансформации оказываются некорректными в модели SC, включая все типы переупорядочивания операций, а также удаление общих подвыражений [32, 32 ]. Тот факт что переупорядочивание инструкций запрещено делает эту модель очень дорогостоящей при реализации на современных процессорах, так как даже относительно строгая модель памяти процессоров x86 допускает переупорядочивание типа запись/чтение. Таким образом, чтобы гарантировать последовательную согласованность, компилятор вынужден вставлять в код тяжеловесные барьеры памяти между инструкциями записи и чтения, что приводит к неоптимальной схеме компиляции.

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

Концептуальная простота и привлекательность модели SC вдохновила многих исследователей на попытки адаптации этой модели и смягчения накладываемых штрафов на время исполнения программы. Общей идеей данных работ была попытка отделения локальных (доступных только одному потоку) и разделяемых переменных. Обращения к локальным переменным могут быть скомпилированы без добавления барьеров памяти, также к ним применим широкий спектр оптимизаций корректных для случая однопоточных программ. Чтобы безопасным образом классифицировать локальные и разделяемые переменные исследователи использовали системы типов [8], статический [40] или динамический анализ [41], поддержку на аппаратном уровне [40, 42], или различные комбинации вышеупомянутых методов.

Несмотря на эти усилия, модель SC все равно имеет существенные накладные расходы. Например, при компиляции на процессоры семейства Armv8 замедление времени работы программ может достигать 70% [41]. Более того, хотя вышеупомянутые техники обычно уменьшают накладные расходы на локальные обращения (которые, зачастую, чаще встречаются в программах), они оказывают меньшее влияние на специфичные приложения, которые активно используют многопоточность, например, такие как неблокирующие структуры данных. Наконец, требуется значительное количество усилий и технической работы, чтобы модифицировать современные компиляторы для поддержки модели SC [32, 41].

6.2. Линейный/частичный порядок на операциях записи

Данный класс моделей был создан на основе моделей с линейным порядком на операциях записей (total store order, TSO) и частичным порядком на операциях записей (partial store order, PSO) [60]. Модели TSO и PSO являются моделями семейств процессоров x86 [9] и SPARC [60] соответственно. В этих моделях потоки оснащены буферами записей. Все операции записи вначале попадают в эти буферы, а потом переносятся в основную память.

Для моделей этого класса схема компиляции для архитектуры x86 является оптимальной, так как x86 предоставляет модель TSO. Однако при компиляции под архитектуры с более слабой моделью памяти, например POWER, необходимо использовать практически такое же количество барьеров, как и при компиляции из модели SC [61].

Модели этого класса допускают большее количество трансформаций кода, чем SC. Использование буферов для операций записи позволяет выполнять переупорядочивание типа запись/чтение в случае TSO и запись/запись – в случае PSO.

Хотя модели TSO и PSO слабее, чем модель SC, тем не менее они все еще предоставляют довольно сильные гарантии, в частности, свойство eDRF и когерентность.

Таким образом, модели этого класса не имеют значительных преимуществ перед моделью SC, и при этом влекут соизмеримые накладные расходы при компиляции для архитектуры c более слабой моделью памяти, чем у x86. Следовательно, выбор этих моделей в качестве моделей для языка программирования оправдан только если предполагается поддержка компиляции исключительно для процессоров архитектуры x86.

6.3. Значения из воздуха

Далее мы переместимся на другой конец спектра моделей памяти и рассмотрим класс, в который входят наиболее слабые модели. Эти модели предоставляют оптимальные схемы компиляции и допускают, практически, любые разумные трансформации программ, но достигают этого ценой введения значений из воздуха (4).

Снова рассмотрим пример программы буферизации операции чтения:

Версия программы справа LBtr может быть получена из программы слева LB путем применения переупорядочивания инструкций типа чтение/запись. Результат $[{{r}_{1}} = 1,{{r}_{2}} = 1]$ является допустимым для программы LBtr. Тогда модель памяти, в которой переупорядочивание типа чтение/запись является корректной трансформацией, также должна допускать этот результат для программы LB. Как было продемонстрировано в § 4.3.4, для того, чтобы получить такой результат, необходимо применить спекулятивное исполнение.

Мы также обсуждали, что неограниченное спекулятивное исполнение может привести к появлению так называемых значений из воздуха, которые нарушают фундаментальные гарантии о поведении программ [16, 55], в частности, гарантии типобезопасности (type-safety) и композициональности. Также не выполняется и гарантия внешней свободы от гонок (eDRF). Чтобы убедиться в этом, рассмотрим еще один пример:

Для модели памяти, допускающей значения из воздуха, результат $[{{r}_{1}} = 1,{{r}_{2}} = 1]$ также является допустимым (обоснование этого результата такое же, как и для примера LB+data из § 4.3.4). Однако этот результат не только не интуитивен, но и противоречит гарантии внешней свободы от гонок. Действительно, в модели SC единственный допустимый сценарий поведения этой программы ведет к результату $[{{r}_{1}} = 0,{{r}_{2}} = 0]$ и не содержит гонок, следовательно, в модели, предоставляющей гарантию eDRF, эта программа также должна иметь только этот единственный сценарий поведения.

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

6.4. Сохранение программного порядка

Наиболее простой способ запретить значения из воздуха был предложен в работе [16]. Основная идея этого подхода – полностью запретить спекулятивное исполнение, что может быть достигнуто путем запрета переупорядочивания инструкций типа чтение/запись. Это решение позволяет не только восстановить свойство внешней свободы от гонок (eDRF) и другие гарантии [21], но также ведет к более простой модели. Абстрактная машина, реализующая данную модель, не нуждается в использовании спекулятивного исполнения и может выполнять инструкции потоков согласно их программному порядку, т.е. в том порядке, в котором они указаны. Память такой машины может быть организована как монотонно растущая история сообщений, где каждый поток имеет свое представление фронта данной истории [22, 46].

Данный подход был формализован в работе [21]. Там же было показано, что многие трансформации над кодом программ, за исключением переупорядочивания инструкций типа чтение/запись, остаются корректными в рамках моделей данного класса (см. табл. 1).

Схема компиляции программ для процессоров семейства x86 является оптимальной, так как модель памяти данной архитектуры гарантирует сохранение порядка между операциями чтения и последующими операциями записи. Однако архитектуры с более слабыми моделями (Arm, POWER) не гарантируют сохранения этого порядка, и таким образом требуют принятия дополнительных мер при компиляции кода. В [16] было предложено компилировать инструкции ослабленного (rlx) чтения как обычные инструкции чтения, за которыми следует ложная инструкция условного ветвления (conditional jump), которая добавляет зависимость между операцией чтения и последующими операциями записи. Гарантируется, что процессоры семейств Arm и POWER сохранят такую зависимость и, таким образом, сохранят порядок между операцией чтения и последующими операциями записи. В работе [23] изучались накладные расходы этой схемы компиляции, при ее применении только к ослабленным (rlx) атомарным обращениям. При компиляции кода для процессоров семейства Armv8 замедление времени работы составило 0% в среднем и 6.3% максимум на наборе тестов, реализующих различные многопоточные структуры данных, например, блокировки, стеки, очереди, деки, ассоциативные массивы и т.д. Заметим, что следует ожидать более существенного замедления времени работы программ при применении данной схемы компиляции также к неатомарным обращениям к памяти.

6.5. Сохранение синтаксических зависимостей

Альтернативное простое решение проблемы значений из воздуха заключается в сохранении синтаксических зависимостей между операциями обращения к памяти [16, 48]. В рамках этого подхода переупорядочивание инструкций типа чтение/запись разрешено, если переставляемые инструкции являются независимыми. Переупорядочивание запрещено, если операция записи зависит от значения, прочитанного операцией чтения, (в этом случае мы говорим что существует зависимость по данным, data dependency), или если это значение было использовано при вычислении адреса операции записи (зависимость по адресу (address dependency), или если путь исполнения программы, ведущей к операции записи, зависит от прочитанного значения (зависимость по управлению, (control dependency). Например, в программе LB+data существует зависимость по данным, так как инструкция $y: = {{r}_{1}}$ записывает значение, прочитанное инструкцией $x: = {{r}_{1}}$.

Заметим, что эти зависимости вычисляются следуя синтаксису программы (отсюда происходит и название), в противоположность семантическим зависимостям. Например, в модифицированной версии программы LB+data, представленной ниже, операция записи в переменную y в левом потоке имеет синтаксическую зависимость от предыдущей операции чтения.

В этом примере синтаксическая зависимость может быть удалена с помощью оптимизации распространения констант – подвыражение $1 + 0 * {{r}_{1}}$ может быть преобразовано в значение 1. Однако если модель памяти гарантирует сохранение синтаксических зависимостей, компилятору запрещено применять эту оптимизацию, так как после удаления зависимости ничто не мешает компилятору или процессору переставить операцию записи до предшествующей операции чтения.

На этом примере можно видеть главный недостаток моделей, сохраняющих синтаксические зависимости: различные оптимизации, сохраняющие трассы (например, распространение констант), оказываются некорректными в этих моделях. Распространение констант является одной из классических оптимизаций, и тот факт, что оно некорректно, препятствует применению моделей этого класса. Заметим, что модели памяти процессоров используют сходный подход и тоже сохраняют синтаксические зависимости между обращениями к разделяемой памяти [11, 12, 14]. Однако в этом случае это не является проблемой, так как процессоры во время исполнения программы не выполняют такие сложные оптимизации, как распространение констант.

В работе [23] изучалось замедление времени работы программ, накладываемое моделью памяти, сохраняющей синтаксические зависимости. Авторы модифицировали оптимизирующие проходы компилятора так, чтобы они сохраняли зависимости между неатомарными и ослабленными (rlx) атомарными обращениями. Затем они измерили время работы программ из тестового набора SPEC CPU2006, скомпилированных модифицированной версией компилятора LLVM для процессоров семейства Armv8, и сообщили об умеренном замедлении на 3.1% в среднем и 17.6% максимум.

6.6. Сохранение семантических зависимостей

Последний рассматриваемый нами подход к решению проблемы значений из воздуха заключается в построении понятия семантических зависимостей, которые могли бы точно характеризовать то, какие пары операций чтения/записи являются независимыми, и отфильтровали бы ложные зависимости как в примере LB+fakedata. Практическая ценность данного подхода заключается в том, что он не требует модификаций существующих компиляторов и процессоров и не накладывает дополнительных расходов на время исполнения скомпилированных программ. Конечной целью подхода является предоставление оптимальных схем компиляции, сохранение корректности большинства существующих трансформаций кода, и в то же время поддержка основных гарантий, таких как внешняя свобода от гонок (eDRF).

Оказывается, что эта задача является весьма трудной и на сегодняшний день не решена. Чтобы дать удовлетворительное определение семантических зависимостей, исследователи были вынуждены обратиться к концептуально сложным моделям памяти [17, 19, 20, 24, 25, 51]. Основная сложность работ в данном направлении – необходимость предоставления формальных доказательств того, что эти модели удовлетворяют предъявляемым требованиям, а именно поддерживают оптимальные схемы компиляции и широкий набор трансформаций, и в то же время сохраняют все важные гарантии о поведении программ.

На сегодняшний день наиболее полное решение данной проблемы предоставляет модель “обещающей” семантики (Promising semantics) [17, 18]. Было доказано, что эта модель допускает оптимальные схемы компиляции [62], разрешает применять большинство локальных и глобальных трансформаций (за исключением слияния потоков), и в то же время предоставляет свойство внешней свободы от гонок и другие гарантии.

6.7. Вспомогательная классификация

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

6.7.1. Когерентные модели

Свойство когерентности, которое также иногда называется последовательной согласованностью по каждой локации (§ 4.3.2), неожиданным образом взаимодействует с трансформацией удаления общих подвыражений (CSE). Впервые эта связь была замечена в контексте ранней версии модели памяти Java [63]. Чтобы увидеть проблему, рассмотрим программу ниже (слева) и ее версию после применения трансформации CSE (справа). Заметим, что оптимизация заменила второе обращение к переменной x присваиванием значения из регистра.

Предположим, что переменные x и y на самом деле указывают на одну и ту же ячейку памяти. При таком предположении можно сделать вывод о том, что сценарий выполнения программы с результатом $[{{r}_{1}} = 0,{{r}_{2}} = 1,{{r}_{3}} = 0]$ должен быть запрещен моделью памяти, гарантирующей когерентность. В самом деле, когерентная модель памяти для программы, содержащей обращения только к одной локации в памяти, допускает только последовательно согласованные сценарии исполнения. Результат $[{{r}_{1}} = 0,{{r}_{2}} = 1,{{r}_{3}} = 0]$ не может быть получен как последовательное чередование инструкций потоков, и, значит, он не является последовательно согласованным и должен быть запрещен. Тем не менее, данный результат допустим для оптимизированной версии этой программы.

Заметим, что несмотря на вышесказанное, компилятор все равно может применить оптимизацию CSE к программе выше, но только в том случае, если он сможет вывести, что переменные x и y указывают на разные локации в памяти. Эта информация может быть получена при помощи анализа псевдонимов (alias analysis) [64]. По сути, в этом случае CSE может быть сведен к комбинации других трансформаций – переупорядочиванию и элиминации операций.

Таким образом, в общем случае свойство когерентность несовместимо с удалением общих подвыражений. Что касается оптимальности схем компиляции, то здесь когерентность не накладывает каких-то дополнительных ограничений, поскольку модели памяти процессоров гарантируют соблюдение когерентности [9, 11, 12, 21].

6.7.2. Модели с возгорающейся семантикой

Возгорающаяся семантика (catch-fire semantics) присваивает неопределенное поведение программам, содержащим гонки на неатомарных обращениях, и, таким образом, влияет на корректность трансформаций. Как было упомянуто ранее, наличие подобного неопределенного поведения позволяет использовать оптимальные схемы компиляции для неатомарных обращений и влечет корректность широкого класса трансформаций, корректных для случая однопоточных программ. Но помимо этого возгорающаяся семантика интересно взаимодействует с трансформацией введения спекулятивной операции чтения.

Рассмотрим следующий пример:

В § 4.2 мы упоминали, что спекулятивное введение операции чтения может быть использовано в комбинации с элиминацией типа чтение/чтение, чтобы вынести инструкцию чтения из ветки условного оператора. В частности, в примере выше спекулятивное введение операции чтения может добавить инструкцию t := y перед условным оператором if, а затем элиминация типа чтение/чтение может заменить вторую операцию чтения присваиванием значения из регистра.

Тонкий момент тут заключается в том, что хотя программа слева не содержит гонок в модели последовательной согласованности, программа справа имеет гонку между операциями чтения и записи переменной y. В предположении, что все обращения в программе выше являются неатомарными, можно заключить, что возгорающаяся семантика должна рассматривать правую программу как имеющую неопределенное поведение. Другими словами, для программы справа допустим любой сценарий исполнения, в то время как для программы слева допустим только сценарий с результатом [r = 0]. Однако необходимость корректности трансформации требует, чтобы множество допустимых сценариев исполнения модифицированной программы было подмножеством сценариев поведения оригинальной программы. Можно видеть, что в этом примере условие корректности нарушается.

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

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