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

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

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

Поскольку ainit −−−→∗ a и tape(path) =ARMR (sat com w), то cmds(path.last) = ‘‘reg := [expr]”. Введём следующие обозначения:path′ℓvalst′≜≜≜≜next-path(path, 1);stJexprKpathcom = w.ℓ = JexprK ;w.val;st[reg 7→ val].Поскольку верно Iview-read-cert (δ, tid, a, t), то существуют τ и view такие, что(τ, view) = comb-time(δ, a, w.tid, w.path) и viewcur (ℓ) ⩽ τ.То, что ⟨ℓ : val@τ,view⟩ ∈ t.M \ t.promises, следует из (δ, tid, a, t) ∈Imem-1-com-cert ∩ Imem-1-com-cert .

Введём обозначение:V ′ = ⟨view′cur , view′acq , view′rel ⟩ ≜ ⟨viewcur ⊔ [ℓ@τ], viewacq ⊔ view, viewrel ⟩.Read from memory ⟨ℓ:val@τ,view⟩Тогда t −−−−−−−−−−−−−−−−−−→ t′ ≜ ⟨M, ⟨path′ , V ′ , promises⟩⟩.Promise tidТо, что выполняется Icert (n − 1, δ, k, a, t′ ), проверяется тривиальным образом.– tape(path) = R stread , где состояние stread указывает, что экземпляр не завершён. Аналогично предыдущему пункту, cmds(path.last) = ‘‘reg :=175[expr]”. Введём следующие обозначения:path′≜ next-path(path, 1);regfcom ≜ regfcom (cmds, tape, path);regf′com ≜ regfcom (cmds, tape, path′ )= regfcom (cmds, tape, path)[reg 7→ ⊥] (by definition);ℓ≜ JexprKpathcom= JexprKst (by Istate-cert (tid, a, t));τ≜ viewcur (ℓ).Из свойств обещающей машины следует, что существуют val и view такие,что ⟨ℓ : val@τ,view⟩ ∈ M.

Введём следующие обозначения:V ′ = ⟨view′cur , view′acq , view′rel ⟩ ≜ ⟨viewcur ⊔ [ℓ@τ], viewacq ⊔ view, viewrel ⟩= ⟨viewcur , viewacq ⊔ view, viewrel ⟩;st′≜ st[reg 7→ val].По определению, выполняется tRead from memory ⟨ℓ:val@τ,view⟩−−−−−−−−−−−−−−−−−−→Promise tidt′≜⟨M, ⟨path′ , st′ , V ′ , promises⟩⟩. Проверка Icert (n − 1, δ, k, a, t′ ) также тривиальна.– tape(path) = W (com im ℓ val). Аналогично предыдущим пунктам,cmds(path.last) = ‘‘[expr0 ] := expr1 ”. Введём следующие обозначения:path′≜ next-path(path, 1);regfcom≜ regfcom (cmds, tape, path);⟨τ, _, view′ ⟩ ≜ a.H(tid, path).stИз Istate-cert (tid, a, t) следует, что ℓ = Jexpr0 Kpathcom = Jexpr0 K и val =stJexpr1 Kpathcom = Jexpr1 K .

Из Imem-1-com-cert (tid, a, t) следует, что существуетview ⩽ view′ такой, что ⟨ℓ : val@τ,view⟩ ∈ t.promises ∩ t.M. То, чтоviewcur (ℓ) < τ, следует из Iview-write-cert (tid, a, t).V′≜ ⟨viewcur ⊔ [ℓ@τ], viewacq ⊔ [ℓ@τ], viewrel ⟩;promises′ ≜ promises \ {⟨ℓ : val@τ,view⟩}.Так,выполняетсяtFulfill promise ⟨ℓ:val@τ,view⟩−−−−−−−−−−−−−−−−→Promise tidt′≜⟨M, ⟨path′ , st, V ′ , promises′ ⟩⟩. Проверка Icert (n − 1, δ, k, a, t′ ) тривиальна.176– tape(path) = W stwrite , где состояние stwrite указывает, что экземпляр незавершён. В этом случае поток обещающей машины с идентификатором tid совершит два перехода: сначала пообещает некоторое сообщение, а потом выполнит это обещание.

