В этой статье мы смоделируем и исследуем протокол двухфазного коммита с помощью TLA+.
Протокол двухфазного коммита практичный и сегодня используется во многих распределённых системах. Тем не менее, он достаточно краткий. Поэтому мы можем быстро смоделировать его и многому научиться. На самом деле этим примером мы проиллюстрируем, какой результат в распределённых системах фундаментально невозможен.
Проблема двухфазного коммита
Транзакция проходит через диспетчеры ресурсов (RM). Все RM должны договориться, будет транзакция завершена или прервана.
Менеджер транзакций (TM) принимает окончательное решение: коммит или отмена. Условием для коммита является готовность к коммиту всех RM. В противном случае транзакцию следует отменить.
Читать полностью »