atomic.v 4.7 KB
Newer Older
1
From iris.program_logic Require Export hoare weakestpre pviewshifts.
Zhen Zhang's avatar
atomic    
Zhen Zhang committed
2
3
From iris.algebra Require Import upred_big_op.
From iris.prelude Require Export coPset.
4
From iris.proofmode Require Import tactics.
Zhen Zhang's avatar
atomic    
Zhen Zhang committed
5
6
7
Import uPred.

Section atomic.
8
9
10
11
  Context `{irisG Λ Σ} {A: Type}.

  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
  Definition atomic_triple
Zhen Zhang's avatar
atomic    
Zhen Zhang committed
12
13
14
15
16
17
18
19
20
21
             (α: 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.

22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
  (* 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 {_} _ _ _ _.
Zhen Zhang's avatar
atomic    
Zhen Zhang committed
42
43
End atomic.

44
(* TODO: Importing in the middle of the file is bad practice. *)
45
From iris.heap_lang Require Export lang proofmode notation.
46
From iris.heap_lang.lib Require Import par.
Zhen Zhang's avatar
atomic    
Zhen Zhang committed
47

48
Section incr.
Zhen Zhang's avatar
atomic    
Zhen Zhang committed
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
  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' _]".
Zhen Zhang's avatar
Zhen Zhang committed
91
      wp_cas_fail.
Zhen Zhang's avatar
atomic    
Zhen Zhang committed
92
93
94
      iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
      iVsIntro. wp_if. by iApply "IH".
  Qed.
95
End incr.
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114


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".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
115
    iVs (inv_alloc N _ (x':Z, l  #x')%I with "[Hl]") as "#?"; first eauto.
116
117
118
119
120
121
122
    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.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
123
    iSpecialize ("Hincr"  $! True%I (fun _ _ => True%I) with "[]").
124
125
    - iIntros "!# _".
      (* open the invariant *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
126
      iInv N as (x') ">Hl'" "Hclose".
127
128
129
130
131
132
133
134
135
      (* mask magic *)
      iApply pvs_intro'.
      { apply ndisj_subseteq_difference; auto. }
      iIntros "Hvs".
      iExists x'.
      iFrame "Hl'".
      iSplit.
      + (* provide a way to rollback *)
        iIntros "Hl'".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
136
        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
137
138
      + (* provide a way to commit *)
        iIntros (v) "[Heq Hl']".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
139
        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
140
141
142
143
    - iDestruct "Hincr" as "#HIncr".
      iSplitL; [|iSplitL]; try (iApply wp_wand_r;iSplitL; [by iApply "HIncr"|auto]).
      iIntros (v1 v2) "_ !>".
      wp_seq.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
144
      iInv N as (x') ">Hl" "Hclose".
145
      wp_load.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
146
      iApply "Hclose". eauto.
147
148
  Qed.
End user.