/tlsf-allocator-verification-progress-report

Primary LanguageRust

TLSFアロケータのdeductive verification

  • Rust実装の正当性を保証したい

  • 現在やったこと・やっていること 現状

現状の方針

  • RefinedRustの適用を試みる

    • 非技術的な動機

      • safety criticalな利用目的なので出来るだけfoundationalな検証を目指したい

      • 自分のスキルセットなどを鑑みて定理証明による手法が使いたい

TODO

  • ビット操作周り

    • 各ビット幅を取るモジュールで証明を整理する

    • count leading/trailing zerosの形式仕様

      • trailing zerosの定義

      • Z.log2 との対応( count_leading_zeros_usize_spec )

    • rotating shift

      • Zrotate_right_usize_spec の証明

  • zhang et.al.の不変条件をrlsfの実装に合うように翻訳してみる

  • インデックス計算の形式化

  • 検証の対象とする性質の検討

    • Rustのアロケータとして要求される仕様について検討する

  • Tlsf::allocate / Tlsf::deallocate に絞って正当性を考えて・スペックを書き始める

    • インフォーマルに検証の対象とする仕様などに関することをまとめる

  • rlsfの実装を読む

    • crates/rlsf/src/tlsf.rs を中心にインフォーマルに正当性を考えてみる

  • crates/rlsf/src/tlsf.rs を現在のフロントエンドで扱える範囲に、書き換える

  • RefinedRustに関する調査

    • 論文を精読/Coqの形式化を読む

    • 文書にまとめる

references