Линеаризуемость: различия между версиями
Irina (обсуждение | вклад) мНет описания правки |
Irina (обсуждение | вклад) м (→Литература) |
||
| (не показано 7 промежуточных версий этого же участника) | |||
| Строка 15: | Строка 15: | ||
Ответ совпадает с вызовом, если имена их объектов и потоков | Ответ ''совпадает'' с вызовом, если имена их объектов и потоков согласуются. ''Вызовом метода'' является пара, состоящая из вызова и следующего подходящего ответа. Вызов ''ожидает'' своего завершения в истории, если за ним не следует подходящий ответ. Если H – история, то ''complete''(H) – это подпоследовательность H, состоящая из всех совпадающих вызовов и ответов. История H является ''последовательной'', если первым событием H является вызов, а за каждым вызовом (кроме, возможно, последнего) немедленно следует подходящий ответ. | ||
Пусть H – история. Потоковая подыстория H|P | Пусть H – история. ''Потоковая подыстория'' H|P представляет собой подпоследовательность событий в H с именем потока P. ''Объектовая подыстория'' H|x аналогично определяется для объекта x. Две истории H и H' ''эквивалентны'', если для каждого потока A выполняется H|A = H'|A. История H ''хорошо согласована'', если каждая потоковая подыстория H|A из H является последовательной. Обратите внимание, что подыстории потоков хорошо согласованной истории всегда последовательны, однако подыстории объектов не обязательно должны быть последовательными. | ||
Последовательная спецификация объекта представляет собой префиксно-замкнутое множество последовательных историй объекта, которое определяет легальные истории этого объекта. Последовательная история H является легальной, если каждая подыстория объекта легальна. Метод | ''Последовательная спецификация'' объекта представляет собой префиксно-замкнутое множество последовательных историй объекта, которое определяет легальные истории этого объекта. Последовательная история H является ''легальной'', если каждая подыстория объекта легальна. Метод называется ''полным'', если он определен для каждого состояния объекта, в противном случае он называется ''частичным''. (Например, метод deq(), который блокирует пустую очередь, является частичным, а метод, отбрасывающий исключение – полным). | ||
История H определяет (нерефлексивный) частичный порядок | История H определяет (нерефлексивный) частичный порядок <math>\to_H</math> для вызовов ее методов: <math>m_0 \to_H m_1</math>, если событие получения результата <math>m_0</math> происходит раньше события вызова <math>m_1</math>. Если история H является последовательной, то порядок H является полным. | ||
Пусть H – история, а x – объект, такой, что Hjx содержит вызовы методов | Пусть H – история, а x – объект, такой, что Hjx содержит вызовы методов <math>m_0</math> и <math>m_1</math>. Вызов <math>m_o \to_x m_1</math>, если <math>m_0</math> предшествует <math>m_1</math> в H|x. Заметим, что <math>\to_x</math> – полный порядок. | ||
| Строка 33: | Строка 33: | ||
'''Определение 1'''. История H является линеаризуемой, если она может быть расширена (путем добавления некоторого, возможно, нулевого количества событий ответа) до истории | '''Определение 1'''. История H является ''линеаризуемой'', если она может быть расширена (путем добавления некоторого, возможно, нулевого количества событий ответа) до истории H' такой, что: | ||
• L1 complete( | • (L1) complete(H') эквивалентна легальной последовательной истории S; | ||
• L2 Если вызов метода | • (L2) Если вызов метода <math>m_0</math> предшествует вызову метода <math>m_1</math> в H, то то же самое верно и в S. | ||
S называется линеаризацией H. (У одной истории может быть несколько линеаризаций). Неформально, расширение H до | S называется ''линеаризацией'' H. (У одной истории может быть несколько линеаризаций). Неформально, расширение H до H' отражает идею о том, что некоторые ожидающие вызовы могут произвести эффект, даже если их ответы еще не были возвращены вызывающему. | ||
== Основные результаты == | == Основные результаты == | ||
| Строка 46: | Строка 46: | ||
'''Свойство локальности''' | '''Свойство локальности''' | ||
Свойство является локальным, если все объекты в совокупности удовлетворяют этому свойству при условии, что каждый отдельный объект удовлетворяет ему. Линеаризуемость локальна: | Свойство является ''локальным'', если все объекты в совокупности удовлетворяют этому свойству при условии, что каждый отдельный объект удовлетворяет ему. Линеаризуемость локальна: | ||
'''Теорема 1. История H линеаризуема тогда и только тогда, когда H|x линеаризуема для | '''Теорема 1. История H линеаризуема тогда и только тогда, когда H|x линеаризуема для каждого объекта x.''' | ||
В части «только когда» доказательство является очевидным. | В части «только когда» доказательство является очевидным. | ||
Для каждого объекта x выберем линеаризацию H|x. | Для каждого объекта x выберем линеаризацию H|x. Обозначим за <math>R_x</math> множество ответов, добавленных к H|x для построения этой линеаризации, а за <math>\to_x</math> – соответствующий порядок линеаризации. Обозначим за H' историю, построенную путем добавления к H каждого ответа в <math>R_x</math>. | ||
Порядки | Порядки <math>\to_H</math> и <math>\to_x</math> могут быть «свернуты» в один частичный порядок. Определим отношение <math>\to</math> на вызовах методов из complete(H'): для вызовов методов <math>m</math> и <math>\bar{m}</math> выполняется <math>m \to \bar{m}</math>, если существуют вызовы методов <math>m_0, ..., m_n</math>, такие, что <math>m = m_0, \bar{m} = m_n</math>, и для каждого i между 0 и n - 1 имеет место либо <math>m_i \to_x m_{i+1}</math> для некоторого объекта x, либо <math>m_i \to_H m_{i+1}</math>. | ||
Оказывается, | Оказывается, <math>\to</math> является частичным порядком. Очевидно, что <math>\to</math> транзитивен. Осталось показать, что <math>\to</math> антирефлексивен: для всех x утверждение <math>x \to x</math> ложно. | ||
Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов | Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов <math>m_0, ..., m_n</math>, такие, что <math>m_0 \to m_1 \to \cdots \to m_n, m_n \to m_0</math>, и каждая пара непосредственно связана с некоторым <math>\to_x</math> или <math>\to_H</math>. | ||
Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом x. Поскольку | Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом x. Поскольку <math>\to_x</math> является полным порядком, должны существовать два вызова метода <math>m_{i-1}</math> и <math>m_i</math> такие, что <math>m_{i-1} \to_H m_i</math> и <math>m_i \to_x m_{i-1}</math>, что противоречит условию линеаризуемости x. | ||
Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за | Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за <math>m_1</math> и <math>m_2</math> вызовы методов разных объектов (переиндексировав их при необходимости). Пусть x – объект, связанный с <math>m_1</math>. Ни один из <math>m_2, ..., m_n</math> не может быть вызовом метода x. Утверждение справедливо для <math>m_2</math> по построению. Пусть <math>m_i</math> – первый вызов метода в <math>m_3, ..., m_n</math>, связанный с x. Поскольку <math>m_{i-1}</math> и <math>m_i</math> не связаны по <math>\to_x</math>, они должны быть связаны по <math>\to_H</math>, поэтому ответ <math>m_{i-1}</math> предшествует вызову <math>m_i</math>. Вызов <math>m_2</math> предшествует ответу <math>m_{i-1}</math>, поскольку в противном случае имело бы место <math>m_{i-1} \to_H m_2</math>, что дает более короткий цикл <math>m_2, ..., m_{i-1}</math>. Наконец, ответ <math>m_1</math> предшествует вызову <math>m_i</math>, поскольку по построению <math>m_1 \to_H m_2</math>. Отсюда следует, что ответ на <math>m_1</math> предшествует вызову <math>m_i</math>, следовательно, <math>m_1 \to_H m_i</math>, что дает более короткий цикл <math>m_1, m_i, ..., m_n</math>. | ||
Поскольку | Поскольку <math>m_n</math> не является вызовом метода x, а <math>m_n \to m_1</math>, из этого следует, что <math>m_n \to_H m_1</math>. Но <math>m_1 \to_H m_2</math> по построению, а так как <math>\to_H</math> транзитивно, то <math>m_n \to_H m_2</math>, что дает более короткий цикл <math>m_2, ..., m_n</math>, так что имеет место противоречие. <math>\square</math> | ||
| Строка 73: | Строка 73: | ||
'''Свойство неблокируемости''' | '''Свойство неблокируемости''' | ||
Линеаризуемость является неблокирующим свойством: ожидающий | Линеаризуемость является ''неблокирующим'' свойством: ожидающий вызов полного метода никогда не должен ждать завершения другого ожидающего вызова. | ||
'''Теорема 2. Пусть inv(m) – вызов полного метода. Если | '''Теорема 2. Пусть inv(m) – вызов полного метода. Если <math>\langle x \; invP \rangle</math> является ожидающим вызовом в линеаризуемой истории H, то существует ответ <math>\langle xresP \rangle</math>, такой, что история <math>H \cdot \langle x \; resP \rangle</math> линеаризуема.''' | ||
Доказательство. Пусть S – любая линеаризация H. Если S включает ответ | Доказательство. Пусть S – любая линеаризация H. Если S включает ответ <math>\langle x \; resP \rangle</math> на <math>\langle x \; invP \rangle</math>, то доказательство тем самым завершается, так как S также является линеаризацией <math>H \cdot \langle x \; resP \rangle</math>. В противном случае <math>\langle x \; invP \rangle</math> также не встречается в S, поскольку линеаризации, по определению, не включают ожидающих вызовов. Поскольку метод является полным, существует ответ <math>\langle x \; resP \rangle</math> такой, что <math>S' = S \cdot \langle x \; invP \rangle \cdot \langle x \; resP \rangle</math> является легальным. S', однако, является линеаризацией <math>H \cdot \langle x \; resP \rangle</math>, и, следовательно, также является линеаризацией H. <math>\square</math> | ||
Из этой теоремы следует, что линеаризуемость сама по себе никогда не приводит к блокировке потока с ожидающим вызовом полного метода. Конечно, блокировки (или даже взаимоблокировки) могут возникать как артефакты конкретных реализаций процесса линеаризации, но они не присущи самому свойству корректности. Данная теорема утверждает, что линеаризуемость является подходящим условием корректности для систем, в которых важны параллелизм и ответ в реальном времени. Альтернативные условия корректности, такие как сериализуемость [ ], не обладают этим свойством неблокируемости. | Из этой теоремы следует, что линеаризуемость сама по себе никогда не приводит к блокировке потока с ожидающим вызовом полного метода. Конечно, блокировки (или даже взаимоблокировки) могут возникать как артефакты конкретных реализаций процесса линеаризации, но они не присущи самому свойству корректности. Данная теорема утверждает, что линеаризуемость является подходящим условием корректности для систем, в которых важны параллелизм и ответ в реальном времени. Альтернативные условия корректности, такие как сериализуемость [1], не обладают этим свойством неблокируемости. | ||
Свойство неблокируемости не исключает блокировку в ситуациях, когда она явно предполагается. Например, может быть разумным, чтобы поток, пытающийся произвести выгрузку из пустой очереди, блокировал ее, ожидая, пока другой поток не выгрузит элемент. Спецификация очереди отражает это намерение, делая спецификацию метода deq () частичной и оставляя его эффект неопределенным при применении к пустой очереди. Наиболее естественной параллельной интерпретацией частичной последовательной спецификации является простое ожидание, пока объект не достигнет состояния, в котором метод определен. | Свойство неблокируемости не исключает блокировку в ситуациях, когда она явно предполагается. Например, может быть разумным, чтобы поток, пытающийся произвести выгрузку из пустой очереди, блокировал ее, ожидая, пока другой поток не выгрузит элемент. Спецификация очереди отражает это намерение, делая спецификацию метода deq() частичной и оставляя его эффект неопределенным при применении к пустой очереди. Наиболее естественной параллельной интерпретацией частичной последовательной спецификации является простое ожидание, пока объект не достигнет состояния, в котором метод определен. | ||
| Строка 90: | Строка 90: | ||
Последовательная согласованность [ ] представляет собой более слабое условие корректности, в котором выполняется требование L1, но не L2: вызовы методов должны происходить по одному в некотором последовательном порядке, но неперекрываюмиеся вызовы могут быть переупорядочены. Любая линеаризуемая история является последовательно согласованной, однако обратное неверно. Последовательная согласованность допускает больший параллелизм, но это не локальное свойство: система, состоящая из множества последовательно согласованных объектов, вовсе не обязательно сама является последовательно согласованной. | ''Последовательная согласованность'' [4] представляет собой более слабое условие корректности, в котором выполняется требование L1, но не L2: вызовы методов должны происходить по одному в некотором последовательном порядке, но неперекрываюмиеся вызовы могут быть переупорядочены. Любая линеаризуемая история является последовательно согласованной, однако обратное неверно. Последовательная согласованность допускает больший параллелизм, но это не локальное свойство: система, состоящая из множества последовательно согласованных объектов, вовсе не обязательно сама является последовательно согласованной. | ||
Большая часть работ по базам данных и распределенным системам использует сериализуемость как основное условие корректности параллельных вычислений. В этой модели транзакция представляет собой «поток управления», который применяет конечную последовательность методов к набору объектов, общих с другими транзакциями. История является сериализуемой, если она эквивалентна той, в которой транзакции выполняются последовательно, то есть без чередования. История строго сериализуема, если порядок транзакций в последовательной истории совместим с их порядком предшествования: если каждый вызов метода одной транзакции предшествует каждому вызову метода другой, то первая сериализуется раньше второй. (Линеаризуемость можно рассматривать как частный случай строгой сериализуемости, в котором транзакции состоят только из одного метода, применяемого к одному объекту). | Большая часть работ по базам данных и распределенным системам использует ''сериализуемость'' как основное условие корректности параллельных вычислений. В этой модели ''транзакция'' представляет собой «поток управления», который применяет конечную последовательность методов к набору объектов, общих с другими транзакциями. История является ''сериализуемой'', если она эквивалентна той, в которой транзакции выполняются последовательно, то есть без чередования. История ''строго сериализуема'', если порядок транзакций в последовательной истории совместим с их порядком предшествования: если каждый вызов метода одной транзакции предшествует каждому вызову метода другой, то первая сериализуется раньше второй. (Линеаризуемость можно рассматривать как частный случай строгой сериализуемости, в котором транзакции состоят только из одного метода, применяемого к одному объекту). | ||
Ни сериализуемость, ни строгая сериализуемость не являются локальными свойствами. Если разные объекты сериализуют транзакции в разном порядке, то не может быть порядка сериализации, общего для всех объектов. Сериализуемость и строгая сериализуемость являются блокирующими свойствами: при определенных обстоятельствах транзакция может быть не в состоянии завершить ожидающий метод, не нарушая сериализуемости. Если несколько транзакций блокируют друг друга, возникает ситуация взаимоблокировки. Для таких транзакций необходимо выполнить откат и перезапуск, что подразумевает наличие дополнительных механизмов для этой цели. | Ни сериализуемость, ни строгая сериализуемость не являются локальными свойствами. Если разные объекты сериализуют транзакции в разном порядке, то не может быть порядка сериализации, общего для всех объектов. Сериализуемость и строгая сериализуемость являются ''блокирующими'' свойствами: при определенных обстоятельствах транзакция может быть не в состоянии завершить ожидающий метод, не нарушая сериализуемости. Если несколько транзакций блокируют друг друга, возникает ситуация ''взаимоблокировки''. Для таких транзакций необходимо выполнить откат и перезапуск, что подразумевает наличие дополнительных механизмов для этой цели. | ||
== Применение == | == Применение == | ||
| Строка 110: | Строка 110: | ||
== Литература == | == Литература == | ||
Понятие линеаризуемости было предложено Херлихи и Винг [3], последовательной согласованности – | Понятие линеаризуемости было предложено Херлихи и Винг [3], последовательной согласованности – Лэмпортом [4], а сериализуемости Эсвараном и коллегами [1]. | ||
1. Eswaran, K.P., Gray, J.N., Lorie, R.A., Traiger, I.L.: The notions of consistency and predicate locks in a database system. Commun. ACM 19(11), 624-633 (1976). doi: http://doi.acm.org/10.1145/ 360363.360369 | 1. Eswaran, K.P., Gray, J.N., Lorie, R.A., Traiger, I.L.: The notions of consistency and predicate locks in a database system. Commun. ACM 19(11), 624-633 (1976). doi: http://doi.acm.org/10.1145/ 360363.360369 | ||
Версия от 22:10, 4 июня 2024
Ключевые слова и синонимы
Атомарность
Постановка задачи
Объект в таких языках, как Java и C++, представляет собой контейнер для данных. Каждый объект предоставляет набор методов, которые являются единственным способом манипулирования внутренним состоянием объекта. У каждого объекта есть класс, который определяет методы, которые он предоставляет, и то, что они делают.
В отсутствие параллелизма метод может быть описан парой, состоящей из предусловия (описывающего состояние объекта перед вызовом метода) и постусловия, описывающего после возвращения метода состояние объекта и возвращаемое значение метода. Однако если объект совместно используется параллельными потоками в многопроцессорной системе, то вызовы методов могут перекрываться во времени, и характеризовать методы в терминах предусловий и постусловий уже не имеет смысла.
Линеаризуемость представляет собой условие корректности для параллельных объектов, которое характеризует параллельное поведение объекта в терминах «эквивалентного» последовательного поведения. Неформально, объект ведет себя так, как если бы каждый вызов метода мгновенно производил эффект в какой-то момент между обращением к нему и его ответом. Это понятие корректности обладает некоторыми полезными формальными свойствами. Во-первых, оно является неблокирующим, что означает, что линеаризуемость как таковая никогда не требует, чтобы один поток ждал, пока другой завершит текущий вызов метода. Во-вторых, оно локально, что означает, что объект, состоящий из линеаризуемых объектов, сам является линеаризуемым. Другие предложенные в литературе условия корректности не обладают хотя бы одним из этих свойств.
Нотация
Выполнение параллельной системы моделируется историей – конечной последовательностью событий вызова метода и ответа на него. Подыстория истории H представляет собой подпоследовательность событий H. Вызов метода записывается как [math]\displaystyle{ \langle x.m(a^*)A \rangle }[/math], где [math]\displaystyle{ x }[/math] – объект, [math]\displaystyle{ m }[/math] – имя метода, [math]\displaystyle{ a^* }[/math] – последовательность аргументов, а [math]\displaystyle{ A }[/math] – поток. Ответ метода записывается как [math]\displaystyle{ \langle x: t(r^*)A \rangle }[/math], где [math]\displaystyle{ t }[/math] – условие завершения, а [math]\displaystyle{ r^* }[/math] – последовательность значений результата.
Ответ совпадает с вызовом, если имена их объектов и потоков согласуются. Вызовом метода является пара, состоящая из вызова и следующего подходящего ответа. Вызов ожидает своего завершения в истории, если за ним не следует подходящий ответ. Если H – история, то complete(H) – это подпоследовательность H, состоящая из всех совпадающих вызовов и ответов. История H является последовательной, если первым событием H является вызов, а за каждым вызовом (кроме, возможно, последнего) немедленно следует подходящий ответ.
Пусть H – история. Потоковая подыстория H|P представляет собой подпоследовательность событий в H с именем потока P. Объектовая подыстория H|x аналогично определяется для объекта x. Две истории H и H' эквивалентны, если для каждого потока A выполняется H|A = H'|A. История H хорошо согласована, если каждая потоковая подыстория H|A из H является последовательной. Обратите внимание, что подыстории потоков хорошо согласованной истории всегда последовательны, однако подыстории объектов не обязательно должны быть последовательными.
Последовательная спецификация объекта представляет собой префиксно-замкнутое множество последовательных историй объекта, которое определяет легальные истории этого объекта. Последовательная история H является легальной, если каждая подыстория объекта легальна. Метод называется полным, если он определен для каждого состояния объекта, в противном случае он называется частичным. (Например, метод deq(), который блокирует пустую очередь, является частичным, а метод, отбрасывающий исключение – полным).
История H определяет (нерефлексивный) частичный порядок [math]\displaystyle{ \to_H }[/math] для вызовов ее методов: [math]\displaystyle{ m_0 \to_H m_1 }[/math], если событие получения результата [math]\displaystyle{ m_0 }[/math] происходит раньше события вызова [math]\displaystyle{ m_1 }[/math]. Если история H является последовательной, то порядок H является полным.
Пусть H – история, а x – объект, такой, что Hjx содержит вызовы методов [math]\displaystyle{ m_0 }[/math] и [math]\displaystyle{ m_1 }[/math]. Вызов [math]\displaystyle{ m_o \to_x m_1 }[/math], если [math]\displaystyle{ m_0 }[/math] предшествует [math]\displaystyle{ m_1 }[/math] в H|x. Заметим, что [math]\displaystyle{ \to_x }[/math] – полный порядок.
Неформально, линеаризуемость требует, чтобы каждый вызов метода мгновенно «производил эффект» в некоторый момент между обращением и ответом. Важным следствием из этого определения является то, что вызовы методов, которые не перекрываются, не могут быть переупорядочены: линеаризуемость сохраняет порядок вызовов методов «реального времени». Формально:
Определение 1. История H является линеаризуемой, если она может быть расширена (путем добавления некоторого, возможно, нулевого количества событий ответа) до истории H' такой, что:
• (L1) complete(H') эквивалентна легальной последовательной истории S;
• (L2) Если вызов метода [math]\displaystyle{ m_0 }[/math] предшествует вызову метода [math]\displaystyle{ m_1 }[/math] в H, то то же самое верно и в S.
S называется линеаризацией H. (У одной истории может быть несколько линеаризаций). Неформально, расширение H до H' отражает идею о том, что некоторые ожидающие вызовы могут произвести эффект, даже если их ответы еще не были возвращены вызывающему.
Основные результаты
Свойство локальности
Свойство является локальным, если все объекты в совокупности удовлетворяют этому свойству при условии, что каждый отдельный объект удовлетворяет ему. Линеаризуемость локальна:
Теорема 1. История H линеаризуема тогда и только тогда, когда H|x линеаризуема для каждого объекта x.
В части «только когда» доказательство является очевидным.
Для каждого объекта x выберем линеаризацию H|x. Обозначим за [math]\displaystyle{ R_x }[/math] множество ответов, добавленных к H|x для построения этой линеаризации, а за [math]\displaystyle{ \to_x }[/math] – соответствующий порядок линеаризации. Обозначим за H' историю, построенную путем добавления к H каждого ответа в [math]\displaystyle{ R_x }[/math].
Порядки [math]\displaystyle{ \to_H }[/math] и [math]\displaystyle{ \to_x }[/math] могут быть «свернуты» в один частичный порядок. Определим отношение [math]\displaystyle{ \to }[/math] на вызовах методов из complete(H'): для вызовов методов [math]\displaystyle{ m }[/math] и [math]\displaystyle{ \bar{m} }[/math] выполняется [math]\displaystyle{ m \to \bar{m} }[/math], если существуют вызовы методов [math]\displaystyle{ m_0, ..., m_n }[/math], такие, что [math]\displaystyle{ m = m_0, \bar{m} = m_n }[/math], и для каждого i между 0 и n - 1 имеет место либо [math]\displaystyle{ m_i \to_x m_{i+1} }[/math] для некоторого объекта x, либо [math]\displaystyle{ m_i \to_H m_{i+1} }[/math].
Оказывается, [math]\displaystyle{ \to }[/math] является частичным порядком. Очевидно, что [math]\displaystyle{ \to }[/math] транзитивен. Осталось показать, что [math]\displaystyle{ \to }[/math] антирефлексивен: для всех x утверждение [math]\displaystyle{ x \to x }[/math] ложно.
Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов [math]\displaystyle{ m_0, ..., m_n }[/math], такие, что [math]\displaystyle{ m_0 \to m_1 \to \cdots \to m_n, m_n \to m_0 }[/math], и каждая пара непосредственно связана с некоторым [math]\displaystyle{ \to_x }[/math] или [math]\displaystyle{ \to_H }[/math].
Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом x. Поскольку [math]\displaystyle{ \to_x }[/math] является полным порядком, должны существовать два вызова метода [math]\displaystyle{ m_{i-1} }[/math] и [math]\displaystyle{ m_i }[/math] такие, что [math]\displaystyle{ m_{i-1} \to_H m_i }[/math] и [math]\displaystyle{ m_i \to_x m_{i-1} }[/math], что противоречит условию линеаризуемости x.
Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за [math]\displaystyle{ m_1 }[/math] и [math]\displaystyle{ m_2 }[/math] вызовы методов разных объектов (переиндексировав их при необходимости). Пусть x – объект, связанный с [math]\displaystyle{ m_1 }[/math]. Ни один из [math]\displaystyle{ m_2, ..., m_n }[/math] не может быть вызовом метода x. Утверждение справедливо для [math]\displaystyle{ m_2 }[/math] по построению. Пусть [math]\displaystyle{ m_i }[/math] – первый вызов метода в [math]\displaystyle{ m_3, ..., m_n }[/math], связанный с x. Поскольку [math]\displaystyle{ m_{i-1} }[/math] и [math]\displaystyle{ m_i }[/math] не связаны по [math]\displaystyle{ \to_x }[/math], они должны быть связаны по [math]\displaystyle{ \to_H }[/math], поэтому ответ [math]\displaystyle{ m_{i-1} }[/math] предшествует вызову [math]\displaystyle{ m_i }[/math]. Вызов [math]\displaystyle{ m_2 }[/math] предшествует ответу [math]\displaystyle{ m_{i-1} }[/math], поскольку в противном случае имело бы место [math]\displaystyle{ m_{i-1} \to_H m_2 }[/math], что дает более короткий цикл [math]\displaystyle{ m_2, ..., m_{i-1} }[/math]. Наконец, ответ [math]\displaystyle{ m_1 }[/math] предшествует вызову [math]\displaystyle{ m_i }[/math], поскольку по построению [math]\displaystyle{ m_1 \to_H m_2 }[/math]. Отсюда следует, что ответ на [math]\displaystyle{ m_1 }[/math] предшествует вызову [math]\displaystyle{ m_i }[/math], следовательно, [math]\displaystyle{ m_1 \to_H m_i }[/math], что дает более короткий цикл [math]\displaystyle{ m_1, m_i, ..., m_n }[/math].
Поскольку [math]\displaystyle{ m_n }[/math] не является вызовом метода x, а [math]\displaystyle{ m_n \to m_1 }[/math], из этого следует, что [math]\displaystyle{ m_n \to_H m_1 }[/math]. Но [math]\displaystyle{ m_1 \to_H m_2 }[/math] по построению, а так как [math]\displaystyle{ \to_H }[/math] транзитивно, то [math]\displaystyle{ m_n \to_H m_2 }[/math], что дает более короткий цикл [math]\displaystyle{ m_2, ..., m_n }[/math], так что имеет место противоречие. [math]\displaystyle{ \square }[/math]
Локальность важна, поскольку позволяет проектировать и строить параллельные системы по модульному принципу; линеаризуемые объекты могут быть реализованы, проверены и выполнены независимо друг от друга. Параллельная система, основанная на нелокальном свойстве корректности, должна либо полагаться на централизованный планировщик для всех объектов, либо удовлетворять дополнительным ограничениям, накладываемым на объекты, чтобы можно было гарантировать, что они следуют совместимым протоколам планирования. Локальность не должна восприниматься как нечто само собой разумеющееся; как будет показано ниже, в некоторых работах можно найти предложения по альтернативным свойствам корректности, не являющимся локальными.
Свойство неблокируемости
Линеаризуемость является неблокирующим свойством: ожидающий вызов полного метода никогда не должен ждать завершения другого ожидающего вызова.
Теорема 2. Пусть inv(m) – вызов полного метода. Если [math]\displaystyle{ \langle x \; invP \rangle }[/math] является ожидающим вызовом в линеаризуемой истории H, то существует ответ [math]\displaystyle{ \langle xresP \rangle }[/math], такой, что история [math]\displaystyle{ H \cdot \langle x \; resP \rangle }[/math] линеаризуема.
Доказательство. Пусть S – любая линеаризация H. Если S включает ответ [math]\displaystyle{ \langle x \; resP \rangle }[/math] на [math]\displaystyle{ \langle x \; invP \rangle }[/math], то доказательство тем самым завершается, так как S также является линеаризацией [math]\displaystyle{ H \cdot \langle x \; resP \rangle }[/math]. В противном случае [math]\displaystyle{ \langle x \; invP \rangle }[/math] также не встречается в S, поскольку линеаризации, по определению, не включают ожидающих вызовов. Поскольку метод является полным, существует ответ [math]\displaystyle{ \langle x \; resP \rangle }[/math] такой, что [math]\displaystyle{ S' = S \cdot \langle x \; invP \rangle \cdot \langle x \; resP \rangle }[/math] является легальным. S', однако, является линеаризацией [math]\displaystyle{ H \cdot \langle x \; resP \rangle }[/math], и, следовательно, также является линеаризацией H. [math]\displaystyle{ \square }[/math]
Из этой теоремы следует, что линеаризуемость сама по себе никогда не приводит к блокировке потока с ожидающим вызовом полного метода. Конечно, блокировки (или даже взаимоблокировки) могут возникать как артефакты конкретных реализаций процесса линеаризации, но они не присущи самому свойству корректности. Данная теорема утверждает, что линеаризуемость является подходящим условием корректности для систем, в которых важны параллелизм и ответ в реальном времени. Альтернативные условия корректности, такие как сериализуемость [1], не обладают этим свойством неблокируемости.
Свойство неблокируемости не исключает блокировку в ситуациях, когда она явно предполагается. Например, может быть разумным, чтобы поток, пытающийся произвести выгрузку из пустой очереди, блокировал ее, ожидая, пока другой поток не выгрузит элемент. Спецификация очереди отражает это намерение, делая спецификацию метода deq() частичной и оставляя его эффект неопределенным при применении к пустой очереди. Наиболее естественной параллельной интерпретацией частичной последовательной спецификации является простое ожидание, пока объект не достигнет состояния, в котором метод определен.
Другие свойства корректности
Последовательная согласованность [4] представляет собой более слабое условие корректности, в котором выполняется требование L1, но не L2: вызовы методов должны происходить по одному в некотором последовательном порядке, но неперекрываюмиеся вызовы могут быть переупорядочены. Любая линеаризуемая история является последовательно согласованной, однако обратное неверно. Последовательная согласованность допускает больший параллелизм, но это не локальное свойство: система, состоящая из множества последовательно согласованных объектов, вовсе не обязательно сама является последовательно согласованной.
Большая часть работ по базам данных и распределенным системам использует сериализуемость как основное условие корректности параллельных вычислений. В этой модели транзакция представляет собой «поток управления», который применяет конечную последовательность методов к набору объектов, общих с другими транзакциями. История является сериализуемой, если она эквивалентна той, в которой транзакции выполняются последовательно, то есть без чередования. История строго сериализуема, если порядок транзакций в последовательной истории совместим с их порядком предшествования: если каждый вызов метода одной транзакции предшествует каждому вызову метода другой, то первая сериализуется раньше второй. (Линеаризуемость можно рассматривать как частный случай строгой сериализуемости, в котором транзакции состоят только из одного метода, применяемого к одному объекту).
Ни сериализуемость, ни строгая сериализуемость не являются локальными свойствами. Если разные объекты сериализуют транзакции в разном порядке, то не может быть порядка сериализации, общего для всех объектов. Сериализуемость и строгая сериализуемость являются блокирующими свойствами: при определенных обстоятельствах транзакция может быть не в состоянии завершить ожидающий метод, не нарушая сериализуемости. Если несколько транзакций блокируют друг друга, возникает ситуация взаимоблокировки. Для таких транзакций необходимо выполнить откат и перезапуск, что подразумевает наличие дополнительных механизмов для этой цели.
Применение
Линеаризуемость широко применяется в качестве основного условия корректности для многих алгоритмов с параллельными структурами данных [5], особенно для структур данных без блокировок и без ожидания [2]. Последовательная непротиворечивость активно используется для описания низкоуровневых систем, таких как аппаратные интерфейсы памяти. Сериализуемость и строгая сериализуемость широко используются для систем баз данных, в которых прикладным программистам должно быть легко сохранять сложные специфические для приложения инварианты, охватывающие множество объектов.
Открытые вопросы
Современные мультипроцессоры часто поддерживают очень слабые модели согласованности памяти. Остается много нерешенных проблем, связанных с тем, как моделировать такое поведение и как обеспечить линеаризуемость объектных реализаций на таких архитектурах.
См. также
Литература
Понятие линеаризуемости было предложено Херлихи и Винг [3], последовательной согласованности – Лэмпортом [4], а сериализуемости Эсвараном и коллегами [1].
1. Eswaran, K.P., Gray, J.N., Lorie, R.A., Traiger, I.L.: The notions of consistency and predicate locks in a database system. Commun. ACM 19(11), 624-633 (1976). doi: http://doi.acm.org/10.1145/ 360363.360369
2. Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. (TOPLAS) 13(1), 124-149 (1991)
3. Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463^92 (1990)
4. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C-28(9),690(1979)
5. Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP '06: Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming, pp. 129-136 (2006). doi: http://doi.acm.org/1 0.1145/1122971.1122992