Телеграмм чат группы cloud

Отдельно хочу прокомментировать эту новость. TLA⁺ — это язык спецификации, основанный на темпоральной логике действий, что позволяет описывать и верифицировать корректность распределенных систем, моделируя их поведение во времени. Есть отличный доклад от команды Elasticsearch о том, как они с помощью модели на TLA⁺ нашли и исправили ошибку, которая воспроизводилась только в сложных высококонкурентных сценариях. Это уже не «фантазии академиков в башнях из слоновой кости», а самый что ни есть реальный, прагматичный и прикладной способ повышать надежность ПО.
В общем, если вы занимаетесь распределенными системами или системами реального времени, есть смысл поучаствовать. Кто знает, вдруг через какое-то время на месте ребят из Elastic будете именно вы рассказывать, как улучшили ваш проект с помощью методов формальной верификации 😉

YouTube

Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch

Elasticsearch is a distributed search and analytics engine based on Apache Lucene. Initially released in 2010, it has quickly become the most popular enterprise search engine, and is commonly used for log analytics, full-text search, operational and security intelligence, business analytics, and metrics use cases. Built as a distributed system since its inception, Elasticsearch effortlessly scales to clusters of hundreds of servers. As part of a larger resiliency effort, Elasticsearch’s core cluster coordination and data replication algorithms have undergone major overhauls in recent years. The use of formal methods, with in particular TLA + , PlusCal and the TLC model checker, has extensively contributed to the goal of creating a much safer and resilient system. This presentation will provide an overview on the various uses of TLA + during the development of Elasticsearch:

We refined and validated an informal specification of the data replication algorithm that has been powering Elasticsearch since version…