Глава 10 Модель памяти: сложные моменты

• 10.1 Почему слабо согласованная память?
• 10.2 Свобода от гонок данных подразумевает последовательную согласованность
• 10.3 Решение задач с использованием DRF-SC
• 10.4 Локальная свобода от гонок данных
• 10.5 Операционное представление модели памяти
• 10.6 Несоответствующие операции

В этой главе описываются подробности модели памяти OCaml с ослабленными гарантиями. Модель памяти с ослабленными гарантиями описывает, какие значения программа OCaml может наблюдать при чтении ячейки памяти. Если вас интересует программирование параллельных задач высокого уровня в OCaml, обратитесь к главе о параллельном программировании 9.

Эта глава предназначена для экспертов, которые хотят понять детали модели памяти OCaml с точки зрения практиков. Для формального определения модели памяти OCaml, её гарантий и компиляции в модели памяти аппаратного обеспечения, пожалуйста, обратитесь к статье PLDI 2018 о Ограничении гонок данных во времени и пространстве. Модель памяти, представленная в этой главе, является расширением модели, представленной в статье PLDI 2018. В этой главе также рассматриваются некоторые практические аспекты модели памяти, которые не покрыты в статье.

10.1 Почему слабо согласованная память?

Простейшая модель памяти, которую мы можем предоставить нашим программам, — это последовательная согласованность. При последовательной согласованности значения, наблюдаемые программой, могут быть объяснены с помощью некоторой интерпретации операций из разных областей программы. Например, рассмотрим следующую программу с двумя областями d1 и d2, выполняющимися параллельно:

let d1 a b =
  let r1 = !a * 2 in
  let r2 = !b in
  let r3 = !a * 2 in
  (r1, r2, r3)

let d2 b = b := 0

let main () =
  let a = ref 1 in
  let b = ref 1 in
  let h = Domain.spawn (fun _ ->
    let r1, r2, r3 = d1 a b in
    Printf.printf "r1 = %d, r2 = %d, r3 = %d\n" r1 r2 r3)
  in
  d2 b;
  Domain.join h

Ссылочные ячейки a и b изначально равны 1. Пользователь может наблюдать r1 = 2, r2 = 0, r3 = 2, если запись в b в d2 произошла до чтения b в d1. Здесь наблюдаемое поведение может быть объяснено с точки зрения чередования операций из разных областей.

Предположим теперь, что a и b являются псевдонимами друг друга.

let d1 a b =
  let r1 = !a * 2 in
  let r2 = !b in
  let r3 = !a * 2 in
  (r1, r2, r3)

let d2 b = b := 0

let main () =
  let ab = ref 1 in
  let h = Domain.spawn (fun _ ->
    let r1, r2, r3 = d1 ab ab in
    assert (not (r1 = 2 && r2 = 0 && r3 = 2)))
  in
  d2 ab;
  Domain.join h

В программе выше переменные ab, a и b ссылаются на одну и ту же ссылочную ячейку. Можно ожидать, что утверждение в основной функции никогда не потерпит неудачу. Объяснение в том, что если r2 равно 0, то запись в d2 произошла до чтения b в d1. Учитывая, что a и b являются псевдонимами, второе чтение a в d1 также должно возвращать 0.

10.1.1 Оптимизации компилятора

Удивительно, но это утверждение может потерпеть неудачу в OCaml из-за оптимизаций компилятора. Компилятор OCaml замечает общую подвыражение !a * 2 в d1 и оптимизирует программу следующим образом:

let d1 a b =
  let r1 = !a * 2 in
  let r2 = !b in
  let r3 = r1 in (* CSE: !a * 2 ==> r1 *)
  (r1, r2, r3)

let d2 b = b := 0

let main () =
  let ab = ref 1 in
  let h = Domain.spawn (fun _ ->
    let r1, r2, r3 = d1 ab ab in
    assert (not (r1 = 2 && r2 = 0 && r3 = 2)))
  in
  d2 ab;
  Domain.join h

Эта оптимизация известна как устранение общей подвыражения (CSE). Такие оптимизации являются допустимыми и необходимыми для высокой производительности, и не изменяют последовательного смысла программы. Однако CSE нарушает последовательное обоснование.

