Диссертация (1149932), страница 7
Текст из файла (страница 7)
Обсуждаются результаты тестирования модели на наборе “лакмусовых” тестов (litmus tests) и RCUструктуре (раздел 2.3). В заключении главы обсуждаются свойства модели (раздел 2.4).2.1Основные понятияOpC11 MM задается операционным способом, следовательно существуетабстрактная машина, связанная с моделью, которая исполняет программы по шагам. Далее для обозначения этой модели используется термин машина OpC11.2.1.1Память и базовый фронтСостояние машины OpC11 включается в себя множество сообщений, которое называется памятью.
Сообщение — это тройка, состоящая из локации, значения и метки времени (timestamp). Метка времени является натуральным числом ииспользуется для упорядочивания сообщений, которые связаны с одной и той желокацией. Такой порядок аналогичен отношению mo в аксиоматической C/C++11MM [4].34Рассмотрим машину OpC11 на примере исполнения следующей программы:[x] :=rlx 0; [y][x] :=rlx 1; a[y] :=rlx 1 bc:=rlx:=rlx:=rlx:=rlx0;[y];[x];[x](MP-rlx-2)Данная программа является очередной вариацией программы MP, в которой вовторой поток было добавлено дополнительное чтение из локации x. После исполнения первых двух инструкций ([x] :=rlx 0; [y] :=rlx 0) память машины будетсодержать два сообщения:M = {⟨x : 0@0⟩, ⟨y : 0@0⟩},где 0 – это метка времени.
После того, как левый поток закончит своё исполнение,в памяти будет находится четыре сообщения:M = {⟨x : 0@0⟩, ⟨y : 0@0⟩, ⟨y : 1@1⟩,⟨x : 1@1⟩}.Заметим, что в C/C++11 MM [4] у рассматриваемой программы есть сценарий поведения с результатом [a = 1, b = 0, c = 0]. Для того, чтобы разрешить этотрезультат, потоки машины OpC11 имеют право при чтении выбирать из памятисообщение не с самой большой меткой времени, как этого требовала бы абстрактная машина, представляющая модель SC, т.е. не самую последнюю запись в локацию. После завершения исполнения левого потока правый поток может сначалапрочитать сообщение ⟨y : 1@1⟩, присвоив в регистр a значение 1, а затем выполнить два чтения из старого сообщения ⟨x : 0@0⟩, получив b = c = 0.Отметим, что C/C++11 MM запрещает сценарий поведения с результатом[a = 1, b = 1, c = 0], поскольку гарантирует, что если поток “увидел” более новуюзапись в локацию (в данном случае это сообщение ⟨x : 1@1⟩), то он не может прочитать более старое, с точки зрения отношения mo, сообщение.
Для того, чтобыподдержать данное ограничение, в OpC11 MM у каждого потока есть т.н. базовыйфронт, viewcur . Базовый фронт — это частичная функция, которая по локации возвращает максимальную метку времени сообщения, связанного с локацией, о котором осведомлен поток. Когда поток пытается прочитать или записать сообщениев локацию ℓ с меткой времени τ, он проверяет, что τ больше или равно, чем значение его базового фронта по ℓ1 .1Строго говоря, поток никогда не “пытается” делать какое-то действие. В формальной модели упомянутая проверка реализуется как дополнительное условие в правилах чтения и записи.35Рассмотрим действие базового фронта на примере сценария поведения программы MP-rlx-2, который приводит к результату [a = 1, b = 1, c = _].
Изначальнов системе существует один поток T 0 с пустым базовым фронтом. После исполнения первых двух инструкций программы ([x] :=rlx 0; [y] :=rlx 0) базовый фронтпотока T 0.viewcur будет указывать на соответствующие сообщения из памяти:T 0.viewcur = [x@0, y@0].Далее машина стартует два потока T 1 и T 2, базовые фронты которых будут равны T 0.viewcur . После исполнения инструкции (левого) потока T 1 память машиныбудет содержать два новых сообщения, а базовый фронт потока T 1 станет равным 1 по обоим локациям, т.к.
поток, сделавший запись, естественным образомосведомлён о ней:T 1.viewcur = [ x@1 , y@1 ];T 2.viewcur = [x@0, y@0].После этого (правый) поток T 2 может прочитать новое сообщение в локацию y,присвоив 1 в регистр a и увеличив свой фронт по локации y до 1:T 1.viewcur = [x@1, y@1];T 2.viewcur = [x@0, y@1 ].Т.к. базовый фронт потока T 2 по локации x равен 0, т.е. поток ещё не осведомлёно новой записи в x, то поток может прочитать либо сообщение ⟨x : 0@0⟩, либосообщение ⟨x : 1@1⟩. Для того, чтобы b равнялось 1, поток T 2 должен выполнитьчтение из более нового сообщения, что обновит его базовый фронт по локации x:T 1.viewcur = [x@1, y@1];T 2.viewcur = [ x@1 , y@1].После этого потоку T 2 остаётся только выполнить последнее чтение (c :=rlx[x]), и поскольку его базовый фронт по локации x равен 1, то он может прочитатьтолько из нового сообщения в локацию x (⟨x : 1@1⟩).
Как следствие, результат[a = 1, b = 1, c = 0] невозможен для программы MP-rlx-2 в OpC11 MM.2.1.2Синхронизация потоковРассмотрим программу MP-rel-acq из главы 1.[x] :=rlx 0; [y] :=rlx 0;[x] :=rlx 1; a :=acq [y];[y] :=rel 1 b :=rlx [x](MP-rel-acq)36Для этой программы результат [a = 1, b = 0] запрещён в C/C++11 MM, т.к. еслиa = 1, то между потоками произошла синхронизация (т.е. в соответствующем графе есть ребро отношения sw), и перед выполнением b :=rlx [x] правый потокдолжен быть осведомлен о записи [x] :=rlx 1.Для того, чтобы выразить такую синхронизацию, у каждого сообщения машины OpC11 есть четвертая дополнительная компонента — фронт сообщения.Фронт сообщения m хранит информацию о сообщениях, о которых узнаёт поток,выполнивший приобретающее (acq) чтение сообщения m.
Если поток T выполняет высвобождающую (rel) запись, то фронтом сообщения, которое будет добавлено в память как результат исполнения записи, будет базовый фронт потокаT на момент выполнения записи. Расслабленные (rlx) записи также помещаютфронт в сообщения, но в соответствии с более сложными правилами, которые будут описаны в разделе 2.1.9.Рассмотрим сценарий поведения MP-rel-acq, в результате которого a = 1.После того, как выполнены две инициализирующие записи и запущены два потока, память и базовые фронты потоков выглядят следующим образом:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0,[y@0]⟩};T 1.viewcur = [x@0, y@0]; T 2.viewcur = [x@0, y@0].После исполнения двух записей (левым) потоком T 1 в память попадает два новыхсообщения, одно из которых было сделано высвобождающей записью:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0,[y@0]⟩,⟨x : 1@1, [x@1]⟩, ⟨y : 1@1, [x@1,y@1]⟩};T 1.viewcur = [x@1, y@1]; T 2.viewcur = [x@0, y@0].После того, как (правый) поток выполняет приобретающее чтение из сообщения⟨y : 1@1,[x@1,y@1]⟩, его базовый фронт увеличивается по обоим компонентам:T 2.viewcur = [ x@1 , y@1].После этого (правый) поток T 2 не может прочитать старое сообщение ⟨x :0@0, [x@0]⟩.
Таким образом OpC11 MM запрещает результат [a = 1, b = 0] дляпрограммы MP-rel-acq.2.1.3Операционные буфераТем не менее, не все слабые сценарии поведения программ, наблюдаемые вC/C++11 MM, могут быть описаны приведенными выше способами. Рассмотрим37программу LB-rlx (load buffering, буферизация записи):[x] :=rlx 0; [y] :=rlx 0;a :=rlx [x]; b :=rlx [y];[y] :=rlx 1 [x] :=rlx 1(LB-rlx)C/C++11 MM допускает сценарий поведения этой программы с результатом [a =1, b = 1]. Такой результат требует, чтобы в момент исполнения инструкции a :=rlx[x] в памяти находилось сообщение ⟨x : 1@_,_⟩.
Это означает, что инструкция[x] :=rlx 1 должна быть выполненной. Аналогичное утверждение верно и дляпары инструкций b :=rlx [y] и [y] :=rlx 1. Таким образом, хотя бы в одном изпотоков инструкция записи должна быть исполнена раньше чтения.Для решения этой проблемы OpC11 MM добавляет в состояние каждогопотока по операционному буферу — списку записей об отложенных инструкциях, которые хранят всю необходимую информацию для дальнейшего исполнения.Так, в частности, когда поток откладывает инструкцию чтения, он заменяет её впрограмме на новое, уникальное символьное значение2 , а в буфер добавляет пару, состоящую из символьного значения и целевой локации.
Для отложенной инструкции записи в буфер сохраняется целевая локация и значение, которое нужнозаписать. Далее поток машины OpC11 может недетерминировано выбрать отложенную инструкцию из буфера и исполнить её, если в буфере перед ней нет инструкции, которая может непосредственно повлиять на результат выбранной. Так,данный механизм позволяет в программе LB-rlx отложить исполнение инструкции чтения в левом потоке, что даёт возможность получить результат [a = 1, b = 1].2.1.4Спекулятивное исполнениеC/C++11 MM поддерживает оптимизацию, которая выносит за пределыусловного оператора инструкцию, которая встречается в обоих ветках оператора.Рассмотрим программу SE-simple (speculative execution, спекулятивное исполне2 OpC11MM описана в стиле редукционных контекстов [13, 18], т.е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
