時系列順に調査・実装などについて、書いていきます。 調査するべき項目が生じたときは Q: …​ として、後に明らかになれば言及します。

2024/09/26以前

Refinedrustの適用可能性について

フロントエンド

Radiumの表現力は十分に見えるが､フロントエンド・Coqによる形式化に手を加える 必要がある。RustからCoqへの変換フロントエンドの機能がrlsfの実装をそのまま扱 うには、不十分だが等価な実装に置き換えることで対応可能だと思われる。 (ref. refinedrust-dev/case_studies/tests)

Radiumの表現力

元論文ではunsafeな実装やreborrowなどが扱えるとされており、rlsfの実装を検証す るのに十分な表現力があるように見える。

標準ライブラリの形式化状況

標準ライブラリに関する形式化などは、まだほとんどなされていない。shim とい う仕組みが用意されていて、手動で書いたRadium/Coqの表現を使った検証が可能。

ビット演算の形式化

TLSFではビット演算を多用するため、Rustによるビット演算の実装を検証できるこ とが望ましい。RefinedRustでは、現在TLSFで用いるビット演算に関する形式化がさ れていないため実装する。

方針

Rustのプリミティブ整数型では、TLSFで扱う wrapping_add / saturating_add / rotate_right のような関数はllvm intrinsicsへコンパイルされ、 [1] Rustの意味論を使って検証することができないため、RefinedRustの only_spec アノ テーションで形式仕様のみ記述する。 only_spec がついたオブジェクトはradiumコー ドが生成されず、仕様のみ生成される。

また、Rustのコンパイラプラグインの事情でプリミティブ型へのメソッドを扱うことが 難しそうだったため、[2] プリミティブへのメソッド呼び出しを通常の関数でラップした上で、 rr::only_spec アノテーションをしている。

RefinedRust/Radiumでは、Rustの整数型はCoqの(無限長の)整数型 Z 上の制限と して形式化されている。Coqの Z は正の数をバイナリ表現で形式化した positive 型を使って以下のように定義されているため、 Z.land / Z.lor の ような論理演算が定義されている。

Inductive Z : Set :=
    | Z0 : Z
    | Zpos : positive -> Z
    | Zneg : positive -> Z.

Z については、様々な数学的成果が形式されているが、ここではビット演算の仕様を 記述するため、 Z.log2 のような数学的な語彙ではなく Z.shiftr のような論理演 算に関する形式化を使う。 Z.log2 のような語彙を使うと、TLSFのインデックス計算 で用いる性質をそのままエンコードしてしまい、形式化の信頼性が損なわれる。 [3]

rotate_right

シフトするビット数が負になり得るケースを含む定義を上手くする方法を考察中。

定義の妥当性を保証する仕様として、n bitシフトしたときにm bit目(0-indexed)が (m - n + ws) mod ws に移動していてほしい(ref. Zrotate_right_spec )

count_(leading|traling)_zeros

0になるまで右シフトする定義が具体的な値に対する計算量が大きすぎたので、代わりに 与えられた幅だけ1ビットづつテストしていく定義を与えた。

RefinedRustを使った検証コードベースに外部のCoqライブラリを導入する

cargo-refinedrust に手を加えて、 RefinedRust.toml にオプション external_coq_libs を追加

QuickChickを導入

Coqのproperty-based testingができるQuickChickを導入。証明に入る前に定義を吟味する際に便利。

2024/09/27

  • 開発環境を自前の flake.nix に移行することを試みた

    • Coqのバージョン、コンパイルしたOCamlコンパイラのバージョンが一致しているにもかかわらず、以下のようなエラーが発生する

      Compiled library stdpp.numbers (in file /nix/store/nsbxf0vixraln8nlsi4frg5kxrpcddmy-coq8.17-stdpp-4be5fd62ddbd5359f912e2cebb415b015c37e565/lib/coq/8.17/user-contrib/stdpp/numbers.vo) makes inconsistent assumptions over library Coq.Init.Ltac

    • 現在は refinedrust-dev/flake.nix のdevShellに依存を追加して使っている

  • 本リポジトリのドキュメント・ rr-ex のcoqdocをwebサイトにした

  • rotate_rightに関する補題を各ビット幅に具体化して示すように方針を変えた

    • 理由: 実際に使うビット幅は限られるため [4]

      • Z上の制限として固定ビット幅の整数に関するビット操作を扱っているVST/CompCertやVellvmでも同様の方針をとっているように見える

