Диссертация (1149932), страница 8
Текст из файла (страница 8)
программа представляется каквыражение, которое постепенно редуцируется. Как следствие, инструкция чтения в этой семантике — этонекоторое подвыражение, которое, будучи вычисленным, заменяется на прочитанное значение. Подробноеописание семантики в виде редукционных контекстов приведено в разделе 2.2.38ние):[x] :=rlx 0; [y] :=rlx 0; [z] :=rlx 0;a :=rlx [x];b :=rlx [y];if aif bthen [z] :=rlx 1;then [x] :=rlx 1[y] :=rlx 1else skipelse [y] :=rlx 1fific :=rlx [z](SE-simple)В этой программе инструкция [y] :=rlx 1 не зависит от условия if-оператора,и поэтому может быть выполнена перед инструкцией a :=rlx [x].
Это позволяетполучить результат c = 1.Для того, чтобы поддержать такие сценарии, в OpC11 MM операционныебуфера могут быть вложенными. Когда исполнение потока подходит к условномуоператору, условие которого зависит от ранее отложенной операции, модель добавляет в буфер кортеж, который содержит символическое представление условия, а также два пустых буфера. Эти буфера в дальнейшем будут пополнятьсяотложенными инструкциями then и else веток оператора.Рассмотрим сценарий поведения программы SE-simple, в результате которого c = 1. После исполнения инициализирующих инструкций записи память машины OpC11 содержит три сообщения:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0,[y@0]⟩, ⟨z : 0@0,[z@0]⟩}.Далее левый поток откладывает выполнение инструкции чтения и начинает спекулятивно, т.е. без вычисления значения условия, исполнять инструкции ветокусловного оператора.
Так, в буфере левого потока оказывается две записи:⟨a :=rlx [x]; if a ⟨⟩ ⟨⟩⟩.Продолжая (спекулятивно) откладывать инструкции, левый поток помешает всеинструкции из условного оператора в соответствующие подбуфера:⟨a :=rlx [x]; if a ⟨[z] :=rlx 1; [y] :=rlx 1⟩ ⟨[y] :=rlx 1⟩⟩.После того, как в подбуферах появляются одинаковые инструкции (в данном случае это [y] :=rlx 1), и перед ними в подбуферах нет конфликтующих инструкций,39OpC11 MM может вынести их на предыдущей уровень буфера:⟨a :=rlx [x]; [y] :=rlx 1; if a ⟨[z] :=rlx 1⟩ ⟨⟩⟩.Далее, поскольку инструкции a :=rlx [x] и [y] :=rlx 1 независимы, то [y] :=rlx1 может быть выполнена, после чего в памяти появляется новое сообщение:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0,[y@0]⟩, ⟨z : 0@0,[z@0]⟩, ⟨y : 1@1,[y@1]⟩}.После этого результат c = 1 получается следующим образом.
Правый поток читаетиз нового сообщения, присваивая 1 в b. Поскольку в правом потоке условие послеэтого было вычислено к значению 1, то может быть выполнена инструкция записив локацию x:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0,[y@0]⟩, ⟨z : 0@0,[z@0]⟩,⟨y : 1@1,[y@1]⟩, ⟨x : 1@1,[x@1]⟩}.После этого левый поток может выполнить отложенное чтение a :=rlx [x] издобавленного сообщения. Так, в буфере левого потока остаётся только одна запись, соответствующая отложенной конструкции if, чьё условие было вычислено к значению 1:⟨if 1 ⟨[z] :=rlx 1⟩ ⟨⟩⟩.После вычисления отложенной конструкции if и выполнения записи в z в памятинаходится шесть сообщений:M = {⟨x : 0@0, [x@0]⟩, ⟨y : 0@0,[y@0]⟩, ⟨z : 0@0,[z@0]⟩,⟨y : 1@1,[y@1]⟩, ⟨x : 1@1,[x@1]⟩, ⟨z : 1@1,[z@1]⟩}.Чтение из последней записи в локацию z приводит к результату c = 1.Идея перевода повторяющихся инструкций из вложенных буферов естественным образом обобщается на случай вложенных условных операторов.2.1.5 sc-инструкцииC/C++11 MM гарантирует наличие тотального порядка sc на sc-событиях,который не противоречит программному порядку po, отношению “синхронизируется с” sw, и порядку памяти mo.
Помимо этого sc-чтение обладает теми жесвойствами, что и приобретающее чтение, а sc-записи — что и высвобождающие записи.40Рассмотрим программу SB-sc (store buffering, буферизация записи):[x] :=sc 0; [y] :=sc 0;[x] :=sc 1; [y] :=sc 1a :=sc [y]; b :=sc [x];(SB-sc)Для этой программы C/C++11 MM запрещает результат [a = 0, b = 0].
Это объясняется тем, что в её сценарии поведения, как минимум, одно из чтений находитсяпозже все остальных событий в отношении sc, а это значит, что соответствующий поток в момент исполнения этого чтения осведомлён о всех (sc-)записях впрограмме.Для того, чтобы гарантировать аналогичное ограничение, в состояние машины OpC11 добавляется глобальный (общий для всех потоков) компонент — scфронт viewsc .
Он используется следующим образом: при выполнении sc-чтенияиз локации ℓ поток обновляет свой базовый фронт на [ℓ@viewsc (ℓ)], а при выполнении sc-записи в локацию ℓ сообщения с меткой времени τ поток обновляет scфронт на [ℓ@τ]. Таким образом, sc-чтение из локации ℓ не может прочитать сообщение в памяти, которое имеет меньшую метку времени, чем метка сообщенияв ту же локацию, которое было записано последней на тот момент sc-записью.2.1.6Неатомарные обращенияСогласно C/C++11 MM, программы с гонками по данным [97], в которыхучаствуют неатомарные обращения к памяти, обладают неопределенном поведением.
Так, рассмотрим программу DR-rlx-na (data race, гонка по данным):[d] :=na 0;[d] :=rlx 1; a :=na [d];(DR-rlx-na)В ней есть гонка по данным между инструкциями [d] :=rlx 1 и a :=na [d].Мы можем идентифицировать эту гонку с помощью базовых фронтов в случаесценария, в котором сначала левый поток выполняет запись, а потом правый —чтение. В такой ситуации правый поток будет выполнять неатомарную операциюнад локацией d, при этом не являясь осведомленным о последний записи в даннуюлокацию. Если OpC11 MM идентифицировала гонку по данным, в которую вовлечена неатомарная операция хотя бы в одном сценарии поведения программы, тосчитается, что программа в целом обладает неопределенным поведением.41Рассмотрим похожую программу, также содержащую гонку по данным:[d] :=na 0;[d] :=na 1; a :=rlx [d];(DR-na-rlx)Идентификация гонки в данном случае не может быть проведена только с помощью базовых фронтов потоков.
Для решения проблемы в состояние машиныOpC11 вводится ещё один глобальный фронт — na-фронт viewna . Подобно scфронту, na-фронт по локации возвращает метку времени последней na-записи внеё. Так, при выполнении любой операции над локацией ℓ поток проверяет, чтоон осведомлён о последней na-записи в ℓ (т.е. его базовый фронт по ℓ больше илиравен viewna (ℓ)), и если это не так, то машина OpC11 сигнализирует о гонке.С помощью такой техники гонка по данным в программе DR-na-rlx идентифицируется в сценарии поведения, в котором na-запись левого потока выполняется до rlx-чтения правого потока.2.1.7Потребляющие чтенияПотребляющее (consume, con) чтение является более слабой версией приобретающего чтения.
Приобретающее чтение обновляет базовый фронт потока спомощью фронта прочитанного сообщения и тем самым влияет на все последующие инструкции, тогда как потребляющее чтение действует только на последующие чтения, которые зависят от него по адресу3 .Рассмотрим программу, в которой используется потребляющее чтение:[p] :=na null; [d] :=na 0; [x] :=na 0;a :=con [p];if a ̸= null[x] :=rlx 1; then b :=na [a];[d] :=na 1;c :=rlx [x][p] :=rel d else b := 0;c := 0fi(MP-con-na-2)В этой программе левый поток передаёт информацию, записанную в локацию d,правому потоку через указатель p. Правый поток с помощью con-чтения заносит3 Инструкциячтения i зависит по адресу от инструкции чтения j, если целевой адрес i зависит отрезультата исполнения j.42в переменную a содержимое указателя p. Если переменная a не равна null, топоток читает из той локации, на которую указывает a (в данном случае на локациюd), а потом — из локации x.
В C/C++11 MM у этой программы существует тривозможных результата исполнения: [a = null, b = 0, c = 0], [a = d, b = 1, c = 1]и [a = d, b = 1, c = 0]. Если в программе con-чтение заменить на acq-чтение,то последний результат станет невозможным, т.к. после выполнения a :=acq [p]с результатом d базовый фронт правого потока будет указывать на сообщения,которые были получены в результате исполнения [x] :=rlx 1 и [d] :=na 1. В тоже время con-чтение a :=con [p] “синхронизирует” только последующее чтениеb :=na [a], т.к. оно является разыменованием результата con-чтения и не влияетна независимое чтение c :=rlx [x].Для поддержки подобного поведения OpC11 MM может аннотировать спомощью фронтов инструкции чтения, которые зависят от con-чтений.
Когда потребляющее чтение получает из памяти сообщение ⟨ℓ : v@τ,view⟩, то, вместотого, чтобы обновить базовый фронт потока с помощью view, как это сделалобы приобретающее чтение, оно помечает все зависимые от него инструкции чтения фронтом view. В дальнейшем, когда помеченная инструкция чтения будет исполняться, она скомбинирует базовый на тот момент фронт потока с фронтомпометкой для того, чтобы вычислить минимальную метку времени, сообщение скоторой доступно для чтения. Аналогичным образом помечаются и обрабатываются отложенные чтения в операционных буферах, которые ссылаются на символьный результат con-чтения.2.1.8Соединение потоковВ момент соединения потоков, т.е.
когда оба потока закончили своё исполнение, естественно ожидать, что все отложенные операции были выполнены,и, соответственно, операционные буфера пусты. Это подтверждается тем, что вC/C++11 MM [4] используется отношение “дополнительно синхронизируется с”(additional-synchronizes-with, asw), которое связывает последние событие потокас первой следующей за потоком инструкцией родительского потока. Отношениеasw является частью отношения hb. Это означает, что родительский поток оказывается осведомлен о всех сообщениях, которые были прочитаны дочерними потоками. В OpC11 MM это выражается так: соединение потоков возможно, толькоесли их операционные буфера пусты, а после соединения потоков родительский43поток получает базовый фронт, равный комбинации базовых фронтов соединяемых потоков.Тем не менее, это противоречит стандартам C и C++11, требующим, чтобыоптимизация секвенциализации (C1 || C2 ⇝ C1 ; C2 ) была корректной. Это делаетпредыдущие предположения некорректными.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
