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

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

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

Вслучае отложенной записи также сохраняется выражение e, результат вычисления которого будет записан как целевое значение. Для представления отложенного присваивания в локальную переменную используется конструкция bind⟨x, e⟩,5 Целеваяопераций.локация отложенной операции может зависеть от других, ещё не вычисленных, отложенных57которая может быть использована для того, чтобы не форсировать вычислениеотложенного чтения:a :=rlx [x]; b := a + 1; ...Для представления информации о спекулятивном исполнении веток условногооператора используется конструкция if ⟨x,e,α1 ,α2 ⟩, где e является представлением условия, а α1 и α2 — вложенных буферов отложенных операций веток thenи else соответственно.

Редукционный контекст Eα, внутри которого возможноспекулятивное исполнение инструкций, представлен следующей грамматикой:Eα ::= [ ] | x := Eα; s | if x then Eα else s fi |if x then s else Eα fiУ конкретного подвыражения редукционного контекста символическое значениеx, представляющее условие спекулятивно исполняемой конструкции, должно совпадать с идентификатором соответствующей записи if ⟨x,e,α1 ,α2 ⟩ в буфере отложенных операций.Вторая добавленная компонента состояния, γ, представляет ограничения, накладываемые на приобретающие чтения, и является списком троек вида⟨ℓ, τ, x⟩. Присутствие тройки ⟨ℓ, τ, x⟩ в списке γ запрещает чтение из памяти сообщения (ℓ, τ), пока отложенная операция с символическим значением x не будетвыполнена.В ходе исполнения программы любая инструкция чтения, записи или присваивания может быть отложена, даже если она находится в условном операторе— для этого в операционный буфер добавляется соответствующий элемент.

Правила откладывания исполнения инструкций приведены на рис. 15.После того, как операция была отложена, она может быть выполнена —см. правила на рис. 16. В этих правилах для записи и чтения опущены стандартные части, связанные с обновлением базового фронта и фронта записи. Рассмотрим подробнее правило Write-Resolve.

С его помощью (недетерминированно) выбирается элемент из буфера отложенных операций, соответствующий некоторойинструкции записи, причём этот элемент обязан содержаться на первом уровнебуфера. Без последнего требования семантика допускала бы “значения из воздуха”. Кроме того, перед выбранным элементом списка не должно быть элементов, которые находятся с ним в конфликте, таких как приобретающее чтение илизапись в ту же локацию. Из новой компоненты отложенных операций убирается соответствующий элемент (φ′ = removeAndUpdate(φ, π, write⟨x, ℓ, WM, v⟩)),58W-Pξ = ⟨M, ψrd , φ, γ⟩x — новое символическое значениеα = φ(π)ξ′ = ⟨M, ψrd , φ[π 7→ append(α, Eα, write⟨x, ι, WM, e⟩)], γ⟩⟨E[Eα[[ι] :=WM e]], ξ⟩ −→ ⟨E[Eα[x]], ξ′ ⟩R-Pξ = ⟨M, ψrd , φ, γ⟩x — новое символическое значение′rdα = φ(π)ξ = ⟨M, ψ , φ[π 7→ append(α, Eα, read⟨x, ι, RM⟩)], γ⟩⟨E[Eα[[ι]RM ]], ξ⟩ −→ ⟨E[Eα[x]], ξ′ ⟩L -Pξ = ⟨M, ψrd , φ, γ⟩e зависит от отложенной операцииx — новое символическое значение′rdα = φ(π)ξ = ⟨M, ψ , φ[π 7→ append(α, Eα, let⟨x,e⟩)], γ⟩⟨E[Eα[x′ := e; s]], ξ⟩ −→ ⟨E[Eα[x′ /x]], ξ′ ⟩Рис.

15. Правила откладывания исполнения инструкций чтения, записи иприсваиванияобновляются фронты зависимых сообщений согласно γ-компоненте (M ′ =updateSync(x, WM, view, γ, M )), а из самой γ-компоненты удаляются зависимости (γ′ = updateDep(x, WM, ψwr , ℓ, τ, γ, φ(π))).Отдельно стоит отметить правило, которое позволяет вынести отложенныеинструкции записи, повторяющиеся в ветках спекулятивно исполняемого условного оператора, на предыдущий уровень вложенности буфера отложенных операций (см. рис. 17).Правила обработки условного оператора (начало и завершение спекулятивного исполнения) приведены на рис.

18.2.3Интерпретация и тестирование моделиИнтерпретатор для OpC11 MM [98] был разработан на языке программирования Racket [16, 17] с использованием средства разработки интерпретаторовPLT/Redex [18,19]. Средство PLT/Redex позволяет описать интерпретатор в стиле,использованном нами для описания модели — как множества правил переписывания состояния некоторой абстрактной машины. Также это средство использует59W-Rξ = ⟨M, ... , φ, γ⟩...write⟨x, ℓ, WM, v⟩ находится на первом уровне φ(π)и не конфликтует с предшествующими элементами спискаφ′ = removeAndUpdate(φ, π, write⟨x, ℓ, WM, v⟩)γ′ = updateDep(x, WM, ψwr , ℓ, τ, γ, φ(π))M ′ = updateSync(x, WM, view, γ, M )ξ′ = ⟨M ′ [(ℓ, τ) 7→ (v, view)], ...

