Диссертация (1149932), страница 15
Текст из файла (страница 15)
Далее, подсистемапамяти отправляет запрос p : [y] := 1 в общий буфер и в основную память (см.рис. 22к, подсистема Flowing), и после этого первый и третий потоки оказываютсяосведомлёнными о нём (см. рис. 22л, подсистема POP). Заметим, что поскольку в78подсистеме POP нет фиксированной топологии буферов, подсистема может осведомить первый поток о запросе p, а потом — третий поток, или наоборот.Теперь запрос o : b := [y] может попасть в общий для всех потоков буфер(см. рис. 22м и 22н) и затем в память, что приведёт к отправке ответа [b ← 1] нанего.
После этого третий поток посылает запрос c := [x]. Этот запрос, попавв основную память, получает ответ [c ← 0]. В конце сценария поведения запросm : [x] := 1 попадает в память. Итак, мы получили результат [a = 1, b = 1, c = 0].В конце исполнения программы в модели ARMv8 POP с подсистемой POPвсе выпущенные запросы записи и барьеров памяти попадают в основную память, и, соответственно, все потоки оказываются осведомлены о них. Следовательно, все записи в одну локацию тотально упорядочиваются отношением Ord.В рамках описанного ниже доказательства корректности компиляции этот порядок используется для введения меток времени на запросах записи в подсистемепамяти.В доказательстве корректности компиляции используется именно подсистема POP, поскольку в [9] доказано, что подсистема POP допускает все сценарииповедения, возможные с подсистемой Flowing, и кроме того является более абстрактной.3.2.3Обещающая модельКак уже было отмечено в этой главе, обещающая модель памяти, аналогично OpC11 MM, использует метки времени, базовые фронты и фронты сообщений.
Так, слабый сценарий поведения программы MP, имеющий результат[a = 1, b = 0], имеет абсолютно ту же структуру в обещающей модели, что и вOpC11 MM. Кратко проиллюстрируем его.[x] := 0; [y] := 0;[x] := 1; a := [y]; //1[y] := 1 b := [x] //0(MP)После исполнения инициализирующих записей и старта потоков память и базовые фронты потоков имеют следующие значения:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0, [y@0]⟩};T 1.viewcur = [x@0, y@0]; T 2.viewcur = [x@0, y@0].79После того, как левый поток выполнил обе записи, в памяти появляются два новыхсообщения, и базовый фронт первого потока обновляется:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0, [x@0]⟩,⟨x : 1@1, [x@1, y@0]⟩, ⟨y : 1@1, [x@0, y@1]⟩};T 1.viewcur = [x@ 1 , y@ 1 ]; T 2.viewcur = [x@0, y@0].Теперь второй поток может прочитать новое сообщение ⟨y : 1@1, [x@0, y@1]⟩ истарое сообщение ⟨x : 1@1, [x@1, y@0]⟩, что приводит к результату [a = 1, b = 0].Рассмотрим, как слабый сценарий поведения с результатом [a = 1, b = 0]программы MP-SY-LD запрещается в обещающей модели:[x] := 0; [y] := 0;[x] := 1;a := [y]; //1fence(sy); fence(ld);[y] := 1b := [x] //0(MP-SY-LD)В рассматриваемой нами схеме компиляции барьеры fence(sy) и fence(ld) являются результатами компиляции высвобождающего и приобретающего барьеров соответственно.
Для их поддержки в обещающей модели используются высвобождающий (viewrel ) и приобретающий (viewacq ) фронты потоков. Последнийаналогичен приобретающему фронту в OpC11 MM.После выполнения инициализирующих записей и старта потоков конфигурация абстрактной машины, реализующей обещающую модель (т.н. обещающеймашины), выглядит следующим образом:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0, [y@0]⟩};T 1.viewcur = [x@0, y@0]; T 1.viewacq = [x@0, y@0]; T 1.viewrel = [x@0, y@0];T 2.viewcur = [x@0, y@0]; T 2.viewacq = [x@0, y@0]; T 2.viewrel = [x@0, y@0].После того, как первый поток выполнил запись [x] := 1, в память добавляется новое сообщение, а базовый и приобретающий фронты потока обновляютсясоответствующей меткой времени:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0, [y@0]⟩, ⟨x : 1@1, [x@1, y@0]⟩};T 1.viewcur = [x@ 1 , y@0]; T 1.viewacq = [x@ 1 , y@0]; T 1.viewrel = [x@0, y@0];T 2.viewcur = [x@0, y@0]; T 2.viewacq = [x@0, y@0]; T 2.viewrel = [x@0, y@0].При этом фронтом сообщения становится высвобождающий фронт viewrel первогопотока, увеличенный на метку времени сообщения по целевой локации.80После того, как первый фронт выполняет высвобождающий барьер, который в программе представлен его скомпилированным вариантом fence(sy), высвобождающий фронт viewrel потока становится равен базовому фронту:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0, [y@0]⟩, ⟨x : 1@1, [x@1, y@0]⟩};T 1.viewcur = [x@1, y@0]; T 1.viewacq = [x@1, y@0]; T 1.viewrel = [x@ 1 , y@0];T 2.viewcur = [x@0, y@0]; T 2.viewacq = [x@0, y@0]; T 2.viewrel = [x@0, y@0].После этого первый поток выполняет вторую запись по тем же правилам, что ипервую:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0, [y@0]⟩,⟨x : 1@1, [x@1, y@0]⟩, ⟨y : 1@1, [x@1, y@1]⟩};T 1.viewcur = [x@1, y@ 1 ]; T 1.viewacq = [x@1, y@ 1 ]; T 1.viewrel = [x@1, y@0];T 2.viewcur = [x@0, y@0]; T 2.viewacq = [x@0, y@0]; T 2.viewrel = [x@0, y@0].Теперь второй поток может выполнить чтение из добавленного сообщения, получая a = 1.
При этом базовый фронт потока viewcur обновляется на [y@1], а приобретающий viewacq — на фронт сообщения, [x@1, y@1], как это было в OpC11MM:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0, [y@0]⟩,⟨x : 1@1, [x@1, y@0]⟩, ⟨y : 1@1, [x@1, y@1]⟩};T 1.viewcur = [x@1, y@1]; T 1.viewacq = [x@1, y@1]; T 1.viewrel = [x@1, y@0];T 2.viewcur = [x@0, y@0]; T 2.viewacq = [x@ 1 , y@ 1 ]; T 2.viewrel = [x@0, y@0].После выполнения приобретающего барьера, который в программе представленего скомпилированным вариантом fence(ld), базовый фронт viewcur второго потока становится равным приобретающему фронту viewacq :M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0, [y@0]⟩,⟨x : 1@1, [x@1, y@0]⟩, ⟨y : 1@1, [x@1, y@1]⟩};T 1.viewcur = [x@1, y@1]; T 1.viewacq = [x@1, y@1]; T 1.viewrel = [x@1, y@0];T 2.viewcur = [x@ 1 , y@ 1 ] T 2.viewacq = [x@1, y@1]; T 2.viewrel = [x@0, y@0].Теперь второй поток не может прочитать старое сообщение ⟨x : 0@0, [x@0]⟩, т.к.T 2.viewcur (x) = 1 > 0.
Таким образом, результат [a = 1, b = 0] запрещается.81Перейдем к рассмотрению слабого сценария поведения программыARM-weak с результатом [a = 1, b = 1, c = 1] в обещающей модели3 .[x] := 0; [y] := 0;a := [x]; //1 b := [x]; c := [y];[x] := 1[y] := b [x] := c(ARM-weak)Для того, чтобы получить интересующий нас результат, обещающая модель, в соответствии со своим названием, использует механизм обещаний. Так,в любой момент исполнения поток может сделать одно из двух следующих действий: либо выполнить следующую инструкцию, либо пообещать сделать некоторую запись в будущем.
Когда поток T обещает сделать запись, он добавляет впамять машины сообщение ⟨ℓ : val@τ,view⟩, где τ — уникальная метка временилокации ℓ, которая больше, чем T.viewcur (τ). После этого сообщение становитсядоступным для чтения другими потоками по обычным правилам, но сам потокT не может читать из этого сообщения, пока не выполнит обещание. Для того,чтобы проверять данное условие, у каждого потока имеется множество обещанных, но ещё не выполненных сообщений T.promises. После каждого перехода вобещающей машине поток, совершивший данный переход, должен пройти сертификацию, т.е. показать, что может выполнить все свои обещания в текущемсостоянии памяти, будучи запущенным в изоляции. Процесс сертификации позволяет решить проблему “значений из воздуха”.Результат [a = 1, b = 1, c = 1] для программы ARM-weak в обещающей машине получается следующим образом.
После выполнения инициализирующих записей и старта дочерних потоков первый поток обещает сообщение⟨x : 1@2,[x@2,y@0]⟩4 . После этого второй поток прочитывает данное сообщение,получая b = 1, и выполняет запись, добавляя сообщение ⟨y : 1@1,[x@0,y@1]⟩ впамять. Далее, третий поток прочитывает добавленное сообщение, получая c = 1,и добавляет в память сообщение ⟨x : 1@1,[x@1,y@0]⟩. Первый поток прочитывает это сообщение, получая a = 1, и после этого выполняет данное ранее обещание⟨x : 1@2,[x@2,y@0]⟩, исполняя инструкцию записи [x] := 1.3 Стоитотметить, что такой результат для программы ARM-weak невозможен в OpC11 MM, но возможен в C/C++11 MM.4 Отметим ещё одно отличие обещающей модели и OpC11 MM. В OpC11 MM метки времени являютсянатуральными числами, и когда поток делает запись сообщения, метка времени сообщения равна увеличенной на единицу максимальной метке по соответствующей локации.
В обещающей модели метки временипредставлены положительными вещественными числами, и при добавлении нового сообщения его меткавремени может быть произвольной с точностью до базового фронта соответствующего потока.823.3Основные идеи доказательства корректности компиляцииВ разделе 1.2.2 было представлено следующее определение понятия корректности компиляции: все результаты, возможные для скомпилированной программы в целевой модели памяти, должны быть также возможны и для изначальной программы в исходной модели памяти. Поскольку рассматриваемая в этойглаве схема компиляции является биекцией, мы можем считать, что изначальнаяи скомпилированная программы совпадают.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
