Проверка линеаризуемости Caffeine Cache
testing
audit-linearizability — это скилл для Claude Code, который анализирует кэш Caffeine на нарушения линеаризуемости по всем публичным методам. Для каждой операции — get, put, remove, replace, compute, bulk-методов вроде getAll и putAll — агент определяет единственную точку линеаризации: атомарный шаг, в момент которого операция становится видимой другим потокам. По каждому методу скилл формулирует точку линеаризации с указанием конкретной инструкции (например, «CAS on CHM bin at line X»), разбирает условные случаи и строит двухпоточный сценарий для подтверждения. Затем предпринимается попытка сконструировать нарушения: некорректный порядок наблюдения значений, двойное выполнение функции в computeIfAbsent, возврат значения после remove. Bulk-операции явно размечаются как нелинеаризуемые в целом, size() проверяется на задокументированность как приблизительное значение, а для async-вариантов кэша исследуется, что является точкой линеаризации — создание future или его завершение. Скилл ориентирован на инженеров, верифицирующих корректность конкурентных структур данных, и работает исключительно на уровне внешней наблюдаемости без анализа внутренней согласованности.
- #linearizability
- #concurrency
- #atomicity
- #correctness
- #sequential-consistency