В оптимизированной программе, даже если запись в b в d2 происходит между первым и вторым чтениями в d1, программа будет наблюдать значение 2 для r3, что приведёт к нарушению утверждения. Наблюдаемое поведение нельзя объяснить чередованием операций из разных областей в исходной программе. Таким образом, оптимизация CSE считается недопустимой при последовательной согласованности.

Один из способов объяснения наблюдаемого поведения — это как если бы операции, выполняемые в области, были переупорядочены. Например, если второе и третье чтения из d2 были переупорядочены,

let d1 a b =
  let r1 = !a * 2 in
  let r3 = !a * 2 in
  let r2 = !b in
  (r1, r2, r3)

то мы можем объяснить наблюдаемое поведение (2,0,2), возвращаемое d1.

10.1.2 Оптимизации аппаратуры

Другим источником переупорядочивания является аппаратура. Современные архитектуры аппаратного обеспечения имеют сложные иерархии кэшей с несколькими уровнями кэша. Хотя согласованность кэша гарантирует, что чтение и запись в одну ячейку памяти соответствуют последовательной согласованности, гарантии для программ, работающих с разными ячейками памяти, гораздо слабее. Рассмотрим следующую программу:

let a = ref 0
and b = ref 0

let d1 () =
  a := 1;
  !b

let d2 () =
  b := 1;
  !a

let main () =
  let h = Domain.spawn d2 in
  let r1 = d1 () in
  let r2 = Domain.join h in
  assert (not (r1 = 0 && r2 = 0))

При последовательной согласованности мы никогда не ожидали бы, что утверждение потерпит неудачу. Однако даже на x86, который предоставляет гораздо более сильные гарантии, чем ARM, записи, выполненные одним процессорным ядром, не публикуются немедленно для всех остальных ядер. Поскольку a и b являются разными ячейками памяти, чтение a и b могут оба наблюдать начальные значения, что приведёт к нарушению утверждения.

Это поведение можно объяснить, если загрузке разрешено переупорядочиться перед предшествующей записью в другую ячейку памяти. Это переупорядочивание может произойти из-за наличия буферов сохранения в ядрах современных процессоров. Каждое ядро фактически имеет FIFO-буфер ожидающих записей, чтобы избежать необходимости блокировки во время завершения записи. Записи в a и b могут находиться в буферах сохранения ядер c1 и c2, выполняющих области d1 и d2 соответственно. Чтения b и a, выполняемые на ядрах c1 и c2 соответственно, не увидят записи, если записи не были переданы из буферов в основную память.

10.2 Свобода от гонок данных подразумевает последовательную согласованность

Цель модели памяти OCaml с ослабленными гарантиями — точно описать, какие порядки сохраняются программой OCaml. Компилятор и аппаратное обеспечение могут свободно оптимизировать программу, пока они соблюдают гарантии упорядочивания модели памяти. Хотя программирование непосредственно под моделью памяти с ослабленными гарантиями сложно, модель памяти также описывает условия, при которых программа будет демонстрировать только последовательно согласованные поведения. Эта гарантия известна как свобода от гонок данных подразумевает последовательную согласованность (DRF-SC). В этом разделе мы опишем эту гарантию. Для этого нам сначала понадобятся некоторые определения.

10.2.1 Ячейки памяти

OCaml классифицирует ячейки памяти на атомные и неатомные. Ссылочные ячейки, поля массивов и поля мутабельных записей являются неатомными ячейками памяти. Неизменяемые объекты — это неатомные ячейки с начальной записью, но без дальнейших обновлений. Атомные ячейки памяти — это те, которые создаются с использованием модуля Atomic.

10.2.2 Взаимоотношение "произошло-раньше"

Представьте, что программы OCaml выполняются абстрактной машиной, выполняющей по одному действию за раз, произвольно выбирая одну из доступных областей на каждом шаге. Мы классифицируем действия на два типа: межобластные и внутриобластные. Межобластное действие — это действие, которое может быть наблюдаемо и может влиять на действия в других областях. Существует несколько межобластных действий:

• Чтение и запись атомных и неатомных ячеек.
• Создание и объединение областей.
• Операции с мьютексами.

С другой стороны, внутриобластные действия не могут ни наблюдаться, ни влиять на выполнение других областей. Примеры включают вычисление арифметического выражения, вызов функции и т. д. Спецификация модели памяти игнорирует такие внутриобластные действия. В дальнейшем мы будем использовать термин «действие» для обозначения межобластных действий.

