Кратко — три подхода:
- Model checking: строится конечная модель (граф состояний) программы и систематически перебираются все состояния/переходы; проверяются свойства (LTL/CTL) — отлично для конечных/ограниченных систем, обнаруживает контрпримеры.
- Доказательства с предусловиями/постусловиями (Hoare‑логика, rely/guarantee, Separation Logic): формулируются утверждения вида $\{P\}C\{Q\}$. Для конкурентности вводят инварианты и правила для критических секций/замков; даёт структурированное, понятное доказательство.
- SMT‑решатели: сводят свойства и поведение программы к формуле в логике (обычно баг‑поиск/инваринты), SMT проверяет выполнимость; подходят для проверки арифметики, указателей и сложных условий, часто в сочетании с инвариантным выводом или абстрактной интерпретацией.
Применение: доказательство отсутствия гонок и сохранения инварианта для простейшего примера с двумя потоками, методом Hoare‑логики с замком.
Псевдокод (разделяемые переменные: $x$, $L$; $L=0$ — свободен, $L=1$ — захвачен):
Thread1:
acquire(L);
x := x + 1;
release(L);
Thread2:
acquire(L);
x := x + 2;
release(L);
Начальное состояние: $x=0,L=0$.
Инвариант, который хотим сохранить: $I:x\ge 0.$
Допущения: операции присваивания и изменения $L$ выполняются атомарно; acquire — выполняется как атомарная проверка/установка $L$ (т.е. позволяется только при $L=0$ и делает $L:=1$).
Доказательство по шагам (Hoare‑тройки):
1) Захват замка (acquire). Правило присваивания даёт:
$\{L=0\wedge I\}L:=1\{L=1\wedge I\}.$ То есть захват не разрушает инвариант $I$ (он касается только $x$).
2) Критическая секция потока 1:
$\{L=1\wedge I\}x:=x+1\{L=1\wedge x\ge 1\}.$ Из $x\ge 0$ после $x:=x+1$ следует $x\ge 1$, значит $I$ сохраняется: $x\ge 1\Rightarrow x\ge 0$.
3) Освобождение замка:
$\{L=1\wedge I\}L:=0\{L=0\wedge I\}.$ Освобождение тоже не трогает $x$.
Аналогично для потока 2:
$\{L=1\wedge I\}x:=x+2\{L=1\wedge x\ge 2\}$,
и затем release сохраняет $I$.
Взаимное исключение (отсутствие гонок): по предположению acquire реализован как атомический переход, допускающий захват только при $L=0$, и делает $L:=1$. Следовательно две критические секции не могут выполняться одновременно: не существует состояния, в котором оба потока имеют $L=1$. Поскольку все операции над $x$ выполняются только внутри критической секции (когда $L=1$ у владельца), конкурентного доступа к $x$ без синхронизации не происходит — значит гонок данных нет.
Итог: при допущениях об атомарности acquire/release и приведённых Hoare‑трюках, каждый шаг сохраняет инвариант $x\ge 0$ и замок обеспечивает взаимное исключение, следовательно отсутствуют гонки и инвариант сохраняется во всей параллельной системе.
Короткое замечание о других методах: тот же пример можно формализовать для model checking — моделью будет кортеж $(x,L,s_1,s_2)$ и проверить, что во всех достижимых состояниях $x\ge 0$ и не существует состояния с одновременным входом в критические секции; или с помощью SMT вывести инвариант $x\ge 0$ автоматическим образом.