• Основной язык
• Система модулей
• Объекты в 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. Предположим, что ранее было объявлено 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.

Эквивалентный код на 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 простым операционным способом с малым шагом. Иными словами, семантика задаётся абстрактной машиной, которая выполняет по одному действию за раз, произвольно выбирая на каждом шаге один из доступных доменов. Это похоже на абстрактную машину, использованную для описания отношения «происходит до» в разделе 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 либо (a) между t7 и t8, либо (b) после t8. Для нашего обсуждения выберем первый вариант. Поскольку новая запись располагается после всех записей в ячейке c, известных домену d2, обновляется и значение фронтира 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 для массивов чисел с плавающей точкой может приводить к разрыву записи. Если несинхронизированная операция копирования выполняется одновременно с записью в перекрывающиеся поля того же массива чисел с плавающей точкой, в поле могут оказаться биты из любой из этих записей.
• В массивах с непрерывным хранением чисел с плавающей точкой или в записях, содержащих только поля с числами с плавающей точкой, на 32-разрядных архитектурах получение или установка поля включает два отдельных обращения к памяти. При наличии гонок данных пользователь может наблюдать разрыв записи.
• Модуль Bytes Bytes допускает смешанные обращения, при которых чтение и запись могут выполняться с разными размерами. Несинхронизированные смешанные обращения приводят к разрыву записи.