Диссертация (1149932), страница 24

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 24)

dom(po; [e]) ∈ C. Для доказательства того, что w выпускаемо, требуетсяпоказать, что выполняются два следующих утверждения.: Пусть f ∈ F и po(f, w). Предположим, что f ̸∈ C. Тогда po(r, f ) и⟨rfe−1 (r), w⟩ ∈ obs; bob+ ⊆ eord. Т.к. rfe−1 (r) ̸∈ I, то существует eord-предшествующее w событие записи, которое не выпущено. Этопротиворечит выбору w.: Пусть существует событие чтения r′ такое, что dob+ (r′ , w). Еслиrfe−1 (r′ ) ̸= ⊥, то ⟨rfe−1 (r′ ), w⟩ ∈ rfe; dob+ ⊆ obs; dob+ ⊆ eord.По определению w это означает, что rfe−1 (r′ ) ∈ I.4.4Аналоги фронтов для ARM-согласованного сценарияВведём вспомогательную функцию T : TimeMap = W → N, сопоставляющую событиям записи в ARM-согласованном сценарии G их порядковые номерав отношении mo так, чтобы выполнялось correct-tmap(G, T ):correct-tmap(G, T ) ≜ ∀w, w′ .(⟨w, w′ ⟩ ∈ mo ⇒ T (w) < T (w′ )) ∧(w ̸∈ codom(mo) ⇒ T (w) = 0).Данная функция, фактически, вводит метки времени на событиях записи G.Далее введём вспомогательные отношения sw (synchronized-with) и hb(happens-before):sw ≜ [F(sy)]; po; rf; po; [F(ld)]hb ≜ (sw ∪ po)+ .Здесь отношение sw представляет пути в графе, соответствующие передачеинформации о событиях записи с помощью ARM-аналогов высвобождающего(F(sy)) и приобретающего (F(ld)) барьеров памяти.

Отношение hb используетсядля определения отношений cur-rel, acq-rel и rel-rel:cur-rel ≜ rf? ; hb,acq-rel ≜ rf? ; hb; ([F(sy)]; po; rf; po)? ,rel-rel ≜ rf? ; hb; [F(sy)]; po.Эти отношения вместе с функцией T будут использованы в симуляции как ограничения для базового, приобретающего и высвобождающего фронтов потока вобещающей модели памяти.122Аналогичным образом отношение msg-rel ⊆ W × W представляет ограничение на фронт сообщения из обещающей модели:msg-rel ≜ rf? ; hb; [F(sy)]; po ∪ [W].Так, из отношения симуляции будет следовать, что если ⟨w, w′ ⟩ ∈ msg-rel и события w и w′ соответствуют сообщениям m и m′ в памяти обещающей модели, тоm.τ = T (w), m′ .τ = T (w′ ) и m′ .view(loc(w)) ⩾ m.τ.4.5Доказательство корректности компиляцииДля доказательства теоремы 5 введём отношение симуляции I между конфигурациями обхода ARM-согласованного сценария G (⟨C, I⟩) и состояниямиобещающей машины (⟨T S, M ⟩):I(C, I, T S, M ) ≜ Imem1 (C, I, T S, M ) ∧ Imem2 (C, I, M ) ∧Iview (C, T S) ∧ Iview-rel (T S) ∧ Istate (C, T S).Утверждение Imem1 (C, I, T S, M ) свидетельствует, что все выпущенные событияI имеют аналоги в памяти обещающей машины, причём выполненные обещаниясоответствуют покрытым событиям записи:Imem1 (C, I, T S, M ) ≜ ∀w ∈ I.

∃view ⩽ dom-view(msg-rel; [w]).let msg ≜ ⟨loc(w) : valw (w)@T (w),view⟩ inlet promises ≜ T S(tid(w)).promises in(w ∈ C ⇒ msg ∈ M \ promises) ∧ (w ̸∈ C ⇒ msg ∈ promises).Здесь dom-view является вспомогательной функцией, которая по множеству записей строит соответствующий фронт:set-view(S) ≜ λℓ. max{T (w) | w ∈ S, loc(w) = ℓ}.dom-view(R) ≜ set-view(dom(R)).Утверждение Imem2 (C, I, M ) обозначает обратное — что для каждого сообщения из M существует соответствующее ему выпущенное событие в I:Imem2 (C, I, M ) ≜ ∀⟨ℓ : v@τ,view⟩ ∈ M. τ ̸= 0 ⇒ ∃w ∈ I.ℓ = loc(w) ∧ v = valw (w) ∧ τ = T (w) ∧ view ⩽ dom-view(msg-rel; [w]).Iview (C, T S) утверждает, что для любого элемента множества следующих событий Next(G, C) фронты, представляющие связанные с ним отношениями cur-rel,123acq-rel и rel-rel события записи, больше, чем базовый, приобретающий и высвобождающие фронты соответствующего потока:Iview (C, T S) ≜ ∀e ∈ Next(G, C).let ⟨cur, acq, rel⟩ ≜ T S(tid(e)).V incur ⩽ dom-view(cur-rel; [e]) ∧acq ⩽ dom-view(acq-rel; [e]) ∧rel ⩽ dom-view(rel-rel; [e]).Iview-rel (T S) показывает, что все обещания, которые ещё не выполнены, имеютспециальную форму фронтов, а именно, состоят из значения высвобождающегофронта соответствующего потока и метки времени самого обещания:Iview-rel (T S) ≜ ∀tid, ⟨ℓ : _@τ,view⟩ ∈ T S(tid).promises.view = [ℓ@τ] ⊔ T S(tid).V.rel.Istate (C, T S) утверждает, что для каждого потока tid существует список переходов{ti }i∈[1..k] , который соответствует событиям в tid-подграфе сценария G, и текущеесостояние потока T S(tid).σ получено с помощью p переходов из списка, где p —это количество покрытых событий |Etid ∩ C|:Istate (C, T S) ≜ ∀tid, k = |Etid |.

