atomic_heap.v 5.69 KB
Newer Older
1
From iris.bi.lib Require Import fractional.
2
3
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
Ralf Jung's avatar
Ralf Jung committed
4
5
From iris.heap_lang Require Export derived_laws.
From iris.heap_lang Require Import notation proofmode.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.prelude Require Import options.
7
8

(** A general logically atomic interface for a heap. *)
9
Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
10
11
  (* -- operations -- *)
  alloc : val;
12
  free : val;
13
14
  load : val;
  store : val;
Ralf Jung's avatar
Ralf Jung committed
15
  cmpxchg : val;
16
  (* -- predicates -- *)
17
  mapsto (l : loc) (q: dfrac) (v : val) : iProp Σ;
18
19
  (* -- mapsto properties -- *)
  mapsto_timeless l q v :> Timeless (mapsto l q v);
20
  mapsto_fractional l v :> Fractional (λ (q : Qp), mapsto l (DfracOwn q) v);
21
  mapsto_as_fractional l q v :>
22
    AsFractional (mapsto l (DfracOwn q) v) (λ q, mapsto l (DfracOwn q) v) q;
23
  mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 - mapsto l q2 v2 - v1 = v2;
24
  (* -- operation specs -- *)
25
  alloc_spec (v : val) :
26
    {{{ True }}} alloc v {{{ l, RET #l; mapsto l (DfracOwn 1) v }}};
27
  free_spec (l : loc) (v : val) :
28
    {{{ mapsto l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
29
  load_spec (l : loc) :
Gregory Malecha's avatar
Gregory Malecha committed
30
     <<<  (v : val) q, mapsto l q v >>> load #l @  <<< mapsto l q v, RET v >>>;
31
  store_spec (l : loc) (w : val) :
32
33
     <<<  v, mapsto l (DfracOwn 1) v >>> store #l w @ 
      <<< mapsto l (DfracOwn 1) w, RET #() >>>;
34
35
36
  (* 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
37
38
39
  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. *)
Ralf Jung's avatar
Ralf Jung committed
40
  cmpxchg_spec (l : loc) (w1 w2 : val) :
41
    val_is_unboxed w1 
42
43
     <<<  v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ 
      <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
44
        RET (v, #if decide (v = w1) then true else false) >>>;
45
}.
Ralf Jung's avatar
Ralf Jung committed
46
Arguments atomic_heap _ {_}.
47

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

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.
60
Notation "e1 <- e2" := (store e1 e2) : expr_scope.
61

Ralf Jung's avatar
Ralf Jung committed
62
Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
63
64
65

End notation.

Ralf Jung's avatar
Ralf Jung committed
66
67
68
69
70
71
72
Section derived.
  Context `{!heapG Σ, !atomic_heap Σ}.

  Import notation.

  Lemma cas_spec (l : loc) (w1 w2 : val) :
    val_is_unboxed w1 
73
74
     <<<  v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ 
    <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
75
        RET #if decide (v = w1) then true else false >>>.
Ralf Jung's avatar
Ralf Jung committed
76
77
78
79
80
81
82
83
  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.

84
85
86
(** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
Definition primitive_alloc : val :=
  λ: "v", ref "v".
87
88
Definition primitive_free : val :=
  λ: "v", Free "v".
89
90
91
Definition primitive_load : val :=
  λ: "l", !"l".
Definition primitive_store : val :=
92
  λ: "l" "x", "l" <- "x".
Ralf Jung's avatar
Ralf Jung committed
93
94
Definition primitive_cmpxchg : val :=
  λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2".
95
96
97
98

Section proof.
  Context `{!heapG Σ}.

99
100
  Lemma primitive_alloc_spec (v : val) :
    {{{ True }}} primitive_alloc v {{{ l, RET #l; l  v }}}.
101
  Proof.
102
    iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l. iApply "HΦ". done.
103
104
  Qed.

105
106
107
108
109
110
  Lemma primitive_free_spec (l : loc) (v : val) :
    {{{ l  v }}} primitive_free #l {{{ l, RET #l; True }}}.
  Proof.
    iIntros (Φ) "Hl HΦ". wp_lam. wp_free. iApply "HΦ". done.
  Qed.

111
  Lemma primitive_load_spec (l : loc) :
Gregory Malecha's avatar
Gregory Malecha committed
112
     <<<  (v : val) q, l {q} v >>> primitive_load #l @ 
113
    <<< l {q} v, RET v >>>.
114
  Proof.
115
    iIntros (Φ) "AU". wp_lam.
116
    iMod "AU" as (v q) "[H↦ [_ Hclose]]".
117
    wp_load. iMod ("Hclose" with "H↦") as "HΦ". done.
118
119
  Qed.

120
  Lemma primitive_store_spec (l : loc) (w : val) :
Gregory Malecha's avatar
Gregory Malecha committed
121
     <<<  v, l  v >>> primitive_store #l w @ 
122
    <<< l  w, RET #() >>>.
123
  Proof.
124
    iIntros (Φ) "AU". wp_lam. wp_let.
125
    iMod "AU" as (v) "[H↦ [_ Hclose]]".
126
    wp_store. iMod ("Hclose" with "H↦") as "HΦ". done.
127
128
  Qed.

Ralf Jung's avatar
Ralf Jung committed
129
  Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
130
    val_is_unboxed w1 
Gregory Malecha's avatar
Gregory Malecha committed
131
     <<<  (v : val), l  v >>>
Ralf Jung's avatar
Ralf Jung committed
132
      primitive_cmpxchg #l w1 w2 @ 
133
134
    <<< 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
135
  Proof.
Ralf Jung's avatar
Ralf Jung committed
136
    iIntros (? Φ) "AU". wp_lam. wp_pures.
137
    iMod "AU" as (v) "[H↦ [_ Hclose]]".
138
    destruct (decide (v = w1)) as [Heq|Hne];
Ralf Jung's avatar
Ralf Jung committed
139
140
      [wp_cmpxchg_suc|wp_cmpxchg_fail];
    iMod ("Hclose" with "H↦") as "HΦ"; done.
Ralf Jung's avatar
Ralf Jung committed
141
  Qed.
142
End proof.
143
144
145
146
147

(* 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;
148
     free_spec := primitive_free_spec;
149
150
     load_spec := primitive_load_spec;
     store_spec := primitive_store_spec;
Ralf Jung's avatar
Ralf Jung committed
151
     cmpxchg_spec := primitive_cmpxchg_spec;
Ralf Jung's avatar
Ralf Jung committed
152
     mapsto_agree := primitive_laws.mapsto_agree |}.