Структуры событий и современные мультипроцессоры

Введение 4
Постановка задачи 7
Обзор 8
Глава 1. Теорема о корректности компиляции 25
1.1. Схема доказательства теоремы 26
1.2. Пример построения структуры событий 28
Глава 2. Симуляция обхода графа IMM 31
2.1. Обход графа IMM 31
2.2. Отношение симуляции 33
2.3. Шаг симуляции 36
Заключение 43
Список литературы 44
Купить

Современные мультипроцессоры и компиляторы высокоуровневых язы­ков программирования выполняют множество оптимизаций при исполнении и компиляции программ соответственно с целью повышения производитель­ности конечного кода. В случае многопоточных программ применение этих оптимизаций может привести к неожиданным сценариям поведения. Рассмот­рим, например, программу LB-nodep, представленную ниже1.
а := x II1
b := у Ц1
а := x II1
b := у Ц1
a := x II1
b := у Ц1
У := 1
x := b
у := 1 + а * 0
x := b
У := a
x := b
(LB-nodep)
(LB-fakedep)
(LB-dep)
При сборке программы оптимизирующий компилятор может выполнить переупорядочивание инструкций a := x и у := 1 в левом потоке, так как дан­ные инструкции независимы. Тем не менее, при исполнении в многопоточной среде эффект от применения данной оптимизации может наблюдаться други­ми потоками. Например, в случае LB-nodep это может привести к сценарию исполнения программы, при котором обе локальные переменные а и b будут содержать значение 1. Подобные сценарии известны как слабые сценарии поведения (weak behaviors).
Моделью памяти (memory model) принято называть семантику мно­гопоточных программ, оперирующих с разделяемой памятью [1]. Слабые модели памяти (weak memory models) призваны описать поведение много­поточных программ с учетом слабых сценариев поведения. Основной иссле­довательской проблемой в данной области является формальное определение модели памяти, которая с одной стороны позволяла бы описывать эффекты от применения широкого класса оптимизаций, в частности, переупорядочи­вание независимых инструкций чтения и записи (load-to-store reordering) и распространение констант (constant propagation), а с другой стороны за­прещала бы появление так называемых значений из воздуха (out-of-thin-air values) [1, 2].
Данную проблему можно продемонстрировать на примере программ LB-nodep, LB-fakedep и LB-dep. Желаемая модель памяти должны допускать сценарий поведения, при котором в результате справедливо, что a = b = 1, для программ LB-nodep и LB-fakedep, но не для программы LB-dep. В слу­чае LB-nodep данный результат может быть обоснован переупорядочиванием независимых инструкций чтения и записи в левом потоке. В случае LB-fakedep тот же результат может быть получен после применения распространения констант и упрощения подвыражения у := 1 + a * 0 до у := 1, а затем пе­рестановки инструкций. В случае LB-dep сценарий поведения, при котором в результате получаем a = b = 1, не может быть обоснован никакой комби­нацией разумных оптимизаций. Значение 1 в данном случае появляется “из воздуха”.
Предъявленные выше требования, то есть поддержка широкого класса оптимизаций и запрещение значений из воздуха, являются критическими для моделей памяти высокопроизводительных языков программирования, таких как C/C++ [3], Java [4], или языка промежуточного представления LLVM (LLVMIR) [5]. Среди нескольких кандидатов [6, 7, 8], удовлетворяющих дан­ным требованиям, в контексте данной работы нас будет интересовать модель Weakestmo [9], основанная на теории структур событий [10]. К её достоин­ствам можно отнести декларативность и поддержку всего спектра возможно­стей модели памяти C/C++ [3]. Тем не менее, у данной модели существуют и недостатки. В частности, ранее для данной модели не была доказана коррект­ность оптимальной схемы компиляции для моделей памяти современных мультипроцессоров, таких как x86 [11], ARM [12] и POWER [13].
Корректность оптимальной схемы компиляции для моделей мультипро­цессоров является ещё одним критический важным требованием, предъявля­емым к моделям памяти высокопроизводительных языков программирова­ния [1]. Оно необходимо для того, чтобы гарантировать, что при компиляции инструкций обращения к разделяемым переменным из языка программиро­вания в инструкции целевого процессора не требовалось вставлять специаль­ные инструкции — барьеры памяти (memory barriers или memory fences) [14], которые могут снижать производительность кода, и при этом программа оста­валась корректной.
В данной работе исправляется данный недостаток. А именно, представ­лено доказательство корректности компиляции из модели Weakestmo в моде­ли современных мультипроцессоров x86, ARM и POWER, формализованное с помощью системы для интерактивного доказательства теорем Coq2 [15]. Предложенное доказательство использует промежуточную модель памяти (intermediate memory model, IMM) [16], предоставляющую удобную абстрак­цию над моделями x86, ARM и POWER, в качестве промежуточного звена между моделью Weakestmo и моделями мультипроцессоров. Поскольку кор­ректность компиляции из модели IMM в модели x86, ARM и POWER уже была показана ранее в работе [16], остается лишь доказать корректность ком­пиляции из модели Weakestmo в модель IMM (корректность компиляции из Weakestmo в модели x86, ARM и POWER получается по транзитивности).
Основной сложностью доказательства является то, что модели Weakestmo и IMM заданы в разных стилях. Модель IMM разрешает спекулятивное испол­нение инструкций вне очереди, но при этом отслеживает синтаксические зави­симости между инструкциями, чтобы запретить появление циклов причинно­следственной связи. С другой стороны, модель Weakestmo исполняет ин­струкции по порядку, но рассматривает единовременно несколько сценариев исполнения объединенных в структуру событий, некоторые из этих сценари­ев исполнения моделируют спекулятивное исполнение инструкций вне оче­реди. С помощью метода симуляции [17] демонстрируется, что построение необходимой структуры событий может симулировать процесс исполнения программы в модели IMM.
Купить