В этой статье мы смоделируем и исследуем протокол двухфазного коммита с помощью TLA+.

Протокол двухфазного коммита практичный и сегодня используется во многих распределённых системах. Тем не менее, он достаточно краткий. Поэтому мы можем быстро смоделировать его и многому научиться. На самом деле этим примером мы проиллюстрируем, какой результат в распределённых системах фундаментально невозможен.

Проблема двухфазного коммита

Транзакция проходит через диспетчеры ресурсов (RM). Все RM должны договориться, будет транзакция завершена или прервана.

Менеджер транзакций (TM) принимает окончательное решение: коммит или отмена. Условием для коммита является готовность к коммиту всех RM. В противном случае транзакцию следует отменить.
Читать дальше ->

https://habr.com/post/434496/?utm_source=habrahabr&utm_medium=rss&utm_campaign=434496