, φ′ [v/x], γ′ ⟩⟨s, ξ⟩ −→ ⟨s[v/x], ξ′ ⟩R-Rξ = ⟨M, ... , φ, γ⟩...read⟨x, ℓ, RM⟩ находится в φ(π)и не конфликтует с предшествующими элементамиφ′ = removeAndUpdate(φ, π, read⟨x, ℓ, RM⟩)γ′ = γ \ {⟨_, _, x⟩}ξ′ = ⟨M, ... , φ′ [v/x], γ′ ⟩⟨s, ξ⟩ −→ ⟨s[v/x], ξ′ ⟩L -Rξ = ⟨M, ψrd , φ, γ⟩bind⟨x, v⟩ находится в φ(π)φ′ = removeAndUpdate(φ, π, bind⟨x, v⟩)ξ′ = ⟨M, ψrd , φ′ [v/x], γ⟩⟨s, ξ⟩ −→ ⟨s[v/x], ξ′ ⟩Рис. 16. Правила по выполнению отложенных инструкций чтения, записи иприсваиванияидеи редукционной семантики [13, 18, 19] и имеет встроенные механизмы разбиения термов на редукционный контекст и подтерм.Реализация базовых правил целевого языка интерпретации, описанных вразделах 2.2.1 и 2.2.2, а также вспомогательных функций, занимает 2070 строккода, реализация различных аспектов C/C++11 MM (разделы 2.2.3–2.2.8) — 1310строк. Код тестов, описанных в разделах 2.3.1 и 2.3.2, занимает 3130 строк.2.3.1“Лакмусовые” тестыПроверка адекватности OpC11 MM и её сравнение с C/C++11 MM были проведены на наборе т.н.

“лакмусовых” тестов (litmus tests) — небольших программ,60W-Pξ = ⟨M, ψrd , φ, γ⟩if ⟨x′′ , e, α1 , α2 ⟩ внутри φ(π)write⟨x, ℓ, WM, v⟩ в списке α1и не конфликтует с предшествующими элементами спискаwrite⟨x′ , ℓ, WM, v⟩ в списке α2и не конфликтует с предшествующими элементами спискаφ′ = promote(x, x′ , φ)γ′ = γ[x′ /x]⟨s, ξ⟩ −→ ⟨s[x′ /x], ξ′ ⟩Рис. 17. Правило по переносу отложенной записи на предыдущий уровеньвложенности буфера отложенных операцийI -S-Iξ = ⟨M, ψrd , φ, γ⟩e зависит от отложенной операцииx — новое символическое значениеα = φ(π)ξ′ = ⟨M, ψrd , φ[π 7→ append(α, Eα, if ⟨x,e, ⟨⟩, ⟨⟩⟩)], γ⟩⟨E[Eα[if e then s1 else s2 fi]], ξ⟩ −→⟨E[Eα[if x then s1 else s2 fi]], ξ′ ⟩I -R-Tξ = ⟨M, ψrd , φ, γ⟩if ⟨x, z, α1 , α2 ⟩ ∈ φ(π)z≠ 0φ′ = φ[if ⟨x, z, α1 , α2 ⟩/α1 ]ξ′ = ⟨M, ψrd , φ′ , γ⟩⟨E[Eα[if x then s1 else s2 fi]], ξ⟩ −→ ⟨E[Eα[s1 ]], ξ′ ⟩I -R-Fif ⟨x, 0, α1 , α2 ⟩ ∈ φ(π)ξ = ⟨M, ψrd , φ, γ⟩φ′ = φ[if ⟨x, z, α1 , α2 ⟩/α2 ]ξ′ = ⟨M, ψrd , φ′ , γ⟩⟨E[Eα[if x then s1 else s2 fi]], ξ⟩ −→ ⟨E[Eα[s2 ]], ξ′ ⟩Рис.

18. Правила начала и завершения спекулятивного исполнения условногооператора61которые являются показательными примерами различных видов взаимодействияпотоков. Эти тесты активно используются в литературе [4, 66, 99–101] для обсуждения свойств моделей памяти. При тестировании нам нужно было проверить, чтоожидаемые результаты исполнения программы и её исходы совпадают. Для этого по каждому тесту средствами PLT/Redex строился полный, т.е.

включающийв себя все возможные сценарии поведения теста, граф состояний и переходов всоответствии с правилам, задающим интерпретатор OpC11. Далее из этого графаизвлекалось множество финальных состояний, которое сравнивалось с ожидаемыми результатами.В табл. 1 предоставлена информация о “лакмусовых” тестах в контекстеOpC11 MM. Столбцы VF–JN показывают, какие аспекты модели требуются дляподдержки нужного поведения тестов.

В таблице использованы следующие сокращения: VF (viewfront) — базовый фронт, ψrd ; WF (write-fronts) — фронтзаписи, ψwr ; SCF (sc-front) — sc-фронт, viewsc ; NAF (na-front) — na-фронт,viewna ; PO (postponed operations) — отложенные операции, α; ARR (acquire readrestrictions) — ограничение приобретающих чтений, γ; CR (consume-reads) —маркировка, связанная с потребляющими чтениями; JN (joining threads) — соединение потоков с не пустыми буферами. Последний столбец C11 представляетинформацию о том, полностью ли совпадают результаты OpC11 MM и С/C++11MM.В таблице тесты разделены на группы; в каждой группе тесты имеют схожую структуру, но различаются модификаторами доступа.

Код тестов и информация об ожидаемом поведении тестов размещён в приложении А.Расхождения с MM C/C++11 MMДля того, чтобы на тестах LB-acq-rlx и LB-acq-rlx-join поддержать те же результаты исполнения, что и в C/C++11 MM, нужно позволить инструкции расслабленной записи, которая следует за инструкцией приобретающего чтения,быть исполненной перед этим чтением. Как и все слабые сценарии поведения,такой сценарий может быть следствием либо компиляторной оптимизации, либооптимизирующего исполнения программы на процессоре. В общем случае перестановка приобретающего чтения с какой бы то ни было последующей инструкцией небезопасна, т.к.

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

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