Коротко — комбинированный подход: формальная модель + автоматическая проверка на уровне моделей + дедуктивная/логическая проверка кода. Ниже — метод, какие свойства проверять, инструменты и реальные ограничения.
Метод (процесс)
- Построить абстрактную модель поведения потоков, мьютексов и условных переменных (учесть семантику wait: освобождение мьютекса и повторное захватывание при пробуждении; учесть Mesa‑ vs Hoare‑семантику, спуріозные пробуждения). Формально: $wait(cv,m)\equiv release(m);block;acquire(m)$.
- Специфицировать инварианты и временные свойства (LTL/CTL). Примеры ниже.
- Проверить модель модель‑чекером (исчерпывающий поиск/ограниченный поиск + POR и симметрии).
- Для кода либо вручную доказать инварианты в системе дедуктивной верификации (concurrent separation logic / Iris / VCC / Verifast), либо сопоставить код и модель и доказывать соответствие (refinement).
- Итеративно уточнять модель по контрпримеру; комбинировать с динамическим тестированием (ThreadSanitizer, JPF) для практической проверки.
Какие свойства проверять
- Safety (безопасность)
- Взаимное исключение: для любых разных потоков $i\ne j$ не выполняется одновременно: $\neg (inC{S}_i\wedge inC{S}_j)$.
- Отсутствие гонок на разделяемой памяти (permissions/invariants в separation logic).
- Сохранение инвариантов состояния: $\square (I)$ (всегда $I$ истинно).
- Корректность использования условной переменной: поток, вызвавший $wait$, действительно освобождает мьютекс и при пробуждении снова его получает; ожидание в цикле: while‑pattern.
- Liveness (жизнеспособность)
- Отсутствие тупиков (deadlock‑freedom): нет циклического ожидания ресурсов. Формально: не существует цикла $(t_1,l_1,\dots ,t_k,l_k)$ такой, что для всех $i$ поток $t_i$ держит $l_i$ и ждет $l_{i+1}$ (индексы по модулю $k$).
- Прогресс для ожидающих по условию: в LTL — $\square (P\Rightarrow ◊\text{awoken})$ (если предикат $P$ истинно, кто‑то будет разбужен).
- Старвэйшн/bounded‑waiting (при необходимости): должна существовать граница ожидания.
- Корректность протоколов сигналов (signal/broadcast): если условие истинно, signal не должен теряться при неправильной реализации.
Инструменты (подбор в зависимости от уровня)
- Высокоуровневая проектная проверка (алгоритмы протоколов):
- TLA+/TLC — удобен для спецификации мьютексов и condvar, LTL.
- Promela/SPIN — модель‑чекер с поддержкой синхронизации, POR.
- UPPAAL — если есть тайминги.
- Код‑ориентированные:
- Java: Java PathFinder (JPF) для исчерпывающего перебора планировок.
- C: CBMC (bounded), SMACK/Boogie, VCC (модель и доказательства), Verifast (separation logic).
- Proof assistants: Coq+Iris, Isabelle/Hoare для формальных доказательств сложных инвариантов.
- Вспомогательные:
- ThreadSanitizer — динамический детектор гонок.
- Systematic testing (CHESS, KLEE) — пермутации планировок.
- Приёмы для борьбы со сложностью: частично‑упорядоченное сокращение (POR), симметричное сокращение, predicate abstraction, assume‑guarantee композиция.
Ограничения реальной сложности
- Комбинаторный взрыв состояний: число состояний растёт экспоненциально с числом потоков и ресурсов; даже с POR легко получить «недостижимые» пределы для больших систем.
- Семантика памяти: реальные weak memory models (ARM/Power) нарушают предположения о атомарности — требуется моделирование памяти или использовать памяти‑специфичные верификаторы.
- Сложность среды: системные вызовы, драйверы, взаимодействие с библиотеками трудно адекватно смоделировать.
- Параметризуемость: доказательство для произвольного числа потоков часто нерешаемо; нужны cutoffs/индуктивные техники.
- Затраты на аннотации и доказательства: инструменты дедуктивной верификации требуют больших усилий по спецификациям и доказательствам.
- Liveness vs fairness: liveness‑свойства обычно требуют fairness‑допущений о планировщике; эти допущения могут не соответствовать реальному окружению.
Практические рекомендации
- Моделируйте минимально достаточное поведение (абстрагируйте несущественное).
- Проверяйте safety сквозь модель‑чекер, а сложные инварианты доказывайте в логике (Iris/VCC).
- Для производственного кода используйте комбинированный подход: статическая верификация критичных примитивов + динамическая проверка (TSan) + тесты на планировки.
- Будьте явны в допущениях (планировщик, память, семантика condvar) и верифицируйте соответствие модели коду (refinement).
Если нужно, могу привести пример минимальной модели с условной переменной в Promela/Spin или шаблон спецификации в TLA+.