atomic_incr.v 3.27 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.program_logic Require Export weakestpre.
Zhen Zhang's avatar
Zhen Zhang committed
2
3
From iris.heap_lang Require Export lang proofmode notation.
From iris_atomic Require Import atomic.
4
5
From iris.proofmode Require Import tactics.
From iris.prelude Require Import coPset.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.heap_lang.lib Require Import par.
Zhen Zhang's avatar
Zhen Zhang committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

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) :=
Ralf Jung's avatar
Ralf Jung committed
22
    atomic_triple (fun (v: Z) => l  #v)%I
Zhen Zhang's avatar
Zhen Zhang committed
23
                  (fun v ret => ret = #v  l  #(v + 1))%I
Ralf Jung's avatar
Ralf Jung committed
24
25
26
                  (nclose heapN)
                  
                  (incr #l).
Zhen Zhang's avatar
Zhen Zhang committed
27
28
29
30
31
32
33
34
35
36
37

  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.
Ralf Jung's avatar
Ralf Jung committed
38
    iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
Zhen Zhang's avatar
Zhen Zhang committed
39
    wp_load.
Ralf Jung's avatar
Ralf Jung committed
40
41
42
    iMod ("Hvs'" with "Hl") as "HP".
    iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
    iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
Zhen Zhang's avatar
Zhen Zhang committed
43
44
45
46
47
    destruct (decide (x = x')).
    - subst.
      iDestruct "Hvs'" as "[_ Hvs']".
      iSpecialize ("Hvs'" $! #x').
      wp_cas_suc.
Ralf Jung's avatar
Ralf Jung committed
48
      iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
49
      iModIntro. wp_if. done.
Zhen Zhang's avatar
Zhen Zhang committed
50
51
    - iDestruct "Hvs'" as "[Hvs' _]".
      wp_cas_fail.
Ralf Jung's avatar
Ralf Jung committed
52
53
      iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
      iModIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
54
55
56
57
58
59
60
61
62
63
  Qed.
End incr.


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

  Definition incr_2 : val :=
    λ: "x",
       let: "l" := ref "x" in
Zhen Zhang's avatar
Zhen Zhang committed
64
       incr "l" ||| incr "l";;
Zhen Zhang's avatar
Zhen Zhang committed
65
66
67
68
69
70
71
72
73
74
       !"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".
Ralf Jung's avatar
Ralf Jung committed
75
    iMod (inv_alloc N _ (x':Z, l  #x')%I with "[Hl]") as "#?"; first eauto.
Zhen Zhang's avatar
Zhen Zhang committed
76
    wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
77
78
    wp_bind (_ ||| _)%E.
    iApply (wp_par (λ _, True%I) (λ _, True%I) with "[]").
Zhen Zhang's avatar
Zhen Zhang committed
79
80
81
82
    iFrame "Hh".
    (* prove worker triple *)
    iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
    rewrite /incr_triple /atomic_triple.
83
    iSpecialize ("Hincr"  $! True%I (fun _ => True%I) with "[]").
Zhen Zhang's avatar
Zhen Zhang committed
84
85
86
87
    - iIntros "!# _".
      (* open the invariant *)
      iInv N as (x') ">Hl'" "Hclose".
      (* mask magic *)
Ralf Jung's avatar
Ralf Jung committed
88
89
      iMod (fupd_intro_mask' (  nclose N) heapN) as "Hvs"; first set_solver.
      iModIntro. iExists x'. iFrame "Hl'". iSplit.
Zhen Zhang's avatar
Zhen Zhang committed
90
91
      + (* provide a way to rollback *)
        iIntros "Hl'".
Ralf Jung's avatar
Ralf Jung committed
92
        iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
Zhen Zhang's avatar
Zhen Zhang committed
93
94
      + (* provide a way to commit *)
        iIntros (v) "[Heq Hl']".
Ralf Jung's avatar
Ralf Jung committed
95
        iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
Zhen Zhang's avatar
Zhen Zhang committed
96
    - iDestruct "Hincr" as "#HIncr".
97
98
      iSplitL; [|iSplitL];
        try (iApply wp_wand_r; iSplitL; [by iApply "HIncr"|auto]).
Zhen Zhang's avatar
Zhen Zhang committed
99
      iIntros (v1 v2) "_ !>".
100
101
      wp_seq. iInv N as (x') ">Hl" "Hclose".
      wp_load. iApply "Hclose". eauto.
Zhen Zhang's avatar
Zhen Zhang committed
102
103
  Qed.
End user.