2024/10/02

2024/10/03

  • rotate shift/count leading zeros周りの補題( count_leading_zeros_usize_spec / Zrotate_right_usize_spec )の証明を進めた

2024/10/04

  • インデックス計算の補題の証明を進めた

  • ビット操作を扱うRustコードの検証のminimal exampleを作った→上手く動かない

    • rr::spec_only でつけた形式仕様がRefinedRustの生成するsidecondisionを満たせていない

  • 抽象仕様(rr-ex/coq/models.v)のドキュメントを少し書いた

  • Q: rr:spec_only でつけた形式仕様に要求されるsidecondisionに関して調査する

2024/10/07

  • A: ビット操作を扱うコードの検証例を直した(これは勘違い)

    • 原因: アノテーションの使い方が間違っていた

      • 関数の引数に関する事前条件の指定には rr::args を使うべき

  • Q: rotate_right のシフト幅が負の場合の扱い

    • 厄介な点: u32 を符号付きとして暗黙的に扱っている(assert_eq!(2, 1usize.rotate_right(u32::MAX)))

    • Coq側で i32 として解釈した分シフトするようにして、事後条件も usize の取る値の範囲でシフト幅の正負が変わることを明示する

2024/10/10

  • RefinedRustのAllocator APIに関する形式化を調査した ref. refinedrustに関するメモ

  • 簡略化した map_floor の検証

    • template tacticが失敗するのでデバッグしていた

    • RefinedRustのspecでタプルを扱う方法がわからない

  • Q: タプルの扱い/どんな型でrefineできるのか

  • block_size_range_not_overwrap の証明を進めた

2024/10/11

  • A: タプルの扱いについてCoqの項 hlist (place_rfn {Coqの型}) でrefineできることがわかった

  • 簡略化した map_floor の検証: RefinedRust側の問題は概ね解決した

  • block_size_range_not_overwrap の証明を進めた( SLI が SLLEN と混同されていた)

  • 抽象仕様の検討

  • Q: 割当済みブロックの追跡

    • 他の検証プロジェクトを調査する

2024/10/17

  • BlockHdr / FreeBlockHdr / Tlsf のアノテーション・変換fix

    • rr_frontend が未対応な部分は sed の力を借りている

  • ビットマップとfreelistの整合性に関する不変条件を追加

  • Q: const parametersの扱い

    • refinedrustでも単純なジェネリクスが扱えるが、const parametersが扱えるかの検証

  • Q: 再帰的な構造に対する述語の書き方

    • first_free[fl][sl].next_free に関する言明

2024/10/18

  • ビット操作周りはなんとかなりそう [5] なので、先にraw pointerを多用するコードが実際に検証できることを確かめたい

  • rawポインタを扱うプログラムの検証の実験,リンクリストの結合で &T から *const T に変換する部分の推論が上手く行かない

    • ローカル変数にアノテーションが出来ないためsideconditionが残ったと思われる cf. rr_ex::silly

  • NonNull APIの形式仕様

  • core::mem::replace の形式仕様

  • 単純化した Tlsf::link_free_block をつかってリンクリストの検証方法を確かめる(wip)

    • link listは以下のような形で実現できそう？ l ↦ v の v はただのバイト列で、layoutやrefinementの条件を足すことで構造体が格納されていることを言えそう (ref. has_layout_val ) [6]

l ↦ v * v @ struct_t ... field ...
   * l' ↦ v' * to_val_or_somthing l' @ field

2024/10/21

  • ptr::write 後 ptr::read する関数の検証が出来ない原因の調査

    • rlsfでは mem::replace を使っているが中身が ptr::read / ptr::write なのでこれは問題

  • Q: type_of_ptr_read ( theories/rust_typing/shims.v )が弱すぎる

    • ptr::read の仕様に該当するものだが、事後条件で読み出した値の uninit が返ることになっている

      • ptr::write の事後条件から情報が減っている

    • enumの初期化周りの都合らしい

    • workaroundの検討

      • 強い条件をadmitしてshimとして使う

      • 特定の構造体について同様の関数を用意してよりつよい条件を証明する→この方針で進める

      • value_t (バイト列として解釈するための型)を使ったインタフェースをラップして使えないか

      • mem::replace を使っている限り &mut を持っているので大丈夫な可能性…​

  • 特定の構造体について同様の関数を用意して証明する

    • refinedrust.examples.rr_ex.generated と extras のtheoryが循環参照になる

      • post_generation_hook で coq/shims.v を generated/ にコピーする

2024/10/24

  • A: ptr::read の仕様が弱い問題 についてrlsfでは mem::replace が用いられており、 &mut が引数なので所有権に関する仮定が使え るので問題にならない

  • mem::replace の検証

  • Q: NonNull を使った検証でフロントエンドがパニックする

    • A: フロントエンドの制約で再帰的な出現が扱えない ( *const T が許されているので NonNull<T> も大丈夫かと思ったが違った)

  • Q: 静的な配列アクセスがサポートされていない？

    • case_studies/minivec では *mut T へ明示的にアドレス計算をして要素にアクセスしている

    • workaround: const fn で要素アクセスをラップして、only_spec

    • 配列のリテラルを含むコードを自動的にスキップするのか上手く行かなかった。

    • *mut T に変換して扱うか、RefindeRust側で配列の要素アクセスを扱えるようにする必要がある

2024/10/25

2024/10/31

  • 配列がサポートされていない問題のworkaround中

    • *mut T はRefinedRustの型システムでは [.line-through]# loc として扱われ、型情報が消えるため# アノテーションが適切でなかった rr_frontendがTに関連する定義を解析してくれず、手動でshimなどをインポートする必要がある

    • TODO: 生成されたスペック中の std_option_Option_ty の定義をファイルの上の方に持ってくる

  • self.first_free をrefineするCoqの型 block_matrix を修正

2024/11/01

  • Q: raw pointer dereferenceの事前条件に関する調査

    • かなり単純な例(silly_deref)についても自動化が働かず、手動で証明する方法を調査している

      • 適切な事前条件をRefinedRustの語彙で表す方法を調査している(アノテーションは main.rs を参照)

unsafe fn silly_deref(x: *mut usize) -> usize {
    *x
}

  • typed_place が残るので関連する補題などを調査中

2024/11/06

#[rr::params("l" : "loc", "vs", "z" : "Z")]
#[rr::args("l" @ "alias_ptr_t")]
#[rr::requires(#iris "l ◁ₗ[π, Owned false] PlaceIn vs @ (◁ value_t (st_of (int usize_t))) ∗ vs ◁ᵥ{π} z @ (int usize_t)")]
#[rr::returns("z")]
unsafe fn silly_deref(x: *mut usize) -> usize {
    *x
}

2024/11/07

  • 構造体のフィールドのraw poitner dereferenceについて調査中

    • l ◁ₗ[π, Owned false] -[b; pf; nf] @ (◁ FreeBlockHdr_ty) のようにして仕様はかけた

    • (*x).next_free = None; の事後条件として l ◁ₗ[π, Owned false] -[b; pf; #None] @ (◁ FreeBlockHdr_ty) を証明したい

      • ptr::write のshimを見ても事前条件は十分に見えるので、手動で証明する方法を探している

  • Q: raw pointer越しのフィールド更新の事後条件の証明方法

  • 抽象仕様の分離論理へのエンコードに関するメモを書いた

2024/11/08

  • 基本的な機能の実現に時間が掛かりそうなため、一度RefinedRustから離れて他の方法を検討する

    • 候補1: Verus

      • 既にmimallocの検証に使われており、他のケーススタディも豊富なため

    • 候補2: C言語実装をVSTで検証する

      • VSTを使った検証プロジェクトは多く、アロケータについても先行研究がある

  • verusによるmimallocの検証コードを読んでいた

2024/11/11

  • Verusのmimalloc検証コード読みつづき

  • verusによるリンクリストの検証例を作っていた

2024/11/13

  • verusによる単方向リンクリストの検証例を作った

  • ハマった点: 以下のエラメッセージがわかりにくかった

    • 実際には以下のスペックは間違っていて、正しくは …​ =~= old(self)@.push(v) だった点の修正 self@ と old(self)@ の同じ要素を含んでいる部分に関するアサーションを追加すれば解決した

    • struct の修飾子や spec の open / closed が関係しているかと思ってしまった

error: assertion failed
  --> ./singly_linked_list_trivial.rs:77:28
   |
77 |                     assert(self@ =~= seq![v].add(old(self)@));
   |                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ assertion failed

note: diagnostics via expansion:
      self.view() =~= empty().push(v).add(old(self).view())
          datatype is opaque here

2024/11/14

  • Verusのtokenized state machineに関する調査

    • 状態器械の定義とRustのコードがそれを満たしていることを保証する機能

    • 並行プログラムも検証できる

  • 使用例がマクロを多用しているのでminimal working exampleを作っている

    • cf. verus/source/rust_verify/state_machines/top_sort_dfs

    • Q: struct_with_invariant! マクロなしで Instance と実装を適切に関連付ける方法がわからない

      • verus-ex/tsm_silly.rs

2024/11/18

2024/11/21

  • Verusのraw pointerサポートについて書いた

2024/11/22

  • Verusによるrlsfの検証を開始

    • インデックス計算に関する定義を追加(wip)

  • Q: usizeに対するビット操作が一部用意されていない(leading_zeros/trailing_zeros)workaround

    • u64/u32などにはu64_leading_zerosとしてある

    • workaround: external_bodyの関数として事前事後条件でプラットフォーム毎に対応する *_leading_zeros などと同等の結果が得られることを言う

2024/11/25

  • Q: const定数の定義でconst fnが呼び出せない→仕様

    • A: 定数の代わりにconst fnを利用

test_verify_one_file! {
    #[test] test1_fails5 verus_code! {
        const fn f() -> u64 { 1 }
        const S: u64 = 1 + f();
    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::f` with mode exec")
}

  • Verusのビット演算に関する調査・インデックス計算の検証つづき

    • rotate_rightの形式仕様

    • usizeのビット演算が未サポートな問題のworkaround

2024/12/09

  • RQ: 対象のユースケースと直接関係しないが、 複数の連続しないメモリ領域をTLSFに追加して適切に処理されるかという問題も証明の対象として良さそう

  • 証明用の状態に関する情報(verus-ex/tlsf.rs GhostTlsf) の定義とメモリ領域の正当性の伝播の流れを設計

2024/12/10

2024/12/12

  • 標準ライブラリの整数に関する補題を調査した

    • ref. calc!, lemma_low_bits_mask_unfold

2024/12/13

  • Q: Tlsf::MAX_POOL_SIZE がOptionになっている意図がわからない

    • A: 特定の環境ではビットマップをあふれるようなサイズのメモリプールを扱いたいため

  • Q: DeallocToken内にヘッダ全体の権限があるとdellocate時にprev_phys_blockを通じて隣接ブロックを結合するのに必要な権限が得られない

    • option 1: ヘッダのアドレスをIDとするトークンをヘッダのPoinsToの代わりに発行する

      • 意味論的にも割り当てられた領域を管理するヘッダへの所有権をユーザーがもっているのはおかしい

  • インデックス計算用の関数のOptionを取り除いた

    • 正常なサイズを受け取ることを仮定できればtotalなため

  • insert_free_block_ptr_alignedの移植つづき

2024/12/16

  • ビット操作に関する証明方法の調査・試行錯誤

    • Q: usize::BITS を具体的な値として計算させる方法/あるいは計算を済ませるのに十分な性質の証明

  • Cargo projectを新しく分けた rlsf-verified

2024/12/17

2024/12/17

  • rlsfのインデックス計算の実装に関するインフォーマルな正当化を文書にまとめている ./rlsf-index-calc.html

2024/12/20

  • インデックス計算関連の補題・証明などをモジュールに切り出した

  • Verusのバグっぽい挙動のminimal exampleを作成

use vstd::prelude::*;
verus! {
const G: usize = 0;
struct B<const N: usize> {}
impl<const N: usize> B<N> {
    fn f() -> B<G> { B {} }
}
}

2024/12/23

  • 先日のバグの報告・workaround

  • インデックス計算に関する補題の証明(wip)

    • Verusで区間に関する理論を扱う方法を模索中

      • set_int_range で整数上の区間を Set として生成できるが、 Set に条件をつけて回るため区間同士の関係の扱いが煩雑になる

      • 半開区間しか扱わないため、集合に関する証明に落とすよりは始点・終点の議論で済ませたい

2024/12/24

  • インデックス計算に関する補題の証明(wip)

    • Q: BlockIndexでtype_invariantとしてstart<endを持つか

      • 現状、半開区間を表す型とその不変条件を別途用意しているが、一緒にしてもいいかも

    • Q: block index(tuple/BlockIndex)上の順序を導入したほうが見通しが良いかもしれない

      • ref. vstd::relations でSet<V>上の関係に関する形式化がある

2024/12/27

  • インデックスから計算されるブロックサイズの一意性の証明を進めた

2025/01/07

  • インデックス計算の検証に関するdesign doc(実装のインフォーマルな正当化)を書き進めた

2025/01/08

  • rlsf_verified::bits のリファクタリング(is_op_spec(arg, res) → op_spec(x) == res)

  • インデックス計算の検証に関するdesign docを書き進めた

    • 重要な行間は埋めることができたような気がしている

2025/01/09

  • ビット演算周りの補題の証明(wip)

    • bit maskと整数剰余との相互関係を使いたいので vstd::bits::lemma_u64_low_bits_mask_is_mod あたりをusizeに移植する必要がある

2025/01/16

  • 添字計算式の再考→有理数上での再定式化

  • Verus上での有理数の形式化

    • [verifier::type_invariant] はspec modeのものには使えず、数学的な対象には admit() などを使って公理化するのが標準的なよう

    • vstd::relations が == で同値関係が定義されていることを仮定しており、VerusはまだPartialEqのユーザー実装をサポートしていないため、 該当部分を再実装

2025/01/17

  • 必要最低限の有理数・半開区間に関する理論をVerus上で形式化できた

    • 公理化の過程で不整合を起こしてしまった

2025/01/20

  • 有理数の形式化を公理ベースから構造体+wf-ness述語(分母が0より大きいことを示す)に移行

    • Verusはspec modeのオブジェクトに不変条件を与えることが実質できないため

2025/01/22

  • broadcast use でパニックする問題の解決

    • broadcast group で指定する補題に broadcast proof fn を指定していなかった

  • 有理数上での諸補題の再構築

2025/01/23

  • 半開区間に関する補題を追加・証明

  • 区間演算について教えて頂いたので調査

    • 将来的に区間演算によって、空きリストの添字が適切な区間に落ちることを記述できると良さそう

    • 区間順序の導入は以前から同等のものを検討していた

      • 要求サイズから添字への関数の単調性を証明する際に役立ちそう

2025/01/24

  • 有理数に関する補題を整備

    • broadcast groupを追加

    • x ÷ y * y = xの証明

2025/01/28

  • search_suitable_free_block_list_for_allocation の移植・形式仕様

  • GhostTlsf の構造見直し

  • Tlsf::update_bitmap のFIXME原因調査

2025/01/30

  • 有理数の構成を再考

    • 正の整数を表す Pos をペアノ自然数と同様に構成し、 i > 0 なる int との全単射によって同一視する方法のPoCを作成 https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=5bff4aee0cbadc50299946b153da9369

      • この不整合 は、Verusの int にかかる形で公理を与えていたことが原因だったため、 Pos を使うことで公理的な形式化をする際に同様の原因による不整合を防げる

        • vstdのように間接的な方法を除いて int を含む公理を作るのはやめたほうが良い 詳細はわからないが以下のような公理をあたえると assert(false) が証明できる

struct Rational;
impl Rational {
    spec fn num() -> int;
    ...
    spec fn new(n: int, d: Pos) -> Self;
}
proof fn axiom_new(n: int, d: Pos)
ensures Rational::new(n, d).num() == n,
        ...
{admit()}

proof fn ex() {
    axiom_new(1, from_int(2));
    axiom_new(0, from_int(2));
    assert(false);
}

  • 以上の例から、公理的な形式化をする際にも struct Rational(int, Pos) のような定義とその上の演算・同値関係はVerus内で定義しておく必要があるように見える

    • また、公理的な形式化ではなくてもすべての定理の前提に requires r.wf() を要求せずにすむ

2025/02/03

  • Pos を使ったリファクタリング(branch: pos-type-refactor)

    • Pos に自動化が効かないため、四則演算について分母と分子への影響を整数で書いた補題をbroadcastする作業中

2025/02/07

  • リファクタリングが完了(自動化もある程度動くようになった)

  • half_open_range に一意性の証明で利用する補題を整備

2025/02/10

  • サーベイ

    • FSMによるアプローチがある

      • Coq上のFSM形式化によるもの: Li, Shaofeng, Lei Qiao, and Mengfei Yang. "Memory state verification based on inductive and deductive reasoning." IEEE Transactions on Reliability 70.3 (2021): 1026-1039.

      • BIPを用いたモデルベースのもの: Lu, Xiutai, et al. "Towards Formal Verification of Dynamic Memory Allocator Properties Using BIP Framework." Proceedings of the 5th International Conference on Computer Science and Application Engineering. 2021.

2025/02/13

  • update_bitmap() のFIXMEを解決

    • arr[index] = val のような要素の変更は未サポートで、 arr.set(index, val) のように書く

2025/02/14

  • Q: 有理数の四則演算に関する証明をある程度自動化したい

    • 同値関係がビルトインのものではないため、等式変形による証明が冗長

    • vstd::arithmetic::mul を参考にbroadcast proofを構成すれば達成できそう

      • Q: メソッドチェインにうまくtriggerを指定できなさそう

2025/02/17

  • アロケータの実装に近い形のリンクリストの検証PoC verus-ex/dll-ex.rs

    • Q: wf_node_ptr を事前条件とすると不整合が起こる

2025/02/27

  • A: この不整合は wf_node 中で含意と連言を取り違えて書いていたことが原因だった

2025/02/28

  • insert の実装と形式仕様が固まった

    • 証明用のメタデータの設計に関して気づいたことがあるため、このままPoCの検証を継続する

      • Mapのキーとして *mut T を int で代用するのがうまく行かなかった(コメント参照)

2025/03/03

  • Q: insert の事前条件として self.ptrs@ のすべての要素と異なっていることが必要だが、メモリ開放処理内で使う際にどのように証明できるか？

    • A: DeallocTokenにtype_invariantとproof methodとしてもっておく

  • リンクリストの検証PoCで insert の証明が完了

2025/03/05

  • PoCの移植開始

    • Q: PointsTo<FreeBlockHdr> からの PointsTo<BlockHdr> への変換

      • 必要に応じて PointsTo<FreeBlockHdr> から p.value().common で情報を見ることでworkaroundできそう

      • Q: prev_phys_block による単方向リストの構造を記憶する方法

        • option 1: PointsTo<FreeBlockHdr>の箇所を(PointsTo<BlockHdr>, PointsToRaw)で持つ

          • next_free,prev_freeを忘れてしまう問題がある

2025/03/10

  • リンクリスト検証PoCに push_front を追加

    • 追加するノードへの権限を PointsToRaw ではなく PointsTo で指定するように変更(初期化済みであることを強制)

  • この問題を解決するアイデア: ghost stateとして以下のようにhlistを持っておく

enum Hdrs { FBH(*mut FreeBlockHdr), UBH(*mut UsedBlockHdr) }
struct GhostTlsf { ..., all_ptrs: Seq<Hdrs>, ... }

  • この問題はVerusの開発によって修正された模様

2025/03/11

  • DeallocTokenの設計検討

    • deallocate() でDeallocTokenをムーブアウトすることでdouble freeを防ぐ

  • 執筆環境構築

    • 3ヶ月後を目処に文章を書いていく

2025/03/13

  • Q: ensures 節でプライベートなフィールドを使っているという旨のエラーが出たが心当たりがない(ref. FIXME@ linked_list.rs )

2025/03/14

  • A: この可視性のエラーは パブリックな関数の ensures 節で言及される構造体は、すべてのフィールドがパブリックでなくてはいけないという意味で、今回はフィールドが一つプライベートだったため起こった

  • 進捗状況をREADMEにまとめ始めた

    • 関数ごとの仕様・実装・証明の状況を示す表を追加した

  • リンクリストのPoCの移植(done)

    • unlink (ノードへのraw pointerを使ってDLLから切り離す)の検証(done)

2025/03/17

  • Rustのアラインメントに関する調査: ref. https://doc.rust-lang.org/reference/type-layout.html#size-and-alignment

    • Q: alloc::Layout に異常なアラインメントを指定できるか/RLSFではどのように扱われるか

      • A: size を丸めたあとに isize の範囲に収まれば、自由な2の冪を指定できる

      • A: RLSFでは先にオーバヘッドを計算し要求サイズを算出した後、空きブロックの探索に入るため、要求サイズが大きすぎて単純に探索が失敗する

2025/03/18

  • allocate() の移植

    • next_phys_block() ヘッダの情報からメモリ上で隣接するブロック(Free/Used)へのポインタを取得する

      • この機能の検証が現状の課題 以前 のアプローチを試している

        • e.g. fn next_phys_block(h: Hdrs) → Hdrs として、FreeBlockHdrが隣接しないという不変条件からUsedBlockHdrからはFreeBlockHdrしか返さないような実装とする

          • wf()かつnext_of(i).is_some()ならば権限も一緒に返す

          • wf()ではないユースケースでは、その場でポインタ演算によって対応する

      • Q: Verusが構造体へのraw pointerと権限をそのフィールドについて分割できれば、話が単純になる

        • e.g. struct T { x: S, y: U } について PointsTo<T> から PointsTo<S> と PointsTo<U> を取得

  • 形式化・証明などの進捗状況に関するセクションを追加

2025/03/24

  • allocate() の移植: 18日にそって next_phys_block の実装・検証

    • next_phys_block のユースケースとしては、

      1. first_freeから取り出したFreeBlockHdrから計算するケース

        • allocate時の余剰ブロックの分割・再登録処理

      2. ユーザから返却されたUsedBlockHdrから計算するケース

        • deallocate時の隣接ブロックの割当済みフラグ確認

    • 各々計算元のヘッダの状態は確認済み

    • 空きブロックの非隣接性から*mut Free→*mut Used, *mut Used→*mut Freeというふうにしか計算できないようにし、 wf-nessが不完全な箇所は、その場でポインタ演算の議論をする

2024/03/27

  • allocate() の移植: 概ね完了

    • 残りはnext_phys_blockのインタフェース周りとヘッダ更新時のメモリ書き込み

    • GhostTlsfとヘッダポインタからヘッダへの権限を取り出すための簡単な方法を作ったほうが良さそう

2024/03/28

  • allocate() の移植が完了

  • deallocate() の移植

1. llvm_fshr, https://llvm.org/docs/LangRef.html#llvm-fshr-intrinsic
2. rustc_plug, rustc_hirでdef_idを取得できないように見える
3. 完全な私見なので、検討の余地があります
4. 余談: 任意幅に一般化するなら、各幅についてlist boolとの間に全単射を構成したほうが良さそう。 stdppやsailなどcircular shiftの形式化を扱う実装を確認したが、listを使った実装になっていた
5. もう少し形式化を成熟させて証明を完了させる必要はあるがRefinedRustで検証を続けるために本質的な制約は無さそうの意
6. 余談: VSTだと直感的に l ↦ struct t { …​ fields } に近い書き方ができるのでハマってしまった