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

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

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

certifiabletid (thread-state(tid,p));certifiabletid (t) ≜ ∃t′ . t −−−−−−→∗ t′ ∧ t′ .promises = ∅;Promise tidthread-state(tid, p) ≜ ⟨p.M, p.T S(tid)⟩.Теорема 7, которая является ключевой в данном приложении и используется в доказательстве лемм 5 и 7, утверждает, что если состояния обещающей иARM+τ машин связаны отношением Ibase , и при этом состояние ARM+τ машиныдостижимо из начального, то состояние обещающей машины сертифицируемо.Теорема 7. ∀(a, p) ∈ Ibase .

ainit −−−→∗ a ⇒ certifiable(p).ARMВ.2.1Структура доказательства теоремы о сертификацииКакие невыполненные обещания есть у потока tid обещающей машины всостоянии p, если оно связано с некоторым состоянием a машины ARM+τ отношением Ibase ? Согласно отношению Imem2 ⊆ Ibase для каждого сообщения (втом числе обещанного, но не выполненного) в памяти обещающей машины вплёнке машины ARM+τ существует завершённый экземпляр инструкции записи, ему соответствующий. Из отношения Imem1 ⊆ Ibase следует, что обещанное,но не выполненное сообщение соответствует экземпляру, чей путь не меньше,170чем текущий указатель потока обещающей машины.

Таким образом, для сертификации поток обещающей машины может совершить серию переходов, которыепокроют плёнку машины ARM+τ вплоть до последнего завершённого экземплярачтения. При этом обещающая машина будет выполнять переходы, которые будутопределены предшествующими экземплярами инструкций в состоянии машиныARM+τ. Именно наличие такой серии переходов мы будем доказывать.Для реализации описанной выше идеи мы используем отношениеIcert (n, δ, k, tid, a, t), которое имеет шесть параметров:– tid — это идентификатор потока, в контексте сертификации которого используется данный элемент отношения;– n — это количество экземпляров на пути от указателя потока до последнего завершённого экземпляра записи в соответствующей плёнке;– k — это номер инструкции, следующей за последним завершённым экземпляром записи;– δ — это частичная функция, имеющая тип P ath ⇀ (Time × V), котораяэкземпляру не завершённой инструкции записи в плёнке потока tid ставитв соответствие пару из метки времени и фронта сообщения, которое былодобавлено в память обещающей машиной;– a — это состояние машины ARM+τ, которое используется для сертификации потока обещающей машины;– t — это состояние потока tid обещающей машины.Перед тем, как предъявить формальное определение данного отношения, мы приведём утверждения лемм, которые его используют.Лемма 12 утверждает, что из (n, δ, k, tid, a, t) ∈ Icert следует, что поток tidобещающей машины сертифицируем.Лемма 12.

