Диссертация (1149932), страница 29
Текст из файла (страница 29)
Далее мы проведём разбор вариантов состояния экземпляра tape(path).Очевидно, что для любого нового состояния p′ , такого что p −−−−→ p′ ,Promiseвыполняется (a, p′ ) ∈ Ireach ∩ Imem3 . Выполнение Iprefix (a, p′ ) следует из того,ARMчто path′ ∈ next-path(path, cmds, tape), INext-Committed(a), и исполнение экземпляра tape(path) завершено. Поскольку переход p −−−−→ p′ будет использоPromiseван для того, чтобы “нагнать” исполнение машины ARM+τ, то он не является переходом Завершение записи. Как следствие, p′ .M = p.M, и утверждениеImem2 (a, p′ ) следует из Imem2 (a, p). Кроме того, очевидно, что будет выполнятьсялибо IPromise is up to ARM (a, p′ ), либо IPromise isn’t up to ARM (a, p′ ) в зависимости от завершённости экземпляра tape(path′ ).164Рассмотрим варианты состояния (завершённого) экземпляра tape(path).– tape(path) = Nop, tape(path) = Assign или tape(path) = If stifgoto k.Во всех трёх случаях переход обещающей машины p −−−−→ p′Promiseбудет внутренним, т.е.
ε-переходом. Поскольку ε-переход не меняет состояние памяти, то утверждение Imem1 (a, p′ ) непосредственно следует из Imem1 (a, p). Аналогично выполняются Iview (a, p′ )(поскольку p′ .T S(tid).V=p.T S(tid).V ), Istate (a, p′ ) (поскольку p′ .T S(tid).st = p.T S(tid).st и regfcom (cmds(tid), tape, path′ ) =regfcom (cmds(tid), tape, path′ )) и Icom-SY (a, p′ ) (поскольку экземплярtape(path) не является ни записью, ни барьером).– tape(path) = F com ld.Обещающая машина делает переход, соответствующий приобретающему барьеру памяти. Как следствие, новый базовый фронт view′cur равенстарому приобретающему фронту viewacq .
Утверждения Imem1 (a, p′ ) иIstate (a, p′ ) выполняются, поскольку переход не меняет состояния локальных переменных и памяти.Проверим, что выполняется Iview (a, p′ ). Для этого нам нужно показать,что следующее утверждение верно:∀tid′ , tape′ = a.tapef(tid′ ), path′′ = p.T S(tid′ ).path,⊔(p′ .T S(tid′ ).viewacq ⩽ sat-reads-view(path′′ , tape′ , H)⊔⊔ com-writes-time(tid′ , path′′ , tape′ , H))∧⊔(p′ .T S(tid′ ).viewcur ⩽ sat-reads-view(lastld(tape′ , path′′ ), tape′ , H)⊔⊔ com-writes-time(tid′ , path′′ , tape′ , H))∧⊔(p′ .T S(tid′ ).viewrel ⩽ sat-reads-view(lastldsy(tape′ , path′′ ), tape′ , H)⊔⊔ com-writes-time(tid′ , lastsy(tape′ , path′′ ), tape′ , H))).Зафиксируем tid′ , tape′ , path′′ .
Если tid′ ̸= tid, то утверждение следует изIview (a, p) и p′ .T S(tid′ ).V = p.T S(tid′ ).V . Пусть tid′ = tid. Как следствие,tape′ = tape и path′′ = path′ . Также верно, что– p′ .T S(tid).viewacq = p.T S(tid).viewacq = viewacq ,– p′ .T S(tid).viewcur = p.T S(tid).viewacq = viewacq ,– p′ .T S(tid).viewrel = p.T S(tid).viewrel = viewrel .165Тогда утверждение в упрощённой форме выглядит так:⊔(viewacq ⩽ sat-reads-view(path′ , tape, H)⊔⊔ com-writes-time(tid, path′ , tape, H))∧⊔(viewacq ⩽ sat-reads-view(lastld(tape, path′ ), tape, H)⊔⊔ com-writes-time(tid, path′ , tape, H))∧⊔(viewrel ⩽ sat-reads-view(lastldsy(tape, path′ ), tape, H)⊔⊔ com-writes-time(tid, lastsy(tape, path′ ), tape′ , H))).Первый и третий конъюнкты следует из того, что выполняетсяIview (a, p) и path′ > path. Второй конъюнкт следует из определенияlastld(tape, path′ ) и Iview (a, p).Утверждение Icom-SY (a, p′ ) выполняется, поскольку экземпляр tape(path)не является ни записью, ни sy-барьером.– tape(path) = F com sy.Обещающая машина делает переход, соответствующий высвобождающему барьеру памяти.
Как следствие, новый высвобождающий фронтview′rel равен старому базовому фронту viewcur . Утверждения Imem1 (a, p′ )и Istate (a, p′ ) выполняются, поскольку переход не меняет состояния локальных переменных и памяти. То, что утверждение Iview (a, p′ ) выполняется, может быть показано аналогичными выкладками, что и в случаеtape(path) = F com ld.Из верности утверждения Icom-SY (a, p) следует, что не существует незавершённого экземпляра записи с путём pathwrite > path.
Это означает, чтовыполняется Icom-SY (a, p′ ).– tape(path) = R (sat com ⟨tid′′ : path′′ @x,val⟩).Обещающая машина делает переход, соответствующий расслабленномучтению. Утверждения Imem1 (a, p′ ) и Icom-SY (a, p′ ) выполняются по тем жесоображениям, что и в первом рассмотренном случае.Поскольку все экземпляры с путями, меньше чем path, завершены, то экземпляр записи (tid′′ , path′′ ), из которого читает экземпляр tape(path), точно завершён. Введём следующие обозначения:a.tapef(tid′′ , path′′ ) = W (com _ x val);(τ, _, view′ ) ≜ a.H(tid′′ , path′′ ) ̸= (⊥, _, ⊥).Наличие соответствующего сообщения ⟨x : val@τ,view⟩ в памяти обещающей машины следует из Imem1 (a, p). То, что метка времени сообщения166не меньше, чем значение базового фронта потока, т.е.
τ ⩾ viewcur (x), слеARMдует из IView(a).По определению переходов обещающей машины мы знаем, что view′cur =viewcur ⊔ [x@τ], view′acq = viewacq ⊔ view, view ⩽ view′ и st′ = st[reg 7→ val].Утверждение Istate (a, p′ ) выполняется, поскольку st′ = st[reg 7→ val] =regfcom (cmds, tape, path)[reg 7→ val] = regfcom (cmds, tape, path′ ).Выполнение утверждения Iview (a, p′ ) следует из определения функцийcom-writes-time и sat-reads-view.– tape(path) = W (com im x val).Обещающая машина делает переход, соответствующий выполнению ранее данного обещания.
Мы знаем, что (τ, _, view′ ) ≜ a.Hτ (tid, path) ̸= ⊥,поскольку экземпляр записи завершён. То, что существует нужное обещание, т.е. ⟨x : val@τ,view⟩ ∈ p.T S(tid).promises, напрямую следуетиз Imem1 (a, p). Фронт view равен viewrel ⊔ [x@τ], поскольку обещающаямашина не имеет возможности делать обещания через высвобождающиебарьеры памяти. Утверждение Istate (a, p′ ) выполняется, поскольку верноIstate (a, p′ ) и выполнение обещания не меняет состояния переменных.
То,ARMчто viewcur (x) < τ следует из IView(a). То, что view ⩽ R′ следует из того,как машина ARM+τ конструирует компоненту Hview .Мы знаем, чтоview′cur = viewcur ⊔ [x@τ];view′acq = viewacq ⊔ [x@τ];promises′ = promises \ {⟨x : val@τ,view⟩}.Утверждение Imem1 (a, p′ ) следует из Imem1 (a, p) и tape(path)=W (com im x val). Утверждение Iview (a, p′ ) следует из определенийфункций com-writes-time и sat-reads-view. Утверждение Icom-SY (a, p′ )верно, т.к.
все экземпляры инструкций, чей путь меньше path, являютсязавершёнными.То, что переход p −−−−→ p′ сертифицируем, т.е. существует конечное числоPromiseпереходов потока tid, после которых все обещания потока выполнены, доказывается в приложении В.2.167Лемма 7. ∀(a, p) ∈ I.¬ Write commit(∀a′ . Prog ⊢ a −−−−−−−−→ a′ ⇒ (a′ , p) ∈ Ipre ∪ I) ∧′ARM +τWrite commitPromise writeARM +τPromise(∀a . Prog ⊢ a −−−−−−−→ a′ ⇒ ∃p′ . Prog ⊢ p −−−−−−−→ p′ ∧ (a′ , p′ ) ∈ Ipre ∪ I).Доказательство. Рассмотрим первый конъюнкт.
Зафиксируем a, p и a′ такие, что¬ Write commit tida −−−−−−−−−−→ a′ . Введём следующие обозначения:ARM +τ⟨path′ , st, ⟨viewcur , viewacq , viewrel ⟩, promises⟩ ≜ p.T S(tid);tape ≜ a.tapef(tid);Нам нужно показать, что (a′ , p) ∈ I ∪ Ipre . Из определений Ireach и Imem3следует, что (a′ , p) ∈ Ireach ∩ Imem3 выполняется. Утверждения Iprefix (a′ , p) иIview (a′ , p) выполняется, потому что переход a −−−−→ a′ не меняет завершённыйARM +τпрефикс a.tapef(tid). Утверждение Icom-SY (a′ , p) следует из Icom-SY (a, p) и требований правила Завершение sy-барьера.Нам нужно показать, что выполняется либо IPromise is up to ARM (a′ , p), либоIPromise isn’t up to ARM (a′ , p).
Если переход a −−−−→ a′ является Уведомление по′′′′ARM +τтока tid о запросе e , для плёнка любого потока не меняется, а значит какследствие того, что (a, p) ∈ I, выполняется IPromise is up to ARM (a′ , p). Иначе, существует некоторый экземпляр (tid, path), часть исполнения которого выполняется на переходе a −−−−→ a′ .
Если path′ ̸= path, то очевидно выполняетсяARM +τIPromise is up to ARM (a′ , p). Рассмотрим вариант path′ = path. В этом случае выполняется либо IPromise is up to ARM (a′ , p), либо IPromise isn’t up to ARM (a′ , p), в зависимостиот завершённости экземпляра a′ .tapef(tid, path).Утверждение (a′ , p) ∈ Imem1 ∩ Imem2 верно, поскольку a −−−−→ a′ не являARM +τется переходом Завершение записи, а значит набор сообщений записи в подсистеме памяти машины ARM+τ не меняется.Так доказывается первый конъюнкт леммы.168Рассмотрим второй конъюнкт.
Зафиксируем a, p и a′ такие, чтоWrite commit tid path x val τa −−−−−−−−−−−−−−−→ a′ . Введём следующие обозначения:ARM +τ⟨path′ , st, ⟨viewcur , viewacq , viewrel ⟩, promises⟩ ≜ p.T S(tid);view′≜ viewrel ⊔ [x@τ];promises′ ≜ promises ∪ {⟨x : val@τ,view′ ⟩};T S′≜ p.T S[tid 7→ ⟨path′ , st, ⟨viewcur , viewacq , viewrel ⟩, promises′ ⟩];tape≜ a.tapef(tid);H≜ a.H;Мы знаем, что метка времени τ не была использована для сообщений к локацииx, поскольку она использована машиной ARM+τ на этом шаге. В обещающей машине переход Обещание записи не имеет ограничений, (с точностью до сертификации, возможность которой доказывается в приложении В.2), поэтому возможенPromise write tid ⟨x:val@τ,view′ ⟩переход p −−−−−−−−−−−−−−−−−→ p′ , где p′ = ⟨p.M ∪ {⟨x : val@τ,view′ ⟩}, T S ′ ⟩.PromiseНам нужно проверить, что выполняется (a′ , p′ ) ∈ Ipre ∪ I.
Как следствие(a, p) ∈ I и определений a′ и p′ , выполняется (a′ , p′ ) ∈ Ireach ∩ Imem3 . Утверждения Iprefix (a′ , p′ ), Iview (a′ , p′ ), Istate (a′ , p′ ) и Icom-SY (a′ , p) выполняются, посколькупереход Завершение записи машины ARM+τ не меняет завершённый префиксa.tapef(tid). Утверждение IPromise is up to ARM (a′ , p) ∪ IPromise isn’t up to ARM (a′ , p) выполняется по тем же соображениям, что и в предыдущем рассмотренном варианте.Утверждение Imem1 (a′ , p′ ) верно, поскольку верно Imem1 (a, p), а измененияпамяти машин отражают требования Imem1 .Проверим, что выполняется Imem2 (a′ , p′ ). Для этого нужно показать, что верно следующее утверждение.∀⟨y : val′ @τ′ ,view′′ ⟩ ∈ p′ .M, τ′ ̸= 0 ⇒∃tid′ , path′′ , view′′′ ⩾ view′′ ,W (com _ y val′ ) = a′ .tapef(tid′ , path′′ ), a′ .H(tid′ , path′′ ) = (τ′ , _, view′′′ ).Зафиксируем сообщение ⟨y : val′ @τ′ ,view′′ ⟩ такое, что τ′ ̸= 0.⟨y : val′ @τ′ ,view′′ ⟩ ∈ p.M ∪ {⟨x : val@τ,view′ ⟩} ⇒∃tid′ , path′′ , view′′′ ⩾ view′′ ,W (com _ y val′ ) = a′ .tapef(tid′ , path′′ ), a′ .H(tid′ , path′′ ) = (τ′ , _, view′′′ ).Если ⟨y : val′ @τ′ ,view′′ ⟩ ∈ p.M, то утверждение является следствием утвержденияImem2 (a, p).
Иначе, ⟨y : val′ @τ′ ,view′′ ⟩ совпадает с ⟨x : val@τ,view′ ⟩. Тогда мы169можем упростить утверждение:∃tid′ , path′′ , view′′′ ⩾ view′ , W (com _ x val) = a′ .tapef(tid, path′′ ),a′ .H(tid′ , path′′ ) = (τ, _, view′′′ ).Выберем tid′ = tid, path′′ = path, view′′′ = view. Тогда утверждение верно по определению a′ .В.2СертификацияПри доказательстве того, что обещающая машина может симулировать исполнение ARM+τ машины, мы используем леммы 5 и 7, в которых конструируется шаг обещающей машины. Согласно определению, после каждого шага обещающая машина должна показывать, что находится в сертифицируемом состоянии(предикат certifiable), т.е. что для каждого потока существует последовательностьлокальных шагов, при исполнении которых поток выполняет все данные обещания (предикат certifiabletid ):certifiable(p) ≜ ∀tid.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