Полностью упорядоченный список действий, выполняемых абстрактной машиной, называется следом выполнения. Для данной программы может быть несколько возможных следов выполнения из-за недетерминированности.

Для данного следа выполнения мы определяем нерефлексивное, транзитивное взаимоотношение «произошло-раньше», которое отражает причинно-следственные связи между действиями в программе OCaml. Взаимоотношение «произошло-раньше» определяется как наименьшее транзитивное отношение, удовлетворяющее следующим свойствам:

• Мы определяем порядок, в котором домен выполняет свои действия, как порядок программы. Если действие x предшествует другому действию y в порядке программы, то x предшествует y в порядке происходит-перед.
• Если x — запись в атомную ячейку, а y — последующее чтение или запись в эту ячейку памяти в трассе выполнения, то x предшествует y в порядке происходит-перед. Для атомных ячеек, compare_and_set, fetch_and_add, exchange, incr и decr считаются выполняющими как чтение, так и запись.
• Если x — это Domain.spawn f, а y — первое действие в недавно созданном домене, выполняющем f, то x предшествует y в порядке происходит-перед.
• Если x — последнее действие в домене d, а y — Domain.join d, то x предшествует y в порядке происходит-перед.
• Если x — операция разблокировки мьютекса, а y — любая последующая операция над этим мьютексом в трассе выполнения, то x предшествует y в порядке происходит-перед.

10.2.3 Гонка данных

В данной трассе два действия называются конфликтующими, если они обращаются к одной и той же неатомной ячейке, по крайней мере одно из них является записью, и ни одно из них не является начальной записью в эту ячейку.

Мы говорим, что программа имеет гонку данных, если существует какая-то трасса выполнения программы с двумя конфликтующими действиями, и не существует отношения происходит-перед между конфликтующими обращениями. Программа без гонок данных называется правильно синхронизированной.

10.2.4 DRF-SC

Гарантия DRF-SC: Программа без гонок данных будет демонстрировать только последовательно согласованное поведение.

DRF-SC — это сильная гарантия для программистов. Программисты могут использовать последовательное рассуждение, т. е. рассуждение, выполняя одно междоменное действие после другого, чтобы определить, есть ли в их программе гонка данных. В частности, им не нужно рассуждать о перестановках, описанных в разделе 10.1, чтобы определить, есть ли в их программе гонка данных. После того, как будет установлено, что конкретная программа не имеет гонки данных, они не должны беспокоиться о перестановках в своем коде.

10.3 Рассуждение с DRF-SC

В этом разделе мы рассмотрим примеры использования DRF-SC для рассуждения о программах. В этом разделе мы будем использовать функции с именами dN для представления доменов, выполняющихся параллельно с другими доменами. То есть мы предполагаем, что существует функция main, которая запускает функции dN параллельно следующим образом:

let main () =
  let h1 = Domain.spawn d1 in
  let h2 = Domain.spawn d2 in
  ...
  ignore @@ Domain.join h1;
  ignore @@ Domain.join h2

Вот простой пример с гонкой данных:

(* Has data race *)
let r = ref 0
let d1 () = r := 1
let d2 () = !r

r — это неатомная ссылка. Два домена соревнуются за доступ к ссылке, и d1 — запись. Поскольку между конфликтующими обращениями нет отношения происходит-перед, возникает гонка данных.

Обе программы, которые мы видели в разделе 10.1, имеют гонки данных. Неудивительно, что они демонстрируют не последовательно согласованное поведение.

Доступ к непересекающимся индексам массива и полям записи параллельно не является гонкой данных. Например,

(* No data race *)
let a = [| 0; 1 |]
let d1 () = a.(0) <- 42
let d2 () = a.(1) <- 42

(* No data race *)
type t = {
  mutable a : int;
  mutable b : int
}
let r = {a = 0; b = 1}
let d1 () = r.a <- 42
let d2 () = r.b <- 42

не имеют гонок данных.

Гонки в атомных ячейках не приводят к гонке данных.

(* No data race *)
let r = Atomic.make 0
let d1 () = Atomic.set r 1
let d2 () = Atomic.get r

Обмен сообщениями

Атомные переменные могут использоваться для реализации неблокирующей связи между доменами.

(* No data race *)
let msg = ref 0
let flag = Atomic.make false
let d1 () =
  msg := 42; (* a *)
  Atomic.set flag true (* b *)
