Диссертация (1149932), страница 10
Текст из файла (страница 10)
8).Память M — это частичная функция, которая по локации и метке временивозвращает сохраненное значение и синхронизационный фронт. Разные аспекты модели используют фронты по-разному, но каждый фронт является частичнойфункцией, которая по локации возвращает некоторую метку времени. Функциябазового фронта возвращает базовый фронт потока по его идентификатору π, гдеидентификатор потока — это список направлений налево (l) / направо (r), которыйпоказывает, как найти подвыражение потока во всем выражении программы, проходя по вершинам par.
Это путь уникально идентифицирует поток. Для вычисления пути по редукционному контексту используется вспомогательная функцияpath.Стартующие дочерние потоки наследуют базовый фронт родительского потока, что в терминах самой простой версии функции spawn определяется следующим образом:spawn(E, ⟨M,ψrd ⟩) ≜ ⟨M, ψrd [π l 7→ viewrd , π r 7→ viewrd ]⟩,где π = path(E) и viewrd = ψrd (π). Когда потоки соединяются, базовый фронт ихродительского потока становится покомпонентным максимумом базовых фронтов49S⟨E[x := v; s], ξ⟩ −→ ⟨E[s[x/v]], ξ⟩I -F⟨E[if 0 then s1 else s2 fi], ξ⟩ −→ ⟨E[s2 ]], ξ⟩I -Tn ̸= 0⟨E[if n then s1 else s2 fi], ξ⟩ −→ ⟨E[s1 ]], ξ⟩R-Ux – новая переменная⟨E[repeat s end], ξ⟩ −→⟨E[x := s; if x then x else repeat s end fi], ξ⟩SJ′ξ = spawn(E, ξ)ξ′ = join(E, ξ)⟨E[spw s1 s2 ], ξ⟩ −→ ⟨E[par s1 s2 ], ξ′ ⟩⟨E[par v1 v2 ], ξ⟩ −→ ⟨E[(v1 , v2 )], ξ′ ⟩C-F⟨E[EU[choice e1 e2 ]], ξ⟩ −→ ⟨E[EU[e1 ]], ξ⟩C-S⟨E[EU[choice e1 e2 ]], ξ⟩ −→ ⟨E[EU[e2 ]], ξ⟩Рис.
7. Базовые правила OpC11 MM50Состояниеξ ::=ПамятьM ::=Функция базового фронта ψrd ::=Фронтview ::=Идентификатор потокаπ —τ ∈Метка времени⟨M, ψrd ⟩(ℓ, τ) ⇀ ⟨v, view⟩π ⇀ viewℓ⇀τ(l|r)∗NРис. 8. Базовое состояние машины OpC11R-Uξ = ⟨M, ψrd ⟩ π = path(E) viewrd = ψrd (π) viewrd (ℓ) = ⊥⟨E[[ℓ]RM ], ξ⟩ −→ ⟨stuck, ξinit ⟩CAS-Uξ = ⟨M, ψrd ⟩ π = path(E) viewrd = ψrd (π) viewrd (ℓ) = ⊥⟨E[casSM,FM (ℓ, e1 , e2 )], ξ⟩ −→ ⟨stuck, ξinit ⟩Рис. 9. Правила чтения из неинициализированной локациидочерних потоков:join(E, ⟨s,ψrd ⟩) = ⟨s, ψrd [π 7→ viewlrd ⊔ viewrrd ]⟩,где π = path(E), viewlrd = ψrd (π l) и viewrrd = ψrd (π r).Далее определяется первый набор правил о “плохих” сценариях поведения— тех, которые включают чтение из неинициализированной локации (см. рис.
9).Эти правила срабатывают в том случае, если поток, пытающийся прочитать значение из локации ℓ, не осведомлен ни об одной записи, т.е. его базовый фронт неопределён для ℓ. В частном случае эти правила применимы, если в локацию небыло сделано ни одной записи.2.2.3Высвобождающие и приобретающие обращенияПравила, описывающие поведение высвобождающих записей и приобретающих чтений, приведены на рис. 10. Высвобождающая запись добавляет в памятьновую запись (ℓ, τ) 7→ (v, view), где v — записываемое значение, а view — фронтдобавленного сообщения, который далее может быть использован для синхрони-51W-Rξ = ⟨M, ψrd ⟩ π = path(E) τ = N extτ(M, ℓ)viewrd = ψrd (π) view = viewrd [ℓ 7→ τ]ξ′ = ⟨M [(ℓ, τ) 7→ (v, view)], ψrd [π 7→ view]⟩⟨E[[ℓ] :=rel v], ξ⟩ −→ ⟨E[v], ξ′ ⟩R-Aviewrdξ = ⟨M, ψrd ⟩ π = path(E) M (ℓ, τ) = (v, view)= ψrd (π) viewrd (ℓ) ⩽ τξ′ = ⟨M, ψrd [π 7→ viewrd ⊔ view]⟩⟨E[[ℓ]acq ], ξ⟩ −→ ⟨E[v], ξ′ ⟩Рис.
10. Правила высвобождающей записи и приобретающего чтениязации с другими потоками. Сам фронт сообщения является обновлённым на [ℓ@τ]базовым фронтом соответствующего потока.Правило обработки приобретающего чтения является недетерминированным, поскольку выбирает из памяти запись (ℓ, τ) 7→ (v, view), метка времени τкоторой не меньше значения базового фронта потока по этой локации viewrd (ℓ).Значение v заменяет инструкцию чтения внутри редукционного контекста E, абазовый фронт потока viewrd комбинируется с прочитанным фронтом сообщенияview.
Здесь и далее правила для CAS-инструкций4 опущены; они могут быть найдены в реализации интерпретатора [98].2.2.4 sc-инструкцииВ состояние машины OpC11 для представления правил обработки scинструкций нужно добавить дополнительную компоненту — глобальный scфронт viewsc :ξ ::= ⟨..., viewsc ⟩Этот фронт по локации определяет максимальную метку времени сообщения вэту локацию, которое было сделано с помощью sc-записи.4 CAS-инструкция(compare-and-set) является частным случаем атомарного чтения и записи (RMW).Эта инструкция прочитывает значение из локации, сравнивает его с ожидаемым значением и в случае совпадения записывает новое значение в локацию.52WSCξ = ⟨M, ψrd , viewsc ⟩ π = path(E) τ = N extτ(M, ℓ)viewrd = ψrd (π) view = viewrd [ℓ 7→ τ]ξ′ = ⟨M [(ℓ, τ) 7→ (v, view)], ψrd [π 7→ view], viewsc [ℓ 7→ τ]⟩⟨E[[ℓ] :=sc v], ξ⟩ −→ ⟨E[v], ξ′ ⟩RSCξ = ⟨M, ψrd , viewsc ⟩ π = path(E) M (ℓ, τ) = (v, view)viewrd = ψrd (π) max(viewrd (ℓ), viewsc (ℓ)) ⩽ τξ′ = ⟨M, ψrd [π 7→ viewrd ⊔ view], viewsc ⟩⟨E[[ℓ]acq ], ξ⟩ −→ ⟨E[v], ξ′ ⟩Рис.
11. Правила обработки sc-инструкцийПравила обработки sc-инструкций приведены на рис. 11. Они совпадаютс правилами для высвобождающих записей и приобретающих чтений с рис. 10с точностью до фрагментов, выделенных серым цветом. Так, правило sc-записиобновляет sc-фронт машины, чтобы по целевой локации ℓ он возвращал меткувремени добавленной записи, а правило sc-чтения проверяет, что метка временивыбранного сообщения не меньше, чем значение sc-фронта по целевой локации.2.2.5Неатомарные обращенияДля обработки неатомарных чтений и записей в состояние машины добавляется глобальный na-фронт:ξ ::= ⟨..., viewna ⟩.Аналогично sc-фронту, na-фронт по локации возвращает максимальную меткувремени na-записи в неё, а сам фронт обновляется в правиле na-записи.na-фронт предназначен для поиска гонок по данным, которые включаютнеатомарные обращения к памяти.
Так, когда поток выполняет na-обращения (см.правила ReadNA и WriteNA на рис. 12), происходит проверка того, что поток осведомлён о последнем сообщении в целевую локацию. Если данное требование невыполняется, то в программе присутствует гонка, и программа имеет неопределённое поведение (см. правила ReadNA-stuck1 и WriteNA-stuck1). Кроме того,если поток выполняет необязательно неатомарное обращение к локации ℓ, о по-53WNAviewrdξ = ⟨M, ψrd , viewna ⟩ π = path(E)τ = N extτ(M, ℓ)rd= ψ (π)view = viewrd [ℓ 7→ τ]viewrd (ℓ) ≡ LastTS(M, ℓ)ξ′ = ⟨M [(ℓ, τ) 7→ (v, ())], ψrd [π 7→ view], viewna [ℓ 7→ τ]⟩⟨E[[ℓ] :=na v], ξ⟩ −→ ⟨E[v], ξ′ ⟩RNAξ = ⟨M, ψrd , viewna ⟩M (ℓ, τ) = (v, view)π = path(E)τ ≡ viewrd (ℓ)τ = LastTS(M, ℓ)ξ′ = ⟨M, ψrd , viewna ⟩⟨E[[ℓ]na ], ξ⟩ −→ ⟨E[v], ξ′ ⟩RNA-1ξ = ⟨M, ψrd , viewna ⟩viewrd = ψrd (π)viewrd (ℓ) ̸= LastTS(M, ℓ)π = path(E)⟨E[[ℓ]na ], ξ⟩ −→ ⟨stuck, ξinit ⟩WNA-1ξ = ⟨M, ψrd , viewna ⟩viewrd = ψrd (π)viewrd (ℓ) ̸= LastTS(M, ℓ)π = path(E)⟨E[[ℓ] :=na v], ξ⟩ −→ ⟨stuck, ξinit ⟩RNA-2ξ = ⟨M, ψrd , viewna ⟩viewrd = ψrd (π)viewrd (ℓ) < viewna (ℓ)π = path(E)⟨E[[ℓ]RM ], ξ⟩ −→ ⟨stuck, ξinit ⟩WNA-2π = path(E)ξ = ⟨M, ψrd , viewna ⟩viewrd = ψrd (π)viewrd (ℓ) < viewna (ℓ)⟨E[[ℓ] :=WM v], ξ⟩ −→ ⟨stuck, ξinit ⟩Рис.
12. Правила обработки неатомарных обращений и идентификации гонок поданным54R-Cξ = ⟨M, ψrd ⟩ π = path(E)M (ℓ, τ) = (v, view)viewrd = ψrd (π)viewrd (ℓ) ⩽ τξ′ = ⟨M, ψrd [π 7→ viewrd [ℓ 7→ τ]]⟩⟨E[[ℓ]con ], ξ⟩ −→ annotate(v, view, π, ⟨E[v], ξ′ ⟩)Рис. 13. Правило обработки потребляющего чтенияследней na-записи в которую он не осведомлён, т.е. его базовый фронт viewrdпо ℓ меньше, чем viewna (ℓ), то это также является состоянием гонки (см. правилаReadNA-stuck2 и WriteNA-stuck2).В отличие от рассмотренных ранее высвобождающих и sc-записей, naзапись не может быть использована для синхронизации (даже как часть высвобождающей цепочки), поэтому её сообщение имеет пустой фронт. Аналогично,na-чтение игнорирует фронт прочитанного им сообщения.2.2.6Потребляющие чтенияВ отличие от приобретающего чтения, которое обновляет базовый фронтпотока, и этим влияет на все последующие экземпляры чтения в потоке, потребляющее чтение влияют только на экземпляры, целевой адрес которых зависит отнего.
Аналогичным образом отличается влияние приобретающего и потребляющего чтений на последующие CAS-инструкции.Для поддержки потребляющих чтений добавлена возможность во время исполнения программы аннотировать инструкции чтения и CAS дополнительнымфронтом view, полученным из потребляющего чтения:sRT ::= ... | [ι]RM, view | casSM,FM, view (ι, v1 , v2 )β ::= ... | read⟨x, ι, RM, view⟩При исполнении аннотированной инструкции базовый фронт потока временноувеличивается на фронт view.При исполнении инструкции потребляющего чтения происходит аннотирование всех последующих зависимых инструкций с помощью соответствующегофронта сообщения (см.
рис. 13).55R-Rviewrdξ = ⟨M, ψrd , ψwr ⟩ π = path(E) M (ℓ, τ) = (v, view)= ψrd (π) viewrd (ℓ) ⩽ τξ′ = ⟨M, ψrd [π 7→ viewrd ⊔ [ℓ@τ]], ψwr ⟩⟨E[[ℓ]rlx ], ξ⟩ −→ ⟨E[v], ξ′ ⟩W-Rξ = ⟨M, ψrd , ψwr ⟩ π = path(E) τ = N extτ(M, ℓ)viewrd = ψrd (π) view = viewrd [ℓ 7→ τ]τrel = ψwr (π)(ℓ)(_, viewsync ) = M (ℓ, τrel )ξ′ = ⟨M [(ℓ, τ) 7→ (v, viewsync [ℓ 7→ τ])], ψrd [π 7→ view], ψwr ⟩⟨E[[ℓ] :=rlx v], ξ⟩ −→ ⟨E[v], ξ′ ⟩W-R’ξ = ⟨M, ψrd , ψwr ⟩ π = path(E) τ = N extτ(M, ℓ)viewrd = ψrd (π) view = viewrd [ℓ 7→ τ]view′wr = ψwr (π)[ℓ 7→ τ]ξ′ = ⟨M [(ℓ, τ) 7→ (v, view)], ψrd [π 7→ view], ψwr [π 7→ view′wr ]⟩⟨E[[ℓ] :=rel v], ξ⟩ −→ ⟨E[v], ξ′ ⟩Рис. 14. Правила расслабленных обращений2.2.7Расслабленные обращенияИсполнение расслабленных инструкций чтения не обновляет базовыйфронт потока на фронт прочитанного сообщения (см.
правило Readext−Relaxedна рис. 14), и это отличает расслабленные инструкции от приобретающих.Для поддержки расслабленных записей в состояние машины OpC11 нужновнести дополнительную компоненту ψwr :ξ ::= ⟨..., ψwr ⟩,где ψwr — это функция, которая по идентификатору потока возвращает его фронтзаписи viewwr . Фронт записи для каждой локации хранит метку времени последней высвобождающей записи, сделанной потоком в эту локацию. Когда потоквыполняет расслабленную запись в локацию ℓ с меткой времени τ (см. правилоWrite-Relaxed на рис.
14), то в добавляемое сообщение записывается фронт, равный комбинации [ℓ@τ] и фронта сообщения, на который указывает viewwr (ℓ). Для56поддержки описанного механизма нужно изменить правило обработки высвобождающей записи (см. правило Write-Release′ на рис. 14): после выполнения данногоправила фронт записи потока по целевой локации возвращает метку времени добавленного сообщения. Аналогично надо изменить другие подобные правила, вчастности, WriteSC.Кроме того, мета-функции, связанные с запуском и соединением потоков,также требуют нового определения:spawn(E, ⟨M,ψrd ,ψwr ⟩) = ⟨M, ψrd [π l 7→ viewrd , π r 7→ viewrd ],ψwr [π l 7→ ⊥, π r 7→ ⊥]⟩join(E, ⟨M, ψrd , ψwr ⟩) = ⟨M, ψrd [π 7→ viewlrd ⊔ viewrrd ], ψwr [π 7→ ⊥]⟩Дочерние потоки при запуске, также как и родительский после соединения, не наследуют фронты записи, т.к.
согласно C/C++11 MM [4] высвобождающие цепочкине могут выходить за пределы потока напрямую.2.2.8Отложенные операции и спекулятивное исполнениеПоддержка отложенных операций и спекулятивного исполнения в машинеOpC11 осуществляется с помощью двух следующих компонент состояния:ξ ::= ⟨..., φ, γ⟩.Функция φ по идентификатору потока π возвращает его иерархический операционный буфер α отложенный операций β:φ ::= π ⇀ αα ::= β∗β ::= read⟨x,ι,RM⟩ | write⟨x,ι,WM,e⟩ | bind⟨x,e⟩ | if ⟨x,e,α,α⟩Каждая отложенная операция β обладает уникальным идентификатором — символьным значением x. Отложенные операции чтения read⟨x,ι,RM⟩ хранят выражение для вычисления целевой локации ι5 , а также модификатор чтения RM.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
