atomic.v 4.71 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
      (* mask magic *)
128
      iVs (pvs_intro_mask' _ heapN) as "Hclose'".
129
      { apply ndisj_subseteq_difference; auto. }
130
      iVsIntro. iExists x'. iFrame "Hl'". iSplit.
131 132
      + (* provide a way to rollback *)
        iIntros "Hl'".
133
        iVs "Hclose'". iVs ("Hclose" with "[Hl']"); eauto.
134 135
      + (* provide a way to commit *)
        iIntros (v) "[Heq Hl']".
136
        iVs "Hclose'". iVs ("Hclose" with "[Hl']"); eauto.
137 138 139 140
    - 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
141
      iInv N as (x') ">Hl" "Hclose".
142
      wp_load.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
143
      iApply "Hclose". eauto.
144 145
  Qed.
End user.