Диссертация (1149932), страница 22
Текст из файла (страница 22)
Prog ⊢ p −−−−−−−→ p′ ∧ (a′ , p′ ) ∈ Ipre ∪ I).Доказательство леммы 7 приведено в приложении В.Основная лемма симуляции непосредственно следует из лемм 5, 6 и 7.Лемма 8. Пусть состояние ARM+τ-машины a и обещающей машины p связаныотношением I, а состояние a′ достижимо за один шаг из a. Тогда существует такоесостояние p′ , достижимое из p, что a′ и p′ также связаны отношением I.∀(a, p) ∈ I, a′ . a −−−−→ a′ ⇒ ∃p′ .
Prog ⊢ p −−−−→∗ p′ ∧ (a′ , p′ ) ∈ I.ARM +τPromiseВернёмся к доказательству теоремы 1. Она доказывается индукцией подлине сценария поведения с помощью леммы 8. Часть утверждения теоремы отом, что конечные состояния памяти совпадают, напрямую следует из отношений Imem1 и Imem2 . Единственное, что осталось доказать, что состояние p являетсяфинальным состоянием обещающей машины (FinalPromise (p, Prog)).Обещающая машина не может сделать нового перехода, т.к. это бы означало, что машина ARM+τ может загрузить новый экземпляр инструкции, аэто противоречило бы FinalARM +τ (a, Prog). Кроме того, все сообщения из состояния p были обещаны и выполнены, потому что выполняется Imem1 (a,p) иImem2 (a, p).1113.8ВыводыВ главе представлено доказательство корректности компиляции из обещающей модели памяти в модель памяти ARMv8 POP.
Это доказательство являетсяважным аргументом в пользу использования обещающей модели как замены существующих моделей памяти промышленных языков программирования. Самодоказательство представляет научный интерес, т.к. использованные ранее схемыдоказательства для случая моделей x86 и Power не применимы к ARMv8 POP.В доказательстве рассмотрено подмножество обещающей модели памяти,в которое входят расслабленные обращения к памяти и высвобождающие и приобретающие барьеры. Тем не менее, доказательство может быть расширено и длядругих конструкций обещающей модели.112Глава 4. Корректность компиляции из обещающеймодели в аксиоматическую модель ARMv8.3В этой главе описывается доказательство корректности эффективной схемыкомпиляции из подмножества обещающей модели памяти [11] в аксиоматическуюмодель памяти ARMv8.3 POP [10].
Рассмотренное подмножество обещающей модели состоит из расслабленных обращений к памяти, высвобождающего и приобретающего барьеров памяти без сертификации.Как было описано в разделе 3.1, доказательство корректности компиляциииз обещающей модели памяти является важной задачей. В главе 3 было рассмотрено доказательство для модели ARMv8 POP [9], однако задача для архитектурыARM оказалась не полностью закрыта — в апреле 2017 года была предложенановая модель памяти ARMv8.3 [10, 109] и потребовалось новое доказательство.Также как и в случае с моделью ARMv8 POP, схема доказательства корректности компиляции, использованная в [11] для моделей x86 и Power, не подходит длямодели ARMv8.3.
Дело в том, что для использования этой схемы нужно, чтобымодель была представлена в виде оптимизаций над более строгой моделью, и всерезультаты сценариев поведения в этой более строгой модели должны быть получены также и в обещающей модели, при этом механизм обещаний не долженбыть использован. Данное утверждение для модели ARMv8.3 не является истинным. Чтобы убедиться в этом, рассмотрим такую программу:a := [x]; //1if a = 1 thenb := [y] //0[y] := 1;fence(sy);[x] := 1Между инструкциями чтения в левом потоке имеется зависимость по управлению, а в правом потоке находится барьер памяти, запрещающий неупорядоченное исполнение записей. В рамках модели памяти ARMv8.3 возможен сценарийпрограммы с результатом a = 1 и b = 0. Следует отметить, что в обоих потокахинструкции не могут быть переставлены.
Модель ARMv8.3 является аксиоматической, и это существенно отличает ее от модели ARMv8 POP [9]. Следовательно, невозможно простым способом задать симуляцию модели ARMv8.3 обещающей моделью. Преодолевая это ограничение, автор диссертационного исследования разработал специальный способ обхода графа модели ARMv8.3 (раздел 4.3),113bob+W(x,1)R(y,1)F(sy)rbeF(ld)rfeW(y,1)R(x,0)bob+Рис.
29. Сценарий поведения программы MP-sy-ld, запрещённый в моделиARMv8.3представленный в виде операционной семантики. Этот обход используется придоказательстве симуляции (раздел 4.5).4.1Модель ARMv8.3Модель ARMv8.3 [10] является аксиоматической и представляет семантикупрограммы в виде набора графов, где каждый граф соответствует определённому запуску программы. Как и в модели C/C++11 [4] она использует отношенияpo, “читает из” rf, порядка памяти mo.
Кроме того, используется производноеотношение “читает ранее” rb (reads before):rb ≜ rf−1 ; mo,связывающее событие чтения a с событием записи b, которое mo-следует за записью, из которой читает a. Композиция отношений ‘;’ задаётся следующим образом:A; B ≜ {⟨a, b⟩ | ∃c. ⟨a, c⟩ ∈ A ∧ ⟨c, b⟩ ∈ B}.Добавление в программу MP барьеров памяти, как и в случае с моделью ARMv8POP, делает невозможным результат [a = 1, b = 0] (см.
рис. 29):[x] := 1;fence(sy);[y] := 1;a := [y]; //1fence(ld);b := [x]; //0(MP-sy-ld)В данном графе опущены инициализирующие записи и добавлено отношение барьеров bob (barrier-ordered-before), которое задаётся так:bob ≜ po; [F(sy)] ∪ [F(sy)]; po ∪ [R]; po; [F(ld)] ∪ [F(ld)]; po,114где [A] ≜ {(a, a) | a ∈ A}. Также в графе заменены ребра отношений rf и rb наrfe и rbe, где e (external) означает, что отношение связывает только события,принадлежащие разным потокам. В представленном графе имеется цикл: bob,rfe, rbe, и это противоречит одной из аксиом, используемой в модели ARMv8.3для задания ARM-согласованного сценария поведения.
Следовательно, данныйграф не является ARM-согласованным, и результат [a = 1, b = 0] запрещен дляпрограммы MP-sy-ld. Ниже представлено формальное определение сценария поведения в модели ARMv8.3 [10].Определение 5. Сценарий поведения G является графом, включающий следующие компоненты.1.
Конечное множество событий E ⊆ N, которое включает начальные события E0 = {ax0 | x ∈ Loc}. Для обозначения событий используютсясимволы a,b, ...2. Функция tid, возвращающая по событию из E номер потока, создавшегоэто событие; любое начальное событие считается относящимся к потокус номером 0, tid(ax0 ) = 0.3. Функция lab, присваивающая каждому событию из E метку; метки могут обозначать следующие операции:– чтение, R(x,v), где x ∈ Loc — это локация, из которой событиечитает значение v ∈ Val;– запись, W(x,v), где x ∈ Loc — это локация, в которую событиезаписывает значение v ∈ Val;– барьер памяти, F(o), где o ∈ {ld,sy} — это тип барьера, причём sy-барьеры более строгие, чем ld, ld ⊏ sy.Каждое начальное событие является инициализирующей записью вопределённую локацию:∀ax0 ∈ E0 .
lab(ax0 ) = W(x,0).Функция lab определяет следующие частичные функции, которые пособытию возвращают:– typ — тип события (R,W или F);– mod — тип барьера;– loc — целевую локацию;– valr — прочитанное значение;1154.5.6.7.– valw — записанное значение.Далее мы будем использовать символы R, W и F в том числе и для обозначения соответствующих множеств событий, например, R — для обозначения множества {e ∈ E | typ(e) = R}.Строгий частичный порядок на событиях po ⊆ E × E, называемый программным порядком; он является объединением непересекающихся множеств {poi }i∈{0}∪Tid , где po0 = E0 × (E \ E0 ), и для каждого потока i ∈ Tidотношение poi является полным порядком на множестве его событий{a ∈ E | tid(a) = i}.Отношения data,ctrl,addr ⊆ po\po0 , удовлетворяющие следующимограничениям:– data ⊆ R × W;– addr ⊆ R × (R ∪ W);– ctrl; po ⊆ ctrl.Они позволяют задавать зависимости по данным, по потоку управленияи по целевому адресу инструкции соответственно.Отношение rf ⊆ [W]; =loc ; [R], удовлетворяющее следующим ограничениям: (i) valw (a) = valr (b) для любой пары ⟨a,b⟩ ∈ rf; (ii) a1 = a2 , если⟨a1 ,b⟩,⟨a2 ,b⟩ ∈ rf; также вводится функция rf−1 , которая определена наобласти отображения rf, codom(rf), и для любого a из codom(rf) верноследующее: ⟨rf−1 (a), a⟩ ∈ rf.Строгий частичный порядок mo на элементах W, являющийся объединением отношений {mox }x∈Loc , где mox — это полный порядок на элементах Wx = {e ∈ W | loc(e) = x}.С помощью суффиксов i и e обозначаются подмножества отношений, которыесвязывают события одного и разных потоков соответственно.
Например, moi ={⟨w, w′ ⟩ ∈ mo | tid(w) = tid(w′ )} и rfe = {⟨w, r⟩ ∈ rf | tid(w) ̸= tid(r)}.Определение 6. Сценарий поведения G является ARM-согласованным, если выполняются следующие условия:– R = codom(rf);()– отношение po|loc ∪ rb ∪ mo ∪ rf не имеет циклов;()– отношение obs ∪ dob ∪ bob не имеет циклов.()116В определении используются следующие производные отношения:obs ≜ rfe ∪ rbe ∪ moe(addr ∪ data); rfi? ∪dob ≜ (ctrl ∪ data); [W]; moi? ∪addr; po; [W]bob ≜4.2po; [F(sy)] ∪ [F(sy)]; po ∪[R]; po; [F(ld)] ∪ [F(ld)]; po(observed-by)(dependency-ordered-before)(barrier-ordered-before)Структура доказательства корректности компиляцииЦентральным результатом данной главы является следующая теорема.Теорема 5.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
