Применение TLA+ для эффективного тестирования распределенных систем

Распределенные системы очень сложно разрабатывать. Даже если агентов всего несколько, число различных состояний системы может превышать тысячи, а то и миллионы. На таких масштабах привычные методы тестирования бессмысленны, а число корнер-кейсов, которые могут возникнуть в случае некорректной реализации системы, вполне способно выйти за практические рамки.

В докладе подробнее изучим проблему разработки и тестирования распределенных систем, рассмотрим язык спецификации TLA+ и его применение для верификации программ. Дополнительно опишем метод тестирования распределенных систем, построенных на акторной модели, совмещающий в себе плюсы и фаззинга, и TLA+.

В качестве примера рассмотрим систему распределенной координации Барсик, которая активно разрабатывается ВКонтакте и основана на алгоритме репликации данных Viewstamped Replication.