Skip to content

Instantly share code, notes, and snippets.

@pandaman64

pandaman64/memory_model.md

Last active December 18, 2020 07:54
Show Gist options
  • Save pandaman64/40c18e7ec3eb337bfb23ea3ddbf56411 to your computer and use it in GitHub Desktop.
Save pandaman64/40c18e7ec3eb337bfb23ea3ddbf56411 to your computer and use it in GitHub Desktop.
Download ZIP
papers on formalized memory models
Raw
memory_model.md

色々メモリモデル

コンパイラ（LLVM）のメモリモデル

✅ Reconclining high-level optimization and low-level code in LLVM (https://dl.acm.org/doi/10.1145/3276495)

Lee, Hur, Jung, Liu, Regehr, Lopes.

  • 低レベル言語（C, C++, Rust）のコンパイラのメモリモデルには二つの相反する目標がある
    • high-level optimization
      • 最適化したい
      • 例:
        • load/storeを移動
        • constant? propagationしたい
    • low-level code
      • ユーザはポインタを使って好きなことをしたい
      • 例:
        • ポインタ演算
          • structへのポインタからメンバへのポインタを計算する
          • 配列全体へのポインタから要素へのポインタを・・・
        • integer pointer cast
          • ポインタ値のハッシュを計算して云々
  • ふつうのメモリモデル(flat memory model)だとつらい

つらい例:

int x[1], y[1];
int *end_x = x + 1; // xのpast-oneを指す

if (x + 1 == y) {
    // ここに来ることはある？
}

最適化の観点からはx + 1 == yをfalseに置き換えて（それぞれ別のメモリブロックを指すポインタなのでequivalentなポインタとはならないはず）． しかしメモリモデルによってはyがxの直後に配置されてるとき，x + 1とyのアドレスはequalな値をもち，trueになりうる． LLVMではポインタ値がequalならポインタとしてequivalentと仮定して最適化を行ってしまうのでmiscompilationが起きる（LLVMの最適化は現行のメモリモデルに対してunsoundである）．

  • やったこと
    • 新しいメモリモデルを定義した
      • Deferred Bounds Checking
      • Twin allocation
    • そのモデルに合わせてLLVM IRのoperational semanticsを定義した
    • メモリモデルに対してsoundとなるようLLVMの最適化を修正した
      • miscompilationを無くせた
      • パフォーマンスは大差ない
      • 修正は千数百行（大きくない）

ポイント

  • ポインタは二種類考える．
    • Logical Pointer. メモリブロック + オフセットで管理する．
      • Logical Pointerに対するinbounds演算は計算元・計算結果がinboundsじゃないとpoisonになる（immediate）
      • 違うメモリブロックに属するポインタの比較はfalse (x + 1 != y)
      • 実はtrueでもいい（非決定的）
    • Physical Pointer. メモリアドレス．基本的にはinteger to pointer castの産物．
      • inboundsチェックはdereferenceのときだけ(deferred)
      • すると操作の移動が自由にできて良いらしい
  • LLVMが確保したメモリアドレスを推測できないようにしたい．
    • できてしまうと変なdependencyが生じてしまうので最適化が難しい/unsoundになる
      • load/storeの移動とか
    • 有限なメモリ空間でやりたい．
    • Twin Allocationは二つメモリ領域を確保していずれかを非決定的に使う
      • メモリアドレスを推測するようなコードは1/2の確率で使ってはいけない方の領域にアクセスするのでUB
      • 実は3つ以上必要になることもあるらしい
  • Note: 非決定的な実行パスのうち一つがUBならば全体がUBとなる
    • 例: x + 1 == yの結果は非決定的にtrue/falseのいずれかをとる．
    • if (x + 1 == y) { ...UB... }というコードはtrue時にUBとなるのでこのif文全体がUB．
    • するとコンパイラはこのif自体をeliminateできてさらなる最適化に繋がる．

気になるrelated works

✅n2263: Clarifying Pointer Provenance v4

Kayvan Memarian, Victor Gomes, Peter Sewell. University of Cambridge

  • Cerberusやってる人たち

  • 提案であってこれで決まるというわけではないが，よく考えられているので参考になりそう

  • "Tracking of provenance in the abstract machine is therefore necessary to make these compilers sound with respect to the standard."

  • pointer provenance (ポインタがどこ由来か)の話

    • エイリアス解析 + 以降の最適化に有用
    • empty/ID
    • empty provenanceでアクセスするのはUB

  • ポインタ値（integer castした値）が等しくても異なるprovenanceを持つポインタはエイリアスしないと（コンパイラによって）みなされる

  • 異なるprovenanceを持つポインタ同士の==比較はindeterminate

    • integer castした場合は値だけで比較（provenanceを気にしない）

  • pointer → integer (+alithmetic) → pointer castしてもprovenanceは保たれる

    • でもXOR linked listは駄目って書いてある
    • コンパイラは大変そうだけどverificationの文脈なら問題ないのかな

  • inter-object subtractionはprovenanceを与えない

  • memcpy(-like)はprovenanceもコピーする

  • provenanceはdata-flowのみに依存

    • 整数値とポインタを比較してその整数値をポインタとして使うとかを禁止っぽい
    • ポインタ同士の値を比較してもprovenance与えないとか

  • per-allocation provenance

    • subobject同士は同じprovenanceを持つ
    • Rustならper-subobject provenanceでいけるのでは
      • どうせborrow stack的なのをやっていくので

  • 最後に詳細なsemanticsが載ってる

気になるrelated work

Verification toolのメモリモデル

✅Automatic Proof-producing Abstraction of C Code, Chapter 7, Heap abstraction

AutoCorresの博論

  • ポインタといっても使うには色々条件あるので（アラインメント）素直なモデル（byte-level heap）だと（証明が）（Isabelle/ユーザにとって）つらくない？という話
    • 型安全な部分のコードはIsabelle/ユーザが簡単に扱えるメモリモデルで済むようにしよう
    • 各型ごとにmapを持つ（かんたん！）
    • 簡単化の正当性は？
      • 元のプログラムは簡単なプログラムのrefinement
      • 簡単化したプログラムで成立する性質は元のプログラムでも成立

お気持ち: （普通のCコードに対して）C-parserの吐くSimplがきわめて規格化されてるのでそれに対してパターンマッチしてあげればうまくいくんだな

プログラムのabstraction． Simplの状態空間を取り換えたプログラムに翻訳してそう．

  • Tuchのheap lifting model
    • "Types, Bytes, and Separation Logic"
    • メモリの各バイトに型タグがついている
      • 先頭バイトはCの型
      • 以降のバイトはfootprint（続きであることを表す）
      • Tuchの実装では型タグは複数付くが，AutoCorresではその一番外側（構造体）のみを使ってるっぽい
        • おそらく，構造体のメンバは構造体の型タグとメンバ型のタグがつく，みたいなことだと思うんだが不明 TODO: 調べる
    • ソースに対するアノテーションコメントで型タグをアップデートできる
      • これでtype punningやmalloc結果の型を付ける
  • Tuchはseparation logicを使ってるがそこは簡略化
  • Tuchのメモリモデルの推論規則が使える
    • 例: heap_lift s p = Some v implies c_guard p
    • →リフトしたメモリに存在するならアラインメントとかはOK
    • 例: heap_lift s p = Some v' implies heap_lift (write_bytes p v s) = (heap_lift s)(p := Some v)
    • →メモリへの書き込みがfunctional updateになって簡単！
  • Limitations of the heap lifting approach
    • 書き込みがたくさんになると項が大きすぎてIsabelleで扱うのがつらい
    • 「その他」が変わらないことをいうのが難しい
      • Tuchはseparation logicを使って対処
    • 普通の（型安全な）関数はliftした後のメモリだけ見れば十分であってほしい
      • これ同意
  • heap abstraction
    • split heapとbyte level heapを行き来できるようにする
    • split heap: 各型Tについて
      • is_valid_T :: T ptr => bool: 型Tのメモリにリフトしてvalid
      • heap_T :: T ptr => T: 型Tの値をメモリから取得
      • の二つを用意する
      • T ptr => T optionの関数一つ用意するより便利らしい
        • アドレスはあまり変わらないのに対し値は良く変わるので分割すると良いとのこと
      • split heapに対するread/writeの前にはポインタのvalidnessについてガードを入れる必要がある
      • c_guardの代わりにis_valid_Tを使う
  • abstracted programsの性質の証明をconcrete programsに生かす
    • corres_HA述語がある
      • concrete programはheap abstracted programの振る舞いのうち一部のみをとるという述語
    • corres_HAが成立するならば，abstracted programで成立する性質はconcrete programでも成立
    • corres_HAとかに関するルールがいっぱいある
    • これらのルールを用いてsyntax-directedにプログラムをabstractする
      • hrs_memみたいなc-parserの生の操作を関数適用やupdateにabstractできるよ！
  • heap abstractionによってstatementが簡単になるからIsabelle/HOLがサクっとやってくれるよ！
  • 型安全でないコードではabstracted programに含まれたガードが成立しないから大丈夫
  • "our work allows high-level reasoning on byte-level heaps without requiring the user to interact with such machinery."
  • abstracted program内でconcrete programを呼ぶ
    • abstractすると今の抽象状態になる具体的状態を非決定的に一つとって実行
    • 非決定的でexistentialがでるんだが，このexistentialを除去する補題が示せるのでOK
  • concrete program内でabstract programを呼ぶ
    • 出力を非決定的に具体化
  • "Tuch et al.’s original framework supports reasoning about programs that dereference pointers to fields of structures. Our simplified version of Tuch et al.’s work and method of program rewriting cannot deal with this particular case at this time." とのこと

気になるrelated works

  • Tuchはbyte-level heap + separation logicをやった
    • "Formal Memory Models for Verifying C Systems Code" 博論
    • "Structured Types and Separation Logic"
    • "Formal verification of C systems code: Structured types, separation logic and theorem proving"
    • "Types, Bytes, and Separation Logic" これはc-parserのNorrishもいる
  • Burstall-Bornat style heapが何のことか気になる
    • "The idea to use separate heaps for separate pointer types and structure fields" ("A Unified Memory Model for Pointers"より)とのこと
    • Burstall. "Some techniques for proving correctness of programs which alter datastructures"
    • Bornat. "Proving pointer programs in Hoare Logic."
    • Mehta and Nipkow. "Proving pointer programs in higher-order logic."
  • Klein et al.'s separation algebra
    • "Mechanised Separation Algebra"

✅A Unified Memory Model for Pointers

Tuch, KleinらNICTAによる論文

  • 型安全なプログラム（プログラミング言語）では異なる型のポインタはエイリアスしない
    • 各型ごとに分割されたヒープを持つことで検証できる
  • OSコードはわざと型安全性を破るようなコードが登場する
    • 検証のsoundnessを保つにはより生に近いメモリモデルが必要
  • できるだけ（便利な）型付きヒープを使いたい
    1. どのmemory locationがどの型に対応するか
    2. "We then need to know that the memory lay-out provides a disjoint layout of values" ?
    3. ↑の情報を使って型無しヒープから型付きのヒープに変換する方法
    • ヒープ更新の推論規則も必要
  • 各C型について
    • Isabelle型
    • typ-tagの一バリアントがある
      • typ-size :: typ-tag => natがある（各型はfixed sizeをもつ）
  • heap-typ-desc :: addr => typ-tag optionがある
    • heap-typ-desc a = Some tはアドレスaが型tの値の先頭である，の意
    • 証明用の存在でありtagged memoryとは違う
      • semanticsには関与しない
      • a history variable (is 何)
      • そもそもtagged memoryが分からんね
    • wf-heap :: heap-type-desc => boolはheap type descriptionがwell formedかどうか
  • lift :: heap-mem => 'a::c-type ptr => 'aが型無しヒープを各C型'aのヒープに持ち上げる
  • lift_c :: heap-state => 'a::c-type ptr => 'a optionはheap descriptionを気にするより強いやつ
    • lift_cを使うと型付きヒープをただのマップっぽく扱えることが証明できる
    • 異なる型同士のポインタがエイリアスしないことも示せる（思ったことも見よ）
    • ↑のルールをIsabelleのsimplification ruleに追加してあげると証明が簡単！
  • 例のところに「1.5年月かけて作りました」と書いてあり，こわい
  • tagged unionなども扱いたいねとのこと
  • malloc/free自体の正当性も証明できる！と言っている

小ネタ

  • Isabelleで'a itselfはTYPE('a)というただ一つの値を持つ型
    • 型を値レベルに持ってくために使われてるっぽい

