increment.v 3.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.
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 done; 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|done|iSplit].
    { eauto 10 with iFrame. }
44
45
46
    iIntros ([]) "H↦ !>".
    destruct (decide (#x' = #x)) as [[= ->]|Hx].
    - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
Ralf Jung's avatar
Ralf Jung committed
47
      wp_if. by iApply "HΦ".
48
    - iLeft. iFrame. iIntros "AU !> HQ".
49
      wp_if. iApply ("IH" with "HQ"). done.
Ralf Jung's avatar
Ralf Jung committed
50
51
52
53
  Qed.

End increment.

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

End increment_client.