# Разбор `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.