分散プロトコルは単体テストできないが、モデル検証はできる
分散バグはデプロイ後の修正コストが高い。モデル検証を使えば、実装コードを1行も書く前にそれらを発見できる。以下はTLA+を使った方法である。
分散プロトコルは単体テストできない。単体テストは1台のマシン上で1つのプロセスを決まった順序で実行する。分散プロトコルは5台のマシン上で10個のプロセスを、制御できない順序で実行する。この2つの現実の間に、バグが潜んでいる。…
2 posts
分散バグはデプロイ後の修正コストが高い。モデル検証を使えば、実装コードを1行も書く前にそれらを発見できる。以下はTLA+を使った方法である。
分散プロトコルは単体テストできない。単体テストは1台のマシン上で1つのプロセスを決まった順序で実行する。分散プロトコルは5台のマシン上で10個のプロセスを、制御できない順序で実行する。この2つの現実の間に、バグが潜んでいる。…
クラッシュオンリーソフトウェアは、あらゆる障害をクラッシュとして扱い、あらゆる起動をリカバリーとして扱う。Webサービスにとってこれは、シャットダウンロジックを削除し、kill -9でも生き残る状態を設計することを意味する。
あなたのWebサービスにはシャットダウンハンドラがある。バッファをフラッシュし、コネクションを閉じ、チェックポイントを書き出す。一度くらいはテストしたかもしれない。本番では、計画的なデプロイのときに年に一度動く程度だ。残りの時間、サービスはOOMキル、ノードの追放、停電、あるいはタイムアウトしてSIGKILLを受けるデ…