Диссертация (1149932), страница 20
Текст из файла (страница 20)
Первый набор состоит из запроса предшествующего барьера ⟨tid, pathsy , dmb⟩. Второй набор включает запросы экземпляров записи, предшествующие экземпляру pathsy ,prev-Ord-req(tid, pathsy , tape, H). Третий набор является объединением множествH⩽ (e.tid, e.path) за каждый запрос записи e, прочитанный потоком до экземпляраpathsy :prev-Ord-req(tid, pathsy , tape, H) ≜{⟨tid : path′ @ℓ′ ,val′ ⟩ | path′ < pathsy , tape(path′ ) = W (com _ ℓ′ val′ )} ∪∪{H⩽ (e.tid, e.path) | path′′ < pathsy , tape(path′′ ) = R (sat com e)}.Почему все эти запросы гарантировано предшествуют запросу w в отношении Ord? Во-первых, все запросы, кроме f ≜ ⟨tid, pathsy , dmb⟩, предшествуют102f , т.к. в момент добавления f подсистема памяти добавила по Ord-ребру (e, f )за каждый запрос e, о котором был осведомлён поток.
Последнее верно в силуследующих рассуждений. О каждом запросе записи e′ , который был отправленпотоком до отправки f , поток естественным образом осведомлён. О каждом запросе записи e′′ , который был прочитан потоком до отправки f , поток осведомлёнпо ограничениям подсистемы памяти. Эти ограничения гарантируют, что запросчтения может получить ответ из запроса записи, только если о них осведомленыодни и те же потоки.Во-вторых, когда поток отправляет запрос w, он добавляет ребро (f, w) вотношение Ord. Значит все упомянутые выше запросы также предшествуют w вотношении Ord в силу транзитивности Ord.Новое вхождение в функцию Hview определяется как поточечный максимум(операция ⊔) на фронтах [ℓ@τ] и viewf(tid, pathsy , pathsy , tape, H), гдеviewf(tid, pathwrite , pathread , tape, H) ≜⊔⊔com-writes-time(tid, pathwrite , tape, H) ⊔ sat-reads-view(pathread , tape, H)определяет фронт запросов из вхождения H⩽ :com-writes-time(tid, path, tape, H) ≜{[ℓ@τ] | path′ < path, tape(path′ ) = W (com _ ℓ _), τ = Hτ (tid, path′ )} ∪{[ℓ@τ] | tid′ , path′ , path′′ < path, τ = Hτ (tid′ , path′ ) ̸= ⊥,tape(path′′ ) = R (sat sat-state ⟨tid′ , path′ , wr ℓ : _⟩), sat-state ̸= inflight}.sat-reads-view(path, tape, H) ≜{Hview (tid′ , path′ ) ̸= ⊥ | ∃ℓ, tid′ , path′ , path′′ < path,tape(path′′ ) = R (sat sat-state ⟨tid′ , path′ , wr ℓ : _⟩), sat-state ̸= inflight}.3.6.4 Симуляция модели ARMv8 POPКак было описано в предыдущем разделе, переходы машины ARM+τ являются переходами ARM-машины с дополнительными ограничениями, что потенциально может означать уменьшение допускаемых сценариев поведения.
Поскольку это бы означало, что мы не смогли бы использовать ARM+τ как промежуточную машину в доказательстве корректности компиляции, то нужно показать,что все сценарии поведения ARMv8 POP также являются сценариями поведенияARM+τ с точностью до компоненты состояния H.103Теорема 3. Пусть набор состояний {si }i∈[0..n] является исполнением программыProg в ARM-машине. Тогда существует такой набор {Hi }i∈[0..n] , что {⟨si , Hi ⟩}i∈[0..n]является исполнением программы Prog в ARM+τ-машине.∀Prog, {si }i∈[0..n] . s0 = sinit ∧ FinalARM (sn , Prog) ∧Prog ⊢ s0 −−−→ ...
−−−→ sn ⇒ ∃{Hi }i∈[0..n] . H0 = ainit .H ∧ARM00ARMProg ⊢ ⟨s , H ⟩ −−−−→ ... −−−−→ ⟨sn , Hn ⟩.ARM +τARM +τДоказательство. В разделе 3.6.2 было показано, как по финальному состояниюв сценарии поведения ARMv8 POP построить отношение mo и функцию mapτ :req ⇀ τ. Здесь мы также строим их по состоянию sn , но с небольшим изменением:мы предполагаем, что функция mapτ задана на экземплярах инструкций, т.е. намножестве Tid × P ath, а не на запросах. Это изменение имеет только стилистический характер, т.к.
по запросу однозначно восстанавливается идентификаторэкземпляра инструкции, кроме случая инициализирующих запросов.Мы конструируем множество {Hi }i∈[0..n] индуктивно. Начальная компонента H0 равна ainit .H. Также мы используем следующий инвариант для состоянийсценария поведения ARM+τ:inv(s, H) ≜ ∀tid, path.(s.tapef(tid, path) = W (com true _ _) ⇒ Hτ (tid, path) = mapτ (tid, path)) ∨(s.tapef(tid, path) ̸= W (com _ _ _) ⇒ Hτ (tid, path) = ⊥).Инвариант утверждает, что метки времени, полученные в ходе исполнения вARM+τ, соответствуют функции mapτ .
Предположим, что мы сконструировали i первых состояний сценария поведения ARM+τ, и инвариант выполняетсяна них. Докажем индукционный переход, рассмотрев различные варианты шагаProg ⊢ si −−−→ si+1 .ARMУведомление потока. Выберем Hi+1 равным Hi . Тогда утверждение inv(si+1 , Hi+1 ) выполняется, т.к. выполняется inv(si , Hi ) иsi+1 .tapef = si .tapef. В разделе 3.6.2 было доказано, что для любого j ∈ [0..n]отношение mo↾sj .Evt ∪ sj .Ord ациклично. Утверждение inv(si+1 , Hi+1 ) гарантирует, что функция mo↾si+1 .Evt равна tedges(si+1 .Evt, Hi+1τ ). Тогдаотношение si+1 .Ord ∪ tedges(si+1 .Evt, Hi+1τ ) ациклично.
Таким образом,все дополнительные ограничения правила Уведомление потока машиныARM+τ выполнены, и она может совершить соответствующий переход.104Завершение записи tid path. Нам нужно рассмотреть два случая.Если соответствующий запрос записи отправлен в подсистему памяти, томы выбираем ему метку времени τ, которая является параметром перехода в машине ARM+τи равна mapτ (tid, path). Мы выбираем Hi+1 в соответствии с определением этой компоненты в правиле Завершение записи машины ARM+τ. Инвариант, очевидно, выполняется по определению. По определению функции mapτ метка времени τ уникальна средизапросов записи в соответствующую локацию. Ацикличность отношенияsi+1 .Ord ∪ tedges(si+1 .Evt, Hi+1τ ) следует из тех же рассуждений, что и впредыдущем случае.
Из этого, в свою очередь, следует, что τ больше всехостальных меток времени запросов записи в ту же локацию среди тех, чтобыли отправлены тем же потоком в подсистему памяти. Метка τ такжебольше всех меток времени предшествующих завершенных экземпляровзаписи в ту же локацию, которые не отправляли запросы, как следствиепринципа выбора метки времени. В плёнке потока нет последующих завершенных записей в ту же локацию, т.к.
запрос был отправлен, следовательно метка времени τ корректна относительно других записей потока.Если запрос записи не был отправлен, то mapτ (tid, path) = ⊥. Известно,что существует последующий экземпляр записи в ту же локацию с меткойвремени τ′ , который отправил запрос в подсистему памяти. Мы выбираемметку времени τ из интервала (τ′ − 1, τ) так, чтобы она была корректнаотносительно требований перехода машины ARM+τ. Мы выбираем Hi+1 всоответствии с переходом Завершение записи машины ARM+τ. При этоминвариант, очевидно, сохраняется.Другие переходы. Мы выбираем компоненту Hi+1 равной Hi . Поскольку востальных правилах машины ARM+τ нет дополнительных ограничений,то машина может сделать соответствующий переход, и при этом инвариантсохранится.3.6.5Фронты машины ARM+τВ разделе 3.2.1 была рассмотрена программа MP-SY-LD.
В ней использование барьеров памяти позволяет запретить слабый сценарий поведения. Для таких целей в обещающей модели используются фронты. Для того, чтобы показать,105что обещающая машина может симулировать машину ARM+τ, вводится аналогфронтов для ARM+τ.Введём фронт viewARM — аналог базового фронта обещающей машины:viewARM (a, tid, path) ≜⊔com-writes-time(tid, path, a.tapef(tid), a.Hτ ) ⊔⊔sat-reads-view(lastCF(tape, path), a.tapef(tid), a.Hview ) .В отличие от viewcur , который определяется в целом для потока, фронт viewARM дополнительно параметризован путём path из тех же соображений, что и состояниепеременных в ARMv8 POP параметризовано путём: машина ARM+τ может исполнять экземпляры не по порядку, поэтому разные экземпляры могут иметь разные ограничения, связанные с метками времени.
Определение фронта viewARMпохоже на определение компоненты Hview в правиле Завершение записи: этотфронт является композицией одинарных фронтов [ℓ@τ], где ℓ и τ — параметры завершенного экземпляра записи, который предшествует path, со значениямиHview , связанными c запросами записи, которые прочитаны потоком до последнего выполненного барьера lastCF(tape, path), предшествующего path.
При этомучитываются и ld, и sy барьеры, так как они оба могут быть использованы какрезультат компиляции приобретающего барьера в обещающей модели.С помощью определения viewARM нужные ограничения задаются следующим образом. Если экземпляр чтения (tid, path) получил ответ от завершенногоэкземпляра записи, то метка времени этой записи не меньше соответствующегозначения viewARM для пути path. Мы не ограничиваем чтения, которые получилиответ от ещё не завершенной записи, так как такие записи не обладают меткамивремени. Аналогично, каждый завершенный экземпляр записи имеет метку времени, превосходящую соответствующее значение viewARM . Упомянутые ограничения формулируются в виде следующей теоремы.Теорема 4.
Пусть состояние ARM+τ-машины a достижимо из начального. Тогдаметка времени завершённого экземпляра записи в локацию ℓ не меньше, чем значение фронта viewARM по этой локации для экземпляра чтения, прочитавшего изэтой записи. Кроме того, метка времени завершённого экземпляра записи больше,106чем значение фронта viewARM для самого экземпляра записи.∀Prog, a, tid, tape = a.tapef(tid), path. Prog ⊢ ainit −−−−→∗ a ⇒ARM +τ(∀e. tape(path) = R (sat _ e) ∧ a.tapef(e.tid, e.path) завершён ⇒a.Hτ (e.tid, e.path) ⩾ viewARM (a, tid, path, e.ℓ)) ∧(∀ℓ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