let d2 () =
  if Atomic.get flag (* c *) then
    !msg (* d *)
  else 0

Обратите внимание, что действия a и d записывают и читают из одной и той же неатомной ячейки msg соответственно, и, следовательно, являются конфликтующими. Нам нужно установить, что a и d имеют отношение происходит-перед, чтобы показать, что у этой программы нет гонки данных.

Действие a предшествует b в порядке программы, и, следовательно, a происходит-перед b. Аналогично, c происходит-перед d. Если d2 видит атомную переменную flag равной true, то b предшествует c в порядке происходит-перед. Поскольку происходит-перед транзитивно, конфликтующие действия a и d находятся в порядке происходит-перед. Если d2 видит flag равной false, то чтение msg не выполняется. Следовательно, нет конфликтующего доступа в этой трассе выполнения. Таким образом, у программы нет гонки данных.

Следующая изменённая версия программы обмена сообщениями имеет гонку данных.

(* Has data race *)
let msg = ref 0
let flag = Atomic.make false
let d1 () =
  msg := 42; (* a *)
  Atomic.set flag true (* b *)
let d2 () =
  ignore (Atomic.get flag); (* c *)
  !msg (* d *)

Теперь домен d2 безусловно читает неатомную ссылку msg. Рассмотрим трассу выполнения:

Atomic.get flag; (* c *)
!msg; (* d *)
msg := 42; (* a *)
Atomic.set flag true (* b *)

В этой трассе d и a являются конфликтующими операциями. Но между ними нет отношения происходит-перед. Следовательно, у этой программы есть гонка данных.

10.4 Локальная свобода от гонок данных

Модель памяти OCaml предлагает сильные гарантии даже для программ с гонками данных. Она предлагает то, что известно как гарантия локальной свободы от гонок данных и последовательной согласованности (LDRF-SC). Формальное определение этого свойства выходит за рамки данной главы руководства. Заинтересованным читателям рекомендуется ознакомиться со статьей PLDI 2018 Bounding Data Races in Space and Time.

Неформально, LDRF-SC утверждает, что части программы, свободные от гонок данных, остаются последовательно согласованными. То есть, даже если у программы есть гонки данных, те части программы, которые не пересекаются с частями, содержащими гонки данных, поддаются последовательному рассуждению.

Рассмотрим следующий фрагмент:

let snippet () =
  let c = ref 0 in
  c := 42;
  let a = !c in
  (a, c)

Обратите внимание, что c — это только что выделенная ссылка. Может ли чтение c вернуть значение, отличное от 42? То есть, может ли a когда-либо не быть 42? Удивительно, но в моделях памяти C++ и Java ответ — да. С моделью памяти C++, если в программе есть гонка данных, даже в не связанных частях, то семантика не определена. Если этот фрагмент был бы связан с библиотекой, содержащей гонку данных, то в соответствии с моделью памяти C++ чтение могло бы вернуть любое значение. Поскольку гонки данных в не связанных местах могут влиять на поведение программы, мы говорим, что модель памяти C++ не ограничена в пространстве.

В отличие от C++, модель памяти Java ограничена в пространстве. Но модель памяти Java не ограничена во времени; гонки данных в будущем будут влиять на поведение прошлого. Например, рассмотрим перевод этого примера на Java. Мы предполагаем предварительное определение Class c {int x;} и общую неизменяемую переменную C g. Теперь фрагмент может быть частью большей программы с параллельными потоками:

(* Thread 1 *)
C c = new C();
c.x = 42;
a = c.x;
g = c;

(* Thread 2 *)
g.x = 7;

Чтение c.x и запись g в первом потоке выполняются в разных ячейках памяти. Следовательно, модель памяти Java позволяет их переупорядочить. В результате запись во втором потоке может произойти до чтения c.x, и, следовательно, c.x возвращает 7.

OCaml-эквивалент кода Java выше:

let g = ref None

let snippet () =
  let c = ref 0 in
  c := 42;
  let a = !c in
  (a, c)

let d1 () =
  let (a,c) = snippet () in
  g := Some c;
  a

let d2 () =
  match !g with
  | None -> ()
  | Some c -> c := 7

Обратите внимание, что происходит гонка данных как на g, так и на c. Рассмотрим только первые три инструкции в snippet:

let c = ref 0 in
c := 42;
let a = !c in
...

