atomic_heap.v 3.87 KB
Newer Older
1 2 3 4 5 6 7 8
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

(** A general logically atomic interface for a heap. *)
Ralf Jung's avatar
Ralf Jung committed
9
Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
10 11 12 13
  (* -- operations -- *)
  alloc : val;
  load : val;
  store : val;
Ralf Jung's avatar
Ralf Jung committed
14
  cas : val;
15 16 17 18 19 20 21 22 23 24 25 26
  (* -- predicates -- *)
  (* name is used to associate locked with is_lock *)
  mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
  (* -- general properties -- *)
  mapsto_timeless l q v : Timeless (mapsto l q v);
  (* -- operation specs -- *)
  alloc_spec v :
    {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
  load_spec (l : loc) :
    atomic_wp (load #l)%E
              (λ '(v, q), mapsto l q v)
              (λ '(v, q) (_:()), mapsto l q v)
27
               
28
              (λ '(v, q) _, v);
Ralf Jung's avatar
Ralf Jung committed
29 30 31
  store_spec (l : loc) (e : expr) (w : val) :
    IntoVal e w 
    atomic_wp (store (#l, e))%E
32 33
              (λ v, mapsto l 1 v)
              (λ v (_:()), mapsto l 1 w)
34
               
35
              (λ _ _, #()%V);
Ralf Jung's avatar
Ralf Jung committed
36 37 38
  cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
    IntoVal e1 w1  IntoVal e2 w2 
    atomic_wp (cas (#l, e1, e2))%E
Ralf Jung's avatar
Ralf Jung committed
39 40
              (λ v, mapsto l 1 v)
              (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
41
               
Ralf Jung's avatar
Ralf Jung committed
42
              (λ v _, #(if decide (v = w1) then true else false)%V);
43
}.
Ralf Jung's avatar
Ralf Jung committed
44
Arguments atomic_heap _ {_}.
45 46 47 48 49 50 51 52

(** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
Definition primitive_alloc : val :=
  λ: "v", ref "v".
Definition primitive_load : val :=
  λ: "l", !"l".
Definition primitive_store : val :=
  λ: "p", (Fst "p") <- (Snd "p").
Ralf Jung's avatar
Ralf Jung committed
53 54
Definition primitive_cas : val :=
  λ: "p", CAS (Fst (Fst "p")) (Snd (Fst "p")) (Snd "p").
55 56 57 58 59 60 61 62 63 64 65 66 67 68

Section proof.
  Context `{!heapG Σ}.

  Lemma primitive_alloc_spec v :
    {{{ True }}} primitive_alloc v {{{ l, RET #l; l  v }}}.
  Proof.
    iIntros (Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
  Qed.

  Lemma primitive_load_spec (l : loc) :
    atomic_wp (primitive_load #l)%E
              (λ '(v, q), l {q} v)%I
              (λ '(v, q) (_:()), l {q} v)%I
69
               
70 71
              (λ '(v, q) _, v).
  Proof.
72 73 74
    iIntros (Q Φ) "? AU". wp_let.
    iMod (aupd_acc with "AU") as ((v, q)) "[H↦ [_ Hclose]]"; first solve_ndisj.
    wp_load. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
75 76
  Qed.

Ralf Jung's avatar
Ralf Jung committed
77 78 79
  Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
    IntoVal e w 
    atomic_wp (primitive_store (#l, e))%E
80 81
              (λ v, l  v)%I
              (λ v (_:()), l  w)%I
82
               
83 84
              (λ _ _, #()%V).
  Proof.
85 86 87
    iIntros (<-%of_to_val Q Φ) "? AU". wp_let. wp_proj. wp_proj.
    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
    wp_store. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
88 89
  Qed.

Ralf Jung's avatar
Ralf Jung committed
90 91 92
  Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
    IntoVal e1 w1  IntoVal e2 w2 
    atomic_wp (primitive_cas (#l, e1, e2))%E
Ralf Jung's avatar
Ralf Jung committed
93 94
              (λ v, l  v)%I
              (λ v (_:()), if decide (v = w1) then l  w2 else l  v)%I
95
               
Ralf Jung's avatar
Ralf Jung committed
96 97
              (λ v _, #(if decide (v = w1) then true else false)%V).
  Proof.
98 99
    iIntros (<-%of_to_val <-%of_to_val Q Φ) "? AU". wp_let. repeat wp_proj.
    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
Ralf Jung's avatar
Ralf Jung committed
100
    destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail];
101
    iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
102 103
  Qed.

104 105 106
  Definition primitive_atomic_heap : atomic_heap Σ :=
    {| alloc_spec := primitive_alloc_spec;
       load_spec := primitive_load_spec;
Ralf Jung's avatar
Ralf Jung committed
107 108
       store_spec := primitive_store_spec;
       cas_spec := primitive_cas_spec |}.
109
End proof.