Аналогично предыдущим пунктам,cmds(path.last) = ‘‘[expr0 ] := expr1 ”. Введём следующие обозначения:path′regfcomℓval≜≜≜≜next-path(path, 1);regfcom (cmds, tape, path);stJexpr0 Kpathcom = Jexpr0 K ;Jexpr1 Kst .Поскольку соответствующий экземпляр записи не завершён, то в памятиARM+τ машины нет связанного с ним запроса, а значит, и нужной метки времени для добавляемого обещающей машиной сообщения.

Поэтомунам нужно выбрать эту метку времени, которую мы будем обозначать τ.Метка τ должна удовлетворять следующим ограничениям.1. viewcur (ℓ) < τ.2. τ ̸∈ {τ′ |⟨ℓ, _, wr τ′ : _⟩ ∈ M}.3. ∀pathwrite ⩾ path. tape(pathwrite ) = W (com _ ℓ _) ⇒τ < a.Hτ (tid, pathwrite ).4. ∀pathread ⩾ path. tape(pathread ) = R (sat com w) ∧a.Hτ (w.tid, w.path) ̸= ⊥ ⇒τ ⩽ a.Hτ (w.tid, w.path).5. ∀pathread < pathld < pathδ−read , w, view.path < pathread ∧tape(pathread ) = R (sat com w) ∧ tape(pathld ) = F com ld ∧tape(pathδ−read ) = R (sat com ⟨tid, path, wr ℓ : _⟩) ∧view = a.Hview (w.tid, w.path) ̸= ⊥ ⇒view(ℓ) ⩽ τ.Поскольку метки времени являются элементами плотного множества Q,то в силу Iview-write-cert (tid, a, t), Iview-read-cert (δ, tid, a, t) и теоремы 4 нужнаяметка τ существует.177Введём следующие обозначения:viewmsgM′V ′ = ⟨view′cur , view′acq , view′rel ⟩δ′≜≜≜≜≜viewrel ⊔ [ℓ@τ];⟨ℓ : val@τ,view⟩;M ∪ {msg};⟨viewcur ⊔ [ℓ@τ], viewacq ⊔ [ℓ@τ], viewrel ⟩;δ[path 7→ ⟨τ, view⟩].Тогда, верно следующее:Promise write ⟨ℓ:val@τ,view⟩t −−−−−−−−−−−−−−−→ ⟨M′ , ⟨path, st, V, promises ∪ {msg}⟩⟩Promise tidFulfill promise ⟨ℓ:val@τ,view⟩−−−−−−−−−−−−−−−−→ t′ ≜ ⟨M′ , ⟨path′ , st, V ′ , promises⟩⟩.Promise tidПроверка Icert (n − 1, δ′ , k, tid, a, t′ ) тривиальна.Теорема 7.

∀(a, p) ∈ Ibase .ainit −−−→∗ a ⇒ certifiable(p).ARMДоказательство. Зафиксируем tid, tape ≜ a.tapef(tid). Введём следующие обозначения:knpathlast-wcompathnext-lastδ≜≜≜≜≜last-write-com(tape).last + 1;length(last-write-com(tape) : k) − length(t.path);last-write-com(tape);pathlast-wcom : k;λpath. ⊥.Если мы сможем показать, что Icert (n, δ, k, tid, a, t) выполняется, то утверждениетеоремы верно по лемме 12.

