1 unstable release
Uses old Rust 2015
0.1.0 | Aug 3, 2017 |
---|
#159 in #consensus
28KB
568 lines
crack ⚡
verify distributed and lock-free algorithms through symbolic execution
appendix: philosophy of reliable engineering
for large stateful systems, extra specification up-front saves tremendous effort overall
- TLA+ is useful, but it's costly to learn. we use this to bridge the gap
- cleanroom methodology: specify the intended behavior of ALL nontrivial blocks
- simulate asynchronous network conditions by delivering messages {on time, late, never} in a test harness that explores different paths (either generative or full-state enumeration) depending on testing compute time budget
in action:
- model core communication algos in TLA+ before coding
- make all messaging pluggable
- make all sources of time pluggable
- rely on typed notions of time to reduce the state space explosion of message delivery latencies
- HEAVILY use
debug_assert!
for all nontrivial blocks
Dependencies
~18MB
~348K SLoC