• Язык OCaml
• Система модулей
• Объекты в OCaml
• Меченные аргументы
• Полиморфные варианты
• Полиморфизм и его ограничения
• Обобщенные алгебраические типы данных
• Расширенные примеры с классами и модулями
• Параллельное программирование
• Модель памяти: сложные моменты

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

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

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

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.

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 считается невалидной при последовательной согласованности.

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

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.

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 соответственно, не увидят записи, если записи ещё не распространились из буферов в основную память.

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

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

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

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

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 в порядке "происходит до".

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

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

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

2.4 DRF-SC

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

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

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 являются конфликтующими операциями. Но нет отношения «происходит до» между ними. Следовательно, эта программа имеет гонку данных.

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

Модель памяти OCaml предлагает сильные гарантии даже для программ с гонками данных. Она предлагает гарантию локальной свободы от гонок данных и последовательной согласованности (LDRF-SC). Формальное определение этого свойства выходит за рамки данной главы руководства. Заинтересованным читателям рекомендуется ознакомиться со статьёй PLDI 2018 о Ограничении гонок данных во времени и пространстве.

Неформально, 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;} и общую не-volatile переменную 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.

Эквивалент кода Java выше на языке OCaml:

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 гарантирует, что даже для программ с гонками данных безопасность памяти сохраняется. Хотя программы с гонками данных могут наблюдать не последовательно согласованное поведение, они не аварийно завершатся.

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

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

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

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

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, сопоставленный начальному значению.

5.2 Домены

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

Например,

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

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

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 *)

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]

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)), потерпит неудачу для этого конкретного выполнения.

6 Несовместимые операции

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

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