Диссертация (1149932), страница 3
Текст из файла (страница 3)
Это связано с тем, что такие модели позволяют реализовать большее13число оптимизаций как на уровне процессора [27], так и на уровне компилятора [28, 29], что увеличивает производительность программ.Рассмотрим следующую программу MP (message passing, передача сообщения):[x] := 0; [y] := 0;(MP)[x] := 1; a := [y]; //1[y] := 1 b := [x] //0Эта программа является упрощенным примером передачи данных между потоками. Первый поток записывает данные в локацию x и потом выставляет флаг(локация y), что данные подготовлены; в свою очередь второй поток проверяетэтот флаг, а потом читает данные. Модель SC гарантирует, что если второй поток увидел, что флаг выставлен (a = 1), то он увидит и подготовленные данные(b = 1).
Тем не менее, эта программа имеет слабый сценарий поведения с результатом [a = 1, b = 0] на таких архитектурах как Power и ARM.С чем связано то, что на упомянутых выше архитектурах возможен результат [a = 1, b = 0]? Оптимизирующий процессор при исполнении программы можетвыполнить независимые инструкции не по порядку. Поскольку первая и втораяинструкции в левом потоке являются обращениями к разным локациям, то процессор может выполнить сначала вторую запись, а потом первую. То же самоеверно и для инструкций в правом потоке. После исполнения инструкций не попорядку хотя бы в одном потоке результат [a = 1, b = 0] становится возможным.Такой сценарий поведения также разрешается моделями памяти некоторыхязыков программирования, например, стандартами языков C11 [30] и C++11 [31],поскольку оптимизирующий компилятор должен иметь возможность переупорядочить независимые обращения к памяти.О корректности программы MP.
Гонки по даннымС точки зрения некоторых языков программирования программа MP можетсчитаться некорректной, т.к. в этой программе есть гонка по данным [32].Определение 1. В программе имеется гонка по данным (data race), если в некотором её сценарии поведения существуют два неупорядоченных обращения к однойи той же ячейке памяти, причём, как минимум, одно из этих обращений являетсяоперацией записи.14Данное определение не является формальным, т.к.
здесь не определяетсяпорядок на операциях над памятью. Это связано с тем, что в разных моделях этотпорядок определяется существенно по-разному. По сути, два обращения неупорядочены, если порядок их исполнения определяется не логикой программы, авнешними факторами, такими как, например, диспетчеризация потоков.В отсутствии гонок по данным большинство слабых моделей памяти гарантируют, что все сценарии поведения являются SC-поведениями. Для того, чтобы добиться отсутствия гонок даже при использовании общей памяти (sharedmemory), применяют блокировки (locks), которые упорядочивают обращения кразделяемому ресурсу.Как следствие, один из способов задать модель памяти для языка программирования выглядит следующим образом: если в программе нет гонок по данным,то её поведение определяется моделью SC, иначе программа является некорректной и обладает неопределенным поведением (undefined behavior).
У такого способа есть, как минимум, два недостатка. Во-первых, языки программирования (например, Java), стремясь обеспечить типобезопасность (type safety), не могут использовать такой способ задания семантики, т.к. гарантируют, что программа неможет иметь неопределенное поведение, если она прошла проверку типов, а наличие или отсутствие гонок по данным не может быть проверено статически. Вовторых, многие высокопроизводительные алгоритмы многопоточного программирования используют парадигму неблокирующей синхронизации (non-blockingsynchronization), которая существенным образом опирается на гонки по данным.Более того, в большинстве случаев реализация самих блокировок использует гонки по данным, что делает невозможным рассуждения о ней в рамках приведеннойвыше упрощённой модели.Из вышесказанного следует, что модель памяти промышленного языка программирования должна обеспечивать корректную семантику, как минимум, длянекоторого множества программ с гонками по данным.1.2Требования к моделям памятиНа данный момент имеется множество моделей памяти как для процессорных архитектур [6, 7, 9, 10, 33, 34], так и для языков программирования [1, 3, 4, 35–40].
Существенным отличием между этими группами моделей являются предъявляемые к ним требования.15Модели процессорных архитектур должны описывать сценарии поведениясуществующих процессоров, а также оставлять пространство для возможных оптимизаций для следующих версий процессоров. Кроме того, такие модели зачастую либо заданы операционно, т.е.
в терминах некоторой абстрактной машины [41], либо имеют эквивалентное операционное представление. Это позволяетопределить модель в терминах, близких и понятных разработчикам архитектуры,а также дать разработчикам компиляторов интуитивно понятное представлениеоб исполнении программы.Модель памяти языка программирования должна быть представлена такимобразом, чтобы, с одной стороны, она разрешала манипуляции над кодом программы, совершаемые в рамках компиляторных оптимизаций, и давала возможность эффективно компилировать программы в целевую процессорную архитектуру, а, с другой стороны, предоставляла разумные гарантии для программиста.Эти требования до некоторой степени противоречат друг другу, поэтому хорошаямодель соблюдает баланс между ними. Для того, чтобы понять, в чём заключаетсяпротиворечие данных требований, остановимся на них подробнее.1.2.1Корректность компиляторных оптимизацийПусть есть некоторый язык программирования L1 и его модель памяти M(memory model).
Тогда под семантикой программы P на языке L в модели M будетпониматься множество возможных сценариев поведения P в M. Это множествобудет обозначаться JPKM . Оптимизацией над программами в языке L мы будемназывать функцию opt, действующую из множества программ на языке L в негоже.Определение 2. Оптимизация opt : L → L называется корректной в модели M,CorrectOptM (opt), если для любой программы P на языке L семантика оптимизированной программы opt(P) является подмножеством семантики изначальнойпрограммы P:∀opt : L → L. CorrectOptM (opt) ⇔ (∀P ∈ L.
Jopt(P)KM ⊆ JPKM ).Какие компиляторные оптимизации должны быть корректны в рамках модели памяти языка программирования? К сожалению, на данный момент не су1 Здесь язык программирования рассматривается как множество высказываний (в нашем случае — про-грамм) на этом языке.16ществует полного списка таких оптимизаций, однако из работ [42–44] можно выделить пять основных групп.1. Локальные оптимизации, не меняющие обращения к памяти. Например,удаление условных переходов, зависимых от заведомо ложного условия:a := 0;if athen b := [x]else skipfi;c := [y]⇝a := 0;skip;c := [y]2. Перестановка независимых обращений к памяти.
Например, перестановка инструкций чтения из разных локаций:a := [x];b := [y]⇝b := [y];a := [x]3. Устранение избыточных обращений к памяти. Например, устранение инструкции чтения, следующей за инструкциями чтения или записи в ту желокацию:a := [x];b := [x]⇝a := [x];b := a[x] := a;b := [x]⇝[x] := a;b := a4. Вставка избыточных обращений к памяти. Например, вставка инструкции чтения в переменную, значение которой далее нигде не используется.5. Глобальныеоптимизации.Например,секвенциализация(sequentialization), которая заменяет параллельную композицию потоков на последовательную:C1 || C2 ⇝ C1 ; C2Желательно, чтобы упомянутые классы оптимизаций были корректными,возможно, с некоторыми оговорками в модели памяти языка программирования.Для этого модель должна быть достаточно слабой, т.е.
позволять сценарии поведения, которые возможны для программы после оптимизации.171.2.2Наличие эффективной схемы компиляцииМодель памяти языка программирования должна учитывать модель памятицелевой платформы, т.е. должна существовать корректная схема компиляции изодной модели в другую.Определение 3. Пусть есть некоторые языки L и L′ и соответствующие моделипамяти M и M′ . Функция compl : L → L′ является корректной схемой компиляции из модели M в модель M′ , если для любой программы P на языке L семантикапрограммы compl(P) в модели M′ является подмножеством семантики P в модели M.Из этого определения следует, что чем слабее модель целевой платформы,т.е. чем больше существует сценариев поведения на целевой платформе, тем больше ограничений накладывается на корректную схему компиляции.Рассмотрим то, как должна быть устроена корректная схема компиляции изболее строгой модели памяти в более слабую на примере компиляции ранее приведенной программы MP из модели SC [1] в модель архитектуры Power [6].
Врамках модели SC программа MP не имеет сценария поведения [a = 1, b = 0],тогда как в модели Power такой сценарий возможен. Для того, чтобы получитькорректную компиляцию, в скомпилированную программу нужно вставить специальные инструкции — т.н. барьеры памяти. Эти барьеры вносят дополнительные ограничения на сценарии поведения программ. Достигается это за счёт того,что барьеры запрещают некоторые компиляторные и процессорные оптимизации.В архитектуре Power есть барьер hwsync, который запрещает переупорядочивание любых инструкций вокруг него. Вставка такого барьера между инструкций впрограмме MP гарантирует отсутствие сценария поведения [a = 1, b = 0] в моделиPower2 :[x] := 0; [y] := 0;[x] := 1; a := [y];(MP-hwsync)hwsync; hwsync;[y] := 1 b := [x]На ряду с hwsync архитектура Power также предоставляет более слабый барьерlwsync, который запрещает только перестановки пар инструкций чтение-чтение,2 Здесьи далее в диссертации используется один и тот же синтаксис для описания как исходных, так искомпилированных программ с точностью до барьеров и модификаторов чтения и записи.18чтение-запись и запись-запись.
Такого барьера также достаточно, чтобы запретитьсценарий [a = 1, b = 0]:[x] := 0; [y] := 0;[x] := 1; a := [y];(MP-lwsync)lwsync;lwsync;[y] := 1 b := [x]В данном случае схема компиляции, использующая барьер lwsync, является более предпочтительной по сравнению со hwsync-схемой, т.к. барьер lwsync на реальных процессорах исполняется быстрее (или, как минимум, не медленнее), чемhwsync.Если рассмотреть модель памяти языка программирования, которая разрешает сценарий поведения с результатом [a = 1,b = 0] (на ряду со всеми остальными сценариями, возможными в рамках модели SC), то для компиляции программыMP из такой модели в модель Power не будет необходимости вставлять барьерыпамяти. Это хорошо, т.к.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