思ったこと

  • type tagはsemanticsに関与しないと書いてあるが，Pointer Provenanceを考えるとtype tagもsemanticsの一部だと思うのねん
    • Rustならborrow stackも入る
    • 「ポインタ値」を扱う操作(integer cast)はtagに無関係になりそう
  • interior pointerの扱い
    • この論文のwell-formednessではある番地は同時に一つの型のメモリ領域にのみ属する
    • この場合interior pointerがうまく扱えない
    • 例: 
      struct A {
  int x;
  int y;
};

struct A s = { .x = 10, .y = 20 };
struct A *pA = &s;
int *px = &s.x;
    • pxのように大きなアロケーションの一部を指すポインタをinterior pointerと呼ぶ
    • このとき，pAとpxはアドレス番地として同じだが異なる型として有効な別のポインタになる．
    • 他の例: 配列の要素1個へのポインタは配列全体に対するinterior pointer
    • この論文のモデルではinterior pointerを簡単に扱えない
      • 異なる型のポインタだがエイリアスする
      • 結局byte levelに落とさないといけなくなる
    • AutoCorresも同じつらみがありそうだが・・・

気になるrelated work

  • Norrish. "C formalised in HOL" 博論
    • Cの詳しいメモリモデル
  • "Ccured: type-saferetrofitting of legacy software"
    • statically verifyできなかったポインタの使用に対して動的チェックを挿入する
    • ある意味Rustっぽい
      • 配列のインデックスチェックとか
  • Hohmuth et al. "Applying source-code verification toa microkernel — the VFiasco project."
    • エイリアス等も扱ったC++のセマンティクス

