increment.v 6.27 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 26 27 28 29 30 31 32 33 34 35 36 37 38 39
(** 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.
    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
    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 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
  (** 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.
    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
    wp_apply load_spec; first by iAccu.
    (* Prove the atomic update for load *)
    iAuIntro. rewrite /atomic_acc. iMod "AU" as (v) "[Hl [Hclose _]]".
    iModIntro. iExists _, _. iFrame "Hl". iSplit.
    { (* proving abort case *) done. }
    iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iIntros "!> _".
    (* Now go on *)
    wp_apply cas_spec; [done|iAccu|].
    (* Prove the atomic update for CAS *)
    iAuIntro. rewrite /atomic_acc. iMod "AU" as (w) "[Hl Hclose]".
    iModIntro. iExists _. iFrame "Hl". iSplit.
    { iDestruct "Hclose" as "[? _]". done. }
    iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx].
    - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
      iIntros "!> _". wp_if. by iApply "HΦ".
    - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
      iIntros "!> _". wp_if. iApply "IH". done.
  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
    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
84
    wp_apply load_spec; first by iAccu.
85
    (* Prove the atomic update for load *)
Ralf Jung's avatar
Ralf Jung committed
86
    iAuIntro. 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 *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
90
    wp_apply cas_spec; [done|iAccu|].
91
    (* Prove the atomic update for CAS *)
Ralf Jung's avatar
Ralf Jung committed
92
    iAuIntro. 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 99
    - iLeft. iFrame. iIntros "AU !> _".
      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". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
120
    wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
121
    iIntros "Hl". wp_apply store_spec; first by iAccu.
122 123 124 125
    (* Prove the atomic update for store *)
    iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
    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. wp_apply incr_spec; first by iAccu. clear x.
      iAuIntro. 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.
    }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
158
    wp_apply par_spec; wp_pures.
159 160
    - iAssumption.
    - iAssumption.
161 162 163 164
    - iIntros (??) "_ !>". done.
  Qed.

End increment_client.