Диссертация (1149932), страница 9
Текст из файла (страница 9)
Данная проблема может быть проиллюстрирована на следующей программе, в которой параллельная композицияс пустым потоком может быть заменена на не пустой поток:[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y] skip b :=rlx [x] skip[x] :=rlx 1[y] :=rlx 1(LB-rlx-join)Если применить такую оптимизацию к одной из композиций потоков, то результат [a = 1, b = 1] станет возможным. Для того, чтобы поддержать данный сценарийповедения, в интерпретаторе модели допускается альтернативное правило соединения потоков как отдельный аспект.2.1.9Расслабленные обращения и синхронизацияМежду расслабленными операциями, высвобождающими записями и приобретающими чтениями существует тонкое взаимодействие. В этом подразделеописываются варианты этого взаимодействия, а также технические решения вOpC11 MM, обеспечивающие его.Высвобождающие цепочкиВ связи с тем, что расслабленное чтение не может участвовать в синхронизации, его исполнение не обновляет базовый фронт потока фронтом прочитанногосообщения, как это происходит в случае приобретающего чтения.
Тем не менее,если приобретающее чтение потока T2 читает из сообщения, которое было добавлено расслабленной записью wrlx потока T1 , то оно должно синхронизироваться свысвобождающей записью в ту же локацию wrel , предшествующую wrlx в потокеT1 , если такая запись существует. Это свойство является аналогом высвобождающих цепочек (release sequences) из C/C++11 MM [4].44Рассмотрим вариант программы MP, в сценариях поведения которого имеется описанная выше синхронизация:[d][f ][x][f ][f ] :=na 0; [d] :=na 0; [x] :=na 0;:=na 5;repeat c :=acq [f ]; c == 2 end;:=rel 1;a :=na [d];:=rel 1;b :=rlx [x]:=rlx 2(MP-rel-acq-na-rlx-2)Единственным значением, которое может получить регистр a, является 5.
Этообъясняется тем, что последнее приобретающее чтение c :=acq [f ] в цикле должно прочитать значение 2, следовательно синхронизироваться с высвобождающейзаписью [f ] :=rel 1. В то же время регистр b может получить как значение 0, таки 1, поскольку запись [f ] :=rel 1, с которой синхронизируется приобретающеечтение, предшествует записи [x] :=rel 1, и поэтому информация об этой записив x не попадает во фронт сообщения, записанного инструкцией [f ] :=rel 1.Для того, чтобы выразить такую синхронизацию, у каждого потока в машине OpC11 имеется фронт записи (write-front) viewwrite . Этот фронт для каждойлокации возвращает метку времени последней высвобождающей записи, сделанной потоком в эту локацию.
Когда поток выполняет расслабленную запись в локацию ℓ с меткой времени τ, в соответствующее сообщение записывается фронт,который является комбинацией [ℓ@τ] и фронта сообщения в ℓ с меткой времениviewwrite (τ), которое было записано высвобождающей записью того же потока.Отложенные расслабленные обращения и синхронизацияРассмотрим вариант программы LB, в которой инструкции чтения являютсярасслабленными, а записи — высвобождающими:[x] :=rlx 0; [y] :=rlx 0;a :=rlx [x]; b :=rlx [y];[y] :=rel 1 [x] :=rel 1(LB-rel-rlx)Согласно C/C++11 MM эта программа имеет сценарий поведения с результатом[a = 1, b = 1], поскольку высвобождающие записи не накладывают никаких дополнительных ограничений в отсутствии приобретающих чтений. Поэтому OpC11MM разрешает исполнять высвобождающие записи даже в тот момент, когдапредшествующие отложенные инструкции чтения ещё не выполнены.45Тем не менее, требуются ввести некоторые ограничения на то, как инструкции чтения могут быть отложены через высвобождающие записи.
Рассмотримещё один вариант программы LB.[x] :=rlx 0; [y] :=rlx 0;a :=acq [x]; b :=rlx [y];[y] :=rlx 1 [x] :=rel 1(LB-rel-acq-rlx)В этой программе в левом потоке есть приобретающее чтение, а в правом —высвобождающая запись. Если это чтение прочитает сообщение, сделанное инструкцией [x] :=rel 1, т.е.
регистр a получит значение 1, то в терминах С/С++11MM между b :=rlx [y] и [y] :=rlx 1 возникнет ребро отношения “предшествует”hb. Следовательно, регистр b не может получить значение 1, т.к. чтение не можетпрочитать то, что записано последующей за ним записью. Таким образом, OpC11MM должна предотвращать ситуацию, когда чтение, которое было отложено черезвысвобождающую запись W , выполняется после того, как другой поток прочиталсообщение W с помощью приобретающего чтения.Для реализации данного ограничения в состояние машины OpC11 добавляется глобальный компонент γ, который является списком троек, состоящих излокации, метки времени некоторого существующего сообщения и символического значения, идентифицирующего отложенное чтение. При выполнении высвобождающей записи W , которая добавляет сообщение локации ℓ с меткой времениτ, для каждого отложенного потоком чтения в список γ добавляется по тройке⟨ℓ,τ, x⟩, где x — символическим значение чтения.
При этом приобретающее чтение из сообщения локации ℓ с меткой времени τ возможно только в том случае,если в γ не осталось записей вида ⟨ℓ, τ, _⟩, а выполнение отложенного чтения ссимволическим значением x удаляет из γ все тройки ⟨_,_,x⟩.Следующая программа иллюстрирует ещё одну особенность, которая связана с откладыванием расслабленных записей через высвобождающие:[x] :=rlx 0; [y] :=rlx 0;[x] :=rlx 1; [y] :=rlx 1;[y] :=rel 1 [x] :=rel 1a :=rlx [x]; b :=rlx [y](WR-rlx-rel)Согласно C/C++11 MM, результат [a = 1, b = 1] возможен для этой программы,и это требует, чтобы сообщения расслабленных записей попали в память после46сообщений высвобождающих.
При этом, если другой (третий) поток выполнитприобретающее чтение из сообщения, сделанного одной из высвобождающих записей, то он должен стать осведомлённым о предшествующей расслабленной записи, а для этого соответствующее сообщение должно находиться в памяти.Аналогично предыдущему пункту, данная проблема решается с помощьюсписка γ. При исполнении высвобождающей записи также, как и для отложенных чтений, в списке γ появляются тройки, связанные с отложенными записями.Единственным отличием от обработки отложенных чтений является то, что привыполнении отложенной записи W не только удаляются все тройки ⟨ℓ, τ, x⟩, гдеx — символьный идентификатор записи, но и увеличивается фронт сообщениялокации ℓ с меткой времени τ на [ℓ′ @τ′ ], где ℓ′ и τ′ связаны с сообщением W .2.2Формальное описание моделиВ разделе приводится математическое определение OpC11 MM, включаяопределение синтаксиса языка, для которого задана модель, представления памяти и фронтов.2.2.1Синтаксис языка модели и базовые правила редукцииСинтаксис языка модели представлен на рис.
6. Мета-переменная e представляет выражения, которые могут быть целыми числами z, локациями ℓ, неизменяемыми локальными переменными x, парами, проекциями пар или бинарными выражениями. Конструкция choice является недетерминированным выбором между двумя выражениями.Программы представляются как операторы s, где x := s1 ; s2 является letвыражением, spw s1 s2 — параллельной композицией потоков, [ι]RM — выражением чтения из памяти. В примерах также используются дополнительные обозначения:– оператор skip вместо константного выражения 0,– выражения x :=RM [ι] и x := e для обозначения x := [ι]RM ; x и x := e; x,– оператор s1 ; s2 вместо x′ := s1 ; s2 , где x′ не встречается в s2 ,– конструкция s1 ||s2 для обозначения spw s1 s2 .Результатом программы является либо значение v, либо значение времениисполнения (run-time value) stuck, которое символизирует, что что-то пошло не47e ::= x | z (∈ Z) | e1 op e2 | choice e1 e2fst e | snd e | (e1 , e2 ) | ιop ::= + | − | ∗ | / | % | == |̸=ι ::= ℓ | xℓ — идентификатор локацииx — локальная переменнаяv ::= ℓ | z | (v1 , v2 )s ::= e | x := s1 ; s2 | spw s1 s2 |if e then s1 else s2 fi | repeat s end |[ι]RM | [ι] :=WM e | casSM,FM (ι, e1 , e2 )sRT ::= stuck | par s1 s2RMWMSMFM::=::=::=::=sc | acq | con | rlx | nasc | rel | rlx | nasc | acqrel | rel | acq | con | rlxsc | acq | con | rlxРис.
6. Синтаксис операций и выражений языка модели OpC11так — в исполнении найдена гонка по данным или была попытка чтения из неинициализированной переменной. Другой конструкцией времени исполнения является par s1 s2 , которая получается в результате редукции spw s1 s2 и представляетнаходящиеся в исполнении потоки. На шаге операционной семантики, которыйредуцирует spw s1 s2 в par s1 s2 , происходит необходимая инициализация компонент машины OpC11.Мета-переменная ξ представляет динамическое состояние машины с точностью до программы. Вычисление программы s в машине OpC11 начинаетсясо стартового состояния ⟨s, ξinit ⟩, где ξinit содержит пустую память и пустой базовый фронт для единственного стартового потока. Переходы машины заданы вредукционном стиле [13], большинство из них имеет следующий вид:...⟨E[s], ξ⟩ −→ ⟨E[s′ ], ξ′ ⟩48Здесь E — это редукционный контекст, заданный так:E ::= [ ] | x := E; s | par E s | par s E.Если в момент исполнения программы запущено более одного потока, т.е.
в программном выражении присутствует узел par, то программное выражение можетбыть недетерминированно разбито на контекст и подпрограмму.Базовые правила семантики, которые не затрагивают операций над памятью, приведены на рисунке 7. Из них интерес представляют правила Spawn и Join,которые описывают старт и соединение дочерних потоков соответственно. Этиправила модифицируют компоненты состояния машины OpC11, которые являются локальными для потоков, например, базовый фронт и операционный буфер.Конкретные представления правил Spawn и Join зависят от многопоточных аспектов модели, которые определяют мета-функции spawn и join.2.2.2Представление памяти и фронтовВ базовом представлении состояние ξ машины OpC11 включает в себя память M и функцию ψrd , которая по идентификатору потока π возвращает его базовый фронт (см. рис.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
