atomic_incr.v 3.26 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
23
24
25
26
    atomic_triple (fun (v: Z) => l  #v)%I
                  (fun v ret => ret = #v  l  #(v + 1))%I
                  (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
64
65
66
67
68
69
70
71
72
73
74
  Qed.
End incr.


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".
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
77
78
79
80
81
82
    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.
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.