protocol-design

分散プロトコルは単体テストできないが、モデル検証はできる

分散バグはデプロイ後の修正コストが高い。モデル検証を使えば、実装コードを1行も書く前にそれらを発見できる。以下はTLA+を使った方法である。

分散プロトコルは単体テストできない。単体テストは1台のマシン上で1つのプロセスを決まった順序で実行する。分散プロトコルは5台のマシン上で10個のプロセスを、制御できない順序で実行する。この2つの現実の間に、バグが潜んでいる。…