Привет! Сегодня мы будем говорить про многопоточность и расскажем про инструмент Lincheck, один из ключевых проектов Лаборатории параллельных вычислений в JetBrains Research. Если в двух словах, то это фреймворк для тестирования многопоточных структур данных под JVM, предоставляющий возможность декларативного написания тестов. Что это значит? Как правило, при написании тестов мы пишем саму логику тестирования. С Lincheck-ом же все иначе — вместо указания того, как тестировать, вы объявляете операции, которые необходимо проверить, критерий корректности (например, линеаризуемость) и возможные ограничения (например, "single-consumer" для очередей) — то есть указываете что тестировать. А дальше Lincheck уже сам со всем разберется. В этом посте мы сделаем краткий обзор Lincheck-а и расскажем про режим model checking, который мы недавно зарелизили и который уже спас нам десятки часов отладки ошибок в алгоритмах.
Обзор Lincheck
Для начала возьмем какой-нибудь простой многопоточный алгоритм, например, алгоритм стека Trieber-а (см. код ниже). В дополнение к стандартным операциям push(value) и pop() мы также добавим нелинеаризуемый (а, следовательно, некорректный) size() — он увеличивается и уменьшается после успешных вызовов push и pop.
class Stack<T>
private val top = atomic<Node<T>?>(null)
private val size = atomic(0)
fun push(value: T): Unit = top.loop { cur ->
val newTop = Node(cur, value)
if (top.compareAndSet(cur, newTop)) { // try to add
size.incrementAndGet() // <-- INCREMENT SIZE
return
}
}
fun pop(): T? = top.loop { cur ->
if (cur == null) return null // is stack empty?
if (top.compareAndSet(cur, cur.next)) { // try to retrieve
_size.decrementAndGet() // <-- DECREMENT SIZE
return cur.value
}
}
val size: Int get() = _size.value
}
class Node<T>(val next: Node<T>?, val value: T)Теперь давайте напишем многопоточный тест для этого стека. Без какого-либо инструмента нам потребуется вручную запускать несколько параллельных потоков, вызывая в них операции над нашим стеком, а затем каким-то образом проверять наличие последовательной истории, которая объяснит полученные результаты. Раньше мы писали такие тесты руками — все они содержали не менее сотни строк шаблонного кода в лучшем случае. Однако с Lincheck этот механизм автоматизирован и тест становится действительно коротким и информативным — взгляните на код ниже!
@StressCTest
@ModelCheckingCTest
class StackTest {
private val s = TrieberStack<Int>()
@Operation fun push(value: Int) = s.push(value)
@Operation fun pop() = s.pop()
@Operation fun size() = s.size
@Test fun runTest() = LinChecker.check(this::class)
}Чтобы написать многопоточный тест с помощью Lincheck, нам необходимо только лишь перечислить операции над структурой данных и пометить их специальной аннотацией @Operation, начальное же состояние указывается в конструкторе (здесь мы создаем новый инстанс TriebeStack<Int>). После этого нам необходимо настроить режимы тестирования, что можно сделать при помощи специальных аннотаций на тестовом классе - @StressCTest для стресс-тестирования и @ModelCheckingCTest для режима model checking. Наконец, мы можем запустить сам анализ, вызвав функцию Linchecker.check(..).
Давайте посмотрим на этот тест снова – всего 12 строк довольно простого кода, который описывает, каким должен быть наш стек – это все, что нужно сделать, имея Lincheck! В результате, он автоматически:
генерирует несколько случайных параллельных сценариев,
проверяет каждый из них при помощи стресс-тестирования или model checking-а, исследуя сценарий столько раз, сколько задано пользователем,
проверяет, что полученные результаты удовлетворяют необходимому свойству корректности (например, линеаризуемости) — на этом этапе мы используем последовательную спецификацию, которая по умолчанию определяется структурой данных для тестирования, но также может быть отдельно написана и задана пользователем (см. параметр
sequentialSpecification).
Если вызов зависает или падает с исключением, или же результат некорректен, то тест завершается с ошибкой, аналогичной приведенной ниже. Здесь мы подошли к главному преимуществу режима model checking. Хотя Lincheck всегда предоставляет неудачный сценарий с некорректными результатами (если таковые обнаружены), при использовании model checking-а он также предоставляет трассу исполнения для воспроизведения ошибки. Обнаруженное неудачное исполнение начинается с первого потока, кладет 7 в стек и останавливается, прежде чем увеличить size. После этого выполнение переключается на второй поток, который извлекает из стека уже помещенное туда 7 и уменьшает размер до -1. Следующий вызов size() возвращает -1, что очевидно некорректно. Хотя данная ошибка кажется понятной даже без трассы, последняя очень помогает при работе с реальными параллельными алгоритмами, такими как примитивы синхронизации в Kotlin Coroutines.
= Invalid execution results =
| push(7): void | pop(): 7 |
| | size(): -1 |
= The following interleaving leads to the error =
| push(7) | |
| top.READ: null | |
| at Stack.push(Stack.kt:5) | |
| top.compareAndSet(null,Node@1): true | |
| at Stack.push(Stack.kt:7) | |
| switch | |
| | pop(): 7 |
| | size(): -1 |
| | thread is finished |
| _size.incrementAndGet(): 0 | |
| at Stack.push(Stack.kt:8) | |
| result: void | |
| thread is finished | |Генерация сценариев
В Lincheck мы указываем количество параллельных потоков и операций в них (можно настроить в аннотациях <Mode>CTest), и он генерирует указанное в этой же конфигурации количество сценариев, заполняя потоки случайно выбранными операциями. Обратите внимание, что операция push(..) в приведенном выше стеке принимает значение типа Int, которое нужно положить в стек. В то же время, сообщение об ошибке содержит конкретный сценарий со входным значением для вызова push(..)— этот параметр также генерируется случайным образом из указанного диапазона (его можно настроить или даже использовать свой генератор). Еще можно добавить ограничения, такие как «single-consumer», чтобы соответствующие операции не могли быть запущены параллельно — это очень важно для многих практических алгоритмов.
Режимы тестирования
Lincheck запускает сгенерированный сценарий либо в режиме стресс-тестирования, либо в режиме model checking. В режиме стресс-тестирования сценарий много-много раз выполняется в параллельных потоках с надеждой получить неверный результат и, таким образом, найти ошибку (на это надеется Lincheck, программист же — на обратное). С другой стороны, model checking исследует множество различных исполнений с ограниченным числом переключений потоков. По сравнению со стресс-тестированием, такой режим предоставляет больше гарантий и трассу неудачного исполнения для обнаруженного некорректного поведения. Однако этот режим использует модель памяти с последовательной согласованностью, таким образом игнорируя эффекты слабых моделей памяти. В связи с этим, на практике мы используем как стресс-тестирование, так и model checking.
Минимизация неудачных сценариев
При написании теста имеет смысл сконфигурировать его так, чтобы выполнялось несколько потоков (лучше 3-4) с несколькими операциями в каждом (скажем, по 3-5 операций на поток). Однако большинство ошибок можно воспроизвести на меньшем количестве потоков и операций, что существенно упрощает понимание причины ошибки. Для этого Lincheck «минимизирует» неудачный сценарий, пытаясь удалить из него операцию и проверяя, продолжает ли тест падать — удаления повторяются до тех пор, пока это возможно.
Model Checking: подробности
Давайте немного углубимся в то, как устроен model checking в Lincheck-е. Надеюсь, до сих пор все было понятно, и если вы никогда раньше не использовали Lincheck, предлагаем написать пару тестов, чтобы попробовать его в деле — просто добавьте зависимость org.jetbrains.kotlinx:lincheck:2.12 в свой Gradle или Maven проект.
Основная причина, по которой мы стали работать над model checking-ом, вызвана нашей болью — довольно часто обнаруживается какая-то нетривиальная ошибка, и ты тратишь несколько часов, пытаясь выяснить, откуда же она взялась — прямо как на анимации ниже! Потратив все эти часы, мы решились вложиться в model checking с читабельным описанием трассы неудачного исполнения. Также, чтобы пользователям не приходилось думать о внутреннем механизме или менять свой код, все должно работать автоматически.
Как показывает наш опыт, большинство сложных параллельных алгоритмов либо используют sequentially consistent модель памяти, либо ошибки в их реализациях могут быть воспроизведены в ней и не требуют relaxed поведения. Поскольку подходы к проверке для слабых моделей памяти довольно сложны, мы решили использовать bounded model checking в рамках sequentially consistent модели памяти. Изначально идея такого bounded model checking-а была навеяна фреймворком CHESS для C# — он изучает все возможные исполнения с ограниченным числом переключений потоков, полностью контролируя исполнение и позволяя переключить контекст в различных местах. В отличие от CHESS, Lincheck ограничивает количество исполнений, которые необходимо изучить, а не количество переключений контекста — таким образом, время тестирования предсказуемо вне зависимости от размера сценария и сложности алгоритма.
Если кратко, Lincheck начинает с исследования всех исполнений, используя только одно переключение контекста, и делает это равномерно, пытаясь сначала рассмотреть совершенно разные исполнения. Таким образом, мы увеличиваем общее покрытие, если количество доступных вызовов недостаточно для того, чтобы изучить все исполнения с текущим количеством переключений. После того, как все исполнения с одним переключением потока рассмотрены, Lincheck начинает рассматривать исполнения с двумя переключениями и так далее, до тех пор, пока доступные вызовы не превысят максимум, или пока всевозможные исполнения с любым количеством переключений не будут исследованы. Эта стратегия помогает не только увеличить покрытие тестирования, но и найти некорректное исполнение с использованием наименьшего числа переключений, что особенно важно для дальнейшего исследования ошибки.
Точки переключения
Lincheck вставляет точки переключения в тестируемый код для того, чтобы получить возможность управления исполнением и переключением потоков. Куда вставляются эти точки переключения? Во-первых, это обращения к разделяемой памяти, такие как чтения и обновления полей и элементов массивов (напоминаем, что речь идет о JVM). Эти чтения и обновления могут выполняться либо соответствующими инструкциями байт-кода, либо специальными методами в AtomicFieldUpdater или Unsafe (весь реальный код написан именно так и не использует никакие j.u.c.AtomicReference). Чтобы вставить точку переключения, мы трансформируем байт-код с помощью фреймворка ASM и добавляем вызовы наших внутренних функций перед каждым обращением. Преобразование выполняется на лету с использованием своего ClassLoader-а. Таким образом, технически мы создаем трансформированную копию тестируемого кода.
Помимо обращений к разделяемой памяти, переключение контекста может произойти или даже принудительно выполниться при использовании блокировок или механизмов park/unpark и wait/notify. Мы заменяем все эти примитивы на свои реализации, которые сохраняют исходные контракты, но не блокируют поток. Поскольку синхронизация также может быть активной (например, spin-lock), Lincheck имеет механизм обнаружения активной блокировки — он запускается, когда одно и то же место в коде посещается слишком много раз.
Дерево исполнений
Чтобы исследовать различные возможные исполнения, Lincheck строит дерево этих исполнений, где ребра обозначают переключения, которые могут быть выполнены планировщиком — см. рисунок ниже с частично построенным деревом исполнений с одним переключением контекста для сценария со стеком из начала поста. Сначала Lincheck решает, с какого потока следует начать исполнение. После этого становятся доступны несколько точек переключения, которые необходимо изучить. На рисунке ниже полностью рассмотрена только первая точка переключения, относящаяся к top.READ.
Чтобы равномерно исследовать различные исполнения, Lincheck поддерживает процент рассмотренных исполнений для каждого поддерева, используя взвешенную вероятность для выбора точки переключения (веса пропорциональны долям неисследованных исполнений). В нашем примере более вероятно, что следующее исполнение начнется со второго потока. Поскольку точное число возможных исполнений неизвестно, изначально все поддеревья имеют одинаковый вес. После того, как все исполнения текущего дерева проанализированы, Lincheck увеличивает количество переключений контекста, тем самым увеличивая глубину дерева.
Трасса исполнения
Ключевым преимуществом model checking-а является то, что он предоставляет трассу исполнения — она показывает, как воспроизвести найденную ошибку. Чтобы повысить читаемость, Lincheck запоминает аргументы и результат каждого обращения к разделяемым переменным (например, чтение, запись или CAS) и вызовам функций. Например, в трассе ошибки с нашим стеком из начала посте первое событие — это чтение null из поля top; номер строки в исходном коде тоже указывается. В то же время, если функция выполняется без переключения контекста, Lincheck показывает вызов этой функции с соответствующими аргументами и результатом без кучи событий внутри нее — это также упрощает последующий анализ найденной ошибки (см. на второй поток).
Проверка гарантий прогресса
Исследуя все возможные точки переключения на текущем уровне, Lincheck пытается завершить текущий поток. Однако если тестируемый алгоритм является блокирующим, Lincheck может остановиться из-за синхронизации или бесконечного цикла. В то же время, такой ситуации никогда не возникнет при неблокирующей реализации, что позволяет легко обнаруживать блокирующее поведение.
Наиболее популярной гарантией прогресса является lock-freedom, которая обеспечивает прогресс во всей системе, в то время как конкретная операция может зависнуть. Однако при помощи описанного выше подхода мы можем проверить только чуть более слабую гарантию — obstruction-freedom — она гарантирует завершение операции за ограниченное число шагов, если все другие потоки остановлены, независимо от того, находятся ли операции в этих остановленных потоках в промежуточном состоянии или нет. Заметим, что именно это и проверяет Lincheck во время исследования новых точек переключения!
Ограничения
Единственное ограничение для model checking-а — это детерминированное поведение тестируемой структуры данных, которое гарантирует воспроизводимость исполнения. Однако некоторые алгоритмы используют случайные числа (Random) под капотом, поэтому мы в Lincheck заменяем стандартные объекты Random-а из Java и Kotlin на свои детерминированные реализации.
Немного рассуждений под конец
Надеемся, что вам понравилась статья и вы узнали для себя что-то новое и интересное. Одна из главных вещей, которую мы хотели продемонстрировать, — это то, что исходно академические подходы (например, model checking) могут успешно применяться в повседневном программировании и быть простыми в использовании. Не бойтесь академии и ученых!
Мы, в свою очередь, уже несколько лет успешно используем Lincheck как для тестирования своих алгоритмов в Kotlin Coroutines (см. сюда), так и для проверки домашних заданий в рамках курса по многопоточному программированию в Университете ИТМО. Надеемся, и для вас Lincheck станет незаменимым помощником при работе над многопоточными алгоритмами! Мы, в свою очередь, постараемся помочь всем и каждому, и сейчас работаем над мультиплатформенностью инструмента, что позволит тестировать алгоритмы не только на JVM, но и на нативных языках, таких как C/C++ или Swift