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

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

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

мы добавили e во множество покрытых событий и убрали msg из множества обещанных сообщений потока tid.– Iview-rel (T S ′ ): выполняется, т.к. Iview-rel (T S) выполняется,T S ′ (tid).V.rel=T S(tid).V.rel и 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.rel⩽ dom-view(rel-rel; [e′ ]).Т.к. ⟨w, e′ ⟩ ∈ cur-rel ⊆ acq-rel, [ℓ@τ] ⩽ dom-view(cur-rel; [e′ ])⩽ dom-view(acq-rel; [e′ ]).189– Istate (C ′ , T S ′ ): очевидно следует из Istate (C, T S) и определенийC ′, T S ′.Лемма 15.

Для любой локации ℓ выполняется [Wℓ ]; cur-rel; [Wℓ ] ⊆ mo.Доказательство. Зафиксируем ⟨w, w′ ⟩ ∈ [Wℓ ]; cur-rel; [Wℓ ]. Тогда по определениюmo, либо mo(w, w′ ), либо mo(w′ , w). Если выполняется первое, то выполняетсяутверждение. Пусть выполняется второе.[Wℓ ]; cur-rel; [Wℓ ] =[Wℓ ]; rf? ; (po ∪ sw)+ ; [Wℓ ] =(по транзитивности po и определению sw)[Wℓ ]; rf? ; po; (sw; po)∗ ; [Wℓ ] =[Wℓ ]; rf? ; po; [Wℓ ] ∪[Wℓ ]; rfe? ; po; (sw; po)+ ; [Wℓ ] ∪⟨w, w′ ⟩ ̸∈ [Wℓ ]; rf? ; po; [Wℓ ], т.к. ⟨w′ , w⟩ ∈ mo и выполняется.Введем вспомогательное отношение eord ≜ (obs ∪ dob ∪ bob)+ , котороеантирефлексивно по определению ARM-согласованности ().

Из определений отношений следует, что po? ; sw; po ⊆ bob? ; bob ∪ bob? ; bob; rfe; bob ⊆eord. По транзитивности eord, ⟨w, w′ ⟩ ∈ eord.Мы знаем, что ⟨w′ , w⟩ ∈ mo. Существует два варианта: ⟨w′ , w⟩ ∈ moe или⟨w′ , w⟩ ∈ moi. Первый вариант противоречит ацикличности eord, т.к. moe ⊆obs. Опровергнем второй вариант, показав, что (eord ∪ moi)+ = (obs ∪ dob ∪bob ∪ moi)+ антирефлексивно.Предположим обратное и рассмотрим цикл минимальной длины, в которомточно есть moi по антирефлексивности eord. Рассмотрим предыдущее реброцикла, которое мы обозначим r, и покажем, что во всех случаях цикл можно укоротить.– Если r ∈ moi, то цикл может быть укорочен, т.к. moi; moi ⊆ moi.– Если r ∈ obs = rfe ∪ rbe ∪ moe, то нужно рассмотреть три варианта.

Поскольку rfe; moi = ∅, то r не может быть из отношения rfe. Вдвух других случаях цикл может быть укорочен, т.к. rbe; moi ⊆ rbe, иmoe; moi ⊆ moe.– Если r ∈ bob, то цикл может быть укорочен, поскольку po; moi ⊆ po.– Если r ∈ dob, то цикл может быть укорочен:190––––addr; po? ; moi ⊆ dob,data; moi ⊆ dob,(addr ∪ data); rfi; moi = ∅,(ctrl ∪ data); [W]; moi? ; moi ⊆ dob..

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

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