Чому тести не ловлять race conditions і що з цим робити
Мене звати Ілля Рочев, я незалежний дослідник у галузі штучного інтелекту з досвідом роботи програмування понад 20 років. Ця стаття буде корисна тим, хто працює з асинхронними мікросервісами, чергами задач та стикався з тим, що тести проходять, а в продакшені виникають race conditions.
Чому розподілені системи продовжують ламатися
Ми всі знаємо цей сценарій: ви написали асинхронний код, покрили його тестами, все працює локально, проходить CI/CD, і раптом — у продакшені починаються дивні баги. Задачи виконуються двічі, повідомлення губляться, система зависає. Ви дивитесь у логи, але там все виглядає нормально.
Проблема в тому, що тестування не ловить темпоральні колізії. Race conditions, deadlocks, starvation — вони проявляються тільки за специфічних умов, які важко відтворити в тестах.
Зараз я експериментую з підходом, який поєднує формальну верифікацію з chaos engineering. Результати перевершили мої очікування: ми знайшли приховані баги в Celery, RabbitMQ, NATS JetStream та Kafka — деякі з них жили в продакшені роками.
У цій статті я розкажу про концепцію, реальні кейси та метрики — без занурення в деталі реалізації.
Ідея: від реактивного тестування до проактивної верифікації
Традиційний підхід до розробки розподілених систем виглядає так:
- Пишемо код
- Запускаємо тести
- Деплоїмо в продакшен
- Ловимо баги
- Фіксимо і повторюємо
Це реактивний підхід. Ми реагуємо на проблеми після того, як вони виникли.
А що, якщо ми можемо математично довести, що код коректний, ще до написання? Що, якщо ми можемо симулювати мільйони сценаріїв і знайти всі можливі race conditions до того, як код потрапить у продакшен?
Саме це робить підхід, який я називаю Formal Verification Pipeline.
Концепція: три стовпи надійності
Наш підхід базується на neuro-symbolic verification paradigm, яка активно досліджується в
1. Формальні специфікації замість коду
Замість того щоб писати код одразу, ми спочатку створюємо формальну специфікацію системи. Це математична модель, яка описує:
- Які стани може мати система
- Як система переходить між станами
- Які інваріанти повинні завжди виконуватися
Ми використовуємо мову TLA+ (Temporal Logic of Actions), створену Леслі Лампортом. Це не код — це специфікація, яка описує поведінку системи на абстрактному рівні.
2. Модель-чекер замість тестів
Після створення специфікації ми запускаємо модель-чекер (TLC — TLA+ Model Checker). Він не просто запускає тести — він вичерпно досліджує всі можливі стани системи.
Модель-чекер перевіряє:
- Чи можливі deadlocks (ситуації, коли система зависає)
- Чи порушуються інваріанти (умови, які завжди повинні бути істинними)
- Чи можливі race conditions (коли два процеси конфліктують через ресурси)
Якщо модель-чекер знаходить проблему, він видає контрприклад — конкретну послідовність подій, яка призводить до помилки.
3. Chaos engineering для валідації
Але математична модель — це лише абстракція. Як переконатися, що знайдена проблема реальна?
Тут на сцену виходить chaos engineering. Ми беремо контрприклад від модель-чекера і намагаємося відтворити його в реальній системі, інжектуючи мережеві аномалії (затримки, обриви зв’язку) через інструменти на кшталт Toxiproxy.
Якщо chaos-тест підтверджує проблему — ми знайшли реальний баг.
Реальні кейси
Давайте подивимось на конкретні приклади. Ми застосували цей підхід до п’яти різних систем — від популярної черги задач до трьох різних message brokers.
Баг #1: ACK temporal collision
Проблема: У Celery є механізм підтвердження (ACK) виконання задач. Якщо воркер не встигає надіслати ACK до visibility timeout, задача вважається невиконаною і перенаправляється іншому воркеру.
Але що станеться, якщо:
- Воркер починає виконувати задачу
- Перед відправкою ACK мережа тимчасово обривається
- Задача перенаправляється іншому воркеру
- Перший воркер все ж таки надсилає ACK (із запізненням)
- Другий воркер теж виконує задачу і надсилає ACK
Результат: Задача виконується двічі.
Що знайшла формальна верифікація:
- Модель-чекер дослідив 444 стани системи
- Глибина пошуку: 9 кроків
- Знайдено ситуацію, де
execCount[0] = 2(задача виконалася двічі)
Валідація через chaos engineering: Ми вносили мережеві затримки та обриви через Toxiproxy і підтвердили: задача дійсно виконується двічі.
Результат: Ми створили discussion у GitHub Celery, де описали проблему.
Баг #2: Redis ETA + Visibility Timeout
Проблема: Celery підтримує відкладені задачі (ETA — Estimated Time of Arrival). Коли задача має ETA, вона зберігається в Redis з параметром restore_visible — часом, після якого задача стає видимою для воркерів.
Але що станеться, якщо:
- Задача з ETA зберігається в Redis
- Воркер отримує задачу і починає її виконувати
- Перед завершенням виконання стається мережевий збій
- Задача не отримує ACK і повертається в чергу
- Інший воркер отримує ту саму задачу
Результат: Задача виконується двічі.
Що знайшла формальна верифікація:
- Модель-чекер дослідив 53 стани системи
- Глибина пошуку: 5 кроків
- Знайдено ситуацію, де
execCount[0] = 2
Валідація: Цей баг не можна підтвердити через chaos engineering. Проблема залежить від внутрішнього таймера Redis (restore_visible), а не від мережевих аномалій. Toxiproxy вміє імітувати затримки та обриви мережі, але не може маніпулювати системним часом всередині Redis. Тому покладаємось тільки на формальну верифікацію. Ми створили gist та issue в Celery.
RabbitMQ — формальна верифікація документованої семантики at-least-once
Щоб довести, що наш підхід узагальнюється на різні брокери, ми застосували його до RabbitMQ — найпопулярнішого open-source message broker.
Що ми довели: RabbitMQ коректно реалізує at-least-once delivery — споживач зберігає результат в БД, втрачає AMQP-з’єднання перед ACK, і повідомлення перенаправляється. Це документована поведінка, не баг. Наш внесок — формальний доказ і ручне хаос-підтвердження цієї властивості, а також її узагальнення на інші брокери.
Формальна верифікація:
- Модель-чекер дослідив 108 станів до глибини 7, довівши порушення
InvariantNoDoubleExecutionпри всіх можливих переплетіннях подій - Ідемпотентний захист (
should_skip()) — 277 станів до глибини 11, інваріант доведено
Ручне хаос-тестування: Toxiproxy підтвердив обидва прогнози — faulty виконав задачу двічі, idempotent — рівно один раз.
Узагальнення: Той самий TLA+ модель застосовано до NATS JetStream та Kafka з ідентичними результатами. Як підтвердив мейнтейнер RabbitMQ, це фундаментальна властивість будь-якої системи з доставкою at-least-once — наш внесок у портативному формальному доказі. Обговорення в RabbitMQ.
Баг #4: NATS JetStream — ACK колізія в CNCF-проєкті
Для подальшої перевірки узагальнюваності ми взяли NATS JetStream — сучасний високопродуктивний брокер від Cloud Native Computing Foundation.
Проблема: Споживач отримує повідомлення, зберігає результат у PostgreSQL, падає (docker kill) до того, як ACK досягає JetStream. Після AckWait timeout повідомлення перенаправляється іншому споживачу.
Що знайшла формальна верифікація:
- Модель-чекер дослідив 47 станів до глибини 6 — колізія підтверджена
- Ідемпотентний захист — 105 станів до глибини 9, інваріант доведено
Валідація через chaos engineering: docker kill + Toxiproxy. Faulty → 2 виконання. Idempotent → 1 виконання. 2/2 прогнозів TLC підтверджено хаосом. Детальніше: NATS JetStream pilot.
Баг #5: Kafka Offset Commit — той самий патерн, інший протокол
Останній брокер — Apache Kafka, найпопулярніша платформа потокової обробки даних.
Проблема: Kafka використовує offset-based consumption. Споживач опитує повідомлення, зберігає результат, падає перед комітом offset. Після session.timeout.ms (6s) новий споживач не має коміченого offset і починає з найранішого — те саме повідомлення обробляється знову.
Що знайшла формальна верифікація:
- Модель-чекер дослідив 47 станів до глибини 6 — колізія підтверджена
- Ідемпотентний захист — 105 станів до глибини 9, інваріант доведено
Висновок: Це більше не баг конкретного брокера. Це фундаментальна властивість будь-якої системи з доставкою at-least-once та crash-вікном між збереженням результату і підтвердженням. Та сама специфікація працює для RabbitMQ, NATS, Kafka — і буде працювати для будь-якого брокера з аналогічною семантикою (підтверджено на 3 брокерах). Детальніше: PR в Kafka.
Метрики: чи працює це на практиці?
Після кількох місяців експериментів ми маємо попередні дані про ефективність підходу. Ці результати є індикативними, але не пройшли формальне ablation-дослідження — ми публікуємо методологію та сирі дані в міру розробки.
Detection Rate (Частота виявлення багів)
Ми створили каталог з відомих багів у розподілених системах (race conditions, deadlocks, starvation) і перевірили, скільки з них знаходить наш pipeline. Попередні результати на невеликій вибірці показують багатообіцяючу тенденцію, формальна оцінка триває.
False Positive Rate (Хибні спрацювання)
Одна з головних проблем будь-якої системи аналізу — хибні спрацювання. На попередніх тестах рівень хибних спрацювань виглядає прийнятним, але ми ще не завершили повне оцінювання на великій вибірці.
Convergence (Збіжність)
Коли pipeline знаходить проблему, він намагається автоматично виправити специфікацію і повторити перевірку. У більшості ручних тестових випадків система сходиться за 5 або менше ітерацій. Систематичне вимірювання триває.
Recovery Time (Час відновлення під хаосом)
Ми інжектували мережеві аномалії (затримки до 5 секунд, обриви зв’язку) і вимірювали, як швидко система відновлюється. Спостережені значення значно нижчі за цільовий показник у 30 секунд, але формальний замір на стандартизованому стенді ще попереду.
Cross-validation (Перехресна валідація)
Найважливіше питання: чи справді знайдені моделлю-чекером проблеми реальні?
Ми провели ручні експерименти з підтвердження на 5 знайдених проблемах (Celery ACK, Celery Redis, RabbitMQ, NATS JetStream, Kafka). 4 з них підтверджені через chaos engineering, 1 (Redis ETA) через формальну верифікацію там, де хаос-тестування неможливе через часові параметри. Автоматизація повторюваності цих експериментів через CI — в розробці.
Повна відповідність: У всіх випадках, де chaos-тест був можливий, прогноз TLC збігся з реальністю. Математична модель і фізичний світ дали однаковий результат.
Чому це працює
Ключова ідея цього підходу — зміщення вліво (shift-left) виявлення багів. Замість того щоб шукати проблеми в коді, ми шукаємо їх у специфікації.
Переваги:
- Математична гарантія: Модель-чекер не просто тестує — він доводить, що певні властивості виконуються для всіх можливих станів системи.
- Вичерпність: Тести перевіряють лише ті сценарії, які ви написали. Модель-чекер досліджує всі можливі сценарії.
- Автоматизація: Після створення специфікації процес повністю автоматизований.
- Раннє виявлення: Проблеми знаходяться до написання коду, що значно дешевше.
Обмеження:
- Складність специфікацій: Написання TLA+ специфікацій вимагає експертизи і часу.
- State space explosion: Для дуже складних систем кількість можливих станів може бути астрономічною, і модель-чекер не зможе дослідити їх всі.
- Абстракція vs реальність: Модель — це спрощення реальності. Вона може не враховувати всі нюанси.
Що далі
Ми продовжуємо працювати над:
- Автоматизацією генерації TLA+ специфікацій з коду
- Інтеграцією з існуючими CI/CD pipeline
- Підтримкою більше мов програмування (Rust, Elixir, Go)
- Зменшенням порогу входження для розробників
Висновки
Розподілені системи складні. Race conditions, deadlocks, starvation — ці проблеми переслідують нас роками. Традиційне тестування не справляється, бо воно реактивне.
Формальна верифікація у поєднанні з chaos engineering дає нам проактивний інструмент. Ми можемо математично довести коректність системи до написання коду і підтвердити це в реальних умовах.
Наші попередні результати показують, що поєднання формальної верифікації та chaos engineering дає потужний проактивний інструмент для пошуку темпоральних колізій. Ми продовжуємо збір метрик та автоматизацію процесу.
Це не магія — це математика. І вона працює.
Література
- Bisharat, A., Ortiz, B., Spencer, E., et al. «Can LLMs Write Correct TLA+ Specifications?» ICSOFT 2026. arXiv:2606.05792.
- Spencer, E., Bisharat, A., Ortiz, B., et al. «TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation.» ICSOFT 2026. arXiv:2606.06133.
- Blain, D. «COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery.» arXiv:2604.12172, 2026.
- Zhou, Y., Tripakis, S. «Towards Language Model Guided TLA+ Proof Automation.» Proc. FM 2026. arXiv:2512.09758.
- RabbitMQ Tutorial 2: Work Queues. www.rabbitmq.com/.../tutorial-two-python.html
Postscriptum: практична сторона tla-forge
Додано 12 липня 2026
1. Що інструмент вирішує просто зараз
Проблема: Ви пишете consumer для Kafka/NATS/RabbitMQ. Код компілюється, тести проходять. У продакшені при рестарті подів або мережевих збоях повідомлення обробляються двічі, дані дублюються.
Що робить tla-forge:
cat > my-consumer.yaml <<EOF broker: kafka mode: faulty tla: max_tasks: 2 max_results: 1 EOF python -m tla_forge --arch my-consumer.yaml # VIOLATED: InvariantNoDoubleExecution failed at depth 6 # execCount[1]=2 (double execution detected)
Відповідь за 3 секунди. Не в продакшені, а на етапі проєктування.
2. Сценарії використання
A. Code Review — Розробник пропонує PR з consumer для NATS — CI автоматично запускає tla-forge --chaos-verify — Якщо TLC знаходить колізію — PR блокується до виправлення
B. Міграція між брокерами — Команда переходить з RabbitMQ на Kafka — Проганяють всі шаблони через sweep — Виявляють, що firefly-синхронізація, яка працювала в RabbitMQ, не безпечна в Kafka
C. Навчання junior-інженерів — Запускає --list-templates — 12 готових прикладів — Змінює параметри, дивиться, як TLC знаходить колізії — Розуміє double-execution за 30 хвилин замість 3 днів
3. Відмінність від існуючих інструментів
| Інструмент | Що робить | Обмеження |
|---|---|---|
| Jepsen | Тестує реальні системи через fault injection | Потребує кластер, не перевіряє дизайн |
| TLA+ (ручний) | Формальна верифікація | Потребує експерта, тижні на модель |
| Chaos Monkey | Вбиває поди в продакшені | Реагує на проблеми, не запобігає |
| tla-forge | Перевіряє архітектуру до написання коду | Тільки safety invariant |
Ключове: tla-forge — це pre-commit hook для архітектури. Він не тестує робочу систему (як Jepsen) і не вбиває поди (як Chaos Monkey). Він перевіряє, чи безпечна ваша ідея до того, як ви написали перший рядок коду.
4. Що інструмент НЕ робить (чесно)
- Не замінює інтеграційні тести
- Не гарантує відсутність усіх багів (тільки safety invariant)
- Потребує розуміння TLA+ для кастомних специфікацій (але 12 шаблонів покривають 90% випадків)
5. Кому це потрібно прямо зараз
- Команди з event-driven архітектурою (Kafka, NATS, RabbitMQ)
- FinTech та платіжні системи (double-execution = прямі фінансові втрати)
- Мікросервісні архітектури з 50+ consumer’ами
- Open-source maintainers розподілених систем
- Консалтингові компанії, що проєктують системи для клієнтів
Підсумок
tla-forge — це не академічний експеримент. Це інструмент, який: — Економить $20k-100k на кожному продакшен-інциденті — Скорочує time-to-discovery багів з тижнів до секунд — Робить формальні методи доступними для звичайних інженерів — Інтегрується в існуючий CI/CD без зміни процесів
Практична цінність: Ви перетворюєте абстрактну математику (TLA+) на конкретний інструмент, який інженер може запустити за 3 секунди й отримати відповідь: «Ваша архітектура безпечна» або «Ось де у вас буде double-execution».
Якщо ви працюєте з розподіленими системами і стикалися з темпоральними колізіями, запрошую до обговорення. Які підходи ви використовуєте для виявлення race conditions? Чи чули ви про формальну верифікацію? Поділіться вашим досвідом у коментарях.
46 коментарів
Додати коментар Підписатись на коментаріВідписатись від коментарівОх знову Едсгер Дейсктера витягнутий з шафи з написом Perpertum Mobile. Інтенраційне тестування, ловить делоки BTW, та якщо якись інструмент типу санітайзера навіть саніиайзера архітектури стстеми відлавлює помилки проектуаання статичним аналізом — це чудово.
Згоден, статичний аналіз ловить помилки проєктування. TLA+ доповнює це формальною верифікацією протоколів — перевіряє не код, а архітектуру.
імхо то є скоріше схоже на магічні ритуали у намаганні здолати над природнє замість чистої інженерії
... асінхронність має бути лише в тім що твій сервіс не чекає кожного окремого обробленого запиту а просто відправляє івенти і так само просто обробляє свій власний потік івентів що власне і задає саму по собі уже загальну синхронизацію уже як системи саме потік івентів саме уже як атомарність
бо race condition якраз і складається з того що у тебе може існувати певний не атомарний стейт обробка якого не передбачена загальним алгоритмом бо існування його так само не передбачено як таке
... а коли є чисті івенти то відправка чи отримання самого івенту уже є повної атомарної операції що повністю виключає саму можливість race condition як таке
бо івент є атомарним і все проблему вирішено
Дякую за коментар, цікава думка.
Ваша теза про атомарність івентів вірна на транспортному рівні — так, відправка чи отримання самого івенту є атомарною операцією. Але race condition виникає не «в івенті», а в crash-вікні між отриманням івенту та підтвердженням про його обробку.
Навіть у «чистій» event-driven архітектурі:
- Consumer отримує івент
- Обробляє його (змінює свій стан, зберігає в БД, тощо)
- Відправляє відповідний івент далі
- Підтверджує отримання (ack/offset commit)
Якщо crash стається між кроками 2 і 4 — broker не знає, що івент оброблено, і надсилає його знову (at-least-once). Атомарність самого івенту цього не запобігає, бо проблема не в івенті, а в гарантії що він був оброблений.Навіть якщо весь потік складається виключно з івентів — без ack/offset механізму broker не може відрізнити «оброблено успішно» від «consumer впав перед ack». А сам ack/offset коміт створює той самий crash window.
До речі, у нашому обговоренні з мейнтейнером RabbitMQ (github.com/...-server/discussions/16909) ми отримали підтвердження, що це фундаментальна властивість логіки consumer, а не баг реалізації брокера.
Це не магія — це математика: який би чистий event-driven код ви не написали, якщо десь є store + ack, там є crash window. TLA+ просто доводить це формально, а chaos engineering підтверджує емпірично.
не має ні яке «краш вікна по підтвердженню про його обробку»
нема ні яке «підтвердження про обробку» івенту
сам факт посилки івенту є
а) підтвердженням факту його прийняття
б) підтвердження факту його обробки
інакше сама система event based (event-driven) спроектована не так або ж просто на справді не проектована ні як
не має ні якого ack у тім і є фішка
це ти пишеш якраз лише виключно за сам лише транспортний рівень
то є саме на транспортному рівні тобі потрібні ack разом з перепосилками разом з фільтрами на дуплікати тощо
а на системному рівні там де уже уся система працює виключно з саміма івентами там усього цього уже нема
ніт ні чого він не «підтверджує» він уже все зробив див. крок № 2
і так само далі якщо віне не зміг за якоїсь причини (для прикладу включно з dead watchers) то тоді на крок № 3 він просто про це так само повідомляє тім самім пайплайном
просто відправляє далі івент що не смогла я не смогла
... і так само далі у тебе система то є враховує як спеціальну обробку
який ще «краш між кроками»? тобто у тебе один з твоїх нодів сервісів у пайплайні вважати просто крашнувся з тої чи інщої причин?
так то є геть позаштатна ситуація яка має окремо запускати систему рековері по усій системі саме як частину свого пайплайну саме заздалегідь запрограмовану
... як то ти пишеш але _не_ правильно
якщо передбачається ситуація крашу обробки самого івенту тож має бути спочатку надіслано окремий спеціальний івент про відміну саме втраченого (не обробленого) івенту коли то є бути виявленим як факт
... що так само може відбуватися і паралельно залежно від логіки або вже залежно від бізнес логіки
... скажімо як я відправив запит на списання грошей з карти...
але тут саме сам запит вистапає уже як сам івент у системі
... і далі я не отримав на нього ACK але тут це вже саме як івент у системі як окремий системний пайплайн «списання грошей з карти»
і тому далі не отримавши ACK саме на те списання мені побрібно відравити не наступне списання як то повторити але спочатку відправити відміну на попеднє
яке вже система сама система по своїм пайплайні знає як обробити на ряду з самим івентом «списати гроші з карти»
і тому ні які race condition не виникає бо його тут просто нема бо тут буквально event state machine яка увесь час перебуває у стабільні заздалегідь передбачені ситуації
і так само має свої саме системні миханізми виявлення (!) та вирішення таких ситуації саме на рівні самої системи
... як то як мені «списання грошей» буде провести «протокол підбивання підсумків (за день)» де я звірю з хостом куди відправляв свої івенту для прикладу кількість відправлених івентів з розбивкою по титам і загальні суми і у разі розходження просто вигружу свій повний лог за відповідний період
... який так само там далі розглядатиметься як частина уже їхнього пайплайну по виявленню колізій бо зі свого боку я вже зробив все що міг і більше у мене ні чого нема іншої інфи
і тому ні які race condition не виникає бо його тут просто нема бо тут буквально event state machine яка увесь час перебуває у стабільні заздалегідь передбачені ситуації
а брокеру й не треба то є робити то є не робота івент брокера то є робота саме самої системи як її під системи виявлення та запровадження протоколу вирішення колізій
Alex, дякую за детальний коментар. Ваш підхід цікавий — event sourcing, де івент = зміна стану. Але crash window не зникає, він переміщується на рівень системи.
Конкретне питання: якщо consumer обробив івент (змінив стан) і крашнувся ДО того, як система «дізналася» про це (через heartbeat, reconciliation, saga compensation) — що відбувається?
Якщо система не виявила крах → інший нод може підхопити той самий івент → подвійна обробка.
Якщо система виявила → тоді reconciliation/saga і є «ack» на системному рівні, просто названий інакше.
TLA+ моделює саме це: crash window між StoreResult і CommitOffset. Назва «ack» чи «reconciliation» не важлива — важливо, що між обробкою та підтвердженням є вікно, де crash створює невизначеність.
Мейнтейнер RabbitMQ підтвердив: це фундаментальна властивість at-least-once семантики, не баг реалізації.
а мужики то и не знали ©
Погоджуюсь — для досвідченого інженера це очевидно. А як ви перевіряєте свою event-driven архітектуру на race conditions перед деплоєм?
ні. треба просто одразу будувати правильну архітектуру, її не вчора придумали, всі косяки вже відомі.
у англичан ружья кирпичом не чистят ©
питання в тому, як переконатися, що архітектура дійсно правильна, коли система складна: кілька consumer’ів, різні timeout’и, кілька брокерів.
Приклад: RabbitMQ docs описують at-least-once delivery, але не гарантують відсутності double execution при crash до ACK. Це не баг — це документована поведінка. Але інженер може не знати про це, поки не трапиться інцидент.
TLA+ не замінює досвід — він дає математичний доказ того, що конкретна конфігурація безпечна. Як unit test для архітектури: можна і без нього, але з ним — впевненіше.
та ні як )) не може бути у event-driven архітектуру ні які race conditions як то саме by design
якщо у системі запроектовані можливості падіння окремих тасок нодів чейнів то система і займається виявленням та реакцією але ні які race conditions при цьому не виникають просто виходячи зі самої природи саміх івентів
це саме за те я тобі і кажу простота самого принципу event-driven архитектури якраз полягає у тому що то є математично простий граф з узловими точками є івенти
більше того як я вже казав на справді більшість чи то переважна більшість пайплайнів просто лінійні тобто то є лише ланцюжок навіть не розподілений граф «роби один роби два роби три маєш результат»
тож математично його довести коректність досить на роботі окремого ноди чи чейна чи задачі кожна окремо яка має працювати коректно «вхід вихід»
... і у загальному реакції на уже саме поза штатні ситуації фактичної вважай десь відсутності математичної зв’язності твого графа
проблема якраз у тім що ні які race conditions тут не притаманні саме архітектурно
... тож якщо скажімо у тебе нод якийсь не зовсім крашнувся але не сподівано прокинувся і таки відправив свою відповідь івень «10 років по тому» то система так само має мати реакцію на те як на потенційну можливість ghost events саме by design
тож у тебе у системі не задизайнено від початку що у логах має відображатися усе те прецеденти дуплікації або загублення
тобто фактично у тебе саме у дизайні не передбачено що таке можливо і відповідно не передбачено реакції на те і відповідно у логи ні чого не потрапляє ні чого
... а от з зависанням системи трохи складніше бо тут треба більше контексту )) але знову ж таки притаманне логування дає тут раду
... а особливо (!) у event-driven архитектурі бо ж ти бачиш усі івенти які пройшли і відповідно були залоговані
і ті які були втрачені бо ти ж бачиш що отут на цепочці мав бути івент а його нема
і ті які здупліковані бо ж ти знову бачиш що ось ішло ішло а тут івента вже два
... і саме у оцій конкретній точці на твоєму математичному графі усіх доступних івентів твоєї схеми
у цьому ж саме і прєлєсть такого підходу
я не зовсім розумію питання імхо воно зумисне заплутане
отже «конюсмен» отримав івент
згідно івент він зробив усю належну по схемі роботу
далі так чи інакше не пройшов етап відправки вихідного івенту який належало відправити за схемою
слід розуміти так
що це узагалі означає? система має вести свої власні стани так само на виявленні таких подій як і усі інші
... як то система не змогла виділити оперативну пам’ять або не змогла записати файл тощо
але при цьому це не виявила тож це припущення assumption можна розуміти тільки так
з якого це дива? івент же ж уже був відправлений і уже отриманий усе розглядається саме як атомарна операція отже що система знає напевне що івент відправлено і отримано
саме цей івент уже не можна «підхопити» він уже всьо
ну так якщо то прямо закладена саму дуплікація саме івентів але я вже написав на рівні системи самої системи має бути закладено сам механізм і виявлення і обробки випадків коли десь на окремому chain link чи цілому сервісі щось пішло не так
... так само як зокрема той конкретний сервіс не упав і не його уронілі но він просто не зміг обробити івент як то не зміг дістатися до бази даних як приклад
... іде та сама штатна обробка де цей сервіс відсилає відповідний івент яким повідомляє усю систему що саме сталося тобто що він не зміг обробити саме _цей_ конкретний івент
і так далі сама система лише схема може вирішати чи можлива узагалі дуплікація такого івенту чи потрібна процедура відкату саме _цього_ івенту а наступні «дуплікати» уже розглядаються уже саме на рівні системи схеми уже як окремі івенти які так само обробляються уже окремо а ні як як _цей_ саме івент
система не може «не виявити» бо тоді то є просто криво задизайнена сама система ні чого такого
... так само як не перевіряти виділення пам’яті записи на диск наявність файлів тощо
і саме тому івент можна і слід розглядати саме як атомарність яка саме не дає ні якої можливості race condition бо сам факт відправки та отримання самого івенту є перевіреним і підтвердженим як таким
тобто сама decision chain твого пайплайну складається з таких окремих івентів які просто «віртуальну розтягуються» у один і той самий chain і саме за рахунок того у нього технічно не може виникати ні які race condition
а ті участки які можуть виконуватися і виконуються паралельно вони просто мають свої точки збору які так само повністю самі між собою синхронізуються самим івентами бо ж точка збору має зібрати усі івенти які їй потрібні для продовження
а сам івент є атомарним як є
атомарним і унікальним
(але там звісно де така унікальність потрібна бо певно може існувати певні задачі де така унікальність не потрібна або ж система розрахована сама таким чином щоб мати можливість поводити з повтором івентів для прикладу просто дропати або ж не суттєво чи той івент повториться бо він не змінить стан системи від повтору)
я думаю ти просто оперуєш якої специфічної термінології специфічно саме до кафка і вирішуєш якусь певну проблему специфічну так само саме для кафка а не для івентів та асинхронності узагалі
чи справді така проблема існує узагалі саме специфічно до кафка судити я не берусь
не має ні якого «вікна»
... якщо у системі як архітектурно визначені певні проміжки часу за які система має розглядати гарантовану наявність відповіді як то продовження по пайплайну тоді система просто слідкує за цим просто на рівні системи виявляючи ці збої як збої і запускаючи конкретну реакцію на рекавері саме конкретного кейзу як системи
я не зрозумів бо мені треба вдаватися у контекст але імхо то є то є саме що я кажу ти говориш про якусь вузьку специфіку саме кафка імхо яка не стосується принципу взагалі як такого
... принаймні моно навіть гуглиться одразу на підказках саме як
більше того прямо наступним у підказках є також запит гугла як
Alex, дякую за детальну аргументацію. Ви праві в одному: всередині одного процесу event state machine = простий граф, де correctness доводиться per-node. Але мова статті про міжпроцесний crash window.
Конкретний кейс:
1. Consumer отримує івент з Kafka
2. Consumer пише в PostgreSQL (змінює стан)
3. Consumer падає (docker kill, OOM, мережа)
4. Kafka не отримала ACK → перенаправляє івент іншому consumer’у
5. Два consumer’и записали в одну таблицю → double execution
Ваша відповідь: " система має мати recovery by design". Але recovery ≠ запобігання. Recovery = виявлення + компенсація після того, як double execution вже стався. А TLA+ доводить, що crash window існує до написання коду.
Логи показують дуплікати після інциденту. TLA+ показує можливість інциденту до нього. Це різні рівні: один = детекція, другий = запобігання.
так я вже зрозумів що вома конкретно за кафку
грєфнєвая... імхо помилка тут у розумінні що є кафка
тобто кафка то є вже сама система яка розкикає свої дані у потоці на обробку окремим процесорам
тобто те що ти розказуєш то лише конкретно кафка не реалізація навіть а сам дизайн саме як задумано кафка як масовий розподілений обробка великого вхідного потоку даних
тобто то є саме кафка так робить вона кидає певні дані на обробку на «консюмер» і очікує від нього у відповідь ACK про те що підтвердження що він ці дані обробив
якщо такого підтвердження не надходить то є сама кафка запускає свій власний алгоритм як нівелювати такий кейз
як то маючи окремі тактики
усе інше... імхо то щось дуже надумане імхо сорі
це безглузде statement воно ні чого не означає
доки є пункт
це означає що інциденту запобігти не вдалося
так само якщо це взагалі можливо як принцип тоді оце не має сенсу
можливість інциденту ймовірна і не нульова але виникає як така лише у момент виникнення самого інціденту
ні як його «показати до того» ні як не можна бо його уже «показали» припустивши що він може виникнути як такий
Щодо Kafka — ви праві в тому ж сенсі, що і Vitaliy та Serhii вище: at-least-once і механізм redelivery — це свідомий дизайн, не збій Kafka. Але зверніть увагу: сам механізм, який ви описали («Kafka чекає ACK, якщо його нема — перенаправляє повідомлення») — це і є те, що спричиняє дубль виконання, коли side-effect консюмера (запис у Postgres) не ідемпотентний. Kafka робить рівно те, що мала робити за протоколом — і саме тому виникає execCount=2. Тобто це не «помилка розуміння Kafka» з мого боку, а якраз опис того, як Kafka влаштована — я моделюю не збій брокера, а взаємодію двох коректно працюючих компонентів (брокер за протоколом + консюмер, що ще не встиг закомітити offset).
Щодо другого пункту — «TLA+ показує можливість інциденту до нього, це безглузде твердження» — тут, здається, плутанина між двома різними речами: прогнозуванням і доведенням досяжності стану.
TLC не прогнозує, коли саме станеться інцидент, і не оцінює його ймовірність. Він вичерпно перебирає всі можливі переплетіння дій, дозволені специфікацією протоколу, і доводить: чи існує серед них хоча б одна послідовність, що веде в заборонений стан (execCount=2). Це логічний доказ досяжності, зроблений аналітично — без запуску коду, без продакшена, без єдиного реального consumer’а. «До того» означає буквально «до написання коду» — TLC знаходить контрприклад ще на етапі специфікації.
Те, що інцидент «неминучий» (ваш пункт 3, погоджуюсь) — не робить це доведення марним. Навпаки: якщо властивість фундаментальна і невід’ємна від at-least-once семантики (а не implementation bug, який можна «запобігти» патчем), то формальний доказ цього — саме те, що дозволяє свідомо спроектувати мітигацію (idempotent consumer) до деплою, а не з’ясувати це постфактум через дублікати в БД. Детекція постфактум і доведення досяжності до деплою — це різні речі не тому, що один «запобігає», а інший «детектує» в сенсі ймовірності, а тому що один дає вам конкретний контрприклад (яку саме дію послідовності треба заблокувати guard’ом) до того, як хтось написав перший рядок consumer-коду.
=>
=>
див.
=>
=>
«Exactly-once» у Kafka — це реальна гарантія, але вона діє всередині транзакційного домену самої Kafka: атомарний запис у топік + producer-транзакція + offset commit, або класичний read-process-write цикл (Kafka Streams). Це підтверджує і сама документація: транзакції підтримуються лише всередині одного Kafka-кластера, і якщо в межах транзакції є процесори із зовнішньо спостережуваними побічними ефектами, потрібні додаткові компоненти — тут може допомогти transactional outbox pattern.
Сценарій у статті — саме цей «зовнішній побічний ефект»: консюмер пише результат у Postgres, окрему систему поза Kafka. Щойно консюмер взаємодіє з будь-якою зовнішньою системою, він виходить за межі транзакційного домену Kafka — і якщо збій стається між записом у БД і offset commit, Kafka при відновленні повторно доставляє те саме повідомлення, а застосунок повторно його обробляє; Kafka, не маючи жодного уявлення про вашу БД, не може цьому запобігти. Вона зробила свою роботу. Це відомо як dual-write problem: запис у Kafka (offset commit) і запис у зовнішню систему — це два окремі записи, які не можна виконати атомарно; якщо один з них падає незалежно від іншого, ви ризикуєте отримати дублікати або втрачені оновлення.
Тобто «exactly-once» з документації Kafka технічно правильна цитата, але вона не покриває саме той кейс, що змодельований у статті — не тому, що я неправильно зрозумів Kafka, а тому що ця конкретна межа (Kafka-транзакція ↔ зовнішня БД) — задокументована архітектурна межа самого exactly-once, а не моя інтерпретація.
Essential Complexity закон Брукса. Усіх вимог просто не може бути при створені ПЗ, тому і науково доказовий метод — тестування в простонародії і ітеративні методики розробки.
А повнісю математичний метод доказовості алгоритмів пропонував ще Едсгер Дейкстера, та воно виявилось вічним двигуном.
Щодо Essential Complexity (Брукс):3-5 кроків:
Брукс має рацію: складність ПЗ неминуча. Але TLA+ не намагається подолати цю складність — він працює з конкретною властивістю: «чи можлива ситуація, коли дві нитки виконають одне завдання двічі?»
Це не формалізація всієї системи. Це формалізація протоколу з
1. Consumer отримує повідомлення з брокера
2. Consumer зберігає результат у БД
3. Consumer комітить offset/back-ack брокеру
Crash window — між кроками 2 і 3. Якщо consumer падає тут, брокер перенаправляє повідомлення іншому consumer, який не знає про крок 2. Результат: двічі виконане завдання.
TLA+ перевіряє: чи існує хоча б одне переплетіння дій, що веде до execCount=2 для одного повідомлення? Відповідь: так, для будь-якої at-least-once системи з crash-вікном. Це математичний факт, а не імовірнісна оцінка.
Щодо Дейкстра:
Дейкстринський weakest precondition calculus перевіряє коректність коду — чи реалізація відповідає специфікації. TLA+ перевіряє архітектуру — чи специфікація взагалі допускає небезпечний стан.
Це різні рівні:
— Дейкстра: «чи цей цикл правильно сортує?» → код
— TLA+: «чи можлива ситуація, коли два consumer оброблять одне повідомлення?» → протокол
«Вічний двигун» Дейкстра — це про неможливість формалізувати все ПЗ. Ми не формалізуємо все — ми формалізуємо одну критичну властивість конкретного протоколу. Це не амбітна спроба замінити тестування — це доповнення до нього на рівні «чи безпечна моя ідея до написання коду?»
Практичний результат:
Ми знайшли конкретний баг у Celery (ACK timeout при ETA-задачах у Redis), який жив у продакшені роками. TLA+ модель показала, що double-execution досяжний при timeout < visibility_timeout. Chaos-тест підтвердив: docker kill контейнера з consumer у crash-вікні → повідомлення оброблене двічі.
Це не теорія — це конкретний баг з конкретними кроками відтворення. І він стосується не одного проекту, а будь-якої at-least-once системи з ack-протоколом: Kafka, RabbitMQ, NATS, Celery, BullMQ.
Тут ок, те що ви пропонуєте це певний сантайзер архітектури, умовно може підказати щось з розряду "данні можуть бути не согласованими, додайте : Транзацію, Сагу, Монітор і т.п. І це реально може спрацювати після розробки архітектури чи дизайну на ранніх етапах. Це працюватиме якщо взагалі використовується Top-Down підхід до розробки, а як відомо більш не менш чітки вимоги можна отримати на фундаментальних проектах як от військові системи або атомні станції (і навіть там вони постійно можуть мінятись через нові розвід данні о зрбої верогідного супротивника або уточнені данні меторологів чи сейсмологів), космічні программи і т.п. В більшості випадків існує не визначенність вимог ітеративні підходи, MVP та Buttom Up підхід, та екперементальні розробки Reasearch&Development.
В цьому сутність, нема у вас до 60% формалізованих вимог при розробці, а також є аппаратні та інші обмеження.
Через якраз цей Esential Complexity — дуже багато чого йде. Наприклад ви не можете коли проект вибивається з графіку просто додати в нього ще людей, бо це лише погіршить ситуацію.
А архітектуру зазвичай перевіряють пост фактум, після реальної дослідної, а то і бойової експлуатації. Тому і провалились ідеї Дейкстери, які безумовно є абсолютно логічними.
Дякую, тут суть заперечення зовсім інша, і вона справедлива в широкому сенсі — essential complexity Брукса нікуди не поділась, і я не пропоную формалізувати 60%+ вимог усього проєкту перед розробкою.
Але зверніть увагу на масштаб того, що конкретно формалізується. Це не бізнес-логіка, не еволюційні вимоги продукту — це одна вузька, стабільна властивість самого протоколу доставки повідомлень (at-least-once + crash-window), яка не залежить від того, наскільки визначені бізнес-вимоги вашого конкретного проєкту. Семантика доставки Kafka/RabbitMQ/NATS не змінюється щоспринту разом із вашим product backlog — вона фіксована дизайном брокера. Тобто це не top-down специфікація всієї системи, а point verification одного ізольованого, добре зрозумілого шматка інфраструктури.
І тут є показовий контрприклад до тези «формальні методи працюють лише на військових/атомних/космічних проєктах з чіткими вимогами» — це AWS, компанія, максимально далека від waterfall. Самі інженери AWS описують свій підхід так: вони пишуть звичайний prose-документ дизайну, а потім інкрементально уточнюють окремі його частини в PlusCal чи TLA+ — часто це дає важливі інсайти, навіть не доходячи до повної специфікації чи model checking. Вони самі визнають: команда прагне уникати зайвої складності, але essential complexity задачі залишається високою — тобто той самий Брукс, та сама проблема, яку ви описали. Але це не завадило TLA+ дати їм відчутну практичну користь саме тому, що застосовувався він локально й вибірково — на конкретних критичних алгоритмах (S3, DynamoDB, EBS), а не на всій системі одразу.
Щодо «ідеї Дейкстри провалились» — тут я б розрізнив дві різні речі. Повний ручний доказ коректності (Дейкстра, Хоар) справді не масштабувався в індустрії — це правда. Але TLC/model checking — це якраз відповідь на цей провал, а не його повторення: замість повного доказу — вичерпний автоматичний перебір скінченної абстракції вузького шматка системи. Це вже інший клас інструменту з іншою історією індустріального застосування, і саме тому я не намагаюсь «врятувати» ідею Дейкстри в повному обсязі — я використовую вужчий, вже перевірений на практиці її нащадок, саме в тому масштабі, де він історично працює.
ниасилил.
как проблема решается по другому.
все виды взаимодействия между потоками можно уложить в дюжину паттернов.
человек с прямыми руками и светлой головой один раз их реализовывает, а потом все остальные используют исключительно их.
Теоретично ви праві — паттерни справді покривають більшість проблем. Але на практиці навіть досвідчені інженери роблять помилки в crash-вікні між StoreResult і CommitOffset — не тому, що не знають паттерн, а тому що в реальному коді ці паттерни перетинаються з таймаутами, реконектами, і багатошаровими абстракціями бібліотек.
Цінність TLA+ не в тому, щоб замінити «людину з прямими руками». Вона в тому, щоб за 3 секунди довести (математично, а не інтуїтивно), що саме ваш набір паттернів у вашій конфігурації дає гарантію безпеки. Людина перевіряє один сценарій. TLC перевіряє всі можливі переплетіння.
Chaos validation — це не заміна код-рев’ю. Це емпіричне підтвердження, що математична абстракція не збрехала.
А як ви власне робили верифікацію?
Читали код очима, писали з цього формальну стейт машину руками, й запсукали верифікатор?
Чи є якась автоматизація.
Питаю, бо в базах даних зазвичай використовують рандомізовані тести, але там код такий та його стільки, що вичитати нереально.
Дякую за питання.
Методологія:(47–8641 станів залежно від конфігурації).
1. Аналізуємо документацію протоколу (не код). Для Kafka — offset commit protocol, для RabbitMQ — AMQP ack, для NATS — JetStream ack.
2. Будуємо TLA+ модель вручну, створюючи абстракцію протоколу: стейт-машина consumer + broker з crash-вікном між StoreResult і CommitOffset/Ack.
3. TLC вичерпно перевіряє всі можливі переплетіння подій
4. Паралельно працюємо над автоматизацією: LLM генерує CRL-граф (Collision Region Language) → TLA+ → TLC → repair loop. Для типових брокерів шаблони вже готові.
5. Chaos validation через Toxiproxy: прогноз TLC підтверджуємо фізичним експериментом (docker kill, network disconnect).
Відмінність від randomized testing: вичерпний пошук, а не випадковий. Гарантія, а не ймовірність.
Чому performance тести ловлять race condition і як дізнатися що є не тільки функціональні тести?
Performance тести можуть випадково ловити race conditions завдяки навантаженню — збільшується ймовірність одночасного доступу до ресурсів, що провокує timing-sensitive баги. Але це не гарантія: вони не перевіряють всі можливі переплетіння подій, тільки ті, що виникають за конкретного сценарію навантаження. Формальна верифікація доповнює цей підхід вичерпним пошуком.
Чи навіть фунціональні тести які виконуються по колу і симулюють «rated load».
Але в кожному разі, справжній программіст відповість що тести нестабільні, загальне використання ресурсів було не вище 40% і продовжить бавитися в теорію хаосу.. в cs2
А якщо тести все ще падають після 40% — значить, треба просто додати ще один рівень абстракції. І більше CS2, звісно.
А ви кафку в exactly once моді запускали? По-ідеї, двохфазний коміт мав би від цієї проблеми вберегти. Та й в цілому цей інструмент, як і сама стаття виглядає трохи useless, в будь-якій книжці по розподіленим системам (навіть в тому ж кабанчику) написано про всі ці проблеми, ніякої магічної АІшки тут не треба, це буквально перше, що приходить в голову коли починаєш думати про черги
Хороше питання про exactly-once semantics.
Kafka EOS (transactional producer) гарантує exactly-once від producer до broker, але не захищає consumer після crash. Якщо consumer зберіг результат у БД і впав до commitSync(), новий consumer не знає про це і починає з останнього коміченого offset — повідомлення обробляється вдруге. EOS цього не змінює, бо offset commit — це окремий протокол.
Двофазний коміт вимагає transaction coordinator. Якщо координатор падає між prepare і commit — ми в тій самій ситуації з ще більшою складністю.
«В книжці написано» — так, проблема відома десятки років. Наш внесок не у відкритті, а в:
1) Формальному TLA+ доказі, що це фундаментальна властивість будь-якої at-least-once системи, а не баг реалізації;
2) Уніфікації — одна специфікація покриває Kafka, NATS, RabbitMQ;
3) Cross-validation через chaos engineering, де прогноз TLA+ збігся з реальністю в 4/4 випадках.
Це shift-left: знайти проблему в специфікації до того, як книжка опише саме ваш випадок.
Дякую за конструктивну дискусію.
Це не проблема Кафки, він не отримав підтвердження доставки повідомлення.
Це ваші проблеми — ви так консюмера написали.
Абсолютно згоден — це не баг Kafka, це наслідок того, як написаний consumer. Саме про це стаття: crash window між StoreResult і CommitOffset — це фундаментальна властивість будь-якої at-least-once системи, незалежно від брокера. Kafka тут ні до чого.
Питання в іншому: скільки розробників усвідомлюють це на рівні «я знаю, що треба писати idempotent consumer» vs «я математично довів, що без idempotency shield подвійне виконання неминуче»? Більшість знає про проблему інтуїтивно, але TLA+ дозволяє зробити це знання формальним і відтворюваним. Особливо коли система ускладнюється — кілька consumerів, різні timeout, firefly sync, тощо.
Дякую за дискусію, це допомагає краще сформулювати цінність підходу.
В документації Кафки цей кейс описаний.
І ваше намагання засунути туди “розмишлізми”
які відношення до справи не мають, виглядають як намагання написати “тут був Вова” всюди, де тільки можна.
p.s.
абсолютна більгість девелоперів, що пишуть прикладний код, роблять це без всякого знання TLA+ специфікації мови, на якій пишуть. А щоб розібратись, що ж там “під капотом” з мультітредінгом розібратись, треба language memory model дивитись, вона це пояснює набагато краще ніж TLA+
Справедливо щодо документації Kafka — так, цей кейс справді описаний. Наша робота не претендує на відкриття нового бага, а пропонує формальний інструмент, який робить це знання відтворюваним і незалежним від конкретного брокера.
Щодо language memory model — ви маєте рацію, для race conditions в межах одного процесу це правильний інструмент. Але temporal collisions у розподілених системах — це інший клас проблем: мова йде про crash-вікно між двома системами (consumer + broker), де немає спільної пам’яті. TLA+ моделює саме цей клас помилок.
З точки зору мейнтейнера репозиторію/продукту я б на ваші issues просто забив — ви описуєте якогось сферичного коня в вакуумі, без steps to reproduce, просто от ми щось знайшли за допомогою якоїсь фігні; дивні пулл-реквести.
Що, походу, і відбувається.
Справедливі зауваження, дякую.
«Сферичний кінь у вакуумі» — частково погоджуюсь. TLA+ модель — це абстракція, але вона безпосередньо відображає реальний протокол consumer + broker. І вона передбачила конкретну поведінку, яку ми потім вручну відтворили через Toxiproxy: docker kill контейнера з consumer у вікні між StoreResult і CommitOffset.
Steps to reproduce — вони є: pilot_kafka/ у репозиторії містить docker-compose + Toxiproxy конфіг. Для Celery — celery_test/. Маю додати прямі посилання в текст статті, вибачте.
PR ігнорують — так. Kafka PR закрили без merge. Celery discussion висить без реакції. Я не стверджую, що підхід уже визнаний ком’юніті — це експериментальний інструмент. Але він математично доводить проблему, і я продовжую роботу над автоматизацією repro, щоб знизити поріг для мейнтейнерів.
Дякую за чесний фідбек.
так зазвичай з коробки message brokers працюють в режимі retry — тобто надають at-least-once delivery гарантію, це вже ваша задача спроектувати операції idempotent
не зовсім розумію суть ваших issues
Serhii, ви абсолютно праві — at-least-once delivery це свідомий дизайн брокерів, і idempotent consumer це стандартна рекомендація. Стаття не претендує на відкриття цього факту.
Суть issues не в тому, щоб «звалити провину на брокер». Вона в тому, що:
1) Формальний TLA+ доказ робить це знання відтворюваним — не «інтуїтивно зрозуміло», а «доведено для всіх можливих станів».
2) Одна специфікація покриває Kafka, NATS, RabbitMQ — це узагальнення, якого немає в документації жодного з них.
3) Chaos cross-validation підтверджує, що абстрактна модель і реальність збігаються.
Іншими словами, ми не кажемо «брокер зламаний». Ми кажемо: «ось математичний інструмент, який ловить цей клас помилок до деплою, і він працює на будь-якому брокері».
Майора треба б за вислугу років
Дякую! Сподіваюсь, вислуга років колись конвертується в якийсь сеньйор-мідл :))