分散システムの検証

厳密な検証からデバッグ用途程度のものまで適当に入れてる

仕様を演繹的に証明

取りうる状態の網羅的な検査

どこをいつ通ったか

コード中に故障するようなコードを挿入してテスト

動かしながら適当にノードを落としたりする

実行時にトレースしながら仕様に違反した状態になっていないかチェック

名前が合っているか不明なので注意

タイマーと送受信の実装を入れ替える

送受信: レイテンシ、ドロップ、リオーダー、重複、(ビザンチン故障)、を起こすように入れ替えられる

タイマー: 時刻取得、タイムアウト

タイマーではないかも

送受信のレイテンシは一様分布だとダメそうなので確率分布を渡してやるとかよさそう (対数正規分布だとシンプルそう)

現実でその事象が起こる確率でもって、このくらいの確率で正しく動くみたいなことが言えるようになるかもしれない

Raftなんかだと再起動が特定のタイミングで起こり続けるとと永遠に進まないみたいなのがあった気がするがそれが起こる確率はとても小さい (悪魔が操作して云々というやつ)

こういうパターンが起こらないみたいなのも書きたいかも

たぶん自分で実際に実装とテストを書いてみないと勘所がわからない

タイムアウトの扱いが難しそう

言語によっても違いそう

Fuzzing Test

その他 (よく知らないので分類できない)

Jepsen

参考

『Simple Testing Can Prevent Most Critical Failures』