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

(** A general logically atomic interface for a heap. *)
9
Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
10 11 12 13
  (* -- operations -- *)
  alloc : val;
  load : val;
  store : val;
14
  cmpxchg : val;
15 16
  (* -- predicates -- *)
  mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
17 18 19 20 21
  (* -- mapsto properties -- *)
  mapsto_timeless l q v :> Timeless (mapsto l q v);
  mapsto_fractional l v :> Fractional (λ q, mapsto l q v);
  mapsto_as_fractional l q v :>
    AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
22
  mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 - mapsto l q2 v2 - v1 = v2;
23
  (* -- operation specs -- *)
24 25
  alloc_spec (v : val) :
    {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
26
  load_spec (l : loc) :
27
    <<<  (v : val) q, mapsto l q v >>> load #l @  <<< mapsto l q v, RET v >>>;
28 29
  store_spec (l : loc) (w : val) :
    <<<  v, mapsto l 1 v >>> store #l w @ 
30
    <<< mapsto l 1 w, RET #() >>>;
31 32 33
  (* This spec is slightly weaker than it could be: It is sufficient for [w1]
  *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
  is outside the atomic triple, which makes it much easier to use -- and the
34 35 36
  spec is still good enough for all our applications.
  The postcondition deliberately does not use [bool_decide] so that users can
  [destruct (decide (a = b))] and it will simplify in both places. *)
37
  cmpxchg_spec (l : loc) (w1 w2 : val) :
38
    val_is_unboxed w1 
39
    <<<  v, mapsto l 1 v >>> cmpxchg #l w1 w2 @ 
40 41
    <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
        RET (v, #if decide (v = w1) then true else false) >>>;
42
}.
Ralf Jung's avatar
Ralf Jung committed
43
Arguments atomic_heap _ {_}.
44

45 46 47 48 49 50 51 52 53 54 55 56
(** Notation for heap primitives, in a module so you can import it separately. *)
Module notation.
Notation "l ↦{ q } v" := (mapsto l q v)
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.

Notation "l ↦{ q } -" := ( v, l {q} v)%I
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.

Notation "'ref' e" := (alloc e) : expr_scope.
Notation "! e" := (load e) : expr_scope.
57
Notation "e1 <- e2" := (store e1 e2) : expr_scope.
58

59
Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
60 61 62

End notation.

63 64 65 66 67 68 69 70
Section derived.
  Context `{!heapG Σ, !atomic_heap Σ}.

  Import notation.

  Lemma cas_spec (l : loc) (w1 w2 : val) :
    val_is_unboxed w1 
    <<<  v, mapsto l 1 v >>> CAS #l w1 w2 @ 
71 72
    <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
        RET #if decide (v = w1) then true else false >>>.
73 74 75 76 77 78 79 80
  Proof.
    iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
    iApply (aacc_aupd_commit with "AU"); first done.
    iIntros (v) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
    iIntros "$ !> HΦ !>". wp_pures. done.
  Qed.
End derived.

81 82 83 84 85 86
(** 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 :=
87
  λ: "l" "x", "l" <- "x".
88 89
Definition primitive_cmpxchg : val :=
  λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2".
90 91 92 93

Section proof.
  Context `{!heapG Σ}.

94 95
  Lemma primitive_alloc_spec (v : val) :
    {{{ True }}} primitive_alloc v {{{ l, RET #l; l  v }}}.
96
  Proof.
97
    iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l. iApply "HΦ". done.
98 99 100
  Qed.

  Lemma primitive_load_spec (l : loc) :
101 102
    <<<  (v : val) q, l {q} v >>> primitive_load #l @ 
    <<< l {q} v, RET v >>>.
103
  Proof.
104
    iIntros (Φ) "AU". wp_lam.
105
    iMod "AU" as (v q) "[H↦ [_ Hclose]]".
106
    wp_load. iMod ("Hclose" with "H↦") as "HΦ". done.
107 108
  Qed.

109 110
  Lemma primitive_store_spec (l : loc) (w : val) :
    <<<  v, l  v >>> primitive_store #l w @ 
111
    <<< l  w, RET #() >>>.
112
  Proof.
113
    iIntros (Φ) "AU". wp_lam. wp_let.
114
    iMod "AU" as (v) "[H↦ [_ Hclose]]".
115
    wp_store. iMod ("Hclose" with "H↦") as "HΦ". done.
116 117
  Qed.

118
  Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
119
    val_is_unboxed w1 
120
    <<<  (v : val), l  v >>>
121
      primitive_cmpxchg #l w1 w2 @ 
122 123
    <<< if decide (v = w1) then l  w2 else l  v,
        RET (v, #if decide (v = w1) then true else false) >>>.
Ralf Jung's avatar
Ralf Jung committed
124
  Proof.
125
    iIntros (? Φ) "AU". wp_lam. wp_pures.
126
    iMod "AU" as (v) "[H↦ [_ Hclose]]".
127
    destruct (decide (v = w1)) as [Heq|Hne];
128 129
      [wp_cmpxchg_suc|wp_cmpxchg_fail];
    iMod ("Hclose" with "H↦") as "HΦ"; done.
Ralf Jung's avatar
Ralf Jung committed
130
  Qed.
131
End proof.
132 133 134 135 136 137 138

(* NOT an instance because users should choose explicitly to use it
     (using [Explicit Instance]). *)
Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
  {| alloc_spec := primitive_alloc_spec;
     load_spec := primitive_load_spec;
     store_spec := primitive_store_spec;
139
     cmpxchg_spec := primitive_cmpxchg_spec;
140
     mapsto_agree := gen_heap.mapsto_agree  |}.