assumptions

  • RefinedRustにおけるMIR/Radiumの操作的意味論の適切さ

  • 検証時に用いるlayout algorithmの適切さ

  • RefinedRustのフロントエンドが変換したRadiumの表現の適切さ

    • フロントエンドが変換できない部分を手動で変換した〜

    • refinedrust-dev/rust_typing/shims.v にある手動で形式化されたRustの機能に関する形式仕様

  • ビット操作などRust以外(e.g. llvm intrinsics)で実装されている部分

  • Coqライブラリが仮定している公理 theories/rust_typing/axioms.v

    • proof irrelevance

証明すると良さそうな性質

APIとして

内部構造に言及する仕様

  • index計算

    • 安全性

    • 正当性はfreelist invariantに含まれる

  • freelist invariant

    • すべてのfreelistはsentinelを持つ

    • すべてのfreelistには規定サイズ範囲のブロックしかない

    • bitmapの更新状況がfreelistの状態と整合している

`sl_bitmap[fl].get_bit(sl)` is set iff `first_free[fl][sl].is_some()`

  • free blockは隣接しない ref. // Invariant: No two adjacent free blocks

  • alignment

  • validな領域(?)を対象としていれば初期化(e.g. insert_free_block)は成功する

    • validな領域

      • 非null

      • Tlsfより長いライフタイムを持つ

      • validな領域からキャストされた領域

  • 要求されたサイズ(+alignment+header)を満たすエントリが存在して、要求サイズのindexより大きければ、割当は成功する

  • 指定されたアドレスに対応するused headerが存在すれば、開放は成功する

  • 割当済みの領域と未割り当ての領域は非交和

Rustコード断片に対するインフォーマルな抽象仕様の検討

Zhang et.al. に習ってrlsfに合った抽象仕様を考え、分離論理の語彙に翻訳してみる。 (cf. ./rr-ex/coq/model.v, /coqdoc にホストしてあるcoqdoc)

Configuration

  • FLLEN: maximum first level index

  • SLLEN: maximum second level index

  • GRANULARITY: 最小のブロックサイズ

    • rlsfでは GRANULARITY

Blockの定義

TLSFがメモリ領域を管理する単位。開始アドレスとサイズの対で表す。 (e.g. block := (start_addr, GRANULARITY*2))

  • block.start で開始アドレスを表す

  • block.size でサイズを表す

  • end_addr block := start block + size block

  • これは FreeBlockHdr あるいは UsedBlockHdr に相当する

TLSFの設定

  • FLLEN: first level listの最大長

  • SLLEN: second level listの最大長

  • GRANULARITY: アロケータが扱う最小のブロックサイズ

    • rlsfでは全ての未割り当てブロックのサイズは GRANULARITY より大きい

TLSF allocatorの構造体/抽象的な状態のモデル

  • bitmap

    • rlsfでは fl_bitmap / sl_bitmap がそれぞれ存在して、 second level bitmapには sl_bitmap[fl].get_bit(sl) のようにアクセスする

  • allocated_block: 割当済みブロックのリスト

    • rlsfでは明示的に対応する構造体があるわけではない

    • 本プロジェクトではalloc関数の事後条件でVSTスタイルのトークンを発行する refinedrust内にも開放可能な領域を示すトークンが定義されている(freeable)

  • free_blocks: 未割り当てブロックのリスト

    • rlsfでは Tlsf::first_free から未割り当てブロックの双方向リンクリストがある

    • 対応するブロックのリスト list block から再帰的な述語でメモリ上の表現に変換する

indexの計算

ref. model.v / Section index.

不変条件

  • 領域が連続したブロックは存在しない

  • tlsf.fl_bitmap のn番目のビットが1のとき、 \([ 2^{n+\log_2 GRANULARITY}, 2^{n+\log_2 GRANULARITY+1} (\) の範囲のサイズを持つ未割り当てブロックリスト(i.e. self.first_free[n])が非空

  • Tlsf::map_floor: free blockを挿入するべきリストを計算

  • Tlsf::map_ceil: 要求サイズ以上のブロックしか存在しないリストを計算,割当時に使う

  • well-formed block

    • ヘッダの末尾がブロックの開始アドレスとなり、ヘッダには非負のサイズ情報が入るので終了アドレスが開始アドレスより先に来ることはない

  • allocated_block と free_blocks は非交和

    • alloc関数の事後条件として分離連言で繋がれたトークン(ヘッダに相当する)を発行することで、 割当済みブロックのヘッダと同じアドレスから始まるブロックはfreelistに含まれないことが保証できる

    • 同じアドレスから始まる複数のブロックが発行されないことを保証する必要がある (初期化時に成立させる)

  • allocated_block / free_blocks 内の任意の block の取る領域は非交和

    • alloc/free関数の事後条件で割り当てるブロックの担当する範囲がfreelistのブロック内にないことをメンテナンスする

他のアロケータ検証プロジェクトにおける割当済みブロックの扱い

DeepSpecDB/binlist malloc/VST

  • VSTのVSUというC言語ライブラリの検証単位をとして規格準拠のmalloc仕様が形式化されており、アロケータ実装・検証者も利用できる

  • malloc時に内部構造のブロックヘッダに相当するロケーションに関する述語 malloc_token を発行(事後条件として P ∗ malloc_token …​ のように出てくる)

  • これを持ち回って開放時に free 関数の事前条件に渡すことでリソースの開放が証明できる

Verusによるmimallocの検証

  • アロケータのインタフェースを変更して、割当時にPhantom typeを発行する

    • VSTとアイデアが似ているように見える

references