Symbolic model checker from scratch in Rust

Transcript

1. Symbolic model checker from scratch in Rust Riru Oda @ri5255 Kernel/VM探検隊@東京 No17 1
2. 2 Agenda • モデル検査とは? • Symbolic Model Checkingの理論と実装 • デモ
3. 3 モデル検査とは? システムが仕様を満たしてることを自動的に検証する技術
4. 4 モデル検査とは? 例) 2つのスレッドp, qが一つの共有変数xを読み書きする While (true) { x = x + 1; x = x – 1; } 仕様: 𝐴𝐺(𝑥 < 2) 全て(All)の実行パスで常に(Globally) x < 2が成り立つ
5. 5 モデル検査とは? 例) 2つのスレッドp, qが一つの共有変数xを読み書きする While (true) { x = x + 1; x = x – 1; } 仕様: 𝐴𝐺(𝑥 < 2) 全て(All)の実行パスで常に(Globally) x < 2が成り立つ
6. 6 モデル検査とは? 例) 2つのスレッドp, qが一つの共有変数xを読み書きする 仕様: 𝐴𝐺(𝑥 < 2) 全て(All)の実行パスで常に(Globally) x < 2が成り立つ While (true) { lock(“mutex”) x = x + 1; x = x – 1; unlock(“mutex”) }
7. 7 モデル検査とは? 例) 2つのスレッドp, qが一つの共有変数xを読み書きする 仕様: 𝐴𝐺(𝑥 < 2) 全て(All)の実行パスで常に(Globally) x < 2が成り立つ While (true) { lock(“mutex”) x = x + 1; x = x – 1; unlock(“mutex”) }
8. 8 モデル検査とは? モデル検査器 システム記述 + 仕様 Ok 反例
9. 9 Agenda • モデル検査とは? • Symbolic Model Checkingの理論と実装 • デモ
10. CTL (Computation Tree Logic) • 𝑝 ∈ 𝐴𝑃 はCTL論理式 • 𝑓 がCTL論理式ならば¬𝑓, 𝐴𝑋 𝑓, 𝐸𝑋 𝑓, 𝐴𝐹 𝑓, 𝐸𝐹 𝑓, 𝐴𝐺 𝑓, 𝐸𝐺 𝑓はCTL論理式 • 𝑓 と 𝑔 が CTL論理式ならば𝑓 ∧ 𝑔, 𝑓 ∨ 𝑔, 𝐴 𝑓 𝑈 𝑔 , 𝐸 𝑓 𝑈 𝑔 , 𝐴 𝑓 𝑅 𝑔 , 𝐸 (𝑓 𝑅𝑔) はCTL論理式 𝑀, 𝑠0 ⊨ 𝐸𝑋 𝑓 𝑀, 𝑠0 ⊨ 𝐴𝐺 𝑓 𝑀, 𝑠0 ⊨ 𝐸(𝑓 𝑈 𝑔) 10
11. CTL Model Checking 例: E(p U q)を満たす状態は? 11
12. CTL Model Checking 答え 12 例: E(p U q)を満たす状態は?
13. CTL Model Checking 答え 13 例: E(p U q)を満たす状態は? どうやって計算する? そもそも計算可能なの?
14. CTL Model Checking via Fixpoint Computation 14 例: E(p U q)を満たす状態は?
15. CTL Model Checking via Fixpoint Computation 15 例: E(p U q)を満たす状態は?
16. CTL Model Checking via Fixpoint Computation 16 例: E(p U q)を満たす状態は?
17. CTL Model Checking via Fixpoint Computation 17 例: E(p U q)を満たす状態は?
18. CTL Model Checking via Fixpoint Computation 形式化 𝜏 𝑍 = 𝑞 ∨ (𝑝 ∧ 𝐸𝑋 𝑍 ) 𝑆𝑎𝑡 𝐸 𝑝 𝑈 𝑞 = 𝐿𝑓𝑝 𝜏 18
19. CTL Model Checking via Fixpoint Computation 形式化 𝜏 𝑍 = 𝑞 ∨ (𝑝 ∧ 𝐸𝑋 𝑍 ) 𝑆𝑎𝑡 𝐸 𝑝 𝑈 𝑞 = 𝐿𝑓𝑝 𝜏 19 𝜏 ∅ = 𝑞 ∨ 𝑝 ∧ 𝐸𝑋 ∅ = 𝑞 = {𝑠1}
20. CTL Model Checking via Fixpoint Computation 形式化 𝜏 𝑍 = 𝑞 ∨ (𝑝 ∧ 𝐸𝑋 𝑍 ) 𝑆𝑎𝑡 𝐸 𝑝 𝑈 𝑞 = 𝐿𝑓𝑝 𝜏 𝜏 ∅ = {𝑠1} 20 𝜏(𝜏(∅)) = 𝑞 ∨ (𝑝 ∧ 𝐸𝑋 𝑠1 ) = {𝑠1, 𝑠2}
21. CTL Model Checking via Fixpoint Computation 形式化 𝜏 𝑍 = 𝑞 ∨ (𝑝 ∧ 𝐸𝑋 𝑍 ) 𝑆𝑎𝑡 𝐸 𝑝 𝑈 𝑞 = 𝐿𝑓𝑝 𝜏 𝜏 ∅ = {𝑠1} 𝜏 𝜏 ∅ = {𝑠1, 𝑠2} 𝜏(𝜏(𝜏(∅))) = {𝑠1, 𝑠2, 𝑠3} 21
22. CTL Model Checking via Fixpoint Computation Theorem (Tarski-Knaster) Let 𝜏 be a predicate transformer on 𝑃 𝑆 . Then if 𝜏 is monotonic it has a greatest and least fixpoint. Lemma If 𝜏 is monotonic and S is finite, then threre is an integer 𝑖0 such that 𝐺𝑓𝑝 𝜏 = 𝜏𝑖0(𝑆) and 𝐿𝑓𝑝 𝜏 = 𝜏𝑖0(∅). Correctness 22
23. CTL Model Checking via Fixpoint Computation Theorem (Tarski-Knaster) Let 𝜏 be a predicate transformer on 𝑃 𝑆 . Then if 𝜏 is monotonic it has a greatest and least fixpoint. Lemma If 𝜏 is monotonic and S is finite, then threre is an integer 𝑖0 such that 𝐺𝑓𝑝 𝜏 = 𝜏𝑖0(𝑆) and 𝐿𝑓𝑝 𝜏 = 𝜏𝑖0(∅). Correctness 23 𝐸𝑋や∨, ∧ はどうやって実装する？ 𝜏 𝑍 = 𝑞 ∨ (𝑝 ∧ 𝐸𝑋 𝑍 )
24. Symbolic Representation of Kripke Structures 24
25. Symbolic Representation of Kripke Structures 25 𝑆 = ¬𝑥0 ∨ 𝑥0 𝑅 = ¬𝑥0 ∧ 𝑥0′ ∨ 𝑥0 ∧ ¬𝑥0′ 𝑞 = ¬𝑥0 𝑝 = 𝑥0 Symbolic Representation
26. Symbolic Representation of Kripke Structures 26 𝑅 = ¬𝑥0 ∧ 𝑥0′ ∨ 𝑥0 ∧ ¬𝑥0′ 𝑞 = ¬𝑥0 𝑝 = 𝑥0 Symbolic Representation • 2つの状態を表すために1つのブール変数𝑥0 を導入 • s0を¬𝑥0, s1を𝑥0で表現する • 遷移後の状態を表現するために新しいブール変数𝑥0′を導入 Idea 𝑆 = ¬𝑥0 ∨ 𝑥0
27. Symbolic Representation of Kripke Structures 27 𝑅 = ¬𝑥0 ∧ 𝑥0′ ∨ 𝑥0 ∧ ¬𝑥0′ 𝑞 = ¬𝑥0 𝑝 = 𝑥0 Symbolic Representation • 2つの状態を表すために1つのブール変数𝑥0 を導入 • s0を¬𝑥0, s1を𝑥0で表現する • 遷移後の状態を表現するために新しいブール変数𝑥0′を導入 Idea 𝐸𝑋,∨,∧ を論理式に対する操作として実装できる 例: 𝑆𝑎𝑡(𝐸𝑋 𝑓 ) = ∃𝑣′[ 𝑓 𝑣′ ∧ 𝑅 𝑣, 𝑣′ ] 𝑆 = ¬𝑥0 ∨ 𝑥0
28. Symbolic Model Checking 例: E(p U q)を満たす状態は? Note • 𝑆𝑎𝑡 𝐸 𝑝 𝑈 𝑞 = 𝐿𝑓𝑝 𝜏 where 𝜏 𝑍 = 𝑞 ∨ 𝑝 ∧ 𝐸𝑋 𝑍 • 𝑆𝑎𝑡(𝐸𝑋 𝑓 ) = ∃𝑣′[ 𝑓 𝑣′ ∧ 𝑅 𝑣, 𝑣′ ] 28 𝑆 = ¬𝑥0 ∨ 𝑥0 𝑅 = ¬𝑥0 ∧ 𝑥0′ ∨ 𝑥0 ∧ ¬𝑥0′ 𝑞 = ¬𝑥0 𝑝 = 𝑥0 Symbolic Representation
29. Symbolic Model Checking 例: E(p U q)を満たす状態は? Note • 𝑆𝑎𝑡 𝐸 𝑝 𝑈 𝑞 = 𝐿𝑓𝑝 𝜏 where 𝜏 𝑍 = 𝑞 ∨ 𝑝 ∧ 𝐸𝑋 𝑍 • 𝑆𝑎𝑡(𝐸𝑋 𝑓 ) = ∃𝑣′[ 𝑓 𝑣′ ∧ 𝑅 𝑣, 𝑣′ ] 29 𝑅 = ¬𝑥0 ∧ 𝑥0′ ∨ 𝑥0 ∧ ¬𝑥0′ 𝑞 = ¬𝑥0 𝑝 = 𝑥0 Symbolic Representation 𝜏 ∅ = ¬𝑥0 𝜏(∅) = ¬𝑥0 ∨ 𝑥0 ∧ 𝐸𝑋(𝑓𝑎𝑙𝑠𝑒 ) = ¬𝑥0 𝑆 = ¬𝑥0 ∨ 𝑥0
30. Symbolic Model Checking 例: E(p U q)を満たす状態は? Note • 𝑆𝑎𝑡 𝐸 𝑝 𝑈 𝑞 = 𝐿𝑓𝑝 𝜏 where 𝜏 𝑍 = 𝑞 ∨ 𝑝 ∧ 𝐸𝑋 𝑍 • 𝑆𝑎𝑡(𝐸𝑋 𝑓 ) = ∃𝑣′[ 𝑓 𝑣′ ∧ 𝑅 𝑣, 𝑣′ ] 30 𝑅 = ¬𝑥0 ∧ 𝑥0′ ∨ 𝑥0 ∧ ¬𝑥0′ 𝑞 = ¬𝑥0 𝑝 = 𝑥0 Symbolic Representation 𝜏 ∅ = ¬𝑥0 𝜏(𝜏 ∅ ) = ¬𝑥0 ∨ 𝑥0 𝜏 𝜏 ∅ = ¬𝑥0 ∨ 𝑥0 ∧ 𝐸𝑋 𝜏 ∅ = ¬𝑥0 ∨ 𝑥0 ∧ ∃𝑥0′[¬𝑥0′ ∧ ( ¬𝑥0 ∧ 𝑥0′ ∨ (𝑥0 ∧ ¬𝑥0′)] ) = ¬𝑥0 ∨ 𝑥0 𝑆 = ¬𝑥0 ∨ 𝑥0
31. Symbolic Model Checking 例: E(p U q)を満たす状態は? Note • 𝑆𝑎𝑡 𝐸 𝑝 𝑈 𝑞 = 𝐿𝑓𝑝 𝜏 where 𝜏 𝑍 = 𝑞 ∨ 𝑝 ∧ 𝐸𝑋 𝑍 • 𝑆𝑎𝑡(𝐸𝑋 𝑓 ) = ∃𝑣′[ 𝑓 𝑣′ ∧ 𝑅 𝑣, 𝑣′ ] 31 𝑅 = ¬𝑥0 ∧ 𝑥0′ ∨ 𝑥0 ∧ ¬𝑥0′ 𝑞 = ¬𝑥0 𝑝 = 𝑥0 Symbolic Representation 𝜏 ∅ = ¬𝑥0 𝜏(𝜏 ∅ ) = ¬𝑥0 ∨ 𝑥0 𝑆 = ¬𝑥0 ∨ 𝑥0 論理式を表現するデータ構造は? 𝜏 𝜏 ∅ = ¬𝑥0 ∨ 𝑥0 ∧ 𝐸𝑋 𝜏 ∅ = ¬𝑥0 ∨ 𝑥0 ∧ ∃𝑥0′[¬𝑥0′ ∧ ( ¬𝑥0 ∧ 𝑥0′ ∨ (𝑥0 ∧ ¬𝑥0′)] ) = ¬𝑥0 ∨ 𝑥0
32. OBDD(Ordered Binary Decision Diagram) 32 例: 𝑥0 ∨ 𝑥1 BDT(Binary Decision Tree)
33. OBDD(Ordered Binary Decision Diagram) 33 例: 𝑥0 ∨ 𝑥1 BDT(Binary Decision Tree) OBDD
34. OBDD(Ordered Binary Decision Diagram) 34 例: 𝑥0 ∨ 𝑥1 BDT(Binary Decision Tree) OBDD Theorem (Bryant[1]) For any Boolean function 𝑓 , there is a unique OBDD denoting 𝑓
35. OBDD(Ordered Binary Decision Diagram) 35 例: 𝑥0 ∨ 𝑥1 BDT(Binary Decision Tree) OBDD Theorem (Bryant[1]) For any Boolean function 𝑓 , there is a unique OBDD denoting 𝑓
36. OBDD(Ordered Binary Decision Diagram) 36 例: 𝑥0 ∨ 𝑥1 BDT(Binary Decision Tree) OBDD Theorem (Bryant[1]) For any Boolean function 𝑓 , there is a unique OBDD denoting 𝑓 𝐸𝑋,∨,∧をOBDDを用いて実装することができる!
37. Implementation in Rust 37 𝑆𝑎𝑡(𝐸𝑋 𝑓 ) = ∃𝑣′[ 𝑓 𝑣′ ∧ 𝑅 𝑣, 𝑣′ ]
38. Implementation in Rust 38 𝜏 𝑍 = 𝑓2 ∨ 𝑓1 ∧ 𝐸𝑋 𝑍 𝑆𝑎𝑡 𝐸 𝑓1 𝑈 𝑓2 = 𝐿𝑓𝑝 𝜏
39. 39 Agenda • モデル検査とは? • Symbolic Model Checkingの理論と実装 • デモ
40. Demo:食事する哲学者問題 40 システム記述
41. Demo:食事する哲学者問題 41 仕様: AG(𝑐𝑟𝑖𝑡𝑖𝑐𝑎𝑙 < 2) 全ての状態がこれを満たすならば相互排他が成り立つ
42. Demo:食事する哲学者問題 42
43. Demo:食事する哲学者問題 43 仕様: EG(𝑐𝑠𝑝 == 0) これを満たす状態が存在するならばスレッドpが飢餓に陥る実行パスが存在する
44. Demo:食事する哲学者問題 44
45. 45 Demo:食事する哲学者問題 例: qがロックをとり続ける実行パス
46. References 46 1. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation" in IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986, doi: 10.1109/TC.1986.1676819. 2. Clarke, E. M., Jr, Grumberg, O., Kroening, D., Peled, D., & Veith, H. (2018). Model Checking, Second Edition. MIT Press. 3. チェシャ猫 (2024). モデル検査器をつくる Code https://github.com/r1ru/model-checker-from-scratch