denisevteev/concurrent-counter

contention-aware counter, councurrent test, checked with GenMC model cheker

Теоретическая справка

Объект называется линеаризуемым, если любую конкурентную историю можно сопоставить какой-то эквивалентной последовательной истории, такой что

• результат выполнения всех методов такой же, как в конкурентной истории
• отвечает заданной последовательной спецификации объекта
• соблюдает частичный порядок

Конкурентная история задает частичный порядок на операциях - это значит, что два вызова упорядочены, если завершение первого вызова в истории идет раньше чем начало второго. В частности, частичный порядок сохраняет упорядоченность вызовов внутри каждого из потоков.

---

Как можно показать, что какой-то объект являестя корректным по какому-то типу согласованности?

Рассмотрим последовательность вызовов данного объекта вместе с соисполняющимися объектами (например, того же самого типа), обычно в других потоках. Тогда любая последовательность действий должна быть корректна в предположении, что объект обладает этим свойством корректности.

---

Чтобы показать, что объект линеаризуем, нужно предъявить алгоритм линеаризации произвольного исполнения (в частном случае – выбрать и обосновать точки линеаризации для каждого вызова).

Чтобы показать, что объект нелинеаризуем, нужно привести пример конкурентной истории, для которой нельзя построить линеаризацию, согласованную с последовательной спецификацией объекта. Иначе говоря, нужно предъявить исполнение, которое допускает реализация объекта, но которое нельзя объяснить никаким последовательным исполнением.

---

Доказательство св-в корректности contention-aware счетчика

Мы будем доказывать св-во линеаризуемости для данного объекта.

Утверждение: счетчик, у которого метод inc() увеличивает значение какой-то ячейка на один, является линеаризуемым.

Доказательство: предоставим точки линеаризации для каждого метода. В inc() это запись A[i] + 1 в A[i]. Благодаря ограничению на операцию inc(), которая лишь инкрементирует текущее значение на один, утверждается, что всегда найдется точка, в которую можно "стянуть" операцию get() и получить последовательное исполнение. Допустим, get() возвращает значение k. Tак как значение в счетчике определяется количеством вызовов inc(), был момент времени, когда значение в счетчике действительно равнялось k. Назовем этот момент между k-ым и k+1-м inc() точкой линеаризации. Этот момент был между началом и завершением вызова get(), иначе get() вернул бы значение, строго большее или меньшее k. Тогда, получившиеся точки линеаризации не будут нарушать порядок на неконкурентных вызовах, а также естественным образом задают последовательное исполнение, согласованное со спецификацией счетчика (после k инкрементов get() возвращает k).

---

Теперь рассмотрим счетчик, у которого метод inc(delta: Int) может принимать произвольное non-negative значение.

Утверждение: такой счетчик не является линеаризуемым.

Доказательство: Приведем конкурентное исполнение, которое не может быть описано никаким эквивалентным последовательным исполнением. (Будем рассматривать такой счетчик, у которого метод inc(delta: Int) использует действительно случаные числа несмотря на то, что в реализации нашего алгоритма применялись псевдо случайные числа.)

Пусть, 4 потока исполняются конкурентно

• A выполняет inc(3802)
• B inc(11)
• C get()
• D get()

Рассмотрим следующее конкурентное исполнение:

1. С прочитал нулевую ячейку, планировщик отстранил от выполнения поток
2. для A random вернул 0, и в нулевую ячейку записали число 3802
3. D завершил метод get(), вернув значение 3802
4. для B random вернул 1, и в первую ячейку положили число 11
5. наконец, C завершил метод get(), вернув значение 11

Таким образом, в результате конкурентного исполнения, потоки C и D вернули разные значения 11 и 3802 соответственно, чего невозможно получить ни одним последовательным исполнением, поэтому данный объект нелинеаризуем.

Ясно, что все последовательные исполнения методов над данным счетчиком могли привести только к тому, что методы get() вернули бы 3813 (оба), 0 (оба), 3802 (оба), 11 (оба), произвольную смесь 3813 и (3802 или 11).