Диссертация (1149932), страница 28

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 28)

Правила переходов ивспомогательные функции машины ARMv8 POPtape ≜ tapef(tid) tape(path) = ⊥ path.last < size(cmds)∃path .(tape(path′ ) ̸= ⊥ ∨ path′ = []) ∧ path ∈ next-path(path′ , cmds, tape)tape′ ≜ tape[path 7→ get-new-tapecell(cmds[path.last])]′Fetch instruction tid pathProg[tid 7→ cmds] ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−−−→ ⟨MPOP , iordf, tapef[tid 7→ tape′ ]⟩ARMe ∈ Evt ¬Prop(tid,e) ∀e′ <Ord e.

Prop(tid,e′ ) Prop′ ≜ Prop ∪ {(tid, e)}Ord′ ≜ (Ord ∪ {(e, e′ ) | Prop(tid,e′ ) ∧ ¬Prop(e.tid,e′ ), e ̸,→ e′ , ¬(e′ <Ord e)})+Propagate e tidProg ⊢ ⟨⟨Evt, Ord, Prop⟩, iordf, tapef⟩ −−−−−−−−→ ⟨⟨Evt, Ord′ , Prop′ ⟩, iordf, tapef⟩ARMtape ≜ tapef(tid) tape(path) = If none k val ≜ [[expr]]com ∈ Zprev-branches-committed(path, tape)(stifgoto , tape′ ) ≜ tape-upd-IfGoto(val, k, path, tape)M′POP ≜ delete-upd-reads(tid, tape′ , MPOP )Branch commit tid pathProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−−→ ⟨M′POP , iordf, tapef′ ⟩ARMtapef(tid, path) = F none ld tapef′ ≜ tapef[(tid, path) 7→ F com ld]prev-reads-committed(path, tapef(tid)) prev-fences-committed(path, tape(tid))prev-branches-committed(path, tapef(tid))Fence commit ld tid pathProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−−−→ ⟨MPOP , iordf, tapef′ ⟩ARMtapef(tid, path) = F none sy tapef′ ≜ tapef[(tid, path) 7→ F com sy]prev-instr-committed(path, tapef(tid))′MPOP ≜ accept-request(⟨tid, path, dmb⟩, MPOP )Fence commit sy tid pathProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−−−→ ⟨M′POP , iordf, tapef′ ⟩ARMtapef(tid, path) = W none Prog(tid)[path.last] = ‘‘[expr0 ] := expr1 ”[[expr0 ]] = ℓ [[expr1 ]] = val tapef′ = tapef[(tid, path) 7→ W (pending ℓ val)]Write pending tid path ℓ valProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−−−−→ ⟨MPOP , iordf, tapef′ ⟩ARMtape ≜ tapef(tid) tape(path) = W (pending ℓ val) cmds ≜ Prog(tid)cmds[path.last] = ‘‘[expr0 ] := expr1 ” [[expr0 ]]com = ℓ [[expr1 ]]com = valprev-fences-committed(path, tape) prev-branches-committed(path, tape)prev-fully-determined(path, tape) no-prev-restartable-reads-from-loc(ℓ, path, tape)im ≜ no-following-com-writes-to-loc(ℓ, path, tape)tape′ ≜ tape-upd-Wcom(im, ℓ, val, cmds, tid, path, tape)tapef′ = tapef[tid 7→ tape′ ] M′′POP ≜ delete-upd-reads(tid, tape′ , MPOP )M′POP ≜ if im then accept-request(⟨tid, path, wr ℓ : val⟩, M′′POP ) else M′′POPWrite commit tid path ℓ val⟨MPOP , iordf, tapef, Prog⟩ −−−−−−−−−−−−−−→ ⟨M′POP , iordf, tapef′ , Prog⟩ARM159tape ≜ tapef(tid) tape(path) = R noneProg(tid)[path.last] = ‘‘reg = [expr]” [[expr]] = ℓ e ≜ ⟨tid, path, rd ℓ⟩′tapef = tapef[(tid, path) 7→ R (requested ℓ)] prev-fences-committed(path, tape)iord′ ≜ append(e, iordf(tid)) iordf′ = iordf[tid 7→ iord′ ] M′POP ≜ accept-request(e, MPOP )Read issue tid path ℓProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−→ ⟨M′POP , iordf′ , tapef′ ⟩ARMtape ≜ tapef(tid) tape(path) = R (requested ℓ) e ≜ ⟨tid, path, rd ℓ⟩ e′ ≜ ⟨tid′ , path′ , wr ℓ : val⟩⟨Evt, Ord, Prop⟩ ≜ MPOP {e, e′ } ⊆ Evt e′ <Ord e propagated-to-same-threads(e, e′ , Prop)∀e∗ , e′ <Ord e∗ <Ord e, getℓ(e∗ ) ̸= ℓ ∧ fully-propagated(e∗ , Prop)¬prev-read-from-other-write(ℓ, e′ , tid, path, iordf(tid))tape′ ≜ tape-upd-Rsat(pln, ℓ, val, cmds, tid, path, tid′ , path′ , tape)tapef′ = tapef[tid 7→ tape′ ] M′POP ≜ delete-upd-reads(tid, tape′ , MPOP )Read satisfy tid path tid′ path′ ℓ valProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−−−−−−−−→ ⟨M′POP , iordf, tapef′ ⟩ARMtape ≜ tapef(tid) tape(path) = R (requested ℓ) e ≜ ⟨tid, path, rd ℓ⟩ e′ ≜ ⟨tid′ , path′ , wr ℓ : val⟩⟨Evt, Ord, Prop⟩ ≜ MPOP {e, e′ } ⊆ Evt e′ <Ord e propagated-to-same-threads(e, e′ , Prop)∀e∗ , e′ <Ord e∗ <Ord e, getℓ(e∗ ) ̸= ℓ ∧ fully-propagated(e∗ , Prop)prev-read-from-other-write(ℓ, e′ , tid, path, iordf(tid))tape′ ≜ tape[path 7→ R none] tapef′ = tapef[tid 7→ tape′ ]M′POP ≜ delete-upd-reads(tid, tape′ , MPOP )Read satisfy (fail) tid path tid′ path′ ℓ valProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−−−−−−−−−−→ ⟨M′POP , iordf, tapef′ ⟩ARMtape ≜ tapef(tid) tape(path) = R none tape(path′ ) = W (pending ℓ val)path′ < path cmds ≜ Prog(tid) cmds[path.last] = ‘‘reg = [expr]” [[expr]]path = ℓno-writes-to-loc-in-between(ℓ, cmds, path′ , path, tape)no-different-write-reads-in-between(ℓ, tid, path′ , path, tape)tape′ ≜ tape-upd-Rsat(inflight, ℓ, val, cmds, tid, path, tid, path′ , tape)tapef′ = tapef[tid 7→ tape′ ] MPOP ≜ delete-upd-reads(tid, tape′ , MPOP )Read satisfy from in-flight write tid path path′ ℓ valProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−−−−−−−−−−−−−−−−→ ⟨M′POP , iordf, tapef′ ⟩ARMtape ≜ tapef(tid) tape(path) = R (sat sat-state ⟨tid′ , path′ , wr ℓ : val⟩)sat-state ̸= com cmds ≜ Prog(tid) prev-fully-determined(path, tape)prev-fences-committed(path, tape) prev-branches-committed(path, tape)∗path′′ = max{path∗ < path|cmds[path∗ .last] = ‘‘[expr0 ] := expr1 [[expr0 ]]pathcom = ℓ}if (tid′ , path′ ) = (tid, path′′ ) then tape(path′ ) is fully determined else tape(path′ ) is committedreads-in-between-committed(path′′ , path, tape, cmds)tape′ ≜ tape[path 7→ R (sat com ⟨tid′ , path′ , wr ℓ : val⟩)] tapef′ = tapef[tid 7→ tape′ ]Read commit tid pathProg ⊢ ⟨MPOP , iordf, tapef⟩ −−−−−−−−−−−→ ⟨MPOP , iordf, tapef′ ⟩ARM160prev-instr-committed(path, tape) ≜ ∀path′ < path, tape(path′ ) is committed.prev-reads-committed(path, tape) ≜ ∀path′ < path, tape(path′ ) = R _ ⇒ tape(path′ ) is committed.prev-fences-committed(path, tape) ≜ ∀path′ < path, tape(path′ ) = F stfence _ ⇒ stfence = com.prev-branches-committed(path, tape) ≜ ∀path′ < path, tape(path′ ) = If stifgoto _ ⇒ stifgoto ̸= none.prev-fully-determined(path, tape) ≜ ∀path′ < path, tape(path′ ) has a fully determined address.no-prev-restartable-reads-from-loc(ℓ, path, tape) ≜∀path′ < path, reg, expr, tape(path′ ) = R stread , cmds[path′ .last] = ‘‘reg = [expr] [[expr]] = ℓ ⇒stread = sat _ _ ∧ tape(path′ ) can’t be restarted.no-following-com-writes-to-loc(ℓ, path, tape) ≜ ∄path′ > path, tape(path′ ) = W (com _ ℓ _).tape-upd-IfGoto(val, k, path, tape) ≜let stifgoto ≜ if val ̸= 0 then taken else ignored inlet pathdrop ≜ if val ̸= 0 then append(path.last + 1, path) else append(path.last + k, path) in(stifgoto , λ path′ →if prefix(pathdrop , path′ ) then ⊥elif path′ = path then If stifgoto kelse tape(path′ )).reads-in-between-committed(path′′ , path, tape, cmds) ≜∀path∗ > path′′ , path∗ < path,∗∗cmds[path∗ .last] = ‘‘reg = [expr] [[expr]]pathcom = x ⇒ tape(path ) is committed.no-writes-to-loc-in-between(ℓ, cmds, path′ , path, tape) ≜∗̸ ∃path∗ > path′ , path∗ < path, cmds[path∗ .last] = ‘‘[expr0 ] := expr1 [[expr0 ]]path = ℓ.no-different-write-reads-in-between(ℓ, tid′ , path′ , path, tape) ≜̸ ∃tid′′ ̸= tid′ , path′′ ̸= path′ , path∗ > path′ , path∗ < path, tape(path∗ ) = R (sat _ ⟨tid′′ , path′′ , wr ℓ : _⟩).delete-upd-reads(tid, tape, ⟨Evt, Ord, Prop⟩) ≜let to-delete ≜ {e ∈ Evt | e.tid = tid, tape′ (e.path) ̸= R (requested _)} inlet Evt′ ≜ Evt \ to-delete inlet Prop′ = Prop \ (N × to-delete) inlet Ord′ = (Ord \ (Evt × to-delete ∪ to-delete × Evt) \ ,→)+ in⟨Evt′ , Ord′ , Prop′ ⟩.accept-request(e, ⟨Evt, Ord, Prop⟩) ≜let Evt′ = Evt ∪ {e} inlet Prop′ = Prop[tid 7→ Prop(tid) ∪ {e}] inlet Ord′ = (Ord ∪ {(e′ , e)|e′ ∈ Prop(tid), e′ ̸,→ e})+ in⟨Evt′ , Ord′ , Prop′ ⟩.161propagated-to-same-threads(e, e′ , Prop) ≜ {tid | Prop(tid, e)} = {tid | Prop(tid, e′ )}fully-propagated(e, Prop) ≜ ∀tid, Prop(tid, e) ∨ ∄e′ .Prop(tid, e′ ).getℓ(e) ≜ match e with ⟨_, _, rd ℓ⟩ | ⟨_, _, wr ℓ : _⟩ → ℓ | _ → ⊥ end.prev-read-from-other-write(ℓ, e′ , tid, path, iord) ≜∃path∗ < path,last_index(⟨tid, path∗ , rd ℓ⟩, iord) > last_index(⟨tid, path, rd ℓ⟩, iord),tape(path∗ ) = R (sat _ req), req ̸= e′ ).get-new-tapecell(S) ≜match S with|‘‘reg := [expr]” → R none|‘‘[expr0 ] := expr1 ” → W none|‘‘fence(fmodARM )” → F none fmodARM|‘‘if expr goto k” → If none k|‘‘reg = expr” → Assign|‘‘nop” → Nopend.e <Ord e′ ≜ (e, e′ ) ∈ Ord.⟨tid, path, reqinfo⟩ ,→ ⟨tid′ , path′ , reqinfo′ ⟩ ≜if sy ∈ {reqinfo,reqinfo′ } then f alseelif reqinfo.ℓ = reqinfo′ .ℓ ̸= ⊥ then f alseelse true.next-path(path, cmds, tape) ≜ f ilter(λpath′ → path′ .last < size(cmds),if path = [] then {[0]}elif tape(path) = ⊥ then ∅elif ∃k, tape(path) = If none k then {snoc(path, path.last + 1), snoc(path, path.last + k)}elif ∃k, tape(path) = If taken k then {snoc(path, path.last + k)}else {snoc(path, path.last + 1)}).tape-upd-restart(cmds, tid, tape) ≜f ixpoint(λtape′ →λpath →if cmds[path.last] = ‘‘reg = [expr]” ∧ JexprKpath = ⊥then R noneelif ∃path′′ , tape′ (path) = R (sat inflight ⟨tid, path′′ , wr _ : _⟩) ∧ tape′ (path′′ ) = W nonethen R noneelif cmds[path.last] = ‘‘[expr0 ] = expr1 ” ∧ (Jexpr0 Kpath = ⊥ ∨ Jexpr1 Kpath = ⊥)then W noneelse tape′ (path))(tape).162tape-upd-Wcom(im, ℓ, val, cmds, tid, path, tape) ≜tape-upd-restart(cmds, tid,λpath′ →if path′ = path then W (com im ℓ val)elif path′ < path then tape(path′ )elif tape(path′ ) = R (sat inflight ⟨tid, path, wr ℓ : val⟩)then tape(path′ ) = R (sat pln ⟨tid, path, wr ℓ : val⟩)elif tape(path′ ) = R (requested ℓ) then R noneelif ∃path′′ < path, tape(path′ ) = R (sat inflight ⟨tid, path′′ , wr ℓ : _⟩) then R noneelif ∃tid′′ , path′′ , ¬(tid′′ = tid ∧ path′′ ⩾ path) ∧ tape(path′ ) = R (sat pln ⟨tid′′ , path′′ , wr ℓ : _⟩)then R noneelse tape(path′ )).tape-upd-Rsat(sat-state, ℓ, val, cmds, tid, path, tid′ , path′ , tape) ≜tape-upd-restart(cmds, tid,λpath′′ →if path′′ = path then R (sat sat-state ⟨tid′ , path′ , wr ℓ : val⟩)elif path′′ < path then tape(path′′ )elif ∃path∗ < path, tape(path′′ ) = R (sat inflight ⟨tid, path∗ , wr ℓ : _⟩) then R noneelif ∃tid∗ , path∗ , ¬(tid∗ = tid ∧ path∗ > path) ∧ ¬(tid∗ = tid′ ∧ path∗ = path′ )∧tape(path′′ ) = R (sat pln ⟨tid∗ , path∗ , wr ℓ : _⟩) then R noneelse tape(path′′ )).163Приложение В.

Доказательство вспомогательныхлемм о симуляции модели ARM+τВ.1Базовые леммыЛемма 5. ∀(a, p) ∈ Ipre . ∃p′ .Prog ⊢ p −−−−→ p′ ∧ (a, p′ ) ∈ Ipre ∪ 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) завершён. Далее в доказательстве мы конструируем состояние обещающей машины p′ такое, что оноудовлетворяет утверждению теоремы.Введём следующие обозначения:cmds⟨viewcur , viewacq , viewrel ⟩view′cur , view′acq , view′relpath′stst′promises′promisesH≜≜≜≜≜≜≜≜≜Prog(tid);p.T S(tid).V ;p′ .T S(tid).V ;p′ .T S(tid).path;p.T S(tid).st;p′ .T S(tid).st;p′ .T S(tid).promises;p.T S(tid).promises;a.H.Мы покажем, что обещающая машина в состоянии p может сделать переход,связанный с tape(path), в состояние p′ , и при этом будет выполняться (a, p′ ) ∈Ipre ∪ I.

Характеристики

Список файлов диссертации