Ждать, пока race conditions проявятся в продакшене, — это не тестирование. Это надежда, замаскированная под добросовестность.

Вы можете запускать приложение неделями, следить за метриками на дашбордах и всё равно зарелизить concurrency-баг, который срабатывает только когда два request попадают в одно и то же окно cache eviction. Проблема не в том, что вам не везёт. Проблема в том, что ваша стратегия тестирования полагается на то, что scheduler проявит злобность в вашу пользу в нужный момент, пока вы случайно смотрите.

Есть лучший путь. Model checking позволяет исследовать все возможные interleaving вашей конкурентной логики за секунды, а не дни. Он найдёт ту race condition, для которой вы не написали тест.

Что на самом деле делает model checking

Model checking — это не fuzzer. Он не швыряет случайные input’ы в код и не молится. Он строит математическую модель возможных состояний системы и исчерпывающе обходит их.

Представьте конкурентную программу как граф. Каждый node — это состояние: значения переменных, содержимое queue, какой thread удерживает какой lock. Каждое edge — это шаг: thread читает значение, захватывает mutex или отправляет сообщение. Scheduler выбирает, какой thread выполняется следующим, и этот выбор ветвит граф.

Model checker проходит по каждому пути этого графа. Если какой-либо путь приводит к тому, что два thread’а пишут в одну память без синхронизации, он сообщает counterexample: точную последовательность шагов, вызывающую баг.

Ключевой инсайт в том, что model checker контролирует scheduler. В продакшене вы во власти операционной системы. В model checker’е вы — операционная система. Вы можете приостановить thread перед выполнением критической строки, дать другому thread’у отработать весь метод, а затем возобновить первый. Вы можете исследовать interleaving, который в реальной жизни потребовал бы космического луча и сетевого сбоя для воспроизведения.

Race condition, которую model checker’ы ловят за миллисекунды

Вот классический баг: две goroutine инкрементируют shared counter.

package main

import (
	"fmt"
	"sync"
)

func main() {
	var counter int
	var wg sync.WaitGroup

	for i := 0; i < 2; i++ {
		wg.Add(1)
		go func() {
			defer wg.Done()
			// Read, increment, write: three steps
			val := counter
			val++
			counter = val
		}()
	}

	wg.Wait()
	fmt.Println(counter) // Expected 2, often prints 1
}

Запустите это тысячу раз — и каждый раз может вывести 2. Scheduler не становится вашим врагом по первому требованию. Но model checker видит трёхшаговую последовательность read-increment-write и знает: если goroutine A читает 0, затем goroutine B читает 0, потом обе инкрементируют и пишут 1, counter окажется равен 1 вместо 2.

Ему не нужно работать днями. Нужно исследовать два branch’а.

Как делать model checking собственного кода

Вам не нужно формально верифицировать всю codebase, чтобы извлечь пользу из model checking. Большинство команд получают 80% выгоды, моделируя те 20% кода, где concurrency действительно имеет значение.

Workflow выглядит так:

  1. Изолируйте конкурентный компонент. Выпилите HTTP handler’ы, запросы к базе данных и логирование. Сконцентрируйтесь на state machine: какие thread’ы или goroutine существуют, какой shared state они трогают и какие примитивы синхронизации используют?

  2. Напишите абстрактную модель. Замените реальные структуры данных упрощёнными версиями, захватывающими поведение, которое вас интересует. Если вы проверяете job queue, вам не нужен реальный job payload. Нужны queue, worker’ы и флаг, показывающий, выполняется ли job.

  3. Определите свойства, которые должны сохраняться. Это ваши invariant’ы. «Два worker’а никогда не обрабатывают один job.» «Job никогда не теряется.» «Cache и база данных никогда не расходятся.»

  4. Запустите model checker. Он либо скажет «все invariant’ы соблюдены», либо выдаст counterexample trace.

Вот как выглядит минимальная модель на Python с простым explicit-state checker’ом:

from collections import namedtuple

# Abstract model of a counter with two threads
State = namedtuple('State', ['counter', 'pc1', 'pc2'])

