颁辞辩による惭蝉驳笔补肠办の証明
7 likes2,168 views
ProofSummit2011 http://partake.in/events/ac41261d-6026-4d09-8814-5ad3e58446e8 における発表
颁辞辩による惭蝉驳笔补肠办の証明
- 1. 2011/09/25 ProofSummit2011 #ProofSummit Coqによる MsgPackシリアライザの 証明と実装 mzp / みずぴー 1 11 9 25
- 2. 自己绍介 @mzp / みずぴー 名古屋のSE Coq / proof-general派 ProofCafeに参加してます 2 11 9 25
- 3. ProofCafe 開催日: 第4土曜日 開催場所: どえりゃあカフェ@名古屋 アダムッチさんのCPDTをみんなで読む ? そろそろ別のことやるかも たまにイベント開催 3 11 9 25
- 4. 2011/09/25 ProofSummit2011 だいたいこんな感じ 11 9 25
- 5. 惭蝉驳笔补肠办を証明した动机 ネットワーク通信がしたい 楽をしたいので、既存のライブラリを 活用したい 要件 ? ある程度の実績がある ? 非同期の呼び出しができる ? いろんな言語のライブラリが充実してる 5 11 9 25
- 6. 惭蝉驳笔补肠办がよさそう オブジェクトのシリアライザ + RPC ? 高速かつ省サイズ(らしい) ? 非同期呼び出しもサポート ? いろんな言語のライブラリがある 6 11 9 25
- 7. 惭蝉驳笔补肠办ライブラリ一覧 7 11 9 25
- 8. 惭蝉驳笔补肠办ライブラリ一覧 OCaml版がないじゃん → 作ろう 7 11 9 25
- 9. バグがこわい 作るのはいいけどバグがこわい 省サイズ化のため仕様が複雑 ? 実装を間違えてないかな? ? テストの網羅性が十分かな? ? この変更しても大丈夫かな? 8 11 9 25
- 10. 証明すればよくね? 証明すれば... ? 全入力に対して正しさが保証される ? 人間が網羅性を考えなくてもOK ? 変更しても大丈夫かを考えなくても OK 証明したほうが楽!! 9 11 9 25
- 11. 証明した(シリアライザだけ) シリアライザ部分のみ 多言語間のデータやり取りには使える RPCは今后の课题 MsgPack = シリアライザ + RPC + RPC-IDL ↑ ここだけ 10 11 9 25
- 12. 公式レポジトリに入って ます(??? msgpack/ocaml/proofというディレクト リがあるよ ↑ これ 11 11 9 25
- 13. 証明の流れ 11 9 25
- 14. 颁辞辩使いました 証明にはCoqを使いました ? 証明したコードをOCamlに変換できる ? 日本語の文書も豊富 ? Twitterでいろんな人に訊ける 13 11 9 25
- 15. 开発の流れ 14 11 9 25
- 16. 証明のアウトライン 1.8/16/32/64bits整数を作る 2.オブジェクトと変換ルールを定義する 3.シリアライズ関数、デシリアライズ関 数を定義する 4.OCamlに変換する 15 11 9 25
- 17. 証明のアウトライン 1.8/16/32/64bits整数を作る 2.オブジェクトと変換ルールを定義する 3.シリアライズ関数、デシリアライズ関 数を定義する 4.OCamlに変換する 16 11 9 25
- 18. 8/16/32/64ビット整数 MsgPackはビットレベルの操作を多用す るのでnatだと不便 標準ライブラリのasciiを組合せて、マ ルチバイトの整数を定義する 17 11 9 25
- 19. 苍补迟との変换 asciiのままだと証明が面倒 natとasciiの相互変換関数を作る 18 11 9 25
- 20. 巨大な苍补迟が扱えない 5000以上のnatを使おうとするとオー バーフローする 16ビットすら扱えない (><) 19 11 9 25
- 21. オーバーフローする理由 Coqのnat := ペアノ数 再帰的に定義されている 値が大きすぎると、ネストが深くなり すぎる 20 11 9 25
- 22. オーバーフローの回避 巨大な自然数が登場しないようにする simplダメ、ゼッタイ 累乗に関する補題を使う 累乗に関する補題 n m (n+m) 2 ?2 =2 n 0 ? n ならば 0 ? 2 n m n ? m ならば 2 ? 2 21 11 9 25
- 23. 証明のアウトライン 1.8/16/32/64bits整数を作る 2.オブジェクトと変換ルールを定義する 3.シリアライズ関数、デシリアライズ関 数を定義する 4.OCamlに変換する 22 11 9 25
- 24. オブジェクトの定义 23 11 9 25
- 25. 変换ルールの定义 24 11 9 25
- 26. ↓これを証明する 25 11 9 25
- 27. 健全性の証明 これを証明するときに定義の誤りが見 付かる(ことが多い) Serialized obj1 xsに関する帰納法で 証明する 26 11 9 25
- 28. 証明のアウトライン 1.8/16/32/64bits整数を作る 2.オブジェクトと変換ルールを定義する 3.シリアライズ関数、デシリアライズ関 数を定義する 4.OCamlに変換する 27 11 9 25
- 29. 変换ルールは実行不可 変換前後の関係を定義してるだけ 実行できるように関数を定義する 28 11 9 25
- 30. 蝉别谤颈补濒颈锄别関数 OCamlっぽい!! 29 11 9 25
- 31. de蝉别谤颈补濒颈锄别関数 ↑失敗するかも 30 11 9 25
- 32. 関数が変换ルールを満す ことを示す serialize/de蝉别谤颈补濒颈锄别関数が変換ルー ルと矛盾しない 31 11 9 25
- 33. 証明のアウトライン 1.8/16/32/64bits整数を作る 2.オブジェクトと変換ルールを定義する 3.シリアライズ関数、デシリアライズ関 数を定義する 4.OCamlに変換する 32 11 9 25
- 34. 翱颁补尘濒への変换 Coq 8.3からCoqの型とOCamlの型が対応 づくようになった ? 例: natとint, optionとoption 33 11 9 25
- 35. まがまがしいコード 34 11 9 25
- 36. 35 11 9 25
- 37. 速度を测ってみた やっぱり速度が気になる 比較対象はRuby版MsgPack 0.4.6 ? 拡張ライブラリを使っているので、ほぼC 言語版と速度が同じ 長さnの配列のシリアライズ速度?デシ リアライズ速度を比較 ? n = 100,1000,10000 36 11 9 25
- 38. シリアライズ Ruby OCaml 100 1000 10000 0 2.5 5.0 7.5 10.0 12.5 15.0 11 9 25
- 39. シリアライズ Ruby OCaml 100 1000 10000 0 2.5 5.0 7.5 10.0 12.5 15.0 11 9 25
- 40. デシリアライズ Ruby OCaml 100 1000 10000 0 5 10 15 20 38 11 9 25
- 41. 2011/09/25 ProofSummit2011 結論:ボロ負け 11 9 25
- 42. まとめ MsgPack for OCamlを作りました バグが怖いのでCoqで証明しました ? 健全性を証明しました ? マルチバイトの扱いで苦労しました 性能はオリジナルの1/10 40 11 9 25
- 43. 今后の课题 性能の向上 やっぱり性能は大事 最適化してもエンバグしてないことが 保証できるし AsciiのExtraction方法を変更すれば性 能を上げれるはず ? Erlangっぽくバイナリ列を操作する Bitstringライブラリがよさそう 41 11 9 25
- 44. 今后の课题 RPCのサポート ネットワーク通信の形式化が必要 π計算/ applpiによって定義できる? IDL処理系はMsgPack側で用意されるら しいので、プラグインを作ればOK 42 11 9 25