Диссертация (1149932), страница 19
Текст из файла (страница 19)
Тогда всезапросы записи и барьеров памяти, которые находятся в подсистеме памяти состояния s, также находятся в подсистеме памяти состояния s′ .∀s, s′ . Prog ⊢ s −−−→∗ s′ ⇒ s.Evt \ {e | e — запрос чтения} ⊆ s′ .Evt.ARMЛемма 4. Пусть состояние ARM-машины s′ достижимо из состояния s. Тогда рёбра отношения s.Ord, которые связывают запросы из множества s′ .Evt, также являются рёбрами в отношении s′ .Ord.∀s, s′ . Prog ⊢ s −−−→∗ s′ ⇒ s.Ord ∩ (s′ .Evt × s′ .Evt) ⊆ s′ .Ord.ARMДоказательство.
Следующая, более слабая, версия утверждения верна, так какнет перехода, который бы удалял Ord-ребро между запросами, который не могутбыть переупорядочены:∀s, s′ . Prog ⊢ s −−−→∗ s′ ⇒ (s.Ord ∩ (s′ .Evt × s′ .Evt)) \ ,→ ⊆ s′ .OrdARMТеперь докажем исходное утверждение. Зафиксируем пару запросов (e, e′ ) ∈s.Ord ∩ (s′ .Evt × s′ .Evt). Мы хотим показать, что (e, e′ ) ∈ s′ .Ord. Если запросы не переупорядочиваемы, e ̸,→ e′ , то утверждение выполняется, т.к.
(e, e′ ) ∈(s.Ord ∩ (s′ .Evt × s′ .Evt)) \ ,→ ⊆ s′ .Ord. Иначе e и e′ являются запросами чтенияили записи к разным локациям. Поскольку s.Ord(e, e′ ), то по лемме 1 существуетконечный путь по s.Ord-рёбрам от e к e′ , что каждое ребро этого пути соединяетне переупорядочиваемые запросы.Предположим, что на этом пути есть запрос барьера памяти e′′ . Тогда из транзитивности s.Ord следует, что {(e, e′′ ), (e′′ , e′ )} ⊆ s.Ord. Следовательно, по ослабленной версии леммы и транзитивности s′ .Ord следует, что{(e, e′′ ), (e′′ , e′ ), (e, e′ )} ⊆ s′ .Ord.Теперь предположим, что на этом пути нет запроса барьера памяти. Тогдапо определению отношения ,→ следует, что все запросы на этом пути оперируютодной и той же локацией. Это противоречит e ̸,→ e′ .983.6.2Модель ARMv8 POP и метки времениЗафиксируем некоторую программу Prog и рассмотрим её завершающийсясценарий поведения в модели ARMv8 POP:Prog ⊢ s0 −−−→ s1 −−−→ ...
−−−→ sn ,ARMARMARMгде s0 = sinit — это начальное состояние машины; sn = s является финальнымсостоянием, т.е. в подсистеме памяти s нет запросов чтения, все потоки осведомлены о всех запросах, исполнение всех экземпляров инструкций завершено, и загрузка новых экземпляров невозможна.Для локации ℓ и множества запросов Evt мы определяем Evtℓ как множествовсех запросов записи из Evt, целевой локацией которых является ℓ:Evtℓ ≜ {⟨tid, path, wr ℓ : val⟩ ∈ Evt | tid, path, val}.Поскольку не существует перехода, который удалял бы запросы записи, то s.Evtℓявляется множеством всех запросов записи в ℓ, которые были отправлены в подсистему памяти за весь сценарий поведения.Зафиксируем локацию ℓ.
Известно, что каждый поток осведомлён о каждомзапросе e ∈ s.Evtℓ , т.к. состояние s является финальным. Также известно, что двазапроса записи в одну локацию не переупорядочиваемы. Как следствие, по лемме2 верно, что moℓ ≜ s.Ord↾s.Evtℓ , где R↾S ≜ R ∩ (S × S), является полным порядком∪на запросах записи в локацию ℓ. Мы определяем отношение mo ≜ ℓ moℓ какобъединение множеств moℓ по всем возможным локациям. Используя позициизапросов во множестве moℓ , мы определяем функцию, которая по запросу записивозвращает его метку времени:index(mo , e), если e = ⟨tid, path, wr ℓ : val⟩ ∈ s.Evt;ℓmapτ (e) ≜⊥,иначе.Наконец, мы показываем, что для любого состояния si из рассмотренного сценария поведения верно, что отношение mo↾si .Evt ∪ si .Ord ациклично.Теорема 2.
∀i ⩽ n, mo↾si .Evt ∪ si .Ord ациклично.Доказательство. Очевидно, что утверждение выполняется при i = 0. Предположим, что существует такой индекс j, что для любого индекса i < j отношение99mo↾si .Evt ∪ si .Ord ациклично, но отношение mo↾sj .Evt ∪ sj .Ord имеет цикл. Известно, что mo↾sn .Evt ∪ sn .Ord = sn .Ord не имеет циклов.
Тогда цикл из mo↾sj .Evt ∪ sj .Ordдолжен быть “удалён” на части сценария поведения Prog ⊢ sj −−−→∗ sn .ARMС этого момента мы будем различать Ord- и mo-ребра. Мы будем называтьпару запросов (e, e′ ) Ord-ребром, если (e, e′ ) ∈ sj .Ord, и mo-ребром, если (e, e′ ) ∈mo↾sj .Evt \ sj .Ord.Рассмотрим цикл минимальной длины в mo↾sj .Evt ∪ sj .Ord. В этом цикледолжно присутствовать mo-ребро, т.к.
отношение sj .Ord ациклично. Такое moребро (e, e′ ) соединяет два запроса записи в локацию ℓ, и при этом mapτ (e) <mapτ (e′ ). Поскольку это ребро является частью цикла, то существует путь от e′к e, состоящий из Ord- и mo-рёбер. Мы можем разбить этот путь на максимальные гомогенные mo- и Ord-подпути. Покажем, что каждый Ord-подпуть состоиттолько из одного ребра.Рассмотрим произвольный Ord-подпуть {e′′i }i∈[0..k] . Запросы e′′0 и e′′k являются запросами записи, т.к. они связаны с другими подпутями mo-ребрами. Потранзитивности отношения sj .Ord (лемма 1) верно sj .Ord(e′′0 , e′′k ), а, значит, подпуть может быть сокращён до этих двух запросов.Таким образом, кратчайший путь от e′ к e в отношении mo↾sj .Evt ∪ sj .Ordпроходит только через запросы записи.
Отношение sn .Ord содержит все mo-ребрапо определению mo. Также оно содержит все Ord-ребра из кратчайшего пути полеммам 3 и 4. Из этого следует, что выбранный цикл присутствует в sn .Ord, чтопротиворечит ацикличности sn .Ord.3.6.3Определение машины ARM+τПо сравнению с ARM-машиной состояние машины ARM+τ обладает однойдополнительной компонентой H : Tid × P ath ⇀ Time × 2ReqSet × V. Эта компонента является частичной функцией, определяемой на экземплярах инструкций записи, которые завершили своё исполнение.
Каждому такому экземпляру(tid, path) функция сопоставляет (i) метку времени, (ii) множество запросов записи и барьеров S в подсистеме памяти, которые гарантировано предшествуютв смысле отношения Ord запросу экземпляра (tid, path), если такой запрос присутствует в подсистеме, и (iii) фронт сообщения в стиле обещающей модели: полокации ℓ он возвращает метку времени, которая является максимальной средизапросов записи в эту локацию из множества S. Для краткости мы определяем100labelProg ⊢ s −−−→ s′ARMlabel ̸∈ {Propagate _ _, Write commit _ _ _ _}labelProg ⊢ ⟨s, H⟩ −−−−→ ⟨s′ , H⟩ARM +τPropagate e tidProg ⊢ s −−−−−−−−→ s′′′ARMs .Ord ∪ tedges(s .Evt, Hτ ) ацикличноPropagate e tidProg ⊢ ⟨s, H⟩ −−−−−−−−→ ⟨s′ , H⟩ARM +τWrite commit tid path ℓ valProg ⊢ s −−−−−−−−−−−−−−→ ⟨M′POP , iordf′ , tapef′ ⟩′ARMtapef (tid, path) = W (com im ℓ val) tape ≜ s.tapef(tid)time-range(im, ℓ, τ, tid, path, tape, H) coherent-thread(ℓ, τ, path, tape, H)uniq-time-loc(ℓ, τ, s.tapef, H) pathsy ≜ lastsy(tape, path)S ≜ if pathsy ̸= []then {⟨tid, pathsy , dmb⟩} ∪ prev-Ord-req(tid, pathsy , tape, H)else ∅S ′ ≜ if im then S ∪ {⟨tid, path, wr ℓ : val⟩} else Sview ≜ [ℓ@τ] ⊔ viewf(tid, pathsy , pathsy , tape, H)H′ ≜ H[(tid, path) 7→ (τ,S ′ ,view)]M′POP .Ord ∪ tedges(M′POP .Evt, H′τ ) ацикличноWrite commit tid path ℓ val τProg ⊢ ⟨s, H⟩ −−−−−−−−−−−−−−−→ ⟨⟨M′POP , iordf′ , tapef′ ⟩, H′ ⟩ARM +τРис.
28. Переходы машины ARM+τпроекции компоненты H: Hτ : Tid × P ath ⇀ Time, H⩽ : Tid × P ath ⇀ 2ReqSet , иHview : Tid × P ath ⇀ V. Компонента H начального состояния машины ARM + τ,ainit ≜ ⟨sinit , Hinit ⟩, присваивает нулевые метки времени всем инициализирующимзаписям: Hinit ≜ [(0tid , []) 7→ ⟨0, λℓ. 0, ∅⟩].Правила переходов машины ARM+τ приведены на рис. 28. Первое правило транслирует все переходы ARM-машины в переходы машины ARM+τ, кромеУведомление потока и Завершение записи; при этом компонента H в правилене используется.
Новое правило Завершение записи обновляет компоненту H, иоба правила Уведомление потока и Завершение записи имеют общее ограничение — объединение отношения Ord и отношения tedges, построенного по меткам101времени, должно быть ациклично. При этом tedges определяется так:tedges(Evt, Hτ ) ≜{(e, e′ ) ∈ Evt × Evt |e, e′ — запросы записи, e.loc = e′ .loc, Hτ (e.tid, e.path) < Hτ (e′ .tid, e′ .path)}.Остальные правила не могут добавить циклов в упомянутое объединение, поэтому в них не требуется такая проверка.Рассмотрим подробнее правило Завершение записи. Оно выбирает метку времени τ, которая должна быть уникальна среди запросов записи в локацию ℓ (предикат uniq-time-loc).
Кроме того, эта метка должна быть согласована с метками времени выполненных экземпляров записи в эту локацию (предикат coherent-thread): τ должно быть больше, чем метки времени предшествующих экземпляров, и меньше последующих. Правило Завершение записи ARMмашины не отправляет запрос на запись (im = false), если существует следующийзавершенный экземпляр записи в ту же локацию. Тем не менее, машина ARM + τприсваивает метку времени завершаемому экземпляру записи и в таком случае.При этом метка времени экземпляра, запрос которого был отправлен в подсистемупамяти, имеет целочисленное значение, а метка времени экземпляра без запросовв подсистеме находится в интервале (τ′ − 1, τ′ ), где τ′ — это метка времени ближайшего последующего завершенного экземпляра записи в ту же локацию, чейзапрос был отправлен (предикат time-range).Если запрос на запись, который мы обозначим w, отправлен в подсистему хранения (im = true), и существует предшествующий экземпляр sy-барьера(pathsy ̸= []), то множество запросов, которые гарантировано предшествуют wв отношении Ord (функция H⩽ ), включает три набора запросов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
