Регулярная семантика

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

Пример

Регулярная семантика слабее линеаризуемости . Рассмотрим пример, показанный ниже, где горизонтальная ось представляет время, а стрелки представляют интервал, в течение которого выполняется операция чтения или записи. Согласно определению обычного регистра, первое чтение может возвращать 5 или 2, как и второе чтение. Первое чтение может вернуть 2, а второе чтение может вернуть 5 (также известное как инверсия нового/старого). Такое поведение не удовлетворяет атомарной семантике . Следовательно, регулярная семантика является более слабым свойством, чем атомарная семантика. С другой стороны, Лесли Лэмпорт доказал, что линеаризуемый регистр может быть реализован из регистров с безопасной семантикой , которые слабее обычных регистров. ^{[ 1 ]}

Теорема от регулярности к атомарности

с одной записью и несколькими чтениями (SWMR) Атомная семантика является регулярным регистром SWMR, если любая из его истории выполнения H удовлетворяет следующему свойству: r1 и r2 — любые два вызова чтения: (r1 →H r2) ⇒ ¬π(r2) →H π(r1)

Прежде чем приступить к доказательству, сначала следует понять, что означает инверсия новое/старое. Как показано на рисунке ниже, глядя на выполнение, можно увидеть, что единственная разница между обычным выполнением и атомарным выполнением заключается в том, что a = 0 и b = 1. В этом выполнении при рассмотрении двух вызовов чтения R .read() → а за которым следует R.read() → b, наше первое значение (новое значение) равно a = 0, а второе значение (старое значение) равно b=1. На самом деле это главное различие между атомарностью и регулярностью.

Приведенная выше теорема утверждает, что регулярный регистр с одним записывающим устройством и несколькими считывателями без новой или старой инверсии. представляет собой атомный регистр. Отсюда R.read() → a →H R.read() → b и R.write(1) →H R.write(0), невозможно иметь π (R.read() → b) =R.write(1) и π (R.read() → a) = R.write(0), если выполнение атомарное. Чтобы доказать приведенную выше теорему, сначала необходимо доказать, что регистр безопасен, регулярен и что он не допускает инверсии нового/старого, что доказывает атомарность. По определению атомарного регистра, атомарный регистр с одним записывающим устройством и несколькими читателями является регулярным и удовлетворяет принципу отсутствия новых/старых. свойство инверсии. Итак, единственное необходимое доказательство — показать, что обычный регистр без инверсии нового/старого является атомарным.

Более того, для любых двух вызовов чтения (r1 и r2), когда регистр регулярен и нет инверсии новое/старое (r1 →H r2) ⇒sn(π(r1)) ⩽ sn(π(r2)). Для любого выполнения (M) существует общий заказ (S), включающий в себя вызовы одних и тех же операций. Можно сказать, что S строится следующим образом: начиная с общего порядка операций записи и вставки операций чтения следующим образом: сначала: операция чтения (r) вставляется после соответствующей операции записи (π(r)). Второе: если две операции чтения (r1,r2) имеют одно и то же (sn(r1)=sn(r2)), то сначала вставьте операцию, выполнение которой начинается первой. S включает в себя все операции вызова M, из чего следует, что S и M эквивалентны. Поскольку все операции упорядочены по их порядковым номерам, это немного общий порядок. Более того, этот общий порядок выполнения M добавляет порядок только к операциям, которые перекрываются в M. Если нет перекрытия между операциями чтения и записи, нет никакой разницы между регулярностью и атомарностью. Наконец, можно утверждать, что S является законным, поскольку каждая операция чтения получает последнее записанное значение, которое предшествует ей в общем порядке. Следовательно, соответствующая история линеаризуема. Поскольку это рассуждение не опирается на конкретный история H, это означает, что регистр является атомарным. Поскольку атомарность (линеаризуемость) является локальным свойством, можно утверждать, что набор регулярных регистров SWMR ведет себя атомарно, как только каждый из них удовлетворяет свойству инверсии отсутствия новых/старых.

Ссылки

^ Лэмпорт, Лесли (1986). «О межпроцессном взаимодействии. Часть I: Базовый формализм» . Распределенные вычисления . 1 (2). Спрингер-Верлаг: 86–101. дои : 10.1007/BF01786228 .

Лэмпорт, Лесли «О межпроцессном взаимодействии» http://research.microsoft.com/en-us/um/people/lamport/pubs/interprocess.pdf (1986).

[1] Лэмпорт, Лесли (1986). «О межпроцессном взаимодействии. Часть I: Базовый формализм» . Распределенные вычисления . 1 (2). Спрингер-Верлаг: 86–101. дои : 10.1007/BF01786228 .

[ 1 ]