✅Types, Bytes, and Separation Logic

Tuch, Klein, NorrishらNICTAによる論文

  • "Our aim is to make verification part of the engineering process"
    • 良い言葉
  • 型付きヒープによってinter-type aliasingは解消できるけどintra-type aliasingは依然として問題
  • intra-type aliasingを記述するためにSeparation Logicを使おう
  • Separation Logicの述語をIsabelleにShallow embeddingしたよ
    • Isabelleの他の述語と混ぜてかける
    • Separation Logicの述語とヒープのリフトの関係を表す定理を色々示した

✅Strucutured Types and Separation Logic

Tuch

  • 構造体のフィールドへのポインタってinter-type aliasing発生するけどどうすんの
  • heap type descriptionを多段にしてフィールドの型と全体の型を同時に扱えるようにする
  • フィールドのアクセス/アップデートを用意する
  • 型Aが型Bの中に含まれるとき A < B
    • A < B かつB型のポインタ経由で書き換えるとき
      • Aのヒープも書き換え
    • A < B かつA型のポインタ経由で書き換えるとき
      • これがBのフィールドなら，Bのヒープも書き換え
      • オフセット前のアドレスのheap type descriptionで判定っぽい？
    • AとBが関係ない場合はそのまま
  • Separation Logicのshallow embeddingもやります

