Диссертация (1149932), страница 16
Текст из файла (страница 16)
Соответственно, нам надо показать,что для любой программы в синтаксисе модели ARMv8 POP и её произвольногосценария поведения в модели ARMv8 POP существует сценарий поведения этойпрограммы с тем же результатом в обещающей модели.До этого момента в рассмотренных примерах под результатом сценария мыпонимали значение локальных переменных после исполнения программы. Тем неменее, для формального определения корректности компиляции между обещающей и ARMv8 POP моделей под результатом сценария удобнее понимать финальное состояние памяти — функцию, которая по локации возвращает значение еёпоследней записи. Так, в случае модели ARMv8 POP под последней записью влокацию ℓ понимается запрос [ℓ] := v, попавший последним в основную память, а в случае обещающей модели — сообщение ⟨ℓ : v@τ,view⟩, где τ являетсямаксимумом среди всех остальных сообщений в ℓ.Также отметим, что далее будут рассматриваться только конечные сценарии поведения в рамках модели ARMv8 POP, т.к. для рассмотрения не завершающихся сценариев пришлось бы ввести ограничения на спекулятивное исполнениепрограмм, которого в модели нет.
Так, следующая программа в модели ARMv8POP имеет сценарий поведения, в котором соответствующий поток бесконечнопосылает запросы на чтение и не получает на них ответы:a := [x];if a ̸= 0 goto −1Здесь инструкция if cond goto shif t имеет следующую семантику: если выражение cond вычисляется к истинному (не нулевому) значению, то к указателю инструкций потока прибавляется значение shif t, иначе — прибавляется единица,т.е.
управление переходит к следующей инструкции.Центральная теорема данной главы, которая утверждает корректность компиляции, формулируется следующим образом:83Теорема 1. Для любой программы Prog и её сценария поведения в модели ARMv8POP, Prog ⊢ sinit −−−→∗ s, где s — финальное состояние, FinalARM (s, Prog), суARMществует сценарий поведения этой программы в обещающей модели, Prog ⊢pinit −−−−→∗ p, где p — финальное состояние FinalPromise (p, Prog); при этом соPromiseстояния памяти в s и p совпадают, same-memory(s, p).Стандартной техникой для доказательства таких утверждений является симуляция [14, 15, 108].
Для этого определяется отношение симуляции, связывающее состояния соответствующих абстрактных машин, и показывается, что еслитекущие состояния машин связаны этим отношением, и симулируемая машина (внашем случае это ARM-машина) делает шаг, то симулирующая машина (в нашемслучае это обещающая машина) может сделать ноль и более шагов так, чтобы новые состояния машин были также связаны отношением симуляции.В доказательстве автор диссертации также использовал технику симуляции,однако не напрямую. Это связано со следующими особенностями нашего случая.1.
В каждый момент исполнения в обещающей машине имеется тотальныйпорядок на сообщениях в конкретную локацию — метки времени. В тоже время в модели ARMv8 POP тотальный порядок на запросах записив локацию может быть гарантированно определён только в конце исполнения.2. В модели ARMv8 POP тот факт, что запрос чтения был удовлетворёниз конкретного запроса записи, накладывает ограничения на дальнейшееисполнение, однако эти ограничения не определяются явно, как это делается с помощью фронтов в обещающей модели.3. ARM-машина может исполнять разные типы инструкций не по порядку,в частности, инструкции записи и инструкции чтения, тогда как обещающая машина — только инструкции записи (механизм обещаний).Отношение симуляции обычно предоставляет достаточно сильную связьмежду компонентами машин.
Так, в нашем случае естественно было бы ожидать,что это отношение связывает каждое конкретное сообщение в памяти обещающей машины с некоторым запросом записи в подсистеме памяти ARM-машины.Тем не менее, первые две особенности, упомянутые выше, не позволяют этогосделать. Чтобы преодолеть данное ограничение, автор диссертационного исследования вводит промежуточную машину ARM+τ. Она является версией ARMмашины, в которой каждый запрос записи w, попавший в подсистему памяти, до-84полнительно помечен следующей информацией: (i) меткой времени; (ii) множеством запросов записи и барьеров памяти S, о которых гарантированно становится осведомлён поток, прочитавший из запроса w; (iii) фронтом, представляющиммножество S. При этом метка времени запроса w отражает то, в каком порядкеотносительно других запросов записи в ту же локацию запрос w попадёт в основную память машины.
Тем не менее, в тот момент, когда запрос записи попадает вподсистему памяти, обычная ARM-машина не может гарантировать никакого конкретного места в этом порядке для запроса. Для решения этой проблемы в правилах переходов машины ARM+τ введены дополнительные ограничения, которыегарантируют ацикличность объединения частичного порядка Ord и порядка, полученного с помощью меток времени.
Наличие данных ограничений означает, чтомашина ARM+τ потенциально имеет меньше сценариев поведения, чем изначальная машина. Следовательно, для того, чтобы использовать ARM+τ как промежуточную машину в доказательстве корректности компиляции, нам нужно доказать,что ARM+τ может симулировать ARMv8 POP, т.е. для каждой конкретной программы ARM+τ имеет не меньший набор сценариев поведения, чем ARMv8 POP(теорема 3, раздел 3.6.4).Из-за третьей особенности мы не можем ввести непосредственное соотношение между шагами ARMv8 POP и обещающей машин.
Так, рассмотрим следующую программу:[x] := 1;fence(ld);a := [y];[z] := 1ARM-машина может исполнить её следующим образом. Сначала она выполняетбарьер памяти fence(ld) (шаг 1), этого отправляет запрос на чтение a := [y], накоторый приходит ответ (шаг 2), посылает запрос на запись [z] := 1 (шаг 3), ипосле этого — запрос [x] := 1 (шаг 4). Обещающая машина не может исполнитьэту программу в том же порядке, поэтому ей позволяется запаздывать (lag) относительно ARM-машины при симуляции. Так, пока ARM-машина делает первыйи второй шаги, обещающая машина запаздывает и не делает ничего.
На третийшаг ARM-машины обещающая машина отвечает обещанием записать сообщение⟨z : 1@_,_⟩. На четвертый шаг обещающая машина отвечает серией шагов: (i)обещает записать сообщение ⟨x : 1@_,_⟩, (ii) выполняет это обещание, (iii) ис-85cmdsS: List S::= reg := [expr]| [expr0 ] := expr1| fence(fmodARM )| if expr goto k| reg := expr | nopfmodARM ::= sy | ldexpr::= reg | ℓ | uop expr| bop expr0 expr1:ereg : Reg − a, b, c, ... (локальные переменные)ℓ : Loc − x, y, z, ... (локации)uop, bop − арифметические операцииk∈ZРис.
23. Синтаксис программ в модели ARMv8 POPполняет приобретающий барьер (поскольку fence(ld) является результатом егокомпиляции), (iv) выполняет инструкцию чтения и (v) обещание ⟨z : 1@_,_⟩.Для выражения запаздывания используется два отношения симуляции, I иIpre . Первое отношение не позволяет обещающей машине запаздывать слишкомсильно: если состояния машин связаны посредством I, то в каждом потоке обещающая машина полностью выполнила префикс программы, который выполненARM-машиной, и ожидает, пока ARM-машина исполнит следующую инструкцию. Второе отношение сигнализирует, что существует единственный поток, вкотором обещающая машина может и должна “догнать” ARM-машину.
Для этихотношений доказывается, что если состояния машин связаны отношением Ipre , тосуществует конечная последовательность шагов обещающей машины, после выполнения которой состояния машин связаны отношением I.3.4Формальное определение модели ARMv8 POPВ этом разделе приводится формализация модели ARMv8 POP, сделаннаядиссертантом, поскольку в [9] модель описана лишь словесно. Синтаксис программ, на которых определена модель, приведён на рис. 23.
Программа представ-86c : If none (−2)a : W (com true x 1)b : If none 7d : Assigne : R (requested z)f : Nopg : R (sat pln ⟨5tid , [0,1], wr y : 6⟩)Рис. 24. Состояния подсистемы управления потока в модели ARMv8 POPляется как функция Prog : Tid → List S, которая по идентификатору потока возвращает список его инструкций. Инструкции бывают следующих типов: чтение(reg := [expr]), запись ([expr0 ] := expr1 ), барьер памяти (fence(fmodARM )), условный переход (if expr goto k), присваивание в локальную переменную (reg :=expr), пустая операция (nop).В этом языке опосредованно, через условные переходы назад, присутствуют циклы, поэтому каждая инструкция может быть исполнена несколько раз и вразных контекстах.
Различные исполнения инструкции мы будем называть экземплярами инструкций (instruction instances) или просто экземплярами. Подсистемауправления ARM-машины может исполнять экземпляры не по порядку и спекулятивно. Более того, исполнение экземпляра происходит за несколько шагов, которые могут быть разделены во времени. Как следствие, в каждый конкретныймомент времени поток может находится в состоянии исполнения многих экземпляров.Аналогично модели памяти Power [33], в представленной формализации используется граф типа дерево для описания состояния подсистемы управления.Пример такого графа приведён на рис.
24. Вершины дерева помечены состояниемэкземпляров инструкций. Ребра дерева выражают программный порядок междуэкземплярами, где вершины с двумя исходящими ребрами представляют условные переходы, условие которых ещё не вычислено.Каждый экземпляр инструкции идентифицируется парой (tid,path), гдеtid — это идентификатор потока, а path : P ath ≜ List N — путь в дереве подсистемы управления от его корня до экземпляра. Этот путь представлен как список позиций инструкций, соответствующих предшествующим экземплярам. Так,путь экземпляра a на рис. 24 — это список [0], путь экземпляра b — [0,1], а путьэкземпляра f — [0,1,8,9].Граф состояния подсистемы управления представлен в виде т.н. плёнкиtape : Tape ≜ P ath ⇀ TapeCell — частичной функции, которая для пути экземпляра возвращает его состояние. Корректная плёнка является префикс-замкнутой:87tapecell ::= R stread | W stwrite| F stfence fmodARM| If stifgoto k | Assign | Nop: TapeCellsat-state ::= pln | inflight | comstread::= none | requested ℓ| sat sat-state ⟨tid, path, wr ℓ : val⟩stwrite::= none| pending ℓ val| com bool ℓ valstfence::= none | comstifgoto ::= none | taken | ignoredval : Val = Loc ∪ ZРис.
25. Язык состояния исполнения инструкций в ARMv8 POPесли она определена для некоторого пути, то она определена и для префикса этогопути.Состояние экземпляра представляется с помощью ячейки плёнки tapecell :TapeCell (см. рис. 25). Её синтаксис симметричен синтаксису инструкций. Рассмотрим возможные состояния экземпляра в зависимости от его типа.Экземпляр инструкции чтения stread может находиться в одном из трёх состояний: (i) none — экземпляр только загружен или его исполнение перезапущено; (ii) requested ℓ — экземпляр отправил запрос в подсистему памяти; (iii)sat sat-state ⟨tid, path, wr ℓ : val⟩ — экземпляра получил ответ от экземпляразаписи (tid, path) со значением val.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
