Линеаризуемость: различия между версиями

История 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 содержит вызовы методов <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> – полный порядок.

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

'''Определение 1'''. История H является ''линеаризуемой'', если она может быть расширена (путем добавления некоторого, возможно, нулевого количества событий ответа) до истории H' такой, что:

• (L1) complete(H') эквивалентна легальной последовательной истории S;

• (L2) Если вызов метода <math>m_0</math> предшествует вызову метода <math>m_1</math> в H, то то же самое верно и в S.

S называется ''линеаризацией'' H. (У одной истории может быть несколько линеаризаций). Неформально, расширение H до H' отражает идею о том, что некоторые ожидающие вызовы могут произвести эффект, даже если их ответы еще не были возвращены вызывающему.

Порядки <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>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>.

Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за <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>.

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

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

'''Теорема 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 включает ответ <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() частичной и оставляя его эффект неопределенным при применении к пустой очереди. Наиболее естественной параллельной интерпретацией частичной последовательной спецификации является простое ожидание, пока объект не достигнет состояния, в котором метод определен.

''Последовательная согласованность'' [4] представляет собой более слабое условие корректности, в котором выполняется требование L1, но не L2: вызовы методов должны происходить по одному в некотором последовательном порядке, но неперекрываюмиеся вызовы могут быть переупорядочены. Любая линеаризуемая история является последовательно согласованной, однако обратное неверно. Последовательная согласованность допускает больший параллелизм, но это не локальное свойство: система, состоящая из множества последовательно согласованных объектов, вовсе не обязательно сама является последовательно согласованной.