4446
правок
Линеаризуемость: различия между версиями
Материал из WEGA
м
→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 63: | Строка 63: | ||
Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом 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. | Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом 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> | Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за <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_2</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> | Поскольку <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> | ||
Локальность важна, поскольку позволяет проектировать и строить параллельные системы по модульному принципу; линеаризуемые объекты могут | Локальность важна, поскольку позволяет проектировать и строить параллельные системы по модульному принципу; линеаризуемые объекты могут реализовываться, проверяться и выполняться независимо друг от друга. Параллельная система, основанная на нелокальном свойстве корректности, должна либо полагаться на централизованный планировщик для всех объектов, либо удовлетворять дополнительным ограничениям, накладываемым на объекты, чтобы можно было гарантировать, что они следуют совместимым протоколам планирования. Локальность не должна восприниматься как нечто само собой разумеющееся; как будет показано ниже, в некоторых работах можно найти предложения по альтернативным свойствам корректности, не являющимся локальными. | ||
'''Свойство неблокируемости''' | '''Свойство неблокируемости''' | ||
Линеаризуемость является ''неблокирующим'' свойством: | Линеаризуемость является ''неблокирующим'' свойством: ожидающее обращение к полному методу никогда не должно ждать завершения другого ожидающего обращения. | ||
'''Теорема 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 включает ответ <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> | Доказательство. Пусть 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> | ||
