atomic.v 4.64 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
From iris.algebra Require Import upred_big_op.
From iris.prelude Require Export coPset.
From iris.proofmode Require Import tactics.
Import uPred.

Section atomic.
  Context `{irisG Λ Σ} {A: Type}.

  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
  Definition atomic_triple
             (α: A  iProp Σ)
             (β: A  val _  iProp Σ)
             (Ei Eo: coPset)
             (e: expr _) : iProp Σ :=
    ( P Q, (P ={Eo, Ei}=>  x:A,
                                α x 
                                ((α x ={Ei, Eo}= P) 
                                 ( v, β x v ={Ei, Eo}= Q x v))
            ) - {{ P }} e @  {{ v, ( x: A, Q x v) }})%I.

  (* Weakest-pre version of the above one. Also weaker in some sense *)
  Definition atomic_triple_wp
             (α: A  iProp Σ)
             (β: A  val _  iProp Σ)
             (Ei Eo: coPset)
             (e: expr _) : iProp Σ :=
    ( P Q, (P ={Eo, Ei}=>  x,
                              α x 
                              ((α x ={Ei, Eo}= P) 
                               ( v, β x v ={Ei, Eo}= Q x v))
            ) - P - WP e @  {{ v, ( x, Q x v) }})%I.

  Lemma atomic_triple_weaken α β Ei Eo e:
    atomic_triple α β Ei Eo e  atomic_triple_wp α β Ei Eo e.
  Proof.
    iIntros "H". iIntros (P Q) "Hvs Hp".
    by iApply ("H" $! P Q with "Hvs").
  Qed.

  Arguments atomic_triple {_} _ _ _ _.
End atomic.

From iris.heap_lang Require Export lang proofmode notation.

Section incr.
  Context `{!heapG Σ} (N : namespace).

  Definition incr: val :=
    rec: "incr" "l" :=
       let: "oldv" := !"l" in
       if: CAS "l" "oldv" ("oldv" + #1)
         then "oldv" (* return old value if success *)
         else "incr" "l".

  Global Opaque incr.

  (* TODO: Can we have a more WP-style definition and avoid the equality? *)
  Definition incr_triple (l: loc) :=
    atomic_triple (fun (v: Z) => l  #v)%I
                  (fun v ret => ret = #v  l  #(v + 1))%I
                  (nclose heapN)
                  
                  (incr #l).

  Lemma incr_atomic_spec:  (l: loc), heapN  N  heap_ctx  incr_triple l.
  Proof.
    iIntros (l HN) "#?".
    rewrite /incr_triple.
    rewrite /atomic_triple.
    iIntros (P Q) "#Hvs".
    iLöb as "IH".
    iIntros "!# HP".
    wp_rec.
    wp_bind (! _)%E.
    iVs ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
    wp_load.
    iVs ("Hvs'" with "Hl") as "HP".
    iVsIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
    iVs ("Hvs" with "HP") as (x') "[Hl Hvs']".
    destruct (decide (x = x')).
    - subst.
      iDestruct "Hvs'" as "[_ Hvs']".
      iSpecialize ("Hvs'" $! #x').
      wp_cas_suc.
      iVs ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
      iVsIntro. wp_if. iVsIntro. by iExists x'.
    - iDestruct "Hvs'" as "[Hvs' _]".
      wp_cas_fail.
      iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
      iVsIntro. wp_if. by iApply "IH".
  Qed.
End incr.

From iris.heap_lang.lib Require Import par.

Section user.
  Context `{!heapG Σ, !spawnG Σ} (N : namespace).

  Definition incr_2 : val :=
    λ: "x",
       let: "l" := ref "x" in
       incr "l" || incr "l";;
       !"l".

  (* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
  Lemma incr_2_safe:
     (x: Z), heapN  N -> heap_ctx  WP incr_2 #x {{ _, True }}.
  Proof.
    iIntros (x HN) "#Hh".
    rewrite /incr_2.
    wp_let.
    wp_alloc l as "Hl".
    iVs (inv_alloc N _ (x':Z, l  #x')%I with "[Hl]") as "#?"; first eauto.
    wp_let.
    wp_bind (_ || _)%E.
    iApply (wp_par (λ _, True%I) (λ _, True%I)).
    iFrame "Hh".
    (* prove worker triple *)
    iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
    rewrite /incr_triple /atomic_triple.
    iSpecialize ("Hincr"  $! True%I (fun _ _ => True%I) with "[]").
    - iIntros "!# _".
      (* open the invariant *)
      iInv N as (x') ">Hl'" "Hclose".
      (* mask magic *)
      iApply pvs_intro'.
      { apply ndisj_subseteq_difference; auto. }
      iIntros "Hvs".
      iExists x'.
      iFrame "Hl'".
      iSplit.
      + (* provide a way to rollback *)
        iIntros "Hl'".
        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
      + (* provide a way to commit *)
        iIntros (v) "[Heq Hl']".
        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
    - iDestruct "Hincr" as "#HIncr".
      iSplitL; [|iSplitL]; try (iApply wp_wand_r;iSplitL; [by iApply "HIncr"|auto]).
      iIntros (v1 v2) "_ !>".
      wp_seq.
      iInv N as (x') ">Hl" "Hclose".
      wp_load.
      iApply "Hclose". eauto.
  Qed.
End user.