Автореферат (1149930), страница 3
Текст из файла (страница 3)
Vafeiadis и D. Dreyer была представлена обещающая модельпамяти, которая очень близка OpC11, но использует другой механизм для выполнения инструкций не по порядку. Этот механизм позволяет поддержать большекомпиляторных оптимизаций, чем модель OpC11. Из-за данного преимуществадиссертант принял решение продолжить свою исследовательскую работу в рамках обещающей модели.В третьей главе приводится описание обещающая модель памяти и операционной модели ARMv8 POP, а также представлено доказательство корректности компиляции из существенного подмножества обещающей модели памятив модель ARMv8 POP.9Обещающая модель памяти является операционной моделью для синтаксиса модели C/C++11.
Она использует те же базовые понятия, что и предложенная диссертантом модель OpC11, метки времени и фронты, однако вместо механизма откладывания выполнения инструкций она, в соответствии со своим названием, использует механизм обещаний. Так, в каждый момент исполнения поток обещающей модели памяти может совершить одно из двух действий: либовыполнить следующую инструкцию, либо пообещать сделать запись в локацию.Последнее может быть выполнено вне зависимости от того, какая инструкция является следующей.
Если поток выбирает пообещать сделать запись в локацию,то он добавляет соответствующее сообщение в память, делая это сообщение видимым для других потоков. Далее в ходе исполнения поток должен будет выполнить соответствующую инструкцию записи, таким образом выполняя сделанноеранее обещание.Для того, чтобы запретить “значения из воздуха”, после каждого исполненного шага каждый поток должен выполнить т.н. сертификацию — предъявить,что он может быть локально исполнен таким образом, что выполнит все оставшиеся обещания. Известно, что задача сертификации является алгоритмическинеразрешимой для языков, полных по Тьюрингу. Следовательно, для обещающей модели невозможно разработать интерпретатор, что является её недостатком по сравнению с представленной в диссертации моделью OpC11.Несмотря на этот недостаток, обещающая модель обладает рядом существенных достоинств.
В частности, обещающая модель не имеет проблемы “значений из воздуха”, что делает возможным для неё разработать выразительнуюпрограммную логику. Также для модели была доказана корректность существенного класса компиляторных оптимизаций и корректность эффективной компиляции в модели памяти процессоров x86 и Power.Открытой проблемой является доказательство корректности компиляциииз обещающей модели памяти в модели памяти архитектуры ARM, которая, наравне с x86 и Power, является одной из наиболее распространённых процессорных архитектур на данный момент.Здесь и далее под корректностью компиляции понимается следующееутверждение.Определение.
Для языков L и L′ с моделями памяти M и M ′ соответственносхема компиляции compile : L → L′ называется корректной, если выполняетсяследующее условие:∀P rog ∈ L. Jcompile(P rog)KM ′ ⊆ JP rogKM ,где JP rogKM — множество результатов сценариев поведения программы P rogв модели памяти M .
В доказательствах корректности компиляции в ARMv8 POPи ARMv8.3 результатом сценария поведения считается финальное состояние памяти.Рассмотренное подмножество обещающей модели памяти (Promise) состоит из расслабленных (relaxed, rlx) записей и чтений, а также высвобождаю10щих (release, rel) и приобретающих (acquire, acq) барьеров памяти. При этом подразумевается следующая схема компиляции:Promise:[x]rlx := aARMv8 POP: [x] := aa := [x]rlxa := [x]fence(acq)fence(ld)fence(rel)fence(sy)Первый и второй столбцы подразумевают, что расслабленные операции записи и чтения из языка, на котором определена обещающая модель, переходят вобычные операции записи и чтения в терминах ARMv8-ассемблера, а приобретающий и высвобождающий барьеры — в барьер по чтению и в полный барьер.Такая схема компиляции считается эффективной и применяется в компиляторахGCC и LLVM.
Поскольку схема компиляции в данном случае является биекцией, то далее в этой главе предполагается, что язык задания обещающей и ARMv8POP моделей совпадает.Основной результат главы сформулирован следующим образом.Теорема. Для любой программы Prog на языке задания модели и её сценарияповедения в модели ARMv8 POP существует такой сценарий поведения Prog вобещающей модели, что финальное состояние памяти в сценариях поведениясовпадает.В рамках доказательства теоремы по сценарию поведения программы в модели ARMv8 POP строится сценарий поведения в обещающей модели. Поскольку обе модели заданы операционным способом, то существуют две абстрактныемашины, которые представляют данные модели. Обычно для решения задачи построения сценария поведения одной машины по сценарию другой используюттехнику симуляции, которая является специальной формой индукции.
В рамкахданной техники вводится отношение симуляции, которое связывает состояниямашин, и доказываются две следующие леммы: отношение симуляции связывает начальные состояния машин (база индукции); для любого шага симулируемой машины существует ноль или более шагов симулирующей машины, послевыполнения которых новые состояния машин опять связаны отношением симуляции (индукционный переход).В доказательстве индукционного перехода сложным является то, что между моделями имеется два существенных различия. Во-первых, обещающая модель может исполнять не по порядку только инструкции записи, в то время какмодель ARMv8 POP может исполнять инструкции в несколько шагов, не по порядку и спекулятивно.
Во-вторых, в обещающей модели в тот момент, когда сообщение попадает в память, этому сообщению присваивается некоторая меткавремени, которая служит его порядковым номером в множестве сообщений, относящихся к той же локации. В модели ARMv8 POP меток времени нет и порядок сообщений одной локации определяется не сразу после того, как сообщенияпопадут в её подсистему памяти и станут видимыми для других потоков.Для того, чтобы обойти первое различие, автор использовал технику “запаздывающей” симуляции.
В рамках данной техники отношение симуляциипредставляется как объединение двух взаимоисключающих отношений, напри11мер, A и B. Далее индукционный переход формулируется следующим образом.Если состояние симулируемой машины x связано с состояние симулирующеймашины y отношением A, т.е. выполняется (x,y) ∈ A, то для любого состоянияx′ , в которое может перейти симулируемая машина, выполняется (x′ , y) ∈ A∪B.С другой стороны, если (x, y) ∈ B, то существует состояние y ′ , в которое может перейти симулирующая машина, что (x, y ′ ) ∈ A ∪ B.
Тогда при условии,′что не существует такой бесконечной цепочки {yi′ }i∈N , что yi′ переходит yi+1и′(x, yi ) ∈ B для всех i, из нового варианта индукционного перехода следует изначальное утверждение симуляции.В доказательстве теоремы отношение A символизирует, что обещающаямашина ждёт, пока ARM-машина выполнит действие, которое обещающая машина может повторить, а отношение B означает, что обещающая машина можетсимулировать несколько действий, уже выполненных ARM-машиной.Для того, чтобы снять второе различие между обещающей и ARMv8 POPмоделями, в доказательстве определяется ограниченная версия ARM-машины,которая добавляет метки времени к сообщениям записи в подсистеме памяти,тем самым определяя порядок на сообщениях к одной локации раньше, чем этоделает обычная ARMv8 POP модель.
Это изменение также добавляет дополнительные ограничения на сценарии поведения ARM-машины. Тем не менее, автор приводит доказательство того, что новая модель эквивалентна исходной, чтопозволяет свести доказательство теоремы к доказательству корректности компиляции из обещающей модели в модифицированную ARMv8 POP модель.В четвертой главе обсуждается аксиоматическая модель памятиARMv8.3. Приводятся рассуждения о том, почему метод доказательства корректности компиляции из обещающей модели памяти, использованный её авторами для аксиоматических моделей архитектур x86 и Power, не подходит длямодели ARMv8.3.
Далее приводится доказательство корректности компиляциииз обещающей модели памяти в подмножество модели ARMv8.3. Доказательство основано на построении операционной семантики обхода аксиоматическихсценариев поведения программ в модели ARMv8.3.В рамках аксиоматической (или декларативной) модели памяти сценарийповедения программы представляется в виде графа, в котором вершинами являются события (операции над памятью), а ребрами — различные отношенияна событиях, такие как программный порядок, отношение “читает из” и др.
Приэтом граф считается согласованным с моделью, если выполняются аксиомы модели, которые обычно формулируются как наличие некоторого полного порядкана подмножестве событий или отсутствие в графе путей определённого типа.При доказательстве корректности компиляции из обещающей модели в аксиоматическую техника симуляции напрямую неприменима, поскольку сценарий поведения в аксиоматической модели не является последовательностью шагов исполнения некоторой абстрактной машины. Поэтому в доказательстве корректности компиляции в модели x86 и Power авторы использовали другой метод. Этот метод состоит из двух частей.
Во-первых, доказывается, что модели12x86 и Power могут быть представлены как набор программных оптимизаций поверх более простых моделей. Эти оптимизации являются доказано корректнымив рамках обещающей модели, из чего следует, что доказательство корректностикомпиляции может быть сведено к аналогичному доказательству для более простых моделей. Далее показывается, что эти более простые модели могут бытьсимулированы моделью, которая является аксиоматическим аналогом обещающей модели без механизма обещаний.Автору работы не удалось применить такой подход для модели ARMv8.3,поскольку эта модель не представима как набор тех же оптимизаций над упрощенной моделью.
Поэтому был разработан альтернативный подход, который заключается в построении операционной семантики обхода аксиоматических сценариев поведения, которая может быть непосредственно симулирована обещающей моделью.Обходом в диссертационном исследовании называется последовательность переходов между конфигурациями исполнения — упорядоченными парами подмножеств вершин сценария поведения ⟨C, I⟩. Подмножество C называется множеством покрытых событий, а подмножество I — множествомвыпущенных событий; элементы этих подмножеств называются покрытыми ивыпущенными соответственно.Конфигурация обхода называется корректной, если выполняются следующие условия.– Множество покрытых событий префикс-замкнуто по отношению программного порядка.– Множество выпущенных событий содержит только события записи.– Если событие записи покрыто, то оно также является выпущенным.При доказательстве симуляции обещающей моделью обхода покрытые событиябудут соответствовать инструкциям, выполненным обещающей машиной, а выпущенные события — сообщениям в памяти обещающей машины.Шаги обхода задаются следующим образом:a ∈ Next(G, C) ∩ Coverable(G, C, I)G ⊢ ⟨C, I⟩ →TC ⟨C ∪ {a}, I⟩w ∈ Issuable(G, C, I) \ IG ⊢ ⟨C, I⟩ →TC ⟨C, I ∪ {w}⟩Здесь первое правило соответствует покрытию события a, а второе — выпускусобытия w; Next(G, C) — обозначает множество событий, непосредственно следующих в отношении программного порядка за покрытыми; Coverable(G, C, I)и Issuable(G, C, I) — это события, покрываемые и выпускаемые в текущей конфигурации, которые определены в соответствии с требованиями обещающей модели к исполнению инструкции и обещанию сообщения соответственно.Далее автор работы приводит доказательство следующей теоремы о полноте обхода.Теорема.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
