Диссертация (1149932), страница 21
Текст из файла (страница 21)
tape(path) = W (com _ ℓ _) ⇒ a.Hτ (tid, path) > viewARM (a, tid, path, ℓ)).Доказательство. Утверждение доказывается с помощью индукции по сценариюповедения Prog ⊢ ainit −−−−→∗ a.ARM +τ3.7Доказательство корректности компиляцииВ этом разделе доказывается основная теорема главы, представленная в разделе 3.3.Теорема 1. Для любой программы Prog и её сценария поведения в модели ARMv8POP, Prog ⊢ sinit −−−→∗ s, где s — финальное состояние, FinalARM (s, Prog), суARMществует сценарий поведения этой программы в обещающей модели, Prog ⊢pinit −−−−→∗ p, где p — финальное состояние FinalPromise (p, Prog); при этом соPromiseстояния памяти в s и p совпадают, same-memory(s, p).Доказательство. Зафиксируем программу Prog.
Используя теорему 3, мы меняем утверждение, которое нужно доказать, на симуляцию обещающей машиноймашины ARM+τ:∀a. Prog ⊢ ainit −−−−→∗ a ∧ FinalARM +τ (a, Prog) ⇒∃p. Prog ⊢ARM +τinitp −−−−→∗Promisep ∧ FinalPromise (p, Prog) ∧ same-memory(a, p).Для того, чтобы доказать это утверждение, введём набор отношений, связывающих состояния машин.
Эти отношения в дальнейшем войдут в отношение симуляции.Следуя представлению обещающей машины в [23], добавим в состояниекаждого потока обещающей машины указатель на следующий к исполнению экземпляр инструкции, который будем обозначать p.T S(tid).path, и функцию состояния локальных переменных p.T S(tid).st. В представлении из раздела 3.5 этичасти состояния скрыты помеченной системой переходов.Отношение Iprefix устанавливает, что все экземпляры инструкций, выполненные обещающей машиной, завершены машиной ARM+τ:Iprefix (a, p) ≜ ∀tid, path′ < p.T S(tid).path. (a.tapef(tid, path′ ) завершено).107Следующие отношения связывают память обещающей машины с подсистемойпамяти ARM+τ.
Отношение Imem1 утверждает, что для каждого завершенного экземпляра записи в ARM+τ существует сообщение в памяти обещающей машиныс теми же локацией, значением и меткой времени, кроме того фронт сообщения небольше, чем соответствующий фронт запроса в ARM+τ. При этом, если путь экземпляра записи меньше, чем указатель обещающей машины, то сообщение былообещано, и обещание выполнено, иначе — только обещано:Imem1 (a, p) ≜ ∀tid, ℓ, val, τ, view′ , path.W (com _ ℓ val) = a.tapef(tid, path) ∧ ⟨τ, _, view′ ⟩ = a.H(tid, path) ⇒∃view ⩽ view′ .(path ⩾ p.T S(tid).path ⇒ ⟨ℓ : val@τ,view⟩ ∈ p.T S(tid).promises)∧(path < p.T S(tid).path ⇒∪⟨ℓ : val@τ,view⟩ ∈ p.M \ p.T S(tid).promises).tidОтношение Imem2 связывает памяти машин в обратном направлении: для каждогосообщения из памяти обещающей машины в плёнке ARM+τ есть соответствующий завершённый экземпляр записи:Imem2 (a, p) ≜ ∀⟨ℓ : val@τ,view⟩ ∈ p.M.
τ ̸= 0 ⇒ ∃tid, path, view′ ⩾ view.W (com _ ℓ val) = a.tapef(tid, path) ∧ a.H(tid, path) = ⟨τ, _, view′ ⟩.Отношение Imem3 связывает инициализирующие записи:Imem3 (a, p) ≜ ∀ℓ. ⟨0tid , [], wr ℓ : 0⟩ ∈ a.MPOP ∧ ⟨ℓ : 0@0,λℓ. 0⟩ ∈ p.M.Отношение Iview утверждает, что фронты обещающей машины ограничены комбинацией фронтов, связанных с завершёнными экземплярами чтений и записеймашины ARM+τ.
Для приобретающего фронта считаются все экземпляры записи и чтения, путь которых меньше path. Для базового фронта считаются все экземпляры записи, путь которых меньше path, и чтения, путь которых меньше последнего завершённого экземпляра ld барьера (lastld(tape, path)). Для высвобождающего фронта учитываются все экземпляры записи вплоть до последнегозавершённого экземпляра sy барьера (lastsy(tape, path)) и все экземпляры чтения до завершённого экземпляра ld барьера, предшествующего этому sy барьеру108(lastldsy(tape, path)).Iview (a, p) ≜ ∀tid, tape = a.tapef(tid), path = p.T S(tid).path.let pathld , pathsy ≜ lastld(tape, path),lastsy(tape, path) inlet pathldsy ≜ lastldsy(tape, path) in⊔(p.T S(tid).viewacq ⩽ viewf(tid, path, path, tape, a.H))∧⊔(p.T S(tid).viewcur ⩽ viewf(tid, pathld , path, tape, a.H))∧⊔(p.T S(tid).viewrel ⩽ viewf(tid, pathldsy , pathsy , tape, a.H).Отношение Istate связывает состояние локальных переменных в потоке обещающей машины со значением функции состояния машины ARM+τ:Istate (a, p) ≜ ∀tid, regf = regfcom (Prog(tid), a.tapef(tid), p.T S(tid).path).∀reg, p.T S(tid).st(reg) = regf(reg).Отношение Icom-SY утверждает, что все экземпляры sy барьера, которые предшествуют завершённому экземпляру записи, выполнены обещающей машиной:Icom-SY (a, p) ≜ ∀tid, tape = a.tapef(tid),pathwrite = last-write-com(tape), pathsy < pathwrite .tape(pathsy ) = F _ sy ⇒ pathsy < p.T S(tid).path,где last-write-com(tape) — это путь последнего завершённого потоком экземпляра записи.
Данное отношение нужно для доказательства сертифицируемости шагов обещающей машины, участвующих в симуляции.Отношение Ireach показывает, что состояния машин достижимы из начального:Ireach (a, p) ≜ Prog ⊢ ainit −−−→∗ a ∧ Prog ⊢ pinit −−−−→∗ p.ARMPromiseОтношение Ibase комбинирует вышеупомянутые отношения:Ibase ≜ Iprefix ∩ Imem1 ∩ Imem2 ∩ Imem3 ∩ Iview ∩ Istate ∩ Icom-SY ∩ Ireach .При симуляции в каждый момент верно одно из двух: либо обещающая машина ожидает, что машина ARM+τ завершит исполнение экземпляра инструкции, либо указатель одного (и только одного) из потоков обещающей машины указывает на завершённый экземпляр инструкции.
Последнее означает, что обещающая машина должна сделать шаг, соответствующий этому экземпляру. Для того,109чтобы задать оба возможных варианта, мы используем вспомогательный предикат:tidIPromiseis up to ARM (tid,a,p) ≜ let tape, path ≜ a.tapef(tid), p.T S(tid).path intape(path) = ⊥ ∨ tape(path) не завершен.С его помощью случай, когда обещающая машина ожидает, выражается предикатом IPromise is up to ARM , а случай, когда обещающая машина должна сделать шаг —предикатом IPromise isn’t up to ARM :tidIPromise is up to ARM (a,p) ≜ ∀ tid.IPromiseis up to ARM (tid,a,p).tidIPromise isn’t up to ARM (a,p) ≜ ∃! tid. ¬ IPromiseis up to ARM (tid,a,p).Данные предикаты используются для определения двух отношений симуляции:Ipre ≜ Ibase ∩ IPromise isn’t up to ARMI ≜ Ibase ∩ IPromise is up to ARMЕсли состояния машин связаны отношением Ipre , то существует поток обещающей машины, который может сделать переход.
После этого перехода состояниямашин снова связаны отношением Ipre , и тот же поток может сделать ещё одиншаг, или состояния связаны отношением I, и все потоки обещающей машиныждут. Это утверждение сформулировано в лемме 5.Лемма 5. ∀(a, p) ∈ Ipre . ∃p′ .Prog ⊢ p −−−−→ p′ ∧ (a, p′ ) ∈ Ipre ∪ I.PromiseДоказательство леммы 5 приведено в приложении В.Как следствие того, что в каждом корректном состоянии машиныARM+τ существует лишь конечное число завершённых экземпляров инструкций,можно показать, что обещающая машина может за конечное число шагов “нагнать” ARM+τ (лемма 6).Лемма 6. ∀(a, p) ∈ Ipre . ∃p′ .
Prog ⊢ p −−−−→∗ p′ ∧ (a, p′ ) ∈ I.PromiseДоказательство. Зафиксируем a и p. Из того, что (a, p) ∈ Ipre , следуетIPromise isn’t up to ARM (a, p). Т.о. известно, что существует единственный поток tid, егоплёнка tape = a.tapef(tid) и путь path = p.T S(tid).path, что исполнение экземпляра tape(path) завершено.
Зафиксируем tid, tape, path, cmds = Prog(tid).Из того, что tape(path) завершён, следует, что существует конечный набор{pathi }i∈[0,n] такой, что:– ∀i, tape(pathi ) завершено;110– ∀i < n, pathi+1 ∈ next-path(pathi , cmds);– ∀path′ ∈ next-path(tape, cmds), tape(path′ ) = ⊥ ∨ tape(path′ ) не завершено.Здесь next-path(pathi , cmds) является функцией, которая по пути экземпляра инструкции восстанавливает путь до непосредственно следующего за ним экземпляра (см. формальное определение функции в приложении Б).Далее лемма доказывается индукцией по n с помощью леммы 5.Предположим, что состояния обещающей и ARM+τ машин связаны отношением I.
Для такой ситуации мы показываем, что машина ARM+τ может сделать шаг. Если этот шаг имеет тип Завершение записи, то обещающая машинаможет пообещать соответствующее сообщение, и новые состояния машин будутсвязаны отношением Ipre ∪ I. Если это другой шаг, то обещающая машина не делает своего ответного шага, но состояния машин опять же связаны отношениемIpre ∪ I.Лемма 7. ∀(a, p) ∈ I.¬ Write commit(∀a′ . Prog ⊢ a −−−−−−−−→ a′ ⇒ (a′ , p) ∈ Ipre ∪ I) ∧ARM +τWrite commitPromise writeARM +τPromise(∀a′ . Prog ⊢ a −−−−−−−→ a′ ⇒ ∃p′ .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
