increment.v 3.68 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 11
atomicity. *)

Section increment.
12 13 14
  Context `{!heapG Σ} {aheap: atomic_heap Σ}.

  Import atomic_heap.notation.
Ralf Jung's avatar
Ralf Jung committed
15 16 17

  Definition incr: val :=
    rec: "incr" "l" :=
18 19
       let: "oldv" := !"l" in
       if: CAS "l" "oldv" ("oldv" + #1)
Ralf Jung's avatar
Ralf Jung committed
20 21 22 23
         then "oldv" (* return old value if success *)
         else "incr" "l".

  Lemma incr_spec (l: loc) :
24
    <<<  (v : Z), l  #v >>> incr #l @  <<< l  #(v + 1), RET #v >>>.
Ralf Jung's avatar
Ralf Jung committed
25
  Proof.
26 27
    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_let.
    wp_apply load_spec; first by iAccu.
28
    (* Prove the atomic update for load *)
Ralf Jung's avatar
Ralf Jung committed
29
    iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
30
    iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
31
    iIntros "$ !> AU !> _".
Ralf Jung's avatar
Ralf Jung committed
32
    (* Now go on *)
33
    wp_let. wp_op. wp_bind (CAS _ _ _)%I.
34
    wp_apply cas_spec; [done|iAccu|].
35
    (* Prove the atomic update for CAS *)
Ralf Jung's avatar
Ralf Jung committed
36
    iAuIntro. iApply (aacc_aupd with "AU"); first done.
37
    iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
38
    iIntros "H↦ !>".
39
    destruct (decide (#x' = #x)) as [[= ->]|Hx].
40
    - iRight. iFrame. iIntros "HΦ !> _".
Ralf Jung's avatar
Ralf Jung committed
41
      wp_if. by iApply "HΦ".
42 43
    - iLeft. iFrame. iIntros "AU !> _".
      wp_if. iApply "IH". done.
Ralf Jung's avatar
Ralf Jung committed
44 45
  Qed.

46 47 48 49 50 51 52 53 54 55 56 57 58 59
  Definition weak_incr: val :=
    rec: "weak_incr" "l" :=
       let: "oldv" := !"l" in
       "l" <- ("oldv" + #1);;
       "oldv" (* return old value *).

  (* 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.
60
    iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_let.
61 62
    wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
    iIntros "Hl". wp_let. wp_op.
63
    wp_apply store_spec; first by iAccu.
64 65 66 67
    (* 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 %[= <-].
68 69
    iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
    { iIntros "[$ $]"; eauto. }
70
    iIntros "$ !>". iSplit; first done.
71
    iIntros "HΦ !> _". wp_seq. done.
72 73
  Qed.

Ralf Jung's avatar
Ralf Jung committed
74 75
End increment.

76 77 78
Section increment_client.
  Context `{!heapG Σ, !spawnG Σ}.

79 80
  Existing Instance primitive_atomic_heap.

81 82 83
  Definition incr_client : val :=
    λ: "x",
       let: "l" := ref "x" in
84
       incr "l" ||| incr "l".
85 86 87 88 89

  Lemma incr_client_safe (x: Z):
    WP incr_client #x {{ _, True }}%I.
  Proof using Type*.
    wp_let. wp_alloc l as "Hl". wp_let.
90 91
    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
92
       to move this to the persisten context even without the additional □. *)
93
    iAssert ( WP incr #l {{ _, True }})%I as "#Aupd".
94 95
    { iAlways. wp_apply incr_spec; first by iAccu. clear x.
      iAuIntro. iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
96
      iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
97 98 99
      (* The continuation: From after the atomic triple to the postcondition of the WP *)
      done.
    }
100 101 102
    wp_apply wp_par.
    - iAssumption.
    - iAssumption.
103 104 105 106
    - iIntros (??) "_ !>". done.
  Qed.

End increment_client.