DistributedCounter.kt - Реализация счетчика с массивом
внутренних счетчиков
DistributedIncrementCounterTest.kt - Тест,
проверяющий внешне линеаризуемое поведение счетчика с инкрементом + 1 (как в условии)
DistributedRandomCounterTest.kt - Тест, показывающий
отсутствие линеаризуемости у счетчика с произвольным инкрементом
По определению, структура данных линеаризуема, если для любого исполнения можно сопоставить эквивалентное ему допустимое последовательное исполнение, которое сохраняет отношение happens-before. Допустимость определяется последовательной спецификацией объекта. Для счетчика верно, что исполнение допустимо, если get возвращает количество increment-ов, сделанных с начала работы со счетчиком.
Заметим, что операции над элементами массива атомарны (FAА и считывание), а значит нам доступна модель чередования при анализе возможных исполнений системы. Чтобы рассмотреть и доказать или опровергнуть линеаризуемость, рассмотрим сценарии исполнения, где параллельно с одной операцией get идет несколько inc из разных потоков. Будем рассматривать такие сценарии, тк эти операции конфликтующие (чтение и запись). Большее количество чтений можно не рассматривать, тк чтение не модифицирует внутреннее состояние. При этом только операции inс тоже рассматривать смысла нет, тк FAА атомарная операция.
Итак, пусть параллельно с операцией в n потоках выполняется суммарно m инкрементов, до этого счетчик имел значение 0. Покажем, что число, которое мы получим, будет в отрезке [0, m]. В дереве чередования будет два крайних случая: когда мы обогнали во внутреннем цикле все инкременты, то есть увеличение происходило в "хвост", который мы уже считали и к концу операции счетчик никак не изменится. В противоположность ему есть случай, когда считывание будет идти медленнее всех, то есть инкременты будут записывать в правую часть массива, которую мы еще не успели считать. В таком случае значение счетчика увеличится ровно на m. Результат других исполнений будет лежать между двумя этими крайними случаями. Таким образом мы видим, чтобы получить допустимое исполнение для операции get, которая выдала значение x (0 <= x <= m), нужно найти место между x и x + 1 инкрементами счетчика, а такое можно сделать всегда, тк инкременты увеличивают всегда на 1. При этом заметим, что это единственно верный алгоритм построения точки линеаризации этой операции, потому что любые другие дадут неверное значение счетчика для последовательной истории.
Однако при выборе такого алгоритма мы получим цикл в отношении happens-before. Представим, что поток P производит считывание (get), а в потоке Q происходят два последовательных инкремента, параллельно считыванию в потоке P. В массиве возьмем всего два элемента. Тогда возможно следующее исполнение:
| N | P | Q |
|---|---|---|
| 1 | read(a[0]) | |
| 2 | FAA(a[0], 1) | |
| 3 | FAA(a[1], 1) | |
| 4 | read(a[1]) |
По построению, единственно возможная точка линеаризации X будет лежать между (2) и (3) операциями. Однако заметим, что эффект от операции (2) мы не заметим, тк записывать она будет в уже считанную ячейку, а операцию (3) заметим, тк она запишет в еще не просуммированную ячейку. Тогда получим следующее отношение happens-before:
- (2) → (3) - тк в одном потоке, program order
- (3) → X - тк операция оказала эффект
- X → (2) - тк операция не оказала эффект
Получим цикл (2) → (3) → X → (2). Следовательно, линеаризация не выполняется, так как в единственно допустимом последовательном исполнении нарушается отношение happens-before.
Заметим однако, что операции inc идентично влияют на результат get, так как эффект от одной операции inc будет такой же, как и от любой другой (увеличение счетчика на 1) и многие состояния в дереве чередования коммутируют. Благодаря этому мы всегда можем в графе hb на операциях inc переставить их местами (даже внутри одного потока) так, чтобы цикла не образовывалось. Поэтому данный счетчик будет вести себя как линеаризуемый, при том, что, формально говоря, он таким не будет.
Для проверки теоретических выкладок на практике, я осуществил проверку с помощью фреймворка LinChecker, которая показала, что данная реализация счетчика проходит проверку на линеаризуемость, так как перестановки идентичных операций LinChecker проверить не может.
Также я проверил с его помощью, что такой же счетчик, но только который увеличивает каждый раз не на 1, а на некоторое
небольшое случайное значение, проверку не проходит, как и предсказывалось. Операции += random не идентичны для модели
счетчика, и их не всегда можно переставить так, чтобы устранить цикл.