increment.v 6.03 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
4
From iris.heap_lang Require Import proofmode notation atomic_heap par.
5
From iris.bi.lib Require Import fractional.
Ralf Jung's avatar
Ralf Jung committed
6
7
Set Default Proof Using "Type".

8
(** Show that implementing fetch-and-add on top of CAS preserves logical
Ralf Jung's avatar
Ralf Jung committed
9
10
atomicity. *)

11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(** First: logically atomic increment directly on top of the physical heap. *)

Section increment_physical.
  Context `{!heapG Σ}.

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

  Lemma incr_phy_spec (l: loc) :
    <<<  (v : Z), l  #v >>> incr_phy #l @  <<< l  #(v + 1), RET #v >>>.
  Proof.
26
    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
27
28
29
30
31
32
33
34
35
36
37
38
39
    wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
    wp_load. iMod ("Hclose" with "Hl") as "AU". iModIntro.
    wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
    destruct (decide (#v = #w)) as [[= ->]|Hx].
    - wp_cas_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
      iModIntro. wp_if. done.
    - wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
      iModIntro. wp_if. iApply "IH". done.
  Qed.
End increment_physical.

(** Next: logically atomic increment on top of an arbitrary logically atomic heap *)

Ralf Jung's avatar
Ralf Jung committed
40
Section increment.
41
42
43
  Context `{!heapG Σ} {aheap: atomic_heap Σ}.

  Import atomic_heap.notation.
Ralf Jung's avatar
Ralf Jung committed
44

45
  Definition incr : val :=
Ralf Jung's avatar
Ralf Jung committed
46
    rec: "incr" "l" :=
47
48
       let: "oldv" := !"l" in
       if: CAS "l" "oldv" ("oldv" + #1)
Ralf Jung's avatar
Ralf Jung committed
49
50
51
         then "oldv" (* return old value if success *)
         else "incr" "l".

52
53
54
55
56
57
  (** A proof of the incr specification that unfolds the definition
      of atomic accessors.  Useful for introducing them as a concept,
      but see below for a shorter proof. *)
  Lemma incr_spec_direct (l: loc) :
    <<<  (v : Z), l  #v >>> incr #l @  <<< l  #(v + 1), RET #v >>>.
  Proof.
58
59
    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
    awp_apply load_spec.
60
    (* Prove the atomic update for load *)
61
    rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
62
    iModIntro. iExists _, _. iFrame "Hl". iSplit.
Ralf Jung's avatar
Ralf Jung committed
63
    { (* abort case *) done. }
64
    iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro.
65
    (* Now go on *)
66
    awp_apply cas_spec; first done.
67
    (* Prove the atomic update for CAS *)
68
    rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
69
    iModIntro. iExists _. iFrame "Hl". iSplit.
Ralf Jung's avatar
Ralf Jung committed
70
    { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
71
72
    iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx].
    - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
73
      iIntros "!>". wp_if. by iApply "HΦ".
74
    - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
75
      iIntros "!>". wp_if. iApply "IH". done.
76
77
78
79
  Qed.

  (** A proof of the incr specification that uses lemmas to avoid reasining
      with the definition of atomic accessors. *)
Ralf Jung's avatar
Ralf Jung committed
80
  Lemma incr_spec (l: loc) :
81
    <<<  (v : Z), l  #v >>> incr #l @  <<< l  #(v + 1), RET #v >>>.
Ralf Jung's avatar
Ralf Jung committed
82
  Proof.
83
84
    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
    awp_apply load_spec.
85
    (* Prove the atomic update for load *)
86
    iApply (aacc_aupd_abort with "AU"); first done.
87
    iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
88
    iIntros "$ !> AU !>".
Ralf Jung's avatar
Ralf Jung committed
89
    (* Now go on *)
90
    awp_apply cas_spec; first done.
91
    (* Prove the atomic update for CAS *)
92
    iApply (aacc_aupd with "AU"); first done.
93
    iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
94
    iIntros "H↦ !>".
95
    destruct (decide (#x' = #x)) as [[= ->]|Hx].
96
    - iRight. iFrame. iIntros "HΦ !>".
Ralf Jung's avatar
Ralf Jung committed
97
      wp_if. by iApply "HΦ".
98
    - iLeft. iFrame. iIntros "AU !>".
99
      wp_if. iApply "IH". done.
Ralf Jung's avatar
Ralf Jung committed
100
101
  Qed.

102
  (** A "weak increment": assumes that there is no race *)
103
104
105
106
107
108
  Definition weak_incr: val :=
    rec: "weak_incr" "l" :=
       let: "oldv" := !"l" in
       "l" <- ("oldv" + #1);;
       "oldv" (* return old value *).

109
110
  (** Logically atomic spec for weak increment. Also an example for what TaDA
      calls "private precondition". *)
111
112
113
114
115
116
117
118
  (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto"
     connective that works on [option Qp] (the type of 1-q). *)
  Lemma weak_incr_spec (l: loc) (v : Z) :
    l {1/2} #v -
    <<<  (v' : Z), l {1/2} #v' >>>
      weak_incr #l @ 
    <<< v = v'  l  #(v + 1), RET #v >>>.
  Proof.
119
    iIntros "Hl" (Φ) "AU". wp_lam.
120
    wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
121
    iIntros "Hl". awp_apply store_spec.
122
    (* Prove the atomic update for store *)
123
    iApply (aacc_aupd_commit with "AU"); first done.
124
125
    iIntros (x) "H↦".
    iDestruct (mapsto_agree with "Hl H↦") as %[= <-].
126
127
    iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
    { iIntros "[$ $]"; eauto. }
128
    iIntros "$ !>". iSplit; first done.
129
    iIntros "HΦ !>". wp_seq. done.
130
131
  Qed.

Ralf Jung's avatar
Ralf Jung committed
132
133
End increment.

134
135
136
Section increment_client.
  Context `{!heapG Σ, !spawnG Σ}.

137
138
  Existing Instance primitive_atomic_heap.

139
140
141
  Definition incr_client : val :=
    λ: "x",
       let: "l" := ref "x" in
142
       incr "l" ||| incr "l".
143
144
145
146

  Lemma incr_client_safe (x: Z):
    WP incr_client #x {{ _, True }}%I.
  Proof using Type*.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
147
    wp_lam. wp_alloc l as "Hl".
148
149
    iMod (inv_alloc nroot _ (x':Z, l  #x')%I with "[Hl]") as "#Hinv"; first eauto.
    (* FIXME: I am only using persistent stuff, so I should be allowed
150
       to move this to the persisten context even without the additional □. *)
151
    iAssert ( WP incr #l {{ _, True }})%I as "#Aupd".
152
153
    { iAlways. awp_apply incr_spec. clear x.
      iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
154
      iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
155
156
157
      (* The continuation: From after the atomic triple to the postcondition of the WP *)
      done.
    }
Ralf Jung's avatar
Ralf Jung committed
158
    wp_apply wp_par.
159
160
    - iAssumption.
    - iAssumption.
161
162
163
164
    - iIntros (??) "_ !>". done.
  Qed.

End increment_client.