Таким образом нам нужно проверить следующее178утверждение:ainit −−−→∗ a ∧ARMt.path ⩽ pathnext-last ∧ (n = length(path next-last ) − length(t.path)) ∧(∀path′ ⩾ t.path, δ(path′ ) = ⊥) ∧(∀path′′ , path′ , stread .path′′ ⩾ path′ ⩾ t.path ∧ tape(path′ ) = R stread ∧ stread ̸= sat com _ ⇒tape(path′′ ) ̸= F _ _) ∧(∀path′ . t.path ⩽ path′ < path next-last ⇒(Prog(tid)[path′ .last] ∈ {‘‘if _ goto _”, ‘‘fence(_)”} ⇒ tape(path′ ) завершён) ∧tape(path′ ) имеет полностью определённый адрес ∧¬Prog(tid)[path′ .last] = ‘‘fence(sy)”) ∧(tid, a, t) ∈ Imem-1-com-cert ∩ Imem-2-cert ∩ Istate-cert ∩ Iwrite-rel-cert ∩ Iview-write-cert ∧(δ, tid, a, t) ∈ Imem-1-tid-cert ∩ Iδ-con-1 ∩ Iδ-con-2 ∩ Iview-read-cert ∧(δ, tid, a) ∈ Iδ-con-3 ∩ Iδ-con-4 .Первые три конъюнкта очевидно выполняются. Четвертый конъюнкт выполняется в силу ограничений перехода Завершение барьера машины ARMv8 POP.

Пятый конъюнкт выполняется по ограничениям перехода Завершение записи машины ARMv8 POP и истинности утверждения Icom-SY (a, p).Утверждения (δ, tid, a) ∈ Iδ-con-3 ∩ Iδ-con-4 и (δ, tid, a, t) ∈ Iδ-con-1 ∩ Iδ-con-2 ∩Imem-1-tid-cert верны, поскольку δ = λpath. ⊥ является нигде не определённой функцией. Утверждение (δ, tid, a, t) ∈ Iview-read-cert верно, поскольку δ = λpath. ⊥ ивыполняется теорема 4.Утверждение (tid, a, t) ∈ Imem-1-com-cert ∩Imem-2-cert ∩Istate-cert непосредственноследует из (a, p) ∈ Imem1 ∩ Imem2 ∩ Istate . Утверждение (tid, a, t) ∈ Iwrite-rel-cert ∩Iview-write-cert следует из (a, p) ∈ Iview и того, что все экземпляры чтения, предшествующие завершённому экземпляру барьера, также являются завершёнными посвойствам модели ARMv8 POP.179Приложение Г.

Представление программГ.1 Помеченная система переходовПервым шагом для построения по программе помеченной системы переходов является генерация всех возможных путей (P ath) исполнения, каждый изкоторых является списком меток:P ath ::= List LabelLabel ::= R(ℓ,v) | W(ℓ,v) | F(fmod) | εДалее по множеству путей строится конечный автомат, принимающий упомянутые пути.Функция построения путей cmds-to-lbls использует вспомогательнуюфункцию inst-to-lbl, которая принимает список инструкций потока ilist, указательна текущую инструкцию pos и состояние локальных переменных st:cmds-to-lbls : cmds → P(P ath)cmds-to-lbls ilist = inst-to-lbl ilist 0 (λreg.0)inst-to-lbl : cmds → N → (Reg → N) → P(P ath)inst-to-lbl ilist pos st ≜if pos < 0 || pos > length(ilist) then {[]}elsematch ilist[pos] with|‘‘nop” → inst-to-lbl ilist (pos + 1) st|‘‘reg := [expr]” →{R(JexprKst ,v) : l | ∀v ∈ Val, l ∈ inst-to-lbl ilist (pos + 1) st[reg 7→ v]}|‘‘reg := expr” → inst-to-lbl (pos + 1) st[reg 7→ JexprKst ]|‘‘[expr0 ] := expr1 ” →{W(Jexpr0 Kst ,Jexpr1 Kst ) : l | ∀l ∈ inst-to-lbl ilist (pos + 1) st}|‘‘fence(fmod)” → {F(fmod) : l | ∀l ∈ inst-to-lbl ilist (pos + 1) st}|‘‘if expr goto k” → let step ≜ if JexprKst then k else 1 ininst-to-lbl (pos + step) stВажно отметить, что каждый поток (в обещающей машине) имеет свою систему переходов, которая представляет программу этого потока и, соответственно, строится с помощью функции cmds-to-lbls.180Г.2 ПредзапускиДля построения по программе ARM-согласованных исполнений стандартноиспользуется следующая схема [65].

