From 57d048661a775b27360b17e9138eef42f637be14 Mon Sep 17 00:00:00 2001 From: hhhh Date: Sun, 14 Jun 2026 23:55:35 +0300 Subject: [PATCH] feat: add tla config for model --- .gitignore | 3 + validate/PartitionsStorageSets copy.cfg | 15 + validate/PartitionsStorageSets.cfg | 15 + validate/PartitionsStorageSets.tla | 191 +++ validate/PartitionsStorageSetsSmoke.cfg | 15 + validate/PartitionsStorageSets_explained.md | 1320 +++++++++++++++++++ validate/README.md | 33 + 7 files changed, 1592 insertions(+) create mode 100644 validate/PartitionsStorageSets copy.cfg create mode 100644 validate/PartitionsStorageSets.cfg create mode 100644 validate/PartitionsStorageSets.tla create mode 100644 validate/PartitionsStorageSetsSmoke.cfg create mode 100644 validate/PartitionsStorageSets_explained.md create mode 100644 validate/README.md diff --git a/.gitignore b/.gitignore index c107a7b..03745ea 100644 --- a/.gitignore +++ b/.gitignore @@ -51,6 +51,9 @@ bin/ # Debug information files *.dwo +# TLA+ states +states/ + # CMake *cmake*/ /CMakeLists.txt diff --git a/validate/PartitionsStorageSets copy.cfg b/validate/PartitionsStorageSets copy.cfg new file mode 100644 index 0000000..308123f --- /dev/null +++ b/validate/PartitionsStorageSets copy.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +INVARIANTS + TypeInvariant + UniqueOwnerForEveryKey + DeadPartitionsAreOutsideTree + +CONSTANTS + PartitionIds = {p0, p1, p2, p3, p4} + Threads = {t0, t1} + NoThread = NoThread + KeyCount = 8 + MinPartitionSize = 2 + MaxPartitionSize = 4 + MaxLoad = 8 diff --git a/validate/PartitionsStorageSets.cfg b/validate/PartitionsStorageSets.cfg new file mode 100644 index 0000000..a17fde2 --- /dev/null +++ b/validate/PartitionsStorageSets.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +INVARIANTS + TypeInvariant + UniqueOwnerForEveryKey + DeadPartitionsAreOutsideTree + +CONSTANTS + PartitionIds = {p0, p1, p2, p3, p4, p5, p6, p7} + Threads = {t0, t1, t2, t3} + NoThread = NoThread + KeyCount = 1024 + MinPartitionSize = 2 + MaxPartitionSize = 8 + MaxLoad = 9 diff --git a/validate/PartitionsStorageSets.tla b/validate/PartitionsStorageSets.tla new file mode 100644 index 0000000..a81437a --- /dev/null +++ b/validate/PartitionsStorageSets.tla @@ -0,0 +1,191 @@ +---- MODULE PartitionsStorageSets ---- +EXTENDS Naturals, FiniteSets + +(* +This model validates only the partition/set logic. +AVL tree lookup and QSBR are abstracted away as the variable `tree`, +which contains ids of currently reachable live partitions. +*) + +CONSTANTS + PartitionIds, + Threads, + NoThread, + KeyCount, + MinPartitionSize, + MaxPartitionSize, + MaxLoad + +ASSUME NoThread \notin Threads +ASSUME KeyCount > 0 +ASSUME MinPartitionSize > 0 +ASSUME MaxPartitionSize >= MinPartitionSize +ASSUME MaxLoad > MaxPartitionSize +ASSUME Cardinality(PartitionIds) >= 3 + +VARIABLES + partitions, + tree, + locks + +vars == <> + +Keys == 0..(KeyCount - 1) + +PartitionRecord == + [ lo : 0..KeyCount, + hi : 0..KeyCount, + dead : BOOLEAN, + load : 0..MaxLoad ] + +KeyInPartition(k, p) == + /\ partitions[p].lo <= k + /\ k < partitions[p].hi + +Status(p) == + IF partitions[p].dead THEN "DEAD" + ELSE IF partitions[p].load > MaxPartitionSize THEN "NEED_SPLIT" + ELSE IF partitions[p].load < MinPartitionSize /\ Cardinality(tree) > 1 THEN "NEED_SHRINK" + ELSE "ALIVE" + +Init == + \E p \in PartitionIds: + /\ tree = {p} + /\ partitions = + [ q \in PartitionIds |-> + IF q = p THEN + [ lo |-> 0, + hi |-> KeyCount, + dead |-> FALSE, + load |-> MinPartitionSize ] + ELSE + [ lo |-> 0, + hi |-> 0, + dead |-> TRUE, + load |-> 0 ] ] + /\ locks = [q \in PartitionIds |-> NoThread] + +TypeInvariant == + /\ partitions \in [PartitionIds -> PartitionRecord] + /\ tree \subseteq PartitionIds + /\ locks \in [PartitionIds -> (Threads \cup {NoThread})] + /\ \A p \in tree: + /\ partitions[p].dead = FALSE + /\ partitions[p].lo < partitions[p].hi + /\ partitions[p].hi <= KeyCount + /\ \A p \in PartitionIds \ tree: + partitions[p].dead = TRUE + +UniqueOwnerForEveryKey == + \A k \in Keys: + \E p \in tree: + /\ KeyInPartition(k, p) + /\ \A q \in tree: + KeyInPartition(k, q) => q = p + +DeadPartitionsAreOutsideTree == + \A p \in PartitionIds: + partitions[p].dead => p \notin tree + +Lock(t, p) == + /\ p \in tree + /\ locks[p] = NoThread + /\ locks' = [locks EXCEPT ![p] = t] + /\ UNCHANGED <> + +Unlock(t, p) == + /\ locks[p] = t + /\ locks' = [locks EXCEPT ![p] = NoThread] + /\ UNCHANGED <> + +\* Abstract user mutation of the set stored inside a locked partition. +GrowPartition(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ partitions[p].load < MaxLoad + /\ partitions' = [partitions EXCEPT ![p].load = @ + 1] + /\ UNCHANGED <> + +ShrinkPartitionLoad(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ partitions[p].load > 0 + /\ partitions' = [partitions EXCEPT ![p].load = @ - 1] + /\ UNCHANGED <> + +SplitPartition(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ Status(p) = "NEED_SPLIT" + /\ partitions[p].lo + 1 < partitions[p].hi + /\ \E left \in PartitionIds \ tree: + \E right \in (PartitionIds \ tree) \ {left}: + \E splitKey \in (partitions[p].lo + 1)..(partitions[p].hi - 1): + \E leftLoad \in 0..partitions[p].load: + LET rightLoad == partitions[p].load - leftLoad IN + /\ rightLoad \in 0..MaxLoad + /\ leftLoad \in 0..MaxLoad + /\ partitions' = + [ partitions EXCEPT + ![p].dead = TRUE, + ![left] = + [ lo |-> partitions[p].lo, + hi |-> splitKey, + dead |-> FALSE, + load |-> leftLoad ], + ![right] = + [ lo |-> splitKey, + hi |-> partitions[p].hi, + dead |-> FALSE, + load |-> rightLoad ] ] + /\ tree' = (tree \ {p}) \cup {left, right} + /\ locks' = + [ locks EXCEPT + ![p] = NoThread, + ![left] = NoThread, + ![right] = NoThread ] + +ShrinkToPrev(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ Status(p) = "NEED_SHRINK" + /\ \E prev \in tree \ {p}: + /\ locks[prev] = t + /\ partitions[prev].hi = partitions[p].lo + /\ partitions[prev].load + partitions[p].load <= MaxLoad + /\ partitions' = + [ partitions EXCEPT + ![prev].hi = partitions[p].hi, + ![prev].load = partitions[prev].load + partitions[p].load, + ![p].dead = TRUE ] + /\ tree' = tree \ {p} + /\ locks' = [locks EXCEPT ![p] = NoThread, ![prev] = NoThread] + +ShrinkToNext(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ Status(p) = "NEED_SHRINK" + /\ \E next \in tree \ {p}: + /\ locks[next] = t + /\ partitions[p].hi = partitions[next].lo + /\ partitions[next].load + partitions[p].load <= MaxLoad + /\ partitions' = + [ partitions EXCEPT + ![next].lo = partitions[p].lo, + ![next].load = partitions[next].load + partitions[p].load, + ![p].dead = TRUE ] + /\ tree' = tree \ {p} + /\ locks' = [locks EXCEPT ![p] = NoThread, ![next] = NoThread] + +Next == + \/ \E t \in Threads, p \in PartitionIds: Lock(t, p) + \/ \E t \in Threads, p \in PartitionIds: Unlock(t, p) + \/ \E t \in Threads, p \in PartitionIds: GrowPartition(t, p) + \/ \E t \in Threads, p \in PartitionIds: ShrinkPartitionLoad(t, p) + \/ \E t \in Threads, p \in PartitionIds: SplitPartition(t, p) + \/ \E t \in Threads, p \in PartitionIds: ShrinkToPrev(t, p) + \/ \E t \in Threads, p \in PartitionIds: ShrinkToNext(t, p) + +Spec == Init /\ [][Next]_vars + +==== diff --git a/validate/PartitionsStorageSetsSmoke.cfg b/validate/PartitionsStorageSetsSmoke.cfg new file mode 100644 index 0000000..5707544 --- /dev/null +++ b/validate/PartitionsStorageSetsSmoke.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +INVARIANTS + TypeInvariant + UniqueOwnerForEveryKey + DeadPartitionsAreOutsideTree + +CONSTANTS + PartitionIds = {p0, p1, p2} + Threads = {t0} + NoThread = NoThread + KeyCount = 3 + MinPartitionSize = 1 + MaxPartitionSize = 2 + MaxLoad = 3 diff --git a/validate/PartitionsStorageSets_explained.md b/validate/PartitionsStorageSets_explained.md new file mode 100644 index 0000000..cb58d14 --- /dev/null +++ b/validate/PartitionsStorageSets_explained.md @@ -0,0 +1,1320 @@ +# Разбор `PartitionsStorageSets.tla` + +Файл `PartitionsStorageSets.tla` описывает упрощенную TLA+ модель для проверки логики партиций, которые хранят множество ключей в виде полуоткрытых интервалов `[lo; hi)`. + +Модель намеренно не проверяет AVL и QSBR. Мы считаем, что: + +- AVL корректно находит нужную партицию; +- QSBR корректно защищает lifetime нод; +- переменная `tree` абстрактно означает "те partition id, которые сейчас достижимы из дерева". + +Главная цель модели: проверить, что операции split/shrink не создают дыр, пересечений и потерянных ключей. + +## Заголовок модуля + +```tla +---- MODULE PartitionsStorageSets ---- +EXTENDS Naturals, FiniteSets +``` + +`MODULE` объявляет имя TLA+ модуля. + +`EXTENDS Naturals, FiniteSets` подключает стандартные модули: + +- `Naturals` - натуральные числа, диапазоны `0..N`, арифметика; +- `FiniteSets` - операции над конечными множествами, например `Cardinality`. + +## Комментарий про абстракцию + +```tla +(* +This model validates only the partition/set logic. +AVL tree lookup and QSBR are abstracted away as the variable `tree`, +which contains ids of currently reachable live partitions. +*) +``` + +Это важное ограничение модели. + +Мы не моделируем: + +- форму AVL-дерева; +- балансировку; +- указатели; +- QSBR epochs; +- освобождение памяти; +- lock-free детали дерева. + +Вместо этого считаем, что `tree` - это множество id живых партиций, которые доступны через дерево. + +## Константы + +```tla +CONSTANTS + PartitionIds, + Threads, + NoThread, + KeyCount, + MinPartitionSize, + MaxPartitionSize, + MaxLoad +``` + +Константы задаются в `.cfg` файле. + +### `PartitionIds` + +```tla +PartitionIds +``` + +Множество всех id партиций, которые модель может использовать. + +Пример из `PartitionsStorageSetsSmoke.cfg`: + +```tla +PartitionIds = {p0, p1, p2} +``` + +Важно: `PartitionIds` - это не только живые партиции. Это пул всех возможных id. Часть из них может быть `DEAD`. + +### `Threads` + +```tla +Threads +``` + +Множество потоков, которые могут брать locks и выполнять операции. + +Пример: + +```tla +Threads = {t0} +``` + +Для более интересных конкурентных сценариев можно поставить: + +```tla +Threads = {t0, t1} +``` + +### `NoThread` + +```tla +NoThread +``` + +Специальное значение, означающее "mutex никем не захвачен". + +Пример: + +```tla +NoThread = NoThread +``` + +Это выглядит странно, но в TLA+ справа `NoThread` в `.cfg` задает символическое значение. + +### `KeyCount` + +```tla +KeyCount +``` + +Количество ключей в модели. + +Если `KeyCount = 3`, то ключи: + +```tla +0, 1, 2 +``` + +В модели полный диапазон ключей задается как `[0; KeyCount)`. + +### `MinPartitionSize` + +```tla +MinPartitionSize +``` + +Нижний порог размера партиции. + +Если `load < MinPartitionSize` и партиций больше одной, партиция считается `NEED_SHRINK`. + +### `MaxPartitionSize` + +```tla +MaxPartitionSize +``` + +Верхний нормальный порог размера партиции. + +Если `load > MaxPartitionSize`, партиция считается `NEED_SPLIT`. + +### `MaxLoad` + +```tla +MaxLoad +``` + +Технический максимум для поля `load`, чтобы пространство состояний было конечным. + +TLC должен перебрать конечное число состояний. Поэтому нельзя разрешить `load` быть любым натуральным числом. + +## Предположения о константах + +```tla +ASSUME NoThread \notin Threads +ASSUME KeyCount > 0 +ASSUME MinPartitionSize > 0 +ASSUME MaxPartitionSize >= MinPartitionSize +ASSUME MaxLoad > MaxPartitionSize +ASSUME Cardinality(PartitionIds) >= 3 +``` + +`ASSUME` задает требования к конфигурации. + +### `NoThread \notin Threads` + +```tla +ASSUME NoThread \notin Threads +``` + +Специальное значение `NoThread` не должно совпадать с реальным потоком. + +Иначе было бы невозможно отличить: + +- lock свободен; +- lock захвачен потоком с id `NoThread`. + +### `KeyCount > 0` + +```tla +ASSUME KeyCount > 0 +``` + +В модели должен быть хотя бы один ключ. + +### `MinPartitionSize > 0` + +```tla +ASSUME MinPartitionSize > 0 +``` + +Минимальный размер должен быть положительным. + +### `MaxPartitionSize >= MinPartitionSize` + +```tla +ASSUME MaxPartitionSize >= MinPartitionSize +``` + +Верхний порог не должен быть меньше нижнего. + +### `MaxLoad > MaxPartitionSize` + +```tla +ASSUME MaxLoad > MaxPartitionSize +``` + +Нужно, чтобы в модели вообще могли появляться состояния `NEED_SPLIT`. + +Если `MaxLoad <= MaxPartitionSize`, то `load > MaxPartitionSize` был бы невозможен. + +### `Cardinality(PartitionIds) >= 3` + +```tla +ASSUME Cardinality(PartitionIds) >= 3 +``` + +Нужно минимум 3 id: + +- один начальный живой partition; +- два новых partition для split. + +## Переменные состояния + +```tla +VARIABLES + partitions, + tree, + locks +``` + +Это состояние модели. + +В TLA+ каждое состояние - это конкретные значения всех переменных из `VARIABLES`. + +### `partitions` + +`partitions` хранит данные всех partition id. + +Тип: + +```tla +partitions \in [PartitionIds -> PartitionRecord] +``` + +То есть это функция: + +```text +partition id -> record партиции +``` + +### `tree` + +`tree` - множество partition id, которые сейчас доступны через дерево. + +Важно: + +```text +p \in tree +``` + +означает, что партиция живая и достижима. + +```text +p \notin tree +``` + +означает, что партиция недоступна из дерева. В этой модели такие партиции должны быть `dead = TRUE`. + +### `locks` + +`locks` хранит владельца mutex для каждой партиции. + +Тип: + +```tla +locks \in [PartitionIds -> (Threads \cup {NoThread})] +``` + +То есть: + +- `locks[p] = NoThread` - lock свободен; +- `locks[p] = t` - lock захвачен потоком `t`. + +## Список всех переменных + +```tla +vars == <> +``` + +`vars` нужен для temporal specification: + +```tla +Spec == Init /\ [][Next]_vars +``` + +Запись `[Next]_vars` означает: + +```text +либо происходит действие Next, +либо состояние не меняется по переменным vars +``` + +Это стандартный способ записывать спецификацию в TLA+. + +## Множество ключей + +```tla +Keys == 0..(KeyCount - 1) +``` + +Если `KeyCount = 8`, то: + +```tla +Keys = 0..7 +``` + +То есть полный диапазон ключей: + +```text +[0; KeyCount) +``` + +## Тип записи партиции + +```tla +PartitionRecord == + [ lo : 0..KeyCount, + hi : 0..KeyCount, + dead : BOOLEAN, + load : 0..MaxLoad ] +``` + +Каждая партиция - это record с полями: + +- `lo` - левая граница интервала; +- `hi` - правая граница интервала; +- `dead` - является ли партиция мертвой; +- `load` - абстрактный размер множества внутри партиции. + +Интервал полуоткрытый: + +```text +[lo; hi) +``` + +То есть ключ `k` принадлежит партиции, если: + +```text +lo <= k < hi +``` + +Почему `lo` и `hi` имеют тип `0..KeyCount`, а не `Keys`: + +- ключи идут от `0` до `KeyCount - 1`; +- правая граница последнего интервала равна `KeyCount`; +- поэтому `hi = KeyCount` должно быть допустимо. + +## Проверка принадлежности ключа партиции + +```tla +KeyInPartition(k, p) == + /\ partitions[p].lo <= k + /\ k < partitions[p].hi +``` + +`KeyInPartition(k, p)` истинно, если ключ `k` лежит внутри интервала партиции `p`. + +Пример: + +```text +partition = [lo |-> 2, hi |-> 5] +``` + +Тогда партиция содержит ключи: + +```text +2, 3, 4 +``` + +И не содержит `5`. + +## Вычисляемый статус партиции + +```tla +Status(p) == + IF partitions[p].dead THEN "DEAD" + ELSE IF partitions[p].load > MaxPartitionSize THEN "NEED_SPLIT" + ELSE IF partitions[p].load < MinPartitionSize /\ Cardinality(tree) > 1 THEN "NEED_SHRINK" + ELSE "ALIVE" +``` + +Статус не хранится отдельным полем. Он вычисляется из текущего состояния. + +Это полезно, потому что нельзя получить противоречивое состояние вида: + +```text +status = "ALIVE", но load > MaxPartitionSize +``` + +### `DEAD` + +```tla +IF partitions[p].dead THEN "DEAD" +``` + +Если `dead = TRUE`, партиция считается мертвой независимо от `load`. + +### `NEED_SPLIT` + +```tla +ELSE IF partitions[p].load > MaxPartitionSize THEN "NEED_SPLIT" +``` + +Если партиция живая и ее нагрузка больше верхнего порога, ее надо split. + +### `NEED_SHRINK` + +```tla +ELSE IF partitions[p].load < MinPartitionSize /\ Cardinality(tree) > 1 THEN "NEED_SHRINK" +``` + +Если партиция живая, маленькая, и в дереве больше одной партиции, ее можно shrink. + +Условие `Cardinality(tree) > 1` нужно потому, что последнюю оставшуюся партицию нельзя удалить. + +### `ALIVE` + +```tla +ELSE "ALIVE" +``` + +Все остальные живые партиции считаются нормальными. + +## Начальное состояние `Init` + +```tla +Init == + \E p \in PartitionIds: + /\ tree = {p} + /\ partitions = + [ q \in PartitionIds |-> + IF q = p THEN + [ lo |-> 0, + hi |-> KeyCount, + dead |-> FALSE, + load |-> MinPartitionSize ] + ELSE + [ lo |-> 0, + hi |-> 0, + dead |-> TRUE, + load |-> 0 ] ] + /\ locks = [q \in PartitionIds |-> NoThread] +``` + +`Init` описывает все допустимые начальные состояния. + +Здесь используется существование: + +```tla +\E p \in PartitionIds: +``` + +Это значит: TLC может выбрать любой `p` из `PartitionIds` как начальную живую партицию. + +### Начальное дерево + +```tla +tree = {p} +``` + +В начале есть ровно одна живая партиция. + +Она покрывает весь диапазон ключей. + +### Начальное значение `partitions` + +```tla +partitions = + [ q \in PartitionIds |-> + IF q = p THEN + ... + ELSE + ... ] +``` + +Это функция по всем partition id. + +Для выбранного `p` создается живая партиция: + +```tla +[ lo |-> 0, + hi |-> KeyCount, + dead |-> FALSE, + load |-> MinPartitionSize ] +``` + +Она покрывает весь диапазон: + +```text +[0; KeyCount) +``` + +Для всех остальных `q` создаются мертвые пустые партиции: + +```tla +[ lo |-> 0, + hi |-> 0, + dead |-> TRUE, + load |-> 0 ] +``` + +### Начальные locks + +```tla +locks = [q \in PartitionIds |-> NoThread] +``` + +Все mutex свободны. + +## TypeInvariant + +```tla +TypeInvariant == + /\ partitions \in [PartitionIds -> PartitionRecord] + /\ tree \subseteq PartitionIds + /\ locks \in [PartitionIds -> (Threads \cup {NoThread})] + /\ \A p \in tree: + /\ partitions[p].dead = FALSE + /\ partitions[p].lo < partitions[p].hi + /\ partitions[p].hi <= KeyCount + /\ \A p \in PartitionIds \ tree: + partitions[p].dead = TRUE +``` + +`TypeInvariant` проверяет базовую корректность формы состояния. + +Это не главный алгоритмический инвариант, но он почти всегда нужен в TLA+ моделях. + +### Тип `partitions` + +```tla +partitions \in [PartitionIds -> PartitionRecord] +``` + +Для каждого partition id есть корректная запись с полями: + +- `lo`; +- `hi`; +- `dead`; +- `load`. + +### Тип `tree` + +```tla +tree \subseteq PartitionIds +``` + +Дерево не может ссылаться на неизвестный partition id. + +### Тип `locks` + +```tla +locks \in [PartitionIds -> (Threads \cup {NoThread})] +``` + +Для каждой партиции lock либо свободен, либо принадлежит одному из потоков. + +### Все партиции в `tree` живые и непустые + +```tla +\A p \in tree: + /\ partitions[p].dead = FALSE + /\ partitions[p].lo < partitions[p].hi + /\ partitions[p].hi <= KeyCount +``` + +Если партиция достижима из дерева: + +- она не `dead`; +- ее интервал непустой; +- правая граница не выходит за общий диапазон. + +### Все партиции вне `tree` мертвые + +```tla +\A p \in PartitionIds \ tree: + partitions[p].dead = TRUE +``` + +Если partition id не достижим из дерева, он должен быть `dead`. + +Это сильное упрощение модели. В реальной системе из-за QSBR может существовать старая нода, которую еще кто-то читает. Но для текущей модели мы проверяем только логическую структуру живых интервалов. + +## Инвариант уникального владельца ключа + +```tla +UniqueOwnerForEveryKey == + \A k \in Keys: + \E p \in tree: + /\ KeyInPartition(k, p) + /\ \A q \in tree: + KeyInPartition(k, q) => q = p +``` + +Это главный инвариант модели. + +Он говорит: + +```text +для каждого ключа существует ровно одна живая партиция, которая содержит этот ключ +``` + +Разберем по частям. + +```tla +\A k \in Keys: +``` + +Для каждого ключа. + +```tla +\E p \in tree: +``` + +Существует живая партиция `p`. + +```tla +KeyInPartition(k, p) +``` + +Эта партиция содержит ключ. + +```tla +\A q \in tree: + KeyInPartition(k, q) => q = p +``` + +Любая другая живая партиция `q`, которая содержит этот ключ, на самом деле является той же самой партицией `p`. + +Иначе говоря: + +- нет дыр; +- нет пересечений; +- каждый ключ покрыт ровно одним интервалом. + +Если этот инвариант падает, значит split или shrink испортил покрытие диапазона. + +## Инвариант `DeadPartitionsAreOutsideTree` + +```tla +DeadPartitionsAreOutsideTree == + \A p \in PartitionIds: + partitions[p].dead => p \notin tree +``` + +Если партиция мертвая, она не должна быть достижима из дерева. + +Этот инвариант частично пересекается с `TypeInvariant`, но он более явно выражает важное свойство структуры данных. + +## Действие `Lock` + +```tla +Lock(t, p) == + /\ p \in tree + /\ locks[p] = NoThread + /\ locks' = [locks EXCEPT ![p] = t] + /\ UNCHANGED <> +``` + +`Lock(t, p)` моделирует взятие mutex партиции `p` потоком `t`. + +Предусловия: + +```tla +p \in tree +``` + +Можно брать lock только у живой достижимой партиции. + +```tla +locks[p] = NoThread +``` + +Lock должен быть свободен. + +Изменение: + +```tla +locks' = [locks EXCEPT ![p] = t] +``` + +В следующем состоянии владелец lock для `p` - поток `t`. + +Остальное не меняется: + +```tla +UNCHANGED <> +``` + +## Действие `Unlock` + +```tla +Unlock(t, p) == + /\ locks[p] = t + /\ locks' = [locks EXCEPT ![p] = NoThread] + /\ UNCHANGED <> +``` + +`Unlock(t, p)` моделирует освобождение mutex. + +Предусловие: + +```tla +locks[p] = t +``` + +Только владелец lock может его освободить. + +Изменение: + +```tla +locks' = [locks EXCEPT ![p] = NoThread] +``` + +В следующем состоянии lock свободен. + +## Действие `GrowPartition` + +```tla +\* Abstract user mutation of the set stored inside a locked partition. +GrowPartition(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ partitions[p].load < MaxLoad + /\ partitions' = [partitions EXCEPT ![p].load = @ + 1] + /\ UNCHANGED <> +``` + +Это абстрактное действие, которое увеличивает размер множества внутри партиции. + +Оно нужно, чтобы в модели могла появиться партиция со статусом `NEED_SPLIT`. + +Предусловия: + +```tla +p \in tree +``` + +Партиция живая. + +```tla +locks[p] = t +``` + +Поток держит mutex этой партиции. + +```tla +partitions[p].load < MaxLoad +``` + +Нельзя выйти за техническую верхнюю границу `MaxLoad`. + +Изменение: + +```tla +partitions' = [partitions EXCEPT ![p].load = @ + 1] +``` + +`@` означает старое значение изменяемого поля. + +То есть: + +```text +new load = old load + 1 +``` + +## Действие `ShrinkPartitionLoad` + +```tla +ShrinkPartitionLoad(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ partitions[p].load > 0 + /\ partitions' = [partitions EXCEPT ![p].load = @ - 1] + /\ UNCHANGED <> +``` + +Это абстрактное действие, которое уменьшает размер множества внутри партиции. + +Оно нужно, чтобы в модели могла появиться партиция со статусом `NEED_SHRINK`. + +Предусловия: + +- партиция живая; +- поток держит ее lock; +- `load > 0`. + +Изменение: + +```text +new load = old load - 1 +``` + +`tree` и `locks` не меняются. + +## Действие `SplitPartition` + +```tla +SplitPartition(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ Status(p) = "NEED_SPLIT" + /\ partitions[p].lo + 1 < partitions[p].hi + /\ \E left \in PartitionIds \ tree: + \E right \in (PartitionIds \ tree) \ {left}: + \E splitKey \in (partitions[p].lo + 1)..(partitions[p].hi - 1): + \E leftLoad \in 0..partitions[p].load: + LET rightLoad == partitions[p].load - leftLoad IN + /\ rightLoad \in 0..MaxLoad + /\ leftLoad \in 0..MaxLoad + /\ partitions' = + [ partitions EXCEPT + ![p].dead = TRUE, + ![left] = + [ lo |-> partitions[p].lo, + hi |-> splitKey, + dead |-> FALSE, + load |-> leftLoad ], + ![right] = + [ lo |-> splitKey, + hi |-> partitions[p].hi, + dead |-> FALSE, + load |-> rightLoad ] ] + /\ tree' = (tree \ {p}) \cup {left, right} + /\ locks' = + [ locks EXCEPT + ![p] = NoThread, + ![left] = NoThread, + ![right] = NoThread ] +``` + +`SplitPartition` моделирует разбиение одной большой партиции на две. + +### Предусловия split + +```tla +p \in tree +``` + +Разбиваем только живую партицию. + +```tla +locks[p] = t +``` + +Поток держит lock этой партиции. + +```tla +Status(p) = "NEED_SPLIT" +``` + +Разбиение разрешено только если партиция слишком большая. + +```tla +partitions[p].lo + 1 < partitions[p].hi +``` + +Интервал должен быть достаточно большим, чтобы его можно было разделить на два непустых интервала. + +Например, `[0; 2)` можно разделить на `[0; 1)` и `[1; 2)`. + +А `[0; 1)` разделить нельзя. + +### Выбор новых partition id + +```tla +\E left \in PartitionIds \ tree: + \E right \in (PartitionIds \ tree) \ {left}: +``` + +TLC недетерминированно выбирает два свободных id: + +- `left`; +- `right`. + +Они должны быть вне текущего `tree`. + +### Выбор точки split + +```tla +\E splitKey \in (partitions[p].lo + 1)..(partitions[p].hi - 1): +``` + +`splitKey` выбирается строго внутри интервала. + +Старый интервал: + +```text +[lo; hi) +``` + +Новые интервалы: + +```text +[lo; splitKey) +[splitKey; hi) +``` + +### Распределение load + +```tla +\E leftLoad \in 0..partitions[p].load: + LET rightLoad == partitions[p].load - leftLoad IN +``` + +Модель не знает, как реальные элементы распределяются между половинами. + +Поэтому она разрешает любое распределение: + +```text +leftLoad + rightLoad = oldLoad +``` + +Это полезная абстракция: TLC проверяет больше вариантов, включая неудобные. + +### Изменение `partitions` + +```tla +partitions' = + [ partitions EXCEPT + ![p].dead = TRUE, + ![left] = + [ lo |-> partitions[p].lo, + hi |-> splitKey, + dead |-> FALSE, + load |-> leftLoad ], + ![right] = + [ lo |-> splitKey, + hi |-> partitions[p].hi, + dead |-> FALSE, + load |-> rightLoad ] ] +``` + +В следующем состоянии: + +- старая партиция `p` становится `dead`; +- `left` становится живой партицией `[old.lo; splitKey)`; +- `right` становится живой партицией `[splitKey; old.hi)`. + +### Изменение `tree` + +```tla +tree' = (tree \ {p}) \cup {left, right} +``` + +В дереве: + +- удаляем старую партицию `p`; +- добавляем две новые. + +### Изменение `locks` + +```tla +locks' = + [ locks EXCEPT + ![p] = NoThread, + ![left] = NoThread, + ![right] = NoThread ] +``` + +После split locks освобождены. + +Это упрощение модели. Если в C++ реализации `get` возвращает пользователю уже locked partition, возможно позднее стоит уточнить это поведение. + +## Действие `ShrinkToPrev` + +```tla +ShrinkToPrev(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ Status(p) = "NEED_SHRINK" + /\ \E prev \in tree \ {p}: + /\ locks[prev] = t + /\ partitions[prev].hi = partitions[p].lo + /\ partitions[prev].load + partitions[p].load <= MaxLoad + /\ partitions' = + [ partitions EXCEPT + ![prev].hi = partitions[p].hi, + ![prev].load = partitions[prev].load + partitions[p].load, + ![p].dead = TRUE ] + /\ tree' = tree \ {p} + /\ locks' = [locks EXCEPT ![p] = NoThread, ![prev] = NoThread] +``` + +`ShrinkToPrev` моделирует слияние маленькой партиции `p` с предыдущей соседней партицией. + +### Предусловия + +```tla +p \in tree +``` + +Удалять можно только живую партицию. + +```tla +locks[p] = t +``` + +Поток держит lock удаляемой партиции. + +```tla +Status(p) = "NEED_SHRINK" +``` + +Партиция маленькая и есть больше одной живой партиции. + +### Выбор предыдущей партиции + +```tla +\E prev \in tree \ {p}: +``` + +TLC выбирает другую живую партицию `prev`. + +```tla +locks[prev] = t +``` + +Тот же поток должен держать lock соседа. + +```tla +partitions[prev].hi = partitions[p].lo +``` + +`prev` должна быть настоящим левым соседом. + +Например: + +```text +prev = [0; 3) +p = [3; 5) +``` + +### Ограничение load + +```tla +partitions[prev].load + partitions[p].load <= MaxLoad +``` + +Нужно, чтобы после слияния `load` не вышел за технический максимум модели. + +### Изменение `partitions` + +```tla +partitions' = + [ partitions EXCEPT + ![prev].hi = partitions[p].hi, + ![prev].load = partitions[prev].load + partitions[p].load, + ![p].dead = TRUE ] +``` + +Сосед `prev` расширяется вправо: + +```text +prev: [prev.lo; prev.hi) +p: [p.lo; p.hi) +``` + +становится: + +```text +prev: [prev.lo; p.hi) +``` + +Партиция `p` становится мертвой. + +### Изменение `tree` + +```tla +tree' = tree \ {p} +``` + +Удаляем `p` из дерева. + +### Изменение `locks` + +```tla +locks' = [locks EXCEPT ![p] = NoThread, ![prev] = NoThread] +``` + +После shrink locks освобождаются. + +## Действие `ShrinkToNext` + +```tla +ShrinkToNext(t, p) == + /\ p \in tree + /\ locks[p] = t + /\ Status(p) = "NEED_SHRINK" + /\ \E next \in tree \ {p}: + /\ locks[next] = t + /\ partitions[p].hi = partitions[next].lo + /\ partitions[next].load + partitions[p].load <= MaxLoad + /\ partitions' = + [ partitions EXCEPT + ![next].lo = partitions[p].lo, + ![next].load = partitions[next].load + partitions[p].load, + ![p].dead = TRUE ] + /\ tree' = tree \ {p} + /\ locks' = [locks EXCEPT ![p] = NoThread, ![next] = NoThread] +``` + +`ShrinkToNext` моделирует слияние маленькой партиции `p` со следующей соседней партицией. + +Это симметрично `ShrinkToPrev`. + +### Выбор следующей партиции + +```tla +\E next \in tree \ {p}: +``` + +TLC выбирает другую живую партицию `next`. + +```tla +partitions[p].hi = partitions[next].lo +``` + +`next` должна быть настоящим правым соседом. + +Например: + +```text +p = [3; 5) +next = [5; 8) +``` + +### Изменение интервала + +```tla +![next].lo = partitions[p].lo +``` + +Правая партиция расширяется влево: + +```text +p: [p.lo; p.hi) +next: [next.lo; next.hi) +``` + +становится: + +```text +next: [p.lo; next.hi) +``` + +Партиция `p` становится мертвой и удаляется из `tree`. + +## Действие `Next` + +```tla +Next == + \/ \E t \in Threads, p \in PartitionIds: Lock(t, p) + \/ \E t \in Threads, p \in PartitionIds: Unlock(t, p) + \/ \E t \in Threads, p \in PartitionIds: GrowPartition(t, p) + \/ \E t \in Threads, p \in PartitionIds: ShrinkPartitionLoad(t, p) + \/ \E t \in Threads, p \in PartitionIds: SplitPartition(t, p) + \/ \E t \in Threads, p \in PartitionIds: ShrinkToPrev(t, p) + \/ \E t \in Threads, p \in PartitionIds: ShrinkToNext(t, p) +``` + +`Next` описывает один шаг системы. + +На каждом шаге TLC выбирает одно из действий: + +- взять lock; +- отпустить lock; +- увеличить `load`; +- уменьшить `load`; +- split; +- shrink в предыдущую партицию; +- shrink в следующую партицию. + +Запись: + +```tla +\/ +``` + +означает логическое "или". + +Запись: + +```tla +\E t \in Threads, p \in PartitionIds: +``` + +означает, что TLC перебирает все варианты потока `t` и партиции `p`. + +Если предусловия действия не выполняются, этот вариант просто невозможен. + +## Спецификация `Spec` + +```tla +Spec == Init /\ [][Next]_vars +``` + +`Spec` - это полное описание поведения системы. + +Оно говорит: + +1. Первое состояние должно удовлетворять `Init`. +2. Каждый следующий шаг должен удовлетворять `[Next]_vars`. + +`[]` означает "всегда". + +`[Next]_vars` означает: + +- либо произошел один из переходов `Next`; +- либо состояние осталось тем же по переменным `vars`. + +## Конец модуля + +```tla +==== +``` + +Так заканчивается TLA+ модуль. + +## Как читать counterexample + +Если TLC найдет ошибку, он покажет последовательность состояний: + +```text +State 1 +State 2 +State 3 +... +``` + +Для этой модели нужно смотреть прежде всего: + +- `tree`; +- `partitions`; +- `locks`; +- какое действие было между состояниями. + +Если нарушился `UniqueOwnerForEveryKey`, значит произошло одно из двух: + +- появился ключ, который не принадлежит ни одной живой партиции; +- появился ключ, который принадлежит двум живым партициям. + +Практически это означает ошибку в логике split/shrink или слишком слабое предусловие действия. + +## Как запускать + +Быстрый smoke-test: + +```bash +java -jar /home/hhhh/bin/toolbox/tla2tools.jar \ + -config validate/PartitionsStorageSetsSmoke.cfg \ + validate/PartitionsStorageSets.tla +``` + +Более тяжелая проверка: + +```bash +java -jar /home/hhhh/bin/toolbox/tla2tools.jar \ + -config validate/PartitionsStorageSets.cfg \ + validate/PartitionsStorageSets.tla +``` + +Smoke-конфиг нужен для быстрой проверки синтаксиса и базовых инвариантов. + +Полный конфиг перебирает гораздо больше состояний и может работать долго. + +## Что модель пока не проверяет + +Текущая модель не проверяет: + +- корректность AVL rotations; +- корректность lock-free публикации новых узлов; +- ABA-проблемы; +- QSBR epochs; +- memory reclamation; +- C++ memory ordering; +- порядок взятия нескольких locks; +- deadlock-freedom; +- liveness. + +Это осознанно. Сейчас модель проверяет только базовую безопасность интервалов: + +```text +каждый ключ всегда принадлежит ровно одной живой партиции +``` + +Следующий логичный шаг - уточнить `shrink`, добавив состояние операции по шагам: + +1. отпустили lock своей партиции; +2. нашли prev; +3. взяли prev lock; +4. снова взяли свой lock; +5. нашли next; +6. взяли next lock; +7. проверили DEAD; +8. удалили текущую партицию. + +Тогда модель начнет проверять больше конкурентных interleavings. diff --git a/validate/README.md b/validate/README.md new file mode 100644 index 0000000..bc225b4 --- /dev/null +++ b/validate/README.md @@ -0,0 +1,33 @@ +# Валидация + +## Описание структуры данных (partitions_storage) +1) Внутри данной структуры данных хранятся множества в виде полуоткрытых интервалов ([X; Y), [Y; Z), ... ) +2) В процессе работы множество может быть разбито на два более маленьких для увелечения производительности доступа +3) В процессе работы множество может быть присаеденено к другому если оно стало слишком маленьким +4) Запросы, которые может поддерживать: + - `get(key)` - отдает множество, в которому принадлежит данный ключ, множество находится в данный момент под mutex_lock + +## Описание работы структуры данных +1) Внутри используется персистентное AVL дерево, которое является lock-free и в узлах, хранит как раз так называемые множества +2) У партиции может быть несколько состояний в момент когда пользователь взяль mutex lock и прочитал состояние: + - ALIVE ( 16 <= `partition.size()` <= 128) + - NEED_SPLIT ( `partition.size()` > 128) + - NEED_SHRINK ( 16 > `partition.size()` && partitions_count > 1) + - DEAD (особое состояние) +3) Как происходит get: + - сначала получаем из AVL дерева ноду на партицию (она защищена QSBR) и берем у нее mutex lock + - проверяем состояние, если DEAD, то возвращаемся к предыдущему шагу. Если ALIVE то возвращаем, иначе выполняем соответствующие команды +4) Как происходит split: + - так как над портицией держится lock то мы пемечяем ее как DEAD + - разделяем на две по некоторому ключу + - вставляем в AVL дерево за место ноды связку из таких node (left, split_key, right) +5) Как происходит shrink (shrink происходит когда множеств больше чем одно): + - отпускаем lock + - находим предыдущею до нас множество и берем у него lock, проверяя не является ли она DEAD + - берем lock у нашей партиции и проверяем что она не DEAD + - находим следующую за нами множество и берем у него lock, проверяя не является ли она DEAD + - помечаем нашу партицию как DEAD + - "убираем" нашу партицию из дерева и запоминаем каким ребенком мы были для предка (left, right) + - если мы были правым ребенком то передаем все множество в следующее множество + - если мы были левым ребенком то передаем все множество в прошлое множество +6) В начальный момент времени существует либо только одно множество, либо несколько их, которые сбалансированы