increment.v 3.05 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.
Ralf Jung's avatar
Ralf Jung committed
5
6
Set Default Proof Using "Type".

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

(* TODO: Move this to iris-examples once gen_proofmode is merged. *)
Section increment.
12
  Context `{!heapG Σ} (aheap: atomic_heap Σ).
Ralf Jung's avatar
Ralf Jung committed
13
14
15
16
17
18
19
20
21
22

  Definition incr: val :=
    rec: "incr" "l" :=
       let: "oldv" := aheap.(load) "l" in
       if: aheap.(cas) ("l", "oldv", ("oldv" + #1))
         then "oldv" (* return old value if success *)
         else "incr" "l".

  Lemma incr_spec (l: loc) :
        atomic_wp (incr #l)
23
                   
Ralf Jung's avatar
Ralf Jung committed
24
25
26
27
                  (λ (v: Z), aheap.(mapsto) l 1 #v)%I
                  (λ v (_:()), aheap.(mapsto) l 1 #(v + 1))%I
                  (λ v _, #v).
  Proof.
28
    iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let.
29
    wp_apply (load_spec with "[HQ]"); first by iAccu.
Ralf Jung's avatar
Ralf Jung committed
30
    (* Prove the atomic shift for load *)
Ralf Jung's avatar
Ralf Jung committed
31
    iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
32
    iIntros (x) "H↦".
Ralf Jung's avatar
Ralf Jung committed
33
    iApply (aacc_intro (_, _) with "[H↦]"); [solve_ndisj|done|iSplit].
34
35
    { iIntros "$ !> $ !> //". }
    iIntros ([]) "$ !> AU !> HQ".
Ralf Jung's avatar
Ralf Jung committed
36
37
    (* Now go on *)
    wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
38
    wp_apply (cas_spec with "[HQ]"); first by iAccu.
Ralf Jung's avatar
Ralf Jung committed
39
    (* Prove the atomic shift for CAS *)
Ralf Jung's avatar
Ralf Jung committed
40
    iAuIntro. iApply (aacc_aupd with "AU"); first done.
41
    iIntros (x') "H↦".
42
43
    iApply (aacc_intro with "[H↦]"); [solve_ndisj| |iSplit].
    { iFrame. simpl. auto. }
Ralf Jung's avatar
Ralf Jung committed
44
    { iIntros "[_ $] !> $ !> //". }
45
46
47
    iIntros ([]) "H↦ !>".
    destruct (decide (#x' = #x)) as [[= ->]|Hx].
    - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
Ralf Jung's avatar
Ralf Jung committed
48
      wp_if. by iApply "HΦ".
49
    - iLeft. iFrame. iIntros "AU !> HQ".
50
      wp_if. iApply ("IH" with "HQ"). done.
Ralf Jung's avatar
Ralf Jung committed
51
52
53
54
  Qed.

End increment.

55
56
57
58
59
60
61
62
63
64
65
66
Section increment_client.
  Context `{!heapG Σ, !spawnG Σ}.

  Definition incr_client : val :=
    λ: "x",
       let: "l" := ref "x" in
       incr primitive_atomic_heap "l" ||| incr primitive_atomic_heap "l".

  Lemma incr_client_safe (x: Z):
    WP incr_client #x {{ _, True }}%I.
  Proof using Type*.
    wp_let. wp_alloc l as "Hl". wp_let.
67
68
    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
69
       to move this to the persisten context even without the additional □. *)
70
    iAssert ( WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd".
71
72
    { iAlways. wp_apply (incr_spec with "[]"); first by iAccu. clear x.
      iAuIntro. iInv nroot as (x) ">H↦".
Ralf Jung's avatar
Ralf Jung committed
73
      iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
74
      { by eauto 10. }
75
76
77
78
      iIntros ([]) "H↦ !>". iSplitL "H↦"; first by eauto 10.
      (* The continuation: From after the atomic triple to the postcondition of the WP *)
      done.
    }
79
80
81
    wp_apply wp_par.
    - iAssumption.
    - iAssumption.
82
83
84
85
    - iIntros (??) "_ !>". done.
  Qed.

End increment_client.