def successors(state):
    """Return all states reachable in one step."""
    results = []
    c, pc1, pc2 = state

    # Thread 1: three-step increment
    if pc1 == 0:
        results.append(State(c, 1, pc2))      # read
    elif pc1 == 1:
        results.append(State(c, 2, pc2))      # increment
    elif pc1 == 2:
        results.append(State(c + 1, 3, pc2))  # write

    # Thread 2: three-step increment
    if pc2 == 0:
        results.append(State(c, pc1, 1))
    elif pc2 == 1:
        results.append(State(c, pc1, 2))
    elif pc2 == 2:
        results.append(State(c + 1, pc1, 3))

    return results

def check():
    initial = State(0, 0, 0)
    visited = set()
    stack = [initial]

    while stack:
        state = stack.pop()
        if state in visited:
            continue
        visited.add(state)

        # Invariant: if both threads finished, counter must be 2
        if state.pc1 == 3 and state.pc2 == 3 and state.counter != 2:
            print(f"BUG: counter={state.counter}")
            return

        stack.extend(successors(state))

    print("No race condition found in model.")

check()

Это не production-grade. Это двадцать строк Python, демонстрирующих идею. Настоящий model checker вроде TLA+, Spin или mCRL2 обрабатывает дедупликацию состояний, свойства темпоральной логики и partial-order reduction, так что вы можете проверять системы с миллионами состояний. Но ментальная модель та же: закодируйте систему, сформулируйте invariant’ы, исследуйте.

Подвох: взрыв пространства состояний

Model checking не бесплатен. Если у вас четыре thread’а, каждый с десятью возможными следующими шагами, ваш граф состояний растёт экспоненциально. Добавьте 64-битное целое — и пространство состояний становится буквально непроверяемым.

Решение — абстракция. Вы не моделируете реальный cache. Вы моделируете «в cache есть key» или «в cache нет key». Вы не моделируете реальную базу данных. Вы моделируете «committed» или «uncommitted».

Вот здесь люди спотыкаются. Они пытаются сделать model checking реального кода, и checker работает вечно. Потом они полностью отказываются от model checking — что всё равно что отказаться от unit test’ов, потому что вы попытались протестировать всё приложение в одном test case’е.

Дисциплина такова: моделируйте concurrency, а не business logic. Если ваша race condition зависит от точного значения user ID, вы уже проиграли. Race conditions случаются из-за interleaving, а не из-за значений данных.

Инструменты, которые реально работают

Если хотите начать делать model checking реального кода — у вас есть варианты.

Для Go: gosim позволяет запускать Go-программы с детерминированным scheduler’ом, которым вы управляете из model checker’а. Он найдёт interleaving, ломающий ваши предположения о sync.Mutex.

Для Rust: shuttle — детерминированный фреймворк для тестирования конкурентности от AWS Labs. Он запускает ваш async-код тысячи раз с разными выборами scheduler’а и находит races, которые loom (другой отличный инструмент) проверяет на уровне memory model.

Для распределённых систем: TLA+ — промышленный выбор. Amazon использовал его для поиска багов в DynamoDB и S3 до релиза. Кривая обучения реальна, но return on investment для критических систем измерим.

Для мягкого старта: Напишите Python-скрипт как выше. Это займёт час, найдёт баги и выстроит интуицию, из-за которой TLA+ станет менее загадочным, когда он понадобится.

Что это не заменяет

Model checking находит logic errors в конкурентном коде. Он не находит performance regressions, memory leaks или баги, проявляющиеся только под продакшен-нагрузкой. Он не скажет, что contention на mutex взлетает при 10 000 requests в секунду.

Используйте его вместе со stress testing, а не вместо него. Stress testing говорит, выживает ли система под нагрузкой. Model checking говорит, выживает ли система при interleaving’ах, которые эта нагрузка создаёт.

С чего начать

Выберите один конкурентный компонент, который уже кусал вас раньше. Job queue, connection pool, rate limiter. Запишите invariant’ы на plain English. Потом потратьте послеобеденное время на постройку крошечной модели.

Вы, скорее всего, найдёте баг, существование которого не подозревали. Или обретёте уверенность, что баг, которого вы боялись, произойти не может. Любой из этих результатов стоит больше, чем ещё одна неделя наблюдения за продакшен-графиками в надежде.

Если вам нужен конкретный следующий шаг — туториал Learn TLA+ выведет вас с нуля до проверки распределённого протокола консенсуса за выходные. Для Go и Rust добавьте shuttle или loom в свою test suite и гоняйте в CI. В первый раз, когда он поймает race до code review, вы удивитесь, почему когда-либо доверяли scheduler’у делать ваше тестирование за вас.