Диссертация (1149932), страница 23
Текст из файла (страница 23)
Для любой программы P rog, результата её компиляции P rogARM иARM-согласованного сценария поведения G программы P rogARM существует такой сценарий поведения обещающей машины, что финальное состояние памятимашины совпадает с состоянием памяти G.Здесь под “финальным состоянием памяти”, также как и в случае корректностикомпиляции для ARMv8 POP, понимается, в случае обещающей семантики, значение последних записей в локации (т.е.
записей с наибольшими метками времени), а в случае ARMv8.3 — события-максимумы в отношении частичного порядка G.mo. Обе модели заданы в существенно разных стилях и, следовательно,имеют множество концептуальных отличий. Их необходимо преодолеть для доказательства теоремы 5. Главным отличием этих моделей является то, что обещающая модель памяти представлена операционно, в терминах шагов некоторойабстрактной машины, а модель ARMv8.3 является аксиоматической и задаёт семантику сценария поведения программы в виде графа с определёнными свойствами.
Для преодоления этого отличия вводится операционная семантика обхода графа ARM-согласованного сценария поведения, шаги которой обещающая машинаможет непосредственно повторять (раздел 4.3). Другим существенным отличиемявляются те способы, которыми данные модели запрещают “плохие” сценарии.Например, такие как чтение потоком старой записи в x в случае, если поток ужевыполнял чтение из более новой записи в x.
Для предотвращения этой ситуациимодель ARMv8.3 использует аксиомы, которые проверяют отсутствие циклов вграфе, а обещающая модель в этом случае использует фронты потоков и сообщений. Для того, чтобы обойти описанное различие между моделями, вводятся117дополнительные отношения на вершинах ARM-согласованного сценария поведения, которые тесно связаны с фронтами обещающей модели (раздел 4.4).
С использованием этих идей и техники симуляции доказывается теорема 5 (раздел4.5).4.3Обход ARM-согласованного сценарияВ этом разделе сначала вводятся вспомогательные определения, затем формализуется понятие шага обхода и доказывается существование последовательности шагов, которые полностью обходят любой ARM-согласованный сценарийповедения (теорема 6).Определение 7. Конфигурацией обхода для ARM-согласованного сценария поведения G называются множества ⟨C, I⟩ такие, что:– C ⊆ G.E,– dom(G.po; [C]) ⊆ C,– C ∩ G.W ⊆ I ⊆ G.W.Элементы C мы будем называть покрытыми (covered) событиями, а I — выпущенными (issued) событиями.Покрытые события при симуляции будут соответствовать префиксу программы, который исполнен обещающей машиной, а выпущенные — записями,находящимся в памяти обещающей машины в соответствующий момент исполнения.Определение 8.
Начальной конфигурацией ARM-согласованного сценария поведения G называется пара ⟨G.E0 , G.E0 ⟩, где G.E0 — это множество инициализирующих записей.Начальная конфигурация является конфигурацией обхода, посколькуG.E0 ⊆ G.E, dom(G.po; [G.E0 ]) = ∅ и G.E0 ∩ G.W = G.E0 .Определение 9. Для сценария поведения G и его покрытия C ⊆ G.E множествомследующих событий Next(G, C) называется множество, состоящие из событий,для которых все po-предшествующие события уже покрыты:Next(G, C) ≜ {b ∈ G.E | dom(G.po; [b]) ⊆ C} \ C.118При симуляции данное множество будет содержать по одному событию длякаждого ещё не завершённого в обещающей машине потока, причём события будут соответствовать следующему переходу в потоке — т.е. переходу, который неявляется обещанием. Так, если бы обещающая семантика была определена поверхнекоторого синтаксиса, то множество следующих событий соответствовало быинструкциям, на которые указывают счётчики команд потоков (program counters)в обещающей модели.Определение 10.
В конфигурации обхода ⟨C, I⟩ событие a является покрываемымдля сценария поведения G и обозначается a ∈ Coverable(G, C, I), если событиеa является:– событием чтения, и связанное с ним событие записи оказывается выпущенным (a ∈ G.R и rf−1 (a) ∈ I),– или выпущенным событием (a ∈ I),– или барьером памяти (a ∈ G.F).В нашем обходе, заданном операционным способом, имеется шаг, который“покрывает” событие, т.е.
добавляет его во множество покрытых. Событие, которое покрывается данным правилом, должно соответствовать представленнымвыше ограничениям. Эти ограничения, в свою очередь, соответствуют ограничениям обещающей машины. Например, обещающая машина может прочитать изнекоторого конкретного сообщения только тогда, когда данное сообщение есть впамяти, т.е.
соответствующее ему событие w уже выпущено (w ∈ I).Определение 11. Для сценария G событие w называется выпускаемым в конфигурации обхода ⟨C, I⟩, w ∈ Issuable(G, C, I), если выполнены следующие условия:– w является событием записи (w ∈ G.W);– все po-предшествующие барьеры покрыты (dom([F]; G.po; [w]) ⊆ C);()– все записи других потоков, от которых зависит w, выпущены()(dom(G.rfe; G.dob+ ; [w]) ⊆ I).Если шаг обхода “выпускает” событие записи, то при симуляции он соответствует обещанию, которое делает обещающая машина. Ограничениеявляется более строгим, чем необходимо для симуляции — в обещающей моделиобещание может быть сделано “через” приобретающий барьер, который соответствует fence(ld) в ARMv8.3.
Тем не менее, более строгое ограничение позволяет119упростить симуляцию. Ограничениетребуется для того, чтобы обещающая модель могла сертифицировать обещание, которое она делает. Шаги обходазадаются так:a ∈ Next(G, C) ∩ Coverable(G, C, I)w ∈ Issuable(G, C, I) \ IG ⊢ ⟨C, I⟩ →TC ⟨C ∪ {a}, I⟩G ⊢ ⟨C, I⟩ →TC ⟨C, I ∪ {w}⟩Здесь левое правило покрывает событие, если оно принадлежит множеству следующих за ним событий и при этом покрываемо в данной конфигурации.
Правоеправило выпускает событие записи, если событие выпускаемо и при этом ещё невыпущено.Для того, чтобы использовать предложенный метод обхода в доказательствекорректности компиляции, нужно показать, что для любого ARM-согласованногосценария поведения существует его полный обход, т.е. обход, который покрываетвсе события из этого сценария.Теорема 6. Для любого ARM-согласованного сценария поведения G существуетобход G ⊢ ⟨G.E0 , G.E0 ⟩ →∗TC ⟨G.E, G.W⟩.Доказательство теоремы основано на следующих вспомогательных леммах.Лемма 9.
Пусть пара множеств ⟨C, I⟩ является достижимой конфигурацией обхода ARM-согласованного исполнения G, т.е. G ⊢ ⟨G.E0 , G.E0 ⟩ →∗TC ⟨C, I⟩. Тогдавсе события из множества C покрываемы (C ⊆ Coverable(G,C,I)), а события изI выпускаемы (I ⊆ Issuable(G,C,I)).Доказательство. Утверждение леммы следует из определений отношенийCoverable и Issuable, а также из того, что размеры множеств покрытых и выпущенных событий при обходе G увеличиваются.Лемма 10. Пусть пара множеств ⟨C, I⟩ является достижимой конфигурацией обхода ARM-согласованного исполнения G, т.е.
G ⊢ ⟨G.E0 , G.E0 ⟩ →∗TC ⟨C, I⟩. Тогдавсе события записи, которые являются элементами множества следующих событий, являются выпускаемыми, т.е. W ∩ Next(G, C) ⊆ Issuable(G,C,I).Доказательство. Зафиксируем w ∈ W ∩ Next(G, C) и покажем, что w ∈Issuable(G, C, I). Т.к. w ∈ Next(G, C), то все po-предшествующие события являются покрытыми (т.е. находятся в C). Из этого следует, что выполняется-120. Кроме того, из леммы 9 следует, что все покрытые события являются покрываемыми.
Таким образом, можно заключить, что выполняется,азначит, для w принадлежит Issuable(G, C, I).Доказательство теоремы 6. ПосколькукаждыйконкретныйARMсогласованный сценарий поведения является конечным графом, а шаги обходанаращивают конфигурации, то для доказательства наличия полного обхода графадостаточно показать, что для каждой не конечной конфигурации существует шагк новой конфигурации. А именно, что для любой конфигурации обхода ⟨C, I⟩ сценария G, достижимой из начальной конфигурации (G ⊢ ⟨G.E0 , G.E0 ⟩ →∗TC ⟨C, I⟩),множество покрытых событий которой не полно (C ̸= G.E), существуют такие C ′и I ′ , что G ⊢ ⟨C, I⟩ →TC ⟨C ′ , I ′ ⟩. Покажем это.Зафиксируем ⟨C, I⟩.
Нам известно, что Next(G, C) ̸= ∅, т.к. C ̸= G.E.Рассмотрим два следующих случая: (i) существует элемент Next(G, C), который покрываем, или сначала выпускаем, а потом покрываем; (ii) все элементыв Next(G, C) не покрываемы и не выпускаемы (для этого случая мы показываем,что в G существует событие записи, которое выпускаемо в данной конфигурации).Случай 1. Зафиксируем элемент a ∈ Next(G, C).
Если a ∈ R и rf−1 (a) ∈ I,или a ∈ F, или a ∈ W ∩ I, тогда a покрываем по определению. Если a ∈ W \ I, тогдаa является выпускаемым по лемме 10.Случай 2. Мы предполагаем, что не существует события из Next(G, C),которое покрываемо или выпускаемо. Таким образом Next(G, C) ⊆ R являетсяследствием леммы 10 и определения покрываемого события. Кроме того, для любого чтения события r из Next(G, C) мы знаем, что rf−1 (r) ̸∈ I. Далее покажем,что существует событие записи, которое выпускаемо в данной конфигурации. Дляэтого введём вспомогательное отношение eord ≜ (obs ∪ dob ∪ bob)+ , котороеантирефлексивно по определению ARM-согласованности ().Мы знаем, что имеется, как минимум, одно событие (чтения) из Next(G, C),которое при этом не покрываемо.
Это означает, что существует событие записи,которое ещё не выпущено. Выберем событие записи w ∈ W \ I, которое являетсяминимальным среди не выпущенных записей по отношению eord, т.е. ∄w′ ∈ W \I. eord(w′ , w). Осталось показать, что событие w выпускаемо.Т.к. w ̸∈ Next(G, C), то существует событие чтения r ∈ Next(G, C) такое,что po(r, w) и rf−1 (r) ̸∈ I. При этом rf−1 (r) = rfe−1 (r), т.к. C ∩ W ⊆ I и121∀e ∈ C.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