Модель памяти OCaml ограничена и по объёму, и по времени. Единственное местоположение памяти здесь — c. Рассматривая только этот фрагмент, нет гонки данных ни по пространству (гонка на g), ни по времени (будущая гонка на c). Следовательно, фрагмент будет иметь последовательно согласованное поведение, и значение, возвращаемое !c, будет 42.

Модель памяти OCaml гарантирует, что даже для программ с гонками данных безопасность памяти сохраняется. Хотя программы с гонками данных могут наблюдать не последовательно согласованное поведение, они не упадут.

10.5 Операционное представление модели памяти

В этом разделе мы описываем семантику модели памяти OCaml. Формальное определение операционного представления модели памяти представлено в разделе 3 статьи PLDI 2018 о Ограничении гонок данных по пространству и времени. Этот раздел представляет собой неформальное описание модели памяти с помощью примера.

Учитывая программу OCaml, которая может содержать гонки данных, операционная семантика указывает значения, которые могут быть получены при чтении из ячейки памяти. Для простоты мы ограничим действия внутри потока только доступом к атомарным и неатомарным ячейкам, игнорируя операции порождения и соединения областей, а также операции над мьютексами.

Мы описываем семантику модели памяти OCaml простым операционным способом с небольшими шагами. То есть семантика описывается абстрактной машиной, которая выполняет по одному действию за раз, произвольно выбирая одну из доступных областей на каждом шаге. Это аналогично абстрактной машине, которую мы использовали для описания отношения happens-before в разделе 10.2.2.

10.5.1 Неатомарные ячейки

В семантике мы моделируем неатомарные ячейки как конечные отображения из временных меток t в значения v. Мы принимаем временные метки за рациональные числа. Временные метки упорядочены, но плотные; между любыми двумя временными метками существует ещё одна.

Например,

a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t8 -> 7]

представляет три неатомарные ячейки a, b и c и их истории. Ячейка a имеет два записи по временным меткам t1 и t2 со значениями 1 и 2 соответственно. Когда мы записываем a: [t1 -> 1; t2 -> 2], мы предполагаем, что t1 < t2. Мы предполагаем, что ячейки инициализируются историей, которая содержит единственную запись по временной метке 0, которая отображается на начальное значение.

10.5.2 Области

Каждая область оснащена фронтиром, который является отображением от неатомарных ячеек до временных меток. Интуитивно, фронт каждой области записывает для каждой неатомарной ячейки самую последнюю запись, известную потоку. Могут быть более поздние записи, но они не гарантируются видимость.

Например,

d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t7]

представляет две области d1 и d2 и их фронты.

10.5.3 Доступ к неатомарным ячейкам

Теперь давайте определим семантику неатомарных чтений и записей. Предположим, что область d1 выполняет чтение b. Для неатомарных чтений области могут читать произвольный элемент истории для этой ячейки, если он не старше временной метки в фронте области. В данном случае, так как фронт d1 по b находится на t3, чтение может вернуть значение 3, 4 или 5. Неатомарное чтение не изменяет фронт текущей области.

Предположим, область d2 записывает значение 10 в c (c := 10). Мы выбираем новую временную метку t9 для этой записи таким образом, чтобы она была позже, чем фронт d2 по c. Обратите внимание на тонкость: эта новая временная метка может не быть позже, чем все остальные в истории, но только позже любой другой записи, известной записывающей области. Следовательно, t9 может быть вставлена в историю c либо (а) между t7 и t8, либо (б) после t8. Давайте выберем первый вариант для нашего обсуждения. Поскольку новая запись появляется после всех записей, известных области d2 в ячейку c, фронт d2 по c также обновляется. Новое состояние абстрактной машины:

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7] (* new write at t9 *)

(* Domains *)
d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t9] (* frontier updated at c *)

10.5.4 Атомарный доступ

Атомарные ячейки содержат не только значения, но и информацию о синхронизации. Мы моделируем атомарные ячейки как пару значения, хранимого в этой ячейке, и фронта. Фронт моделирует информацию о синхронизации, которая объединяется с фронтами потоков, которые работают с ячейкой. Таким образом, неатомарные записи, сделанные одним потоком, могут стать известными другому, обмениваясь через атомарную ячейку.

Например,

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

показывает две атомарные переменные A и B со значениями 10 и 5 соответственно, и своими собственными фронтами. Мы используем прописные имена переменных для обозначения атомарных ячеек.