∀n, δ, k, tid, a, t. Icert (n, δ, k, tid, a, t) ⇒ certifiabletid (t).Доказательство данной леммы проводится индукцией по n. Базу индукциимы выделили в лемму 13, а индукционный переход — в лемму 14.Лемма 13. ∀k, δ, tid, a, t, Icert (0, δ, k, tid, a, t), t.promises = ∅.Лемма 14. ∀n ̸= 0, δ, k, tid, a, t, Icert (n, δ, k, tid, a, t).∃δ′ , t′ .Prog(tid) ⊢ t −−−−−−→∗ t′ ∧ Icert (n − 1, δ′ , k, tid, a, t′ ).Promise tid171В.2.2Описание вспомогательного отношенияОтношение Icert определяется следующим образом.Icert ⊂ N × (P ath ⇀ (Time × V)) × N × Tid × StateARM +τ × TStatePromiseIcert (n, δ, k, tid, a, t) ≜let tape ≜ a.tapef(tid) inlet pathlast-wcom ≜ last-write-com(tape) inlet pathnext-last ≜ pathlast-wcom : k inainit −−−→∗ a ∧ARMt.path ⩽ pathnext-last ∧ (n = length(path next-last ) − length(t.path)) ∧(∀path′ ⩾ t.path, δ(path′ ) = ⊥) ∧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)”) ∧(∀path′′ , path′ , stread .(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 .В определении используются отношения, определённые ниже.tidIw−cert(tid, a, p) ≜let tape, path ≜ a.tapef(tid), p.T S(tid).path in∃path′ ⩾ path.tape(path′ ) является завершённой записью.Iwrite-rel-cert (tid, a, t) ≜ ∀path ⩾ t.path.let tape ≜ a.tapef(tid) inlet pathld ≜ lastld(tape, path) in⊔t.viewrel ⩽ com-reads-view(pathld , tape, a.H)⊔⊔com-writes-time(tid, path, tape, a.H).172Iview-write-cert (tid, a, t) ≜ ∀path′ ⩾ t.path, ℓ. a.tapef(tid, path′ ) = W (com _ ℓ _) ⇒t.viewcur (ℓ) < a.Hτ (tid, path′ ) ∧((∃path′′ .

t.path ⩽ path′′ < path′ ∧ a.tapef(tid, path′′ ) = F com ld) ⇒t.viewacq (ℓ) < a.Hτ (tid, path′ )).comb-time(δ, tidt , a) ≜ λtid, path.if tid = tidt ∧ a.H(tid, path) = ⊥ then δ(path)elif ∃τ, view, ⟨τ, _, view⟩ = a.Hτ (tid, path) then ⟨τ, view⟩else ⊥.Iview-read-cert (δ, tid, a, t) ≜ ∀path′ ⩾ t.path, w, τ.a.tapef(tid, path′ ) = R (sat com w) ∧ ⟨τ, _⟩ = comb-time(δ, tid, a, w.tid, w.path) ⇒t.viewcur (w.ℓ) ⩽ τ ∧((∃path′′ .

t.path ⩽ path′′ < path′ ∧ a.tapef(tid, path′′ ) = F com ld) ⇒t.viewacq (w.ℓ) ⩽ τ).Istate-cert (tid, a, t) ≜let regfcom ≜ regfcom (Prog(tid), a.tapef(tid), t.path) in∀reg. regfcom (reg) = ⊥ ∨ t.st(reg) = regfcom (reg).Imem-1-tid-cert (δ, tidt , a, t) ≜ ∀path, τ, view, ℓ, expr0 , expr1 .⟨τ, view⟩ = δ(path) ∧ ‘‘[expr0 ] := expr1 ” = Prog(tidt , path.last) ∧ ℓ = Jexpr0 Kpathcom ⇒∃val.Jexpr1 Kpathcom ∈ {⊥, val} ∧ ⟨ℓ : val@τ,view⟩ ∈ t.M \ t.promises.Imem-1-com-cert (tidt , a, t) ≜ ∀tid, ℓ, val, τ, view′ , path.W (com _ ℓ val) = a.tapef(tid, path) ∧ ⟨τ, _, view′ ⟩ = a.H(tid, path) ⇒∃view ⩽ view′ . ⟨ℓ : val@τ,view⟩ ∈ t.M ∧(tid ̸= tidt ∨ path < t.path ⇒ ⟨ℓ : val@τ,view⟩ ̸∈ t.promises) ∧(tid = tidt ∧ path ⩾ t.path ⇒ ⟨ℓ : val@τ,view⟩ ∈ t.promises).Imem-2-cert (tid, a, t) ≜ ∀⟨ℓ : val@τ,view⟩ ∈ t.promises.

τ ̸= 0 ⇒∃view′ ⩾ view, path ⩾ t.path.W (com _ ℓ val) = a.tapef(tid, path) ∧ ⟨τ, _, view′ ⟩ = a.H(tid, path).173Iδ-con-1 (δ, tidt , a, t) ≜ ∀path < t.path. δ(path) ̸= ⊥ ⇔(∃expr0 , expr1 . ‘‘[expr0 ] := expr1 ” = Prog(tidt , path.last) ∧a.tapef(tidt , path) isn’t committed).Iδ-con-2 (δ, tidt , a, t) ≜ ∀path, ⟨τ, view⟩ = δ(path),‘‘[expr0 ] := expr1 ” = Prog(tidt , path.last), ℓ = Jexpr0 Kpathcom .view = [ℓ@τ] ⊔ t.viewrel ∧ t.viewcur (ℓ) ⩾ τ.Iδ-con-3 (δ, tidt , a) ≜ ∀path, path′ ̸= path,⟨τ, _⟩ = comb-time(δ, tidt , a, tidt , path), ⟨τ′ , _⟩ = comb-time(δ, tidt , a, tidt , path′ ),‘‘[expr0 ] := expr1 ” = Prog(tidt , path.last),‘‘[expr′0 ] := expr′1 ” = Prog(tidt , path′ .last).′′ path′Jexpr0 Kpathcom = Jexpr0 Kcom ⇒ τ ̸= τ .Iδ-con-4 (δ, tidt , a) ≜ ∀pathδ < pathread < pathld < pathδ−read ,⟨τ, _⟩ = δ(pathδ ), w, ℓ, view.tape(pathread ) = R (sat com w) ∧ tape(pathld ) = F com ld ∧tape(pathδ−read ) = R (sat com ⟨tidt , pathδ , wr ℓ : _⟩) ∧view = a.Hview (w.tid, w.path) ̸= ⊥ ⇒view(ℓ) ⩽ τ.В.2.3 Доказательство лемм и теоремы о сертификацииЛемма 13.

∀k, δ, tid, a, t, Icert (0, δ, k, tid, a, t), t.promises = ∅.Доказательство. Зафиксируем k, δ, tid, a, t. Поскольку Icert (0, δ, k, tid, a, t) выполняется и верно, что length(t.path) = length(last-write-com(a.tapef(tid))) + 1, тоt.path = last-write-com(a.tapef(tid)) : k.Предположим, что существует ещё не выполненное обещание, т.е. ∃⟨ℓ :val@τ,view⟩ ∈ t.promises. Тогда, из Imem-2-cert (tid, a, t) следует, что существуетфронт view′ ⩾ view и путь path ⩾ t.path такие, что W (com _ ℓ val) =a.tapef(tid, path). А значит path ⩾ t.path > last-write-com(a.tapef(tid)). Т.о. мыполучили противоречие с определением last-write-com.174Лемма 14. ∀n ̸= 0, δ, k, tid, a, t, Icert (n, δ, k, tid, a, t).∃δ′ , t′ .Prog(tid) ⊢ t −−−−−−→∗ t′ ∧ Icert (n − 1, δ′ , k, tid, a, t′ ).Promise tidДоказательство. Зафиксируем n, tid, a, t.

Введём следующие обозначения:tape≜ a.tapef(tid);⟨M, ⟨path, st, V, promises⟩⟩ ≜ t;cmds≜ Prog(tid).Далее в доказательстве нам нужно рассмотреть варианты tape(path). Варианты,при которых tape(path) ∈ {Nop, Assign, If _ _, tape(path) = F _ _}, проверяютсятривиальным образом (в этих случаях δ′ = δ). Рассмотрим оставшиеся варианты.– tape(path) = R (sat com w).

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

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