atomic_heap.v 2.62 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
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. *)
Structure atomic_heap Σ `{!heapG Σ} := AtomicHeap {
  (* -- operations -- *)
  alloc : val;
  load : val;
  store : val;
  (* -- 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)
               
              (λ '(v, q) _, v);
  store_spec (l : loc) (w : val) :
    atomic_wp (store (#l, w))%E
              (λ v, mapsto l 1 v)
              (λ v (_:()), mapsto l 1 w)
               
              (λ _ _, #()%V);
}.

(** 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").

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
               
              (λ '(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.

  Lemma primitive_store_spec (l : loc) (w : val) :
    atomic_wp (primitive_store (#l, w))%E
              (λ v, l  v)%I
              (λ v (_:()), l  w)%I
               
              (λ _ _, #()%V).
  Proof.
    iIntros (Φ) "Aupd". wp_let. wp_proj. wp_proj.
    iMod (aupd_acc with "Aupd") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
    wp_store. iMod ("Hclose" $! () with "H↦"). done.
  Qed.

  Definition primitive_atomic_heap : atomic_heap Σ :=
    {| alloc_spec := primitive_alloc_spec;
       load_spec := primitive_load_spec;
       store_spec := primitive_store_spec |}.
End proof.