В начале по программе строятся предзапуски — графы исполнений, в которых определена только часть нужных отношениймежду событиями, а именно отношения порядка po и зависимостей по даннымdata, управлению ctrl и адресу addr.PreExecs ≜ P(⟨set : P(E), lab : set ⇀ Label,po : P(set × set), ctrl : P(set × set), addr : P(set × set), data : P(set × set)⟩)При этом для каждой инструкции чтения генерируется столько вариантов соответствующего события, сколько существует возможных значений соответствующеготипа данных.

Далее для каждого предзапуска недетерменированно выбираютсяотношения mo и rf таким образом, чтобы получалось ARM-согласованное исполнение. Важно отменить, что не для всех предзапусков существуют подходящие moи rf.Функция построения предзапусков по списку команд потокаcmds-to-vertices использует вспомогательную функцию inst-to-vertex, котораяпринимает список инструкций потока ilist, указатель на текущую инструкциюpos, состояние локальных переменных st и отношение зависимости локальнойпеременной от сгенерированного события dep. Последний параметр нужен дляотношений зависимости.cmds-to-vertices : cmds → PreExecscmds-to-vertices ilist ≜ inst-to-vertex ilist 0 (λreg.0) ∅181inst-to-vertex : cmds → N → (Reg → N) → P(Reg × E) → PreExecsinst-to-vertex ilist pos st dep ≜if pos < 0 || pos > length(ilist) then {⟨∅, ⊥, ∅, ∅, ∅, ∅⟩}elselet a ≜ fresh-vertex inmatch ilist[pos] with|‘‘nop” → inst-to-vertex ilist (pos + 1) st dep|‘‘reg := [expr]” →let dep′ ≜ (dep \ {reg} × E) ∪ {⟨reg, a⟩} inlet ℓ ≜ JexprKst inlet addr′ ≜ codom([regs(expr)]; dep) × {a} in{⟨set ∪ {a}, lab[a 7→ R(ℓ,v)], po ∪ {a} × set, ctrl, addr ∪ addr′ , data⟩ | ∀v ∈ Val,⟨set, lab, po, ctrl, addr, data⟩ ∈ inst-to-vertex ilist (pos + 1) st[reg 7→ v] dep′ }|‘‘reg := expr” →let dep′ ≜ (dep \ {reg} × E) ∪ {reg} × regs(expr)} ininst-to-vertex ilist (pos + 1) st[reg 7→ JexprKst ] dep′|‘‘[expr0 ] := expr1 ” →let ℓ ≜ Jexpr0 Kst inlet v ≜ Jexpr1 Kst inlet addr′ ≜ codom([regs(expr0 )]; dep) × {a} inlet data′ ≜ codom([regs(expr1 )]; dep) × {a} in{⟨set ∪ {a}, lab[a 7→ W(ℓ,v)], po ∪ {a} × set, ctrl, addr ∪ addr′ , data ∪ data′ ⟩ |⟨set, lab, po, ctrl, addr, data⟩ ∈ inst-to-vertex ilist (pos + 1) st dep}|‘‘fence(fmod)” →{⟨set ∪ {a}, lab[a 7→ F(fmod)], po ∪ {a} × set, ctrl, addr, data⟩ |⟨set, lab, po, ctrl, addr, data⟩ ∈ inst-to-vertex ilist (pos + 1) st dep}|‘‘if expr goto k” →let step ≜ if JexprKst then k else 1 inlet dver ≜ codom([regs(expr)]; dep) in{⟨set, lab, po, ctrl ∪ dver × set, addr, data⟩ |⟨set, lab, po, ctrl, addr, data⟩ ∈ inst-to-vertex ilist (pos + step) st dep}В определении функции inst-to-vertex используется вспомогательная функция regs, которая по выражению вычисляет множество регистров, от которых этовыражение зависит.182regs : e → P(Reg)regs e ≜match e with|ℓ|v→∅| reg → {reg}| uop expr → regs expr| bop expro expr1 → (regs expr0 ) ∪ (regs expr1 )Как было отмечено выше, функция cmds-to-vertices строит предзапускитолько одного потока.

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

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