気になるrelated work

  • Siff, Chandra, et.al. "Coping with type casts in C"
    • physical subtyping?の話とのこと

✅Proving Pointer Programs in Hoare Logic (2000)

Bornatの論文

頑張りがあり，大変そう．

  • "The power of the Floyd/Hoare treatment of imperative programs lies in its use of variable substitution to capture the semantics of assignment"
    • 事前条件/事後条件が項への代入で結び付けられるということ
  • ポインタを使った再帰的プログラムの検証のつらみ
    1. pointer aliasing
    2. heap data structuresに対するassertionが帰納的な式になる
    3. 代入の局所性がheapについてのassertionにおいても保たれる?ことの証明が複雑
  • 人が考えるようにメモリについて機械に推論させたい
    • メモリ列ではなくオブジェクトや配列として
  • コンポーネント .f と配列インデックス [i] を同一視してやる
    • コンポーネントが異なればエイリアスしない (e.g. .f vs .g)
      • 代入を一段階内側に入れれる→inductive?
    • コンポーネントが同じときは親が同じかを見る必要がある
    • "it makes possible a formal treatment of object component substitution into inductively defined formulae"

気になるrelated work

  • "proof carrying code"
    • Necula G. and Lee P.: Safe, Untrusted Agents using Proof-Carrying Code. Mobile Agentsand Security
    • Appel A.W., Felty A.P.: A Semantic Model of Types and Machine Instructions for Proof-Carrying Code
  • Burstall R.M.: Some techniques for proving correctness of programs which alter datastructures.

