Диссертация (1149932), страница 32
Текст из файла (страница 32)
Для того, чтобы получить предзапуск всей программы,предзапуски потоков программы должны быть покомпонентно объединены, а также в каждый получившийся предзапуск должны быть добавлены события инициализирующей записи:prog-to-vertex : Prog → PreExecsprog-to-vertex Prog ≜let E(tid) ≜ cmds-to-vertices Prog(tid) in∪⊔∪let P ≜ {⟨ tid∈dom(Prog) petid .set, tid∈dom(Prog) petid .lab, tid∈dom(Prog) petid .po,∪∪∪tid∈dom(Prog) petid .ctrl, tid∈dom(Prog) petid .addr, tid∈dom(Prog) petid .data⟩| tid ∈ dom(Prog), petid ∈ E(tid)} inlet Einit , labinit ≜ {eℓ , [eℓ 7→ W(ℓ,0)] | ℓ ∈ Loc} in⊔let lab′ ≜ labinit in{⟨set ∪ Einit , lab ⊔ lab′ , po ∪ (Einit × set), ctrl, addr, data⟩| ⟨set, lab, po, ctrl, addr, data⟩ ∈ P }Г.3 Связь между системой переходов и предзапускамиДля того, чтобы определить связь между системой переходов, на которойстроится исполнение потока обещающей модели, и предзапуска потока в моделиARMv8.3, мы вводим отношение ≈:≈: LabelPromise → LabelARM → BooleanlblPromise ≈ lblARM ≜match lblPromise , lblARM with| R(ℓ,v), R(ℓ,v) | W(ℓ,v), W(ℓ,v)| F(rel), F(sy) | F(acq), F(ld) → true| _, _ → false183Это отношение, по сути, является отношением компиляции.
Так, оно связываетметки переходов чтения и записи с событиями чтения и записи, только если ониимеют одинаковые параметры: целевую локацию и значение. Кроме того, отношение ≈ связывает метку высвобождающего барьера F(rel) с событием полногобарьера F(sy), а приобретающего барьера F(acq) — с событием ld-барьера.Теорема 8.
Для любого события из предзапуска, построенного по списку инструкций cmds, существует путь в системе переходов, построенной по cmds, которыйимеет эквивалентный событию переход. Кроме того, верно и обратное: для любого перехода некоторого пути в системе переходов, построенной по cmds, существует предзапуск cmds и событие в нём, эквивалентное этому переходу.∀cmds.(∀⟨set, lbl, po, _, _, _⟩ ∈ cmds-to-vertices cmds.∃path ∈ cmds-to-lbls cmds[tid]. ∀n ∈ N, a ∈ nth po n.∃k ∈ N.
path[n + k] ≈ lbl a) ∧(∀path ∈ cmds-to-lbls cmds.∃⟨set, lbl, po, _, _, _⟩ ∈ cmds-to-vertices cmds. ∀n ∈ N.path[n] ̸= ε ⇒ ∃k ∈ N, a ∈ nth po (n − k). path[n] ≈ lbl a).Теорема тривиальным образом обобщается на случай программ, т.е. функций, которые по идентификатору потока возвращают его список инструкций.В формулировке теоремы 8 присутствует функция nth, которая по бинарному отношению rel и натуральному числу n возвращает множество элементов изобласти определения rel, до которых в rel существует путь длины n, но не n + 1:nth : {A : Set} → P(A × A) → N → P(A)nth rel n ≜ codom(reln ) \ codom(reln+1 ).Доказательство теоремы 8. Верно по определению функций cmds-to-lbls иcmds-to-vertices.184Приложение Д.
Доказательство леммы о шагесимуляции обещающей модели и обхода сценарияARMv8.3Лемма 11. Пусть для некоторых конфигураций обхода ⟨C, I⟩ и ⟨C ′ , I ′ ⟩ сценария 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Доказательство.
Существует два варианта: G ⊢ C, I →TC ⟨C ′ , I ′ ⟩ соответствуетпокрытию или выпуску некоторого события e ∈ E. Введем обозначения tid ≜tid(e) и ⟨σ, V, promises⟩ ≜ T S(tid). Начнем с рассмотрения варианта, когда G ⊢C, I →TC ⟨C ′ , I ′ ⟩ соответствует выпуску события записи e.Выпуск события e. Из определения →TC следует, что C ′ = C, I ′ = I ∪ {e}и e ∈ Issuable(G, C, I) \ I. Введем обозначения:ℓ, v, τ ≜ loc(e), valw (e), T (e)mview ≜ [ℓ@τ] ⊔ V.relmsg≜ ⟨ℓ : v@τ,mview⟩Мы знаем, что в M нету сообщения для локации ℓ с меткой времени τ, т.к. функция T выдает уникальные для одной локации метки времени для событий записи(correct-tmap(G, T )), и у каждого сообщения из M существует соответствующееему сообщение в I (Imem2 (C, I, M )).M ′ , promises′ ≜ M ∪ {msg}, promises ∪ {msg}T S′≜ T S[tid 7→ ⟨σ, V, promises′ ⟩]mview ∈ M ′ , т.к. [ℓ@τ] ∈ M ′ и V.rel ∈ M . Таким образом⟨⟨σ, V, promises⟩, M ⟩ ⇝Promise tid ⟨⟨σ, V, promises′ ⟩, M ′ ⟩ выполняется.
Осталосьпроверить, что I(C, I ′ , T S ′ , M ′ ) выполняется.– Imem1 (C, I ′ , T S ′ , M ′ ) ∧ Imem2 (C, I ′ , M ′ ):Единственным нетривиальным утверждением, которое нужно проверить,является mview ⩽ dom-view(msg-rel; [e]). По определению, mview =[ℓ@τ] ⊔ V.rel [ℓ@τ] = [loc(e)@T (e)] ⩽ dom-view(msg-rel; [e]), т.к.⟨e, e⟩ ∈ msg-rel. Из Iview (C, T S) следует V.rel ⩽ dom-view(rel-rel; [e′ ]),где e′ ∈ Next(G, C) и tid(e′ ) = tid(e). Т.к.
e ̸∈ C и по определению Next, ⟨e′ , e⟩ ∈ po? . Из определения rel-rel и msg-rel следует185rel-rel; [e′ ]; po? ; [e] ⊆ msg-rel; [e]. Утверждение выполняется, т.к. V.rel ⩽dom-view(rel-rel; po; [e′ ]).– Iview-rel (T S ′ ): выполняется по Iview-rel (T S) и определениям mview и T S ′ .– Iview (C, T S ′ ): т.к. ∀tid. T S ′ (tid).V = T S(tid).V и Iview (C, T S ′ ), инвариант выполняется.– Istate (C, T S ′ ): следует из того, что Istate (C, T S) выполняется и, для любого tid, T S(tid).σ = T S ′ (tid).σ.Покрытие события e.
В этом случае C ′ = C ∪ {e}, I ′ = I. Т.к. Istate (C, T S)выполняется, существуют такие t и σ′ , что t ≈ lab(e). Рассмотрим варианты e.– e ∈ F(ld). В этом случае label(t) = F acq по Istate (C, T S).V′≜ ⟨V.acq, V.acq, V.rel⟩T S ′ , M ′ ≜ T S[tid 7→ ⟨σ′ , V ′ , promises⟩], MПроверим, что I(C ′ , I, T S ′ , M ) выполняется.– Imem1 (C ′ , I, T S ′ , M ) ∧ Imem2 (C ′ , I, M ): выполняется, т.к. e ̸∈ W иI(C, I, T S, M ) выполняется.– Iview-rel (T S ′ ): выполняется, т.к. Iview-rel (T S) выполняется иT S ′ (tid).{V.rel, promises} = T S(tid).{V.rel, promises}.– 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′ ]).Зафиксируем e′ . Если tid(e′ ) ̸= tid, то утверждение следует из Iview (C, T S). Предположим, что tid(e′ ) = tid. Тогдаpo|imm (e, e′ ), т.к. e ∈ Next(G, C).
Мы знаем, что V.acq ⩽dom-view(acq-rel; po; [e]), т.к. Iview (C, T S) выполняется. Намнужно показать, чтоV.acq ⩽ dom-view(cur-rel; [e′ ]) ∧V.acq ⩽ dom-view(acq-rel; [e′ ]) ∧V.rel ⩽ dom-view(rel-rel; [e′ ]).Т.к. dom(acq-rel; [e]) ⊆ dom(acq-rel; [e′ ]) и acq-rel; [e]; po; [e′ ] ⊆cur-rel; [e′ ], утверждение выполняется.186– Istate (C ′ , T S ′ ): очевидно следует из Istate (C, T S) и определенийC ′, T S ′.– e ∈ F(sy). В этом случае label(t) = F rel по Istate (C, T S).V ′ ≜ ⟨cur, acq, cur⟩T S ′ ≜ T S[tid 7→ ⟨σ′ , V ′ , promises⟩]M′ ≜ MНе существует w ∈ I такого, что po(e, w). Иначе не это противоречилобы w ∈ Issuable(G, C, I) по лемме 9 Из этого следует, что не существуетw ∈ I \C такого, что tid(w) = tid, и promises = ∅ по Imem1 (C, I, T S, M ).Проверим I(C ′ , I, T S ′ , M ).– Imem1 (C ′ , I, T S ′ , M ) ∧ Imem2 (C ′ , I, M ): выполняется, т.к.
e ̸∈ W иI(C, I, T S, M ) выполняется.– Iview-rel (T S ′ ):Зафиксируем поток tid′ . Если tid′ ̸= tid, то утверждение выполняется по Iview-rel (T S). Если tid′ = tid, то утверждение выполняется, т.к. T S ′ (tid).promises = T S(tid).promises = ∅.– 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′ ]).Зафиксируем e′ . Если tid(e′ ) ̸= tid, то утверждение следуетиз Iview (C, T S). Если tid(e′ ) = tid, то po|imm (e, e′ ), т.к. e ∈Next(G, C).
Нам нужно показать, чтоV.cur ⩽ dom-view(cur-rel; [e′ ]) ∧V.acq ⩽ dom-view(acq-rel; [e′ ]) ∧V.cur ⩽ dom-view(rel-rel; [e′ ]).Т.к. dom(cur-rel; [e]) ⊆ dom(cur-rel; [e′ ]) и rel-rel; [e]; po; [e′ ] ⊆cur-rel; [e′ ], утверждение выполняется.– Istate (C ′ , T S ′ ): очевидно следует из Istate (C, T S) и определенийC ′, T S ′.187– e ∈ R. В этом случае label(t) = R (ℓ, v) по Istate (C, T S).ℓ, v≜ loc(e), valr (e)σ, V, promises ≜ T S(tid)Т.к.
e ∈ R ∩ Coverable(G, C, I) из определения →TC , существует событиезаписи w ∈ I ∩ dom(rf; [e]). По Imem1 (C, I, T S, M ) существует фронтview такой, что msg ≜ ⟨ℓ : v@T (w),view⟩ ∈ M . V.cur ⩽ T (w) по лемме15.V ′ ≜ ⟨V.cur ⊔ [ℓ@T (w)], V.acq ⊔ view, V.rel⟩T S ′ ≜ T S[tid 7→ ⟨σ′ , V ′ , promises⟩]Нужно проверить I(C ′ , I, T S ′ , M ).– Imem1 (C ′ , I, T S ′ , M ) ∧ Imem2 (C ′ , I, M ): выполняется, т.к. e ̸∈ W иI(C, I, T S, M ) выполняется.– Iview-rel (T S ′ ): выполняется, т.к. Iview-rel (T S) выполняется иT S ′ (tid).{V.rel, promises} = T S(tid).{V.rel, promises}.– 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′ ]).Зафиксируем e′ . Если tid(e′ ) ̸= tid, то утверждение следует из Iview (C, T S).
Предположим, что tid(e′ ) = tid. Тогдаpo|imm (e, e′ ), т.к. e ∈ Next(G, C). Нам нужно показать, чтоV.cur ⊔ [ℓ@T (w)] ⩽ dom-view(cur-rel; [e′ ]) ∧V.acq ⊔ view⩽ dom-view(acq-rel; [e′ ]) ∧V.rel⩽ dom-view(rel-rel; [e′ ]).Т.к. ⟨w, e′ ⟩ ∈ cur-rel, [ℓ@T (w)] ⩽ dom-view(cur-rel; [e′ ]). ИзIview-rel (T S) следует, что view = [ℓ@T (w)] ⊔ T S(tid(w)).V.rel.Т.к. ⟨w, e′ ⟩ ∈ acq-rel, [ℓ@T (w)] ⩽ dom-view(acq-rel; [e′ ]). Т.к.T S(tid(w)).V.rel ⩽ dom-view(rel-rel; [w]) и dom(rel-rel; [w]) ⊆dom(acq-rel; [e′ ]), утверждение выполняется.– Istate (C ′ , T S ′ ): очевидно следует из Istate (C, T S) и определенийC ′, T S ′.188– e ∈ W.
В этом случае label(t) = W (ℓ, v) по Istate (C, T S).ℓ, v, τ≜ loc(e), valw (e), T (e)⟨σ, V, promises⟩ ≜ T S(tid)⟨cur, acq, rel⟩ ≜ V.e ∈ I, т.е. e ∈ W ∩ Coverable(G, C, I). Из Imem1 (C, I, T S, M ) следует,что существует view такое, что msg ≜ ⟨ℓ : v@τ,view⟩ ∈ M . cur(ℓ) < τследует по лемме 15.cur′ , acq′ ≜ cur ⊔ [ℓ@τ], acq ⊔ [ℓ@τ]V′≜ ⟨cur′ , acq′ , rel⟩T S′≜ T S[tid 7→ ⟨σ′ , V ′ , promises \ msg⟩]view = rel по Iview-rel (T S).Нужно проверить I(C ′ , I, T S ′ , M ).– Imem1 (C ′ , I, T S ′ , M ) ∧ Imem2 (C ′ , I, M ): выполняется, т.к.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
