Диссертация (1149932), страница 14
Текст из файла (страница 14)
Таким образом гарантируется, что если a = 1, то b = 1.В приведенных выше сценариях было важно, что подсистема памяти можетпереупорядочивать лишь некоторые пары сообщений. Какие пары могут быть переупорядочены, а какие не могут, определяется отношением eold ,→ enew :Определение 4.
Запросы eold и enew могут быть переупорядочены, что обозначается eold ,→ enew , если среди них нет полного барьера, и они оперируют над разнымилокациями.Отметим, что в доказательстве корректности компиляции рассматриваетсяослабленная версия модели ARMv8 POP [9], которая допускает большее числосценариев поведения, поскольку в ней подсистема управления не отсылает запросы, соответствующие барьеру fence(ld), в подсистему памяти2 .
Поскольку нам1 Вместополного барьера в этой программе можно использовать барьер на запись fence(st), однакобарьер на запись не соответствует ни одной конструкции в обещающей модели, так же, как и в C/C++11MM.2 Почему рассмотренная модель допускает большее число поведений? Предположим, что модель посылает запросы fence(ld) в память, но они могут быть переупорядочены со всеми остальными. Такая мо-73удалось доказать корректность компиляции для ослабленной версии модели, токорректность компиляции сохраняется и для исходной модели.Теперь рассмотрим сценарий поведения программы ARM-weak, в которомполучается результат [a = 1, b = 1, c = 1]:[x] := 0; [y] := 0;a := [x]; //1 b := [x]; c := [y];[x] := 1[y] := b [x] := c(ARM-weak)Такой результат получается в модели ARMv8 POP, если у первого и второго потоков есть общий буфер, который не виден третьему потоку.
Для получения результата [a = 1, b = 1, c = 1] первый поток отправляет оба запроса (на чтение a := [x]и на запись [x] := 1) в подсистему памяти, а второй поток отправляет запросна чтение b := [x], и после этого все запросы попадают в общий для первого ивторого потоков буфер (см. рис. 21а). Поскольку запросы на чтение b := [x] и назапись [x] := 1 находятся в одном буфере, и ближе к основной памяти находитсязапрос на запись, то подсистема памяти может послать ответ [b ← 1] второму потоку, а сам поток после этого — послать запрос [y] := 1, который через общийбуфер и переупорядочивание с запросами о локации x в нём попадает в основнуюпамять (см. рис. 21б).
Теперь третий поток посылает запрос на чтение c := [y](см. рис. 21в), который разрешается в общей памяти с ответом [c ← 1]. Послеэтого третий поток посылает запрос на запись [x] := 1 (см. рис. 21г), которыйдалее используется для отправки ответа на запрос чтения a := [x], приводя крезультату [a = 1, b = 1, c = 1].3.2.2Абстрактная подсистема памяти: POPВ [9] подсистема памяти модели ARM представлена в двух вариантах:Flowing и POP (partial order propagation). Несмотря на то, что мы называем модельиз [9] моделью ARMv8 POP, до этого момента в примерах использовалась подсистема памяти Flowing, поскольку она более наглядна.
Тем не менее, у Flowingесть два ключевых недостатка, которые решаются в POP — более абстрактном вариантом подсистемы памяти. Во-первых, вместо того, чтобы представлять буферкак список запросов и рассматривать в нём перестановки, математически удобнеедель, очевидно, допускает больше сценариев поведения, чем оригинальная, накладывающая ограниченияна переупорядочивание с fence(ld). Также очевидно, что полученная модель допускает те же сценарии,что и модель, которая не посылает запросы fence(ld).74Поток 1Поток 2Поток 3Поток 1Поток 2b := [x][x] := 1a := [x][x] := 1a := [x]Память[x] := 0; [y] := 0Память[x] := 0; [y] := 1а)Поток 1Поток 3Поток 2б)Поток 3Поток 1Поток 2Поток 3[x] := 1a := [x][x] := 1a := [x]c := [y]Память[x] := 0; [y] := 1[x] := 1Память[x] := 0; [y] := 1в)г)Рис.
21. Состояние подсистемы памяти ARMv8 POP при исполнении программыARM-weakпредставлять его как частично упорядоченное множество. Во-вторых, подсистемаFlowing требует введения конкретной топологии буферов, что при рассужденияхо всех сценариях поведения программы заставляет дополнительно рассматриватьи варианты топологий.В подсистеме POP нет линейных буферов и фиксированной топологии. Вместо этого состояние подсистемы представляется как тройка ⟨Evt, Ord, Prop⟩, гдеEvt — это множество текущих запросов в подсистеме, Ord — это частичный порядок на запросах из Evt, а Prop — функция, которая по идентификатору потокавозвращает множество “распространённых” на поток запросов. Если запросы e иe′ упорядочены отношением Ord, т.е. Ord(e, e′ ), то мы пишем e <Ord e′ .Для того, чтобы понять, как подсистема POP работает и соотносится с подсистемой Flowing, рассмотрим слабый сценарий поведения следующей программы с результатом [a = 1, b = 1, c = 0]:[x] := 1;a := [x]; // 1[y] := ab := [y];// 1c := [x + b ∗ 0] // 0(WRC-data-addr)В данной программе подсистема управления модели ARMv8 POP во втором и третьем потоках не может отправить запросы, относящиеся ко второй строке, пока75Поток 1Поток 2Поток 3m : [x] := 1 n : a := [x] o : b := [y]k : [x] := 0; l : [y] := 0б)а)Поток 1Поток 2Поток 3n : a := [x] o : b := [y]m : [x] := 1k : [x] := 0; l : [y] := 0в)Поток 1Поток 2Поток 3o : b := [y]n : a := [x]m : [x] := 1k : [x] := 0; l : [y] := 0д)Evt = {k, l, m, n, o}Ord = {(k, m), (k, n), (l, o)}Prop(T 1) = {k, l, m}Prop(T 2) = {k, l, n}Prop(T 3) = {k, l, o}Evt = {k, l, m, n, o}Ord = {(k, m), (k, n),(l, o), (m, n)}Prop(T 1) = {k, l, m}Prop(T 2) = {k, l, n, m}Prop(T 3) = {k, l, o}г)Evt = {k, l, m, n, o}Ord = {(k, m), (k, n),(l, o), (m, n)}Prop(T 1) = {k, l, m, n}Prop(T 2) = {k, l, n, m}Prop(T 3) = {k, l, o}е)Рис.
22. Состояние подсистем Flowing и POP при исполнении программыWRC-data-addrне получит ответ на первые инструкции. Это связано с тем, что во втором потокемежду инструкциями существует зависимость по данным, а в третьем — мнимая(fake) зависимость по адресу. Таким образом, эффект слабого сценария поведенияв ARMv8 POP должен быть получен за счёт подсистемы памяти.Для того, чтобы воспроизвести упомянутый результат, в рамках подсистемыFlowing нужно выбрать такую же топологию буферов, как и для слабого сценарияповедения программы ARM-weak, т.е. должен присутствовать буфер, общий дляпервого и второго потоков.76Поток 1Поток 2Поток 3p : [y] := 1o : b := [y]m : [x] := 1k : [x] := 0; l : [y] := 0и)ж)Поток 1Поток 2Поток 3o : b := [y]m : [x] := 1k : [x] := 0; p : [y] := 1к)Поток 1Поток 2Поток 3m : [x] := 1o : b := [y]k : [x] := 0; p : [y] := 1м)Evt = {k, l, m, o, p}Ord = {(k, m), (l, o), (l, p)}Prop(T 1) = {k, l, m}Prop(T 2) = {k, l, m, p}Prop(T 3) = {k, l, o}Evt = {k, l, m, o, p}Ord = {(k, m), (l, o),(l, p), (p, o)}Prop(T 1) = {k, l, m, p}Prop(T 2) = {k, l, m, p}Prop(T 3) = {k, l, o, p}л)Evt = {k, l, m, o, p}Ord = {(k, m), (l, o),(l, p), (p, o)}Prop(T 1) = {k, l, m, p, o}Prop(T 2) = {k, l, m, p, o}Prop(T 3) = {k, l, o, p}н)Рис.
22. Состояния подсистем Flowing и POP при исполнении программыWRC-data-addr (продолжение)77Пусть все три потока отправили по одному запросу в подсистему памяти.Соответствующие состояния Flowing и POP представлены на рис. 22а и 22б. Заметим, что для краткости мы помечаем запросы в Flowing буквенными идентификаторами и используем их в описании состояния POP.Когда поток T отправляет запрос e в подсистему памяти POP, во множествоOrd добавляется по ребру (e′ , e) для каждого запроса e′ , о котором поток T осведомлён (т.е. e′ ∈ Prop(T )) и который также не может быть переупорядочен с e(т.е. e′ ̸,→ e). Поэтому на рис. 22б отношение Ord не пусто — в нём присутствуют ребра, связывающие отправленные потоками запросы с инициализирующимизаписями в локации.Далее, подсистема памяти может перенести запрос m : [x] := 1 в буфер,общий для первого и второго потоков.
В терминах подсистемы POP это означает,что второй поток оказывается осведомлён об этом запросе (см. рис. 22в и 22г).Запрос m попадает во множество Prop(T 2), а в отношение Ord добавляется ребро(m, n).В общем случае, когда поток T ′ оказывается осведомлён о запросе e потокаT , т.е., в терминах Flowing, e попадает в видимый для T ′ буфер, или, в терминахPOP, e становится элементом Prop(T ′ ), то подсистема POP добавляет по ребру(e, e′ ) во множество Ord для каждого запроса e′ ∈ Prop(T ′ )\Prop(T ), если запросыне могут быть переупорядочены (т.е.
e ̸,→ e′ ) и между ними нет обратного ребра(e′ , e) в отношении Ord. В данном сценарии программы WRC-data-addr запросыm и n не переупорядочиваемы, т.к. они оперируют одной и той же локацией x,поэтому на рис. 22г между ними появляется Ord-ребро.Далее, запрос n попадает в буфер, общий для первого и второго потоков(подсистема Flowing, рис. 22д), что соответствует тому, что первый поток становится осведомлённым о запросе n (подсистема POP, рис.
22е). Теперь запросn : a := [x] непосредственно следует за запросом m : [x] := 1 в общем дляпервого и второго потоков буфере (подсистема Flowing), о запросах осведомленыодни и те же потоки, и между ними нет никакого запроса в отношении Ord (подсистема POP). Это означает, что и Flowing, и POP могут отправить ответ [n ← 1]на запрос n : a := [x]. После получения ответа второй поток отправляет запрос p : [y] := 1 в подсистему памяти (см. рис. 22ж и 22и).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