Rustメモリモデルの形式化

👀Leveraging Rust Types for Modular Specification and Verification

ETH Zurich

👀Stacked Borrows

Ralf Jung

  • Stacked Borrows, an operational semantics for memory accesses in Rust
  • Implemented an interpreter, testing the Rust standard library
  • alias informationを使って最適化したい vs unsafe Rust
    • 特にreorderingができると後の最適化に繋がる
    • Rustのaliasing ruleを使うと intraprocedural に最適化を正当化できる
    • unsafe Rustでは↑のaliasing ruleを破れる
      • 破るようなプログラムはUBなので最適化してヨシ！
      • となるようなoperational semanticsを作りました
  • borrow checkerのdynamic版への拡張
    • per-location (dynamic) stack
    • lifetimeからは独立
      • lifetime checkによってunsafeプログラムの意味論が変わってほしくない
      • lifetimeは消去されるのでoptimization phaseでは依存できない
  • "every use of the reference (and everything derived from it) must occur before the next use of the reference (after the reference got created)"
    • "stack principle"
  • 各参照にポインタIDをタグとして割り振る
    • 生ポインタはタグを持たない（タグ⊥を持つ）
  • スタックで使ってもいいborrowを管理する
    • Unique(t): タグtの&mut Tを作った
    • SharedRW(t): *mut Tを作った
    • SharedRO(t): &Tを作った
  • "使った"参照はスタックトップに来る（基本的には）
    • その参照よりも上にあった参照はスタックから失われるので使用不可
    • Reborrowをuseとみなすことで「一つ前のアイテムがreferent」の関係を維持できる
    • read accessの場合はその上にSharedRO(_)が乗っててもいい
      • SharedROはスタックトップから（0個以上連続して）のみ登場する
  • 参照の引数は関数のプロローグで"retagging"される
    • 素性が真っ当な参照が渡されているのを保証したい
    • retagはreborrowを自身に対して行っているのと同じ
      • 引数の参照がフレッシュなタグを持つようになる
      • "Reconclining high-level..."でローカル変数に対して時間を付与しているのと気持ち似ている
    • "Basically, any time a reference łentersž our scope, it should get retagged" でどこでretagするか決めてる
  • protectors
    • Rustにおいて引数の参照は関数の実行をoutliveする
    • 関数の実行は参照をprotectしており，protectedな参照をpopするのはUB
    • エピローグにretagするとかじゃ駄目なんだろうか
      • 参照値自体は変わりうるがoutliveするのは引数で渡されたlocationなのでアレそう？
  • Rustにおけるinterior mutabilityはUnsafeCellを経由しなければいけない
    • UnsafeCellによるアノテートをStacked Borrowsでも使うよ
    • &UnsafeCellを作った時はSharedROではなくSharedRWが追加される
      • ただし，参照の作成はread accessに数えず，referentの次に追加（スタックトップではない）
      • RefCellとの兼ね合い
      • 生ポインタも同じ
  • read accessはUniqueをdisableするだけ（SharedRWはそのまま残す）
    • そうでないと不当にUBになるコードがある

👀RustHorn: CHC-based Verification for RustPrograms

Matsushita

  • Rust-style ownershipのところ"A safe dialect of C"のciteがダブってる

気になるrelated work

  • Suenaga, K., Kobayashi, N.: Fractional ownerships for safe memory dealloca-tion.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment