Fork

Stateful model checker для многопоточных тестов на С++.

Чекер посещает все состояния, достижимые при исполнении многопоточного теста, и проверяет в них заданные пользователем инварианты.

При нарушении инварианта model checker печатает кратчайшую детализированную траекторию, которая приводит к его нарушению.

Автор – Мария Феофанова!!missing!!.

Принцип работы

Чекер перехватывает обращения к примитивам синхронизации (мьютексам, условным переменным, атомикам и т.д.), останавливает исполнение (с помощью переключения контекста), делает снимок текущего состояния (стеки потоков, куча) и порождает все возможные продолжения ("ветвит" исполнение).

Ограничения

• Подходит для проверки изолированных примитивов синхронизации или базовых инфраструктурных компонент, но не подходит для больших программ.
• Проверяет только выполнение инвариантов (см. FORK_ASSERT). Liveness свойства не поддерживаются.
• Исполнение ветвится только в точках обращения к примитивам синхронизации / атомикам.
• Моделируются только последовательно согласованные исполнения (memory_order::seq_cst), не поддерживаются слабые модели памяти.

Поддержка стандартной библиотеки

• mutex
• condition_variable
• atomic
• thread
• this_thread::yield, this_thread::get_id

TODO

• thread_local

Links

• Презентация (коротко)
• Диплом (подробно)

Prerequisites

OS: Linux

Libraries: binutils-dev

Как запускать тесты

Чекер можно запустить в одном из двух режимов - Explore и Trace.

Режим Explore

В режиме по умолчанию чекер исследует все возможные состояния, достижимые при исполнении теста.

Запустите цель теста в Debug / Release сборке.

Режим Trace

В режиме Trace чекер воспроизводит и печатает приводящую к нарушению инварианта траекторию, найденную ранее в режиме Explore.

Запустите ту же цель в Debug сборке с флагом -DFORK_TRACE=1.

Как писать тесты

• Тело теста писать внутри макроса FORK_TEST
• Для thread, mutex, condvar, atomic заменить namespace std на fork::stdlike

Инструменты чекера

Инструменты Explore

Инварианты

Локальный инвариант:

// Где-то в коде теста
std::optional<int> value = lf_stack.TryPop();
FORK_ASSERT(value, "Empty stack");

Глобальный инвариант:

// См. пример DieHard
fork::GetChecker()
      .AddInvariant([&]() -> std::tuple<bool, std::string> {
        return {big != kWant, "Puzzle solved"};
      });

Ветвления

Fork() – создает точку ветвления.

ForkGuarded<T> – декоратор, отключающий форки на время вызова методов объекта T.

// Верим в его корректность
fork::ForkGuarded<LFStack<int>> stack;
// Теперь каждый отдельный `Push` / `TryPop` – атомарен для чекера
stack->Push(1);
stack->Push(2);

FORK_ATOMICALLY – отключает форки в заданном блоке кода:

// Для чекера такой блок - одна точка ветвления и
// одна атомарная операция
FORK_ATOMICALLY {
  // Опасно: операции над разными атомиками!
  if (a.load() == 7) {
    b.store(3);
  }
};

Рандомизация

Рандомизация – еще один способ ветвить исполнение.

// Чекер посетит обе ветки!
if (fork::Either()) {
  lock.Lock();
  // <- Critical section
  lock.Unlock();
} else {
  if (lock.TryLock()) {
    // <- Critical section
    lock.Unlock();
  }
}

size_t RandomNumber(size_t max) – обобщение Either. Генерирует "случайное число" от 0 до max включительно и создает max + 1 развилку – по одной на каждый возможный результат RandomNumber.

size_t RandomNumber(size_t lo, size_t hi) – аналогично.

LFStack<int> stack;
int pushes = fork::RandomNumber(1, 3);
// 3 продолжения: 1/2/3 вставки в стек
for (size_t i = 0; i < pushes; ++i) {
  stack.Push(i);
}

Рандомизация используется самим чекером для реализации очередей ожидания в мьютексах и условных переменных.

Pruning

TODO

Инструменты Trace

FORK_NOTE(context, message) – заметка о событии при исполнении для детализации трейса.

ShowLocalState() / ShowState() – показать в трейсе локальное / разделямое состояние в текущий момент времени.

PrintState

Позволяет печатать текущее разделяемое состояние в режиме Trace:

// В начале теста
fork::GetChecker()
  .PrintState(
  [&lock, &in_critical_section]() {
    trace::StateDescription d{"SharedState"};
    d.Add("TicketLock", lock);
    d.Add("in_critical_section", in_critical_section);
    return d;
  });

В Add поддерживаются

• целочисленные типы
• std::string
• atomic

Для поддержки пользовательских типов нужно либо написать для них метод DescribeState(), либо воспользоваться макросом FORK_DESCRIBE:

class TicketLock {
 public:
  void Lock();
  void Unlock();
  
  FORK_DESCRIBE(next_free_ticket_, owner_ticket_);
  
 private:
  atomic<size_t> next_free_ticket_{0};
  atomic<size_t> owner_ticket_{0};
};