atomic_heap.v 3.81 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
72
73
74
75
76
              (λ '(v, q) _, v).
  Proof.
    iIntros (Φ) "Aupd". wp_let.
    iMod (aupd_acc with "Aupd") as ((v, q)) "[H↦ [_ Hclose]]"; first solve_ndisj.
    wp_load. iMod ("Hclose" $! () with "H↦"). done.
  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.
Ralf Jung's avatar
Ralf Jung committed
85
    iIntros (<-%of_to_val Φ) "Aupd". wp_let. wp_proj. wp_proj.
86
87
88
89
    iMod (aupd_acc with "Aupd") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
    wp_store. iMod ("Hclose" $! () with "H↦"). done.
  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.
Ralf Jung's avatar
Ralf Jung committed
98
    iIntros (<-%of_to_val <-%of_to_val Φ) "Aupd". wp_let. repeat wp_proj.
Ralf Jung's avatar
Ralf Jung committed
99
100
101
102
103
    iMod (aupd_acc with "Aupd") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
    destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail];
    iMod ("Hclose" $! () with "H↦"); done.
  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.