Диссертация (1149932), страница 13
Текст из файла (страница 13)
На более чем 20 запусках программы не было получено stuck-состояния.Далее, в программу была внесена ошибка синхронизации, а именно удалены вызовы функции syncWithReader, помеченные серым фоном на рис. 19. Крометого, автором учитывались ещё два дополнительных критерия корректности программы. Во-первых, все значения r11, r12, r21 и r22 должны быть из множества{0, 1, 11, 111, 1101}, что гарантирует корректность прочтения списка. Во-вторых,должны выполняться неравенства r11 ⩽ r12 и r21 ⩽ r22, поскольку после каждого добавления и изменения в списке сумма его элементов увеличивается.68Тест был запущен 20 раз на компьютере с процессором Core i7 2.5Ghz, 8Gbоперативной памяти и операционной системой Linux.
Каждый из запусков завершился менее чем за 27 секунд, и критерий корректности переменных r∗ не нарушался (см. табл. 2). Тем не менее из-за того, что в модифицированной версии программы вызовы функции syncWithReader не предшествуют освобождению локации с помощью оператора delete, потоки-читатели обращаются к “удалённым”локациям, о чём свидетельствует графа stuck.Аналогично, рандомизированное тестирование указывает на наличие ошибки, если в функции traverse приобретающее чтение внутри цикла repeat поменять на расслабленное.
Это приводит к тому, что между читателем и писателемне происходит синхронизации, и позволяет читателю провести чтение из локацийa, b, c и d, о которых он не осведомлён. Последнее приводит к stuck-состояниюпо правилу Read-Uninit.2.4ВыводыВ данной главе была представлена операционная модель памяти дляC/C++11, OpC11 MM. Эта модель задана как множество аспектов, которые описывают различные особенности C/C++11. Ключевыми понятиями модели являются фронты и операционные буфера.
Фронты используются для представлениязнания (осведомленности) потоков о текущем состоянии общей памяти, операционные буфера позволяют откладывать исполнение инструкций и производитьспекулятивные вычисления.OpC11 MM рассмотрена на наборе тестовых программ из литературы, а также на RCU-структуре, в результате был сделан следующий вывод: поведение модели совпадает с C/++11 MM на большинстве программ. OpC11 MM предлагает синтаксический способ обработки спекулятивного исполнения, что позволяетоставить модель вычисляемой, т.е.
даёт возможность реализовать её интерпретатор. Но следует отметить, что по этой же причине модель не поддерживает некоторые компиляторные оптимизации, связанные с семантическими свойствами программы.69Глава 3. Корректность компиляции из обещающеймодели в операционную модель ARMv8 POPВ этой главе доказывается корректность эффективной схемы компиляциииз подмножества обещающей модели памяти [11] в модель памяти ARMv8 POP[9]. Рассмотренное подмножество обещающей модели состоит из расслабленныхобращений памяти, высвобождающего и приобретающего барьеров памяти.3.1Мотивация доказательства корректности компиляцииОбещающая модель (Promise MM) является операционной моделью памяти для языков программирования.
Она похожа на OpC11 MM, описанную впредыдущей главе: память представляется как множество событий, упорядоченных метками времени, а ключевым механизмом модели также являются фронты. Существенным отличием обещающей модели от OpC11 MM является то, чтопервая предлагает семантический способ для эмуляции переупорядочивания инструкций: вместо того, чтобы откладывать операции, поток может пообещать,что он в будущем сделает определенную запись; обещанное сообщение становится доступным для чтения другими потоками.
Как следствие, обещающая модельподдерживает больше оптимизаций и ближе к C/C++11 MM. Негативным отличием обещающей модели от OpC11 MM является то, что упомянутый механизмобещаний требует, чтобы после каждого шага исполнения обещающей моделипроисходила сертификация — механизм, гарантирующий отсутствие “значенийиз воздуха”. Сертификация является алгоритмически неразрешимой в случае, когда обещающая модель задана для языка, полного по Тьюрингу, и следовательно,в этом случае для обещающей невозможно разработать интерпретатор.
Несмотряна это, научное сообщество рассматривает обещающую модель как кандидата назамену моделей памяти языков C/C++ и Java. Для того, чтобы модель действительно смогла стать частью стандартов этих языков, должна быть доказана корректность компиляции во все основные целевые платформы: x86, Power, ARM.Модель памяти ARMv8 POP является операционной и описывает многопоточное поведение процессорной архитектуры ARMv8.0. В этой версии архитектуры появилось несколько новых инструкций, которые предназначены не толькоупростить компиляцию из языков C/C++11, но и повысить производительностьцелевых программ.
Так, в частности, в модели появились отдельные инструкции70приобретающего чтения и высвобождающей записи. Кроме того, модель ARMv8POP является очень слабой, т.е. позволяет слабые сценарии поведения, которыене наблюдаются в рамках других моделей памяти процессорных архитектур.Для обещающей модели памяти ранее была доказана корректность компиляции в модели x86-TSO [7] и Power [6] в [11]. Доказательство было основанона том, что модели x86-TSO и Power представимы в виде набора локальных переупорядочиваний, для которых доказана корректность в обещающей модели памяти, над более строгими моделями. Для более строгих моделей верно, что всехих сценарии поведения могут быть воспроизведены в подмножестве обещающеймодели, в котором не используется механизмы обещаний и, как следствие, сертификации.Такой подход не применим для модели ARMv8 POP. Так, следующая программа в модели ARMv8 POP имеет слабый сценарий поведения с результатомa = 1:[x] := 0; [y] := 0;(ARM-weak)a := [x]; //1 b := [x]; c := [y];[x] := 1[y] := b [x] := cВ этой программе любое переупорядочивание инструкций невозможно, следовательно упомянутый сценарий поведения воспроизводим в обещающей моделитолько с помощью механизма обещаний.3.2Описание моделей на примерахМы начнём обсуждение ARMv8 POP и обещающей моделей с того, что покажем, как в них воспроизводится слабое поведение программы MP.[x] := 0; [y] := 0;[x] := 1; a := [y]; //1[y] := 1 b := [x] //0(MP)Схема компиляции из обещающей модели в ARMv8 POP, рассмотренная в доказательстве корректности компиляции, имеет следующий вид:Promise:[x] :=rlx aARMv8 POP: [x] := aa :=rlx [x]fence(acq)fence(rel)a := [x]fence(ld)fence(sy)Она является биекцией на инструкциях обоих моделей, поэтому все программы вэтой главе будут представлены в одном синтаксисе — синтаксисе модели ARMv8POP.71Поток 1Поток 2[y] := 1b := [x][x] := 1a := [y]Память[x] := 0; [y] := 0Поток 1Поток 2[x] := 1Поток 1Поток 2[x] := 1b := [x]a := [y][y] := 1b := [x][y] := 1Память[x] := 0; [y] := 0Память[x] := 0; [y] := 0а)б)в)Рис.
20. Состояние подсистемы памяти ARMv8 POP при исполнении программыMP3.2.1Модель ARMv8 POPМодель ARMv8 POP задана операционно, и, соответственно, существуетнекоторая абстрактная машина (ARM-машина) которая описывает сценарии поведения в рамках этой модели. ARM-машина состоит из двух компонент: подсистемы управления (thread subsystem) и подсистемы памяти (storage subsystem).До некоторой степени эти подсистемы можно рассматривать как набор вычислительных ядер (подсистема управления), которые, выполняя программу, посылаютзапросы в оперативную и кэш-память (подсистема памяти).
Подсистема памяти вARM-машине представлена как иерархическая система буферов, где каждый буфер является изменяемым списком запросов, а у основания иерархической системы находится память — функция из локаций в значения. Запросы бывают трёхвидов: на чтение, на запись и барьер памяти.Результат [a = 1, b = 0] в ARM-машине может быть получен двумя способами. Во-первых, подсистема управления имеет право исполнять инструкции не попорядку (out-of-order execution). Так, первый поток в программе MP может отправить запрос на запись [y] := 1 в подсистему памяти до запроса [x] := 1, а второйпоток, соответственно, может увидеть эти запросы в отличном от программногопорядке.
Во-вторых, подсистема памяти также может переупорядочить запросывнутри себя. Так, сначала оба потока могут отправить по два запроса в подсистемупамяти (см. рис. 20а). После этого подсистема переупорядочивает независимыезапросы [x] := 1 и [y] := 1, отправляет [y] := 1 в общий для двух потоковбуфер, как и запросы второго потока (см. рис. 20б). Поскольку в общем буферезапросы [y] := 1 и a := [y] находятся рядом, то подсистема памяти может послать ответ [a ← 1] на запрос a := [y] в подсистему управления (cм.
рис. 20в).72После этого запрос [x] := 1 отправляется в общий буфер, а затем все оставшиесязапросы отправляются в память, что приводит к результату [a = 1, b = 0].В разделе 1.2.2 было сказано, что аналогичный сценарий поведения в случае архитектуры Power может быть запрещен с помощью барьеров памяти. Этоверно и для модели ARMv8 POP.
Так, следующая программа не имеет сценарияповедения с результатом [a = 1, b = 0]:[x] := 0; [y] := 0;a := [y]; //1[x] := 1;fence(sy); fence(ld);[y] := 1b := [x] //0(MP-SY-LD)Полный барьер fence(sy) в первом потоке заставляет подсистему управления отправить все три запроса в исходном порядке; кроме того, запрос, соответствующий полному барьеру, не может быть переупорядочен с другими запросами внутри подсистемы памяти1 . Так, барьер fence(sy) гарантирует, что запрос [y] := 1попадает в общий буфер подсистемы памяти только после [x] := 1. Во втором потоке барьер на чтение fence(ld) запрещает подсистеме управления отправлятьзапрос на чтение b := [x] до того момента, пока она не получит ответ на запросa := [y].
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
