Skip to content

Latest commit

 

History

History
57 lines (33 loc) · 11 KB

01-berns-lynch.md

File metadata and controls

57 lines (33 loc) · 11 KB

Нижняя оценка на число ячеек памяти для протокола взаимного исключения

Теорема (Бернс, Линч)

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

Доказательство.

Предположим, работают n и есть протокол, который:

  • гарантирует взаимное исключение (ВИ);
  • гарантирует свободу от взаимной блокировки (СВБ);
  • использует меньше n ячеек памяти.

Никаких других предположений нет. Докажем, что такого протокола не существует.

Для n=2.

Даны потоки T₁, T₂ и ячейка памяти X₁. Рассмотрим два случая:

  1. пусть поток T₁ ничего не пишет и заходит в критическую секцию (СВБ). Тогда пришедший поток T₂ увидет мьютекс в исходном состоянии и также пройдет в критическую секцию. Нарушается ВИ;
  2. пусть поток T₁ пишет что-то в ячейку X₁ и планировщик останавливает выполнение потока T₁ перед его первой записью в X₁. После этого пришедший поток T₂ проходит в критическую секцию (СВБ). Тогда проснувшийся поток T₁ первый действием уничтожит все следы существования потока T₂, записав свое значение в X₁. Таким образом, (по СВБ) он проходит в критическую секцию. Нарушается ВИ.

В обоих случаях получено противоречие, следовательно, для n=2 теорема доказана.

Для n=3.

Даны потоки T₁, T₂, T₃ и ячейки памяти X₁, X₂. Ясно, что каждый поток что-то пишет хотя бы в одну из ячеек памяти. Рассмотрим такую конфигурацию, что T₁ и T₂ остановлены перед своими первыми записями в X₁ и X₂ соответственно (без потери общности), причем ячейки X₁ и X₂ содержат начальные значения. Пусть поток T₃ проходит в критическую секцию. Далее T₁ делает свою запись в X₁, затем T₂ делает свою запись в X₂. Таким образом, стерты все следы существования потока T₃. Тогда (по СВБ) один из потоков T₁, T₂ проходит в критическую секцию. Нарушается ВИ.

Докажем, что описанную конфигурацию всегда можно получить. Пусть поток T₁ выполняет следующие операции: mutex.lock() -> mutex.unlock() -> mutex.lock() -> mutex.unlock() -> mutex.lock() -> mutex.lock(). Так как методов lock() вызвано три, а ячеек памяти две, то по принципу Дирихле в одну из ячеек памяти первая запись осуществлена дважды. Пусть для определенности эти записи в ячейку X₁ на первой и третьей итерации.

Остановим поток T₁ перед его первой записью в X₁ на первой итерации. Далее запускаем поток T₂: ясно, что он пишет что-то в ячейку X₂ (по доказанному для n=2). Остановим его перед первой записью в ячейку X₂. (Возможно, он при этом что-то записал в X₁!) Далее запускаем поток T₁ и останавливаем его перед первой записью в ячейку X₁ на третьей итерации. По построению это первая запись потока T₁, то есть значение X₂ начальное: был вызван метод unlock(). Таким образом, T₁ остановлен перед первой записью в X₁, T₂ остнановлен перед первой записью в X₂. Искомая конфигурация получена, что и доказывает теорему для n=3.

Для произвольного n.

Докажем утверждение индукцией по n. База рассмотрена выше. Далее везде считаем, что для меньшего, чем n, числа потоков, теорема доказана.

Даны потоки T₁, T₂, …, T_[n+1] и ячейки памяти X₁, X₂, …, X_n. Ясно, что каждый поток что-то пишет хотя бы в одну из ячеек памяти. Рассмотрим такую конфигурацию, что T₁, T₂, …, T_n остановлены перед своими первыми записями в X₁, X₂, …, X_n соответственно (без потери общности), причем ячейки X₁, X₂, …, X_n содержат начальные значения. Пусть поток T_[n+1] проходит в критическую секцию. Далее T₁ делает свою запись в X₁, затем T₂ делает свою запись в X₂, …, затем T_n делает свою запись в X_n. Таким образом, стерты все следы существования потока T_[n+1]. Тогда (по СВБ) один из потоков T₁, T₂, …, T_n проходит в критическую секцию. Нарушеается ВИ.

Докажем, что описанную конфигурацию всегда можно получить, индукцией по числу потоков.

Утверждение. Пусть 1≤k≤n. Тогда существует конфигурация, когда T₁, T₂, …, T_k остановлены перед своими первыми записями в разные k ячеек памяти, причем все ячейки памяти содержат начальные значения.

База при k=1 очевидна.

Пусть теперь k > 1. По предположению индукции возможно получить конфигурацию, когда T₁, T₂, …, T_k пишут в разные k ячеек памяти. Обозначим через ConfigureThreads() последовательность операций, приводящую к такой конфигурации. Из k потоков в k ячеек памяти из n возможных существует C[n,k] различных отображений. Тогда пусть потоки выполняют ConfigureThreads() -> ConfigureThreads() -> … -> ConfigureThreads() всего C[n,k]+1 раз. По принципу Дирихле найдется такие две ConfigureThreads(), которые делают одно и то же соответствие между T₁, T₂, …, T_k и k ячейками памяти. Пусть для определенности это первый и последний вызов ConfigureThreads(), а запись осуществела в ячейки памяти X₁, X₂, …, X_k соответственно.

Рассмотрим найденное выполение операций ConfigureThreads() -> …. Остановим потоки в рассмотренной выше конфигурации. Далее запустим T_[k+1]. Ясно, что он пишет что-то в какую-то из ячеек X_[k+1], …, X_n (по предположению индукции для меньшего n). Остановим его перед первой записью в какую-то из этих ячеек. (Возможно, он при этом что-то записал в какие-то из ячеек X₁, …, X_k!) Далее запускаем наши ConfigureThreads() и останавливаем их перед своими первыми записями в X₁, …, X_k на последней итерации. По построению ячейки X_[k+1], …, X_n содержат начальные значения. Таким образом, потоки T₁, …, T_k, T_[k+1] остановлены перед своими первыми записями в разные k+1 ячеек памяти. Утверждение доказано.

Значит, искомая конфигурация существует для k=n, что и доказывает теорему в общем случае.

Замечания.

  • Каждый метод lock() не обязан требовать обращения ко всем n ячейкам памяти. Например, в турнирном дереве мьютексов один вызов обращается к O(log(n)) ячейкам.
  • Для построения противоречия мы не использовали никаких предположений о разрядности ячеек памяти.
  • Доказательство работает даже для случая недетерминированного исполнения.
  • Доказательство не работает, если используется операция exchange(): с ее помощью можно атомарно менять значение в ячейке памяти и читать старое значение, на основании которого делать выводы о наличии других потоков.
  • Каждый ConfigureThreads() для k потоков построен с помощью C[n,k-1]+1 операций ConfigureThreads() для k-1 потоков. Таким образом, для построения «плохого исполнения» в случае n потоков используется экспоненциальное число операций (сумма биномиальных коэффициентов).