Диссертация (1149932), страница 18
Текст из файла (страница 18)
Приэтом M ⊂ Msg — это память машины, являющаяся множеством сообщений вида⟨ℓ : val@τ,view⟩ : Msg, состоящих из целевой локации ℓ : Loc, значения val : Val,метки времени τ : Time = Q, и фронта сообщения view : V = Loc → Time.T S : Tid → TS — это функция, которая по идентификатору потока возвращаетего состояние. Состояние потока TS : TS является тройкой ⟨σ, V, promises⟩, где σ— это локальное состояние потока в рамках описанной ниже помеченной системыпереходов (labeled transition system, LTS), V = ⟨viewcur ,viewacq ,viewrel ⟩ : V × V × V93(-)()cur(ℓ) < tR = rel ⊔ [ℓ@τ]′cur = cur ⊔ [ℓ@τ]acq′ = acq ⊔ cur′cur(ℓ) ⩽ tcur = cur ⊔ [ℓ@τ]acq′ = acq ⊔ cur′′R(ℓ,τ,R)W(ℓ,τ,R)⟨cur,acq,rel⟩ −−−−→ ⟨cur′ ,acq′ ,rel⟩⟨cur,acq,rel⟩ −−−−→ ⟨cur′ ,acq′ ,rel⟩(()W(ℓ,v)⟨ℓ : v@τ,R⟩ ∈ MR(ℓ,v)R(ℓ,τ,R)σ −−−→ σ′V −−−−→V ′⟨⟨σ, V, P ⟩, M ⟩ −−−−−−→ ⟨⟨σ′ , V ′ , P ⟩, M ⟩⟨⟨σ, V, P ⟩, M ⟩ −−−−−−→ ⟨⟨σ′ , V ′ , P ′ ⟩, M ′ ⟩Promise tid(-Promise tid)(F(acq)W(ℓ,τ,R)σ −−−→ σ′V −−−−→V ′m = ⟨ℓ : v@τ,R⟩′′′∀v , view .
⟨ℓ : v @τ,view′ ⟩ ̸∈ MM ′ = M ∪ {m}P ′ = P \ {m})-)F(rel)′σ −−−−→ σ′σ −−−−→ σ⟨⟨σ, ⟨cur,acq,rel⟩, P ⟩, M ⟩ −−−−−−→⟨⟨σ, ⟨cur,acq,rel⟩, ∅⟩, M ⟩ −−−−−−→Promise tidPromise tid⟨⟨σ′ , ⟨acq,acq,rel⟩, P ⟩, M ⟩()⟨⟨σ′ , ⟨cur,acq,cur⟩, ∅⟩, M ⟩(σ−→ σ′)∀v, view. ⟨m.ℓ : v@m.τ,view⟩ ̸∈ MP ′ = P ∪ {m}M ′ = M ∪ {m}∀ℓ. ∃v, view.
⟨ℓ : v@m.view(ℓ),view⟩ ∈ M ′⟨⟨σ, V, P ⟩, M ⟩ −−−−−−→ ⟨⟨σ′ , V, P ⟩, M ⟩⟨⟨σ, V, P ⟩,M ⟩ −−−−−−→ ⟨⟨σ, V, P ′ ⟩,M ′ ⟩εPromise tid(Promise tid)⟨TS, M⟩ −−−−−−→ ⟨TS′ , M′ ⟩Promise tid⟨TS′ , M′ ⟩ −−−−−−→∗ ⟨TS′′ , M′′ ⟩Promise tidTS′′ .promises = ∅⟨T S[tid 7→ TS], M⟩ −−−−→ ⟨T S[tid 7→ TS′ ], M′ ⟩PromiseРис. 27. Переходы обещающей машины— это базовый, приобретающий и высвобождающий фронты потока, promises ⊂Msg — это множество сообщений, которые были обещаны потоком, но еще невыполнены.Обещающая модель памяти задана на помеченной системе переходов, а нена программах непосредственно. В приложении Г.1 приводится метод построения системы переходов по программе.
Метка в системе переходов может быть: (i)операцией чтения из локации ℓ значения v (R(ℓ,v)), (ii) операцией записи в локацию ℓ значения v (W(ℓ,v)), (iii) барьером памяти с модификатором fmod (F(fmod)),(iv) внутренним переходом (ε). Последний тип описывает действия потока, кото-94рые не затрагивают память, например, присваивание в локальную переменную иисполнение оператора условного перехода.Стоит отметить, что в работе [23], на основе которой написана эта глава,обещающая модель задана непосредственно на синтаксисе модели ARMv8 POP.Тем не менее, для того, чтобы не вводить разные определения в главах 3 и 4, в диссертации обещающая модель определяется “поверх” системы переходов.
Также вдоказательстве корректности компиляции автор диссертации исходит из предположения, что система переходов может быть восстановлена по программе согласовано со схемой компиляции и функциями вычисления значения модели ARMv8POP (см. приложения Г.1, Г.2 и Г.3).Перед исполнением любой программы память обещающей машины состоитиз записей во все локации Minit ≜ {⟨ℓ : 0@0,viewinit ⟩ | ℓ ∈ Loc}, где viewinit ≜ λℓ. 0.В целом начальное состояние машины выглядит так:pinit ≜ ⟨λtid. ⟨σ = σinit , V = ⟨viewinit , viewinit , viewinit ⟩, promises = ∅⟩, Minit ⟩.Перейдем к описанию шагов исполнения обещающей машины (см. рис.
27).Только правило () оперирует над всем состоянии машины, остальные правила заданы локально для потока. Правило () требует от потока, которыйсовершает локальный переход, провести сертификацию обещаний, т.е. показать,что существует изолированный запуск потока, в рамках которого он выполнит всесвои обещания.Выполнение приобретающего барьера () делает базовыйфронт потока viewcur , равным приобретающему фронту потока viewacq ,где последний является объединением фронтов сообщений, прочитанныхпотоком к этому моменту, и меток времени записей, произведенныхпотоком.Выполнение высвобождающего барьера ( ) делает высвобождающий фронт потока viewrel равным базовому фронту потока viewcur . Врезультате фронты сообщений, которые поток добавит в память после выполнения высвобождающего барьера, будут содержать информацию о записях, совершённых потоком до выполнения высвобождающего барьера.Кроме того, переход, соответствующий высвобождающему барьеру, имеет дополнительное ограничение — в момент его выполнения у потока недолжно быть невыполненных обещаний, т.е.
promises должен быть равенпустому множеству.95Чтение из локации ℓ () выполняется потоком следующим образом.Поток выбирает из памяти машины некоторое сообщение ⟨ℓ : val@τ,view⟩.При этом метка времени записи τ должна быть больше, чем значение базового фронта потока viewcur (ℓ), а само сообщение не должно находится вомножестве обещанных, но не выполненых потоком сообщений promises.Это правило увеличивает базовый фронт потока на [ℓ@τ], а приобретающий — на view.Обещание записи ⟨ℓ : val@τ,view⟩ () добавляет сообщение в память машины и в множество promises. При этом целевая локация ℓ и значение val могут быть произвольными, т.е.
они не зависят от локальногосостояния потока σ. Метка времени должна быть уникальной среди сообщений локации ℓ, уже находящихся в памяти. Этот переход не обновляетфронты потока. Также легко заметить, что этот переход недетерминирован,но ограничен сертификацией.Выполнение обещания ⟨ℓ : val@τ,view⟩ () удаляет сообщение измножества невыполненных обещаний promises. При этом данный переходдолжен быть возможен в рамках помеченной системы переходов локальW(ℓ,val)ных состояний, т.е. должно существовать состояние σ′ такое, что σ −−−−→σ′ . При этом метка времени τ должна быть больше значения базовогофронта viewcur (ℓ), и фронт сообщения view должен быть равен композиции высвобождающего фронта viewrel и [ℓ@τ].
Переход также увеличиваетбазовый и приобретающий фронты потока на [ℓ@τ].Внутренний переход () соответствует шагу исполнения потока, который не взаимодействует с памятью, например: присваивание в локальную переменную, исполнение условного перехода или пустой операции.Такой переход меняет только локальное состояние потока.3.6Промежуточная машина ARM+τВ этом разделе описывается промежуточная машина ARM+τ , а также доказывается, что она симулирует ARM-машину.
Для этого сначала показывается корректность некоторых базовых утверждений про подсистему памяти ARMмашины, а затем приводится подход для ввода меток времени для конкретногосценария поведения ARMv8 POP.963.6.1Свойства подсистемы памяти модели ARMv8 POPЛемма 1. Пусть состояние ARM-машины s достижимо из начального. Тогда отношение s.Ord равно транзитивному замыканию разности его самого и отношения,→.
Кроме того, оно ациклично.∀s. Prog ⊢ sinit −−−→∗ s ⇒ s.Ord = (s.Ord \ ,→)+ ∧ (s.Ord ациклично).ARMДоказательство. Утверждение верно для начального состояния sinit . Измененияв подсистеме памяти бывают трёх типов: (i) удаление запроса, (ii) отправка запроса в подсистему и (iii) уведомление потока о запросе. Рассмотрим, как меняется состояние подсистемы памяти при каждом из этих изменений в предположении, что начальное состояние памяти равно ⟨Evt, Ord, Prop⟩, а изменённое —⟨Evt′ , Ord′ , Prop′ ⟩:Удаление запроса eEvt′ = Evt \ {e},Prop′ = Prop \ {(tid, e) | tid},Ord′ = (Ord \ ({e} × Evt) \ (Evt × {e}) \ ,→)+ .Отправка запроса e потоком tidEvt′ = Evt ∪ {e},Prop′ = Prop ∪ {(tid, e)},Ord′ = (Ord ∪ {(e′ , e) | Prop(tid, e′ ), e′ ̸,→ e})+ .Поток tid становится осведомлённым о запросе eEvt′ = Evt,Prop′ = Prop ∪ {(tid, e)},Ord′ = (Ord ∪ {(e, e′ ) | Prop(tid,e′ ), ¬Prop(e.tid,e′ ), e ̸,→ e′ , ¬(e′ <Ord e)})+ .Очевидно, что во всех трёх случаях Ord′ = (Ord′ \ ,→)+ .
Также отношение Ord′ациклично, поскольку в случае удаления события Ord′ ⊆ Ord, отправка запросадобавляет в Ord-компоненту только ребра, входящие в новый запрос e, а в третьемслучае происходит проверка на ацикличность Ord′ .Леммы 2 и 3 доказываются аналогично.97Лемма 2. Пусть состояние ARM-машины s достижимо из начального. Тогда длялюбых двух запросов, которые не могут быть переупорядочены и о которых осведомлён один и тот же поток, верно, что запросы совпадают или между ними естьребро в отношении s.Ord.∀s,e,e′ ,tid. Prog ⊢ sinit −−−→∗ s ∧ e ̸,→ e′ ∧ s.Prop(tid, e) ∧ s.Prop(tid, e′ ) ⇒′ARM′e = e ∨ s.Ord(e, e ) ∨ s.Ord(e′ , e).Лемма 3. Пусть состояние ARM-машины s′ достижимо из состояния s.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