Во время атомарных чтений фронт ячейки объединяется с фронтом области, выполняющей чтение. Например, предположим, что d1 читает B. Чтение возвращает 5, и фронт d1 обновляется путём объединения с фронтом B, выбирая более позднюю временную метку для каждой ячейки. Состояние абстрактной машины до атомарного чтения:

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t9]

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

В результате атомарного чтения состояние абстрактной машины обновляется до:

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t2; b -> t4; c -> t7] (* frontier updated at a and b *)
d2: [a -> t1; b -> t4; c -> t9]

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

Во время атомарных записей значение, хранимое в атомарной ячейке, обновляется. Фронты как записывающей области, так и ячейки, в которую записывается, обновляются до объединения двух фронтов. Например, если d2 записывает 20 в A в текущем состоянии машины, состояние машины обновляется до:

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t2; b -> t4; c -> t7]
d2: [a -> t1; b -> t5; c -> t9] (* frontier updated at b *)

(* Atomic locations *)
A: 20, [a -> t1; b -> t5; c -> t9] (* value updated. frontier updated at c. *)
B: 5,  [a -> t2; b -> t4; c -> t6]

10.5.5 Выводы из семантики

Давайте пересмотрим пример из предыдущей статьи (раздел 10.1).

let a = ref 0
and b = ref 0

let d1 () =
  a := 1;
  !b

let d2 () =
  b := 1;
  !a

let main () =
  let h = Domain.spawn d2 in
  let r1 = d1 () in
  let r2 = Domain.join h in
  assert (not (r1 = 0 && r2 = 0))

Эта программа имеет гонку данных на a и b, и поэтому программа может продемонстрировать не последовательно согласованное поведение. Давайте используем семантику, чтобы показать, что программа может продемонстрировать r1 = 0 && r2 = 0.

Начальное состояние абстрактной машины:

(* Non-atomic locations *)
a: [t0 -> 0]
b: [t1 -> 0]

(* Domains *)
d1: [a -> t0; b -> t1]
d2: [a -> t0; b -> t1]

Существует несколько возможных расписаний выполнения этой программы. Давайте рассмотрим следующее расписание:

1: a := 1 @ d1
2: b := 1 @ d2
3: !b     @ d1
4: !a     @ d2

После первого действия a:=1 области d1, состояние машины:

(* Non-atomic locations *)
a: [t0 -> 0; t2 -> 1] (* new write at t2 *)
b: [t1 -> 0]

(* Domains *)
d1: [a -> t2; b -> t1] (* frontier updated at a *)
d2: [a -> t0; b -> t1]

После второго действия b:=1 области d2, состояние машины:

(* Non-atomic locations *)
a: [t0 -> 0; t2 -> 1]
b: [t1 -> 0; t3 -> 1] (* new write at t3 *)

(* Domains *)
d1: [a -> t2; b -> t1]
d2: [a -> t0; b -> t3] (* frontier updated at b *)

Теперь, для третьего действия !b области d1, обратите внимание, что фронт d1 по b находится на t1. Следовательно, чтение может вернуть либо 0, либо 1. Давайте предположим, что оно возвращает 0. Состояние машины не обновляется неатомарным чтением.

Аналогично, для четвёртого действия !a от d2, граница d2 в a находится в t0. Следовательно, это чтение также может вернуть либо 0, либо 1. Предположим, что оно возвращает 0. Таким образом, утверждение в исходной программе assert (not (r1 = 0 && r2 = 0)) потерпит неудачу для этого конкретного выполнения.

10.6 Несоответствующие операции

Существуют определенные операции, которые не соответствуют модели памяти.

• Функция Array.blit для массивов с плавающей точкой может привести к разрыву. Когда несинхронизированная операция blit выполняется одновременно с некоторыми перекрывающимися операциями записи в поля того же массива с плавающей точкой, поле может оказаться содержащим биты от любой из записей.
• В случае массивов с плавающей точкой или записей, содержащих только поля с плавающей точкой на 32-битных архитектурах, получение или установка поля включает в себя два отдельных обращения к памяти. При наличии гонок данных пользователь может наблюдать разрыв.
• Модуль Bytes Bytes допускает смешанный доступ, где чтение и запись могут быть различного размера. Несинхронизированный смешанный доступ приводит к разрыву.