∃{σi }i∈[0..k] , {ti }i∈[1..k] .let p ≜ |Etid ∩ C| inεtj→∗ −→ σj+1 ) ∧T S(tid).σ = σp ∧ (∀j ∈ [0..k − 1]. σj −∀n ∈ [1..k], a ∈ nth ([Etid ]; po; [Etid ]) (n − 1). tn+1 ≈ lab(a).Здесь функция nth, вызванная с аргументами porder и n, возвращает элементы сномером n из отношения частичного порядка porder, a предикат t ≈ lab(a) является истинным тогда и только тогда, когда метка перехода t соответствует меткесобытия a. Формальные определения nth и ≈ приведены в приложении Г.3.С помощью отношения симуляции показывается, что обещающая машинаможет сделать шаг, повторяющий шаг обхода ARM-согласованного исполнения:Лемма 11. Пусть для некоторых конфигураций обхода ⟨C, I⟩ и ⟨C ′ , I ′ ⟩ ARMсогласованного сценария G, а также некоторого состояния обещающей машины⟨T S, M ⟩ выполняется G ⊢ ⟨C, I⟩ →TC ⟨C ′ , I ′ ⟩ и I(C, I, T S, M ). Тогда существуют такие T S ′ и M ′ , что ⟨T S, M ⟩ −−−−→+ ⟨T S ′ , M ′ ⟩ и I(C ′ , I ′ , T S ′ , M ′ ).PromiseДоказательство леммы 11 приведено в приложении Д.124Основной результат данной главы, теорема 5 о корректности компиляциииз обещающей модели в модель ARMv8.3, доказывается с использованием приведённой леммы.Теорема 5.

Для любой программы P rog, результата её компиляции P rogARM иARM-согласованного сценария поведения G программы P rogARM существует такой сценарий поведения обещающей машины, что финальное состояние памятимашины совпадает с состоянием памяти G.Доказательство. Зафиксируем ARM-согласованный сценарий G. Покажем, чтообещающая модель может симулировать обход сценария G, т.е. существуют такие T S и M , что I(G.E, G.W, T S, M ) и ⟨T S init , Minit ⟩ −−−−→∗ ⟨T S, M ⟩. Для этогоPromiseпроведём индукцию по полному обходу сценария G, существование которого следует из теоремы 6. Базой индукции в данном случае является то, что начальнаяконфигурация обхода сценария G связана отношением I с начальным состояниемобещающей машины, т.е.

I(G.E0 , G.E0 , T S init , Minit ) выполняется. Это утверждение очевидным образом следует из определения I. Индукционным переходом вданном случае является лемма 11. Из истинности I(G.E, G.W, T S, M ) следует, чтофинальное состояние памяти машины M совпадает с состоянием памяти G.4.6ВыводыВ этой главе приведено доказательство корректности компиляции для подмножества обещающей модели памяти [11] в модель памяти ARMv8.3 [10]. Рассмотренное подмножество состоит из ослабленных операций чтения и записи,приобретающих и высвобождающих барьеров памяти.Доказательство базируется на новой идее обхода аксиоматических сценариев поведения, который может быть симулирован обещающей машиной. Данная идея может быть использована для доказательств корректности компиляциив другие модели памяти, что ценно, т.к.

подобные задачи регулярно появляютсяввиду бурного развития области. В дальнейшие планы входит расширение доказательства до полной обещающей модели памяти. Для этого нужно будет поддержать операции приобретающего чтения (read acquire) и высвобождающей записи(write release), атомарные инструкции чтения и записи (read-modify-write), частным случаем которых является сравнение с обменом (compare-and-set), а такжеполные барьеры памяти (SC fences). Поддержка данных инструкций потребуетнебольшого усложнения обхода ARM-согласованных исполнений, а также суще-125ственного усложнения отношения симуляции ввиду большого количества деталей, связанных с упомянутыми инструкциями в рамках обещающей модели памяти.126ЗаключениеОсновные результаты работы заключаются в следующем.1. Разработана операционная модель памяти C/C++11. Данная модель допускает такие же сценарии поведения, что и модель C/С++11 на большинстве тестов, приведенных в литературе, но не обладает сценариямиповедения со “значениями из воздуха”.

В отличие от обещающей модели, предлагаемая модель является запускаемой, что упрощает разработкусредств анализа программ для неё. Недостатком модели является то, онанакладывает синтаксические ограничения на поведения программ.2. Доказана корректность компиляции из существенного подмножестваобещающей модели в операционную модель памяти ARMv8 POP.3.

Доказана корректность компиляции из существенного подмножестваобещающей модели в аксиоматическую модель памяти ARMv8.3.В рамках рекомендации по применению результатов работы в индустрии и научных исследованиях указывается, что модель памяти промышленного языка программирования должна быть лишена сценариев поведения, имеющих“значения из воздуха”, а также либо быть представленной в операционной форме,либо иметь эквивалентный операционный аналог.

Последнее позволяет реализовать интерпретатор модели и выполнять отладку программ в рамках модели.Также были определены перспективы дальнейшей разработки тематики, основным из которых является разработка обобщенной аксиоматической модели памяти для процессорных архитектур, которая будет определена для синтаксиса модели C/C++11 и окажется строгим надмножеством существующих моделей памяти x86, Power и ARM, а также для которой будет применим предложенный метод доказательства корректности компиляции из обещающей модели памяти.

Характеристики

Список файлов диссертации