increment.v 3.46 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
4
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
5
From iris.heap_lang Require Import proofmode notation atomic_heap par.
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
12
atomicity. *)

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

  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)
                  (λ (v: Z), aheap.(mapsto) l 1 #v)%I
                  (λ v (_:()), aheap.(mapsto) l 1 #(v + 1))%I
26
                   
Ralf Jung's avatar
Ralf Jung committed
27
28
                  (λ v _, #v).
  Proof.
29
30
    iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let.
    wp_apply (load_spec with "HQ").
Ralf Jung's avatar
Ralf Jung committed
31
    (* Prove the atomic shift for load *)
32
33
34
35
    iApply (aupd_intro with "AU"); first done. iIntros "!# AU".
    iMod (aupd_acc with "AU") as (x) "[H↦ [Hclose _]]"; first solve_ndisj.
    iModIntro. iExists (#x, 1%Qp). iFrame "H↦". iSplit; first done.
    iIntros ([]) "H↦". iMod ("Hclose" with "H↦") as "AU". iIntros "!> 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").
Ralf Jung's avatar
Ralf Jung committed
39
    (* Prove the atomic shift for CAS *)
40
41
    iApply (aupd_intro with "AU"); first done. iIntros "!# AU".
    iMod (aupd_acc with "AU") as (x') "[H↦ Hclose]"; first solve_ndisj.
Ralf Jung's avatar
Ralf Jung committed
42
43
    iModIntro. iExists #x'. iFrame. iSplit.
    { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
44
    iIntros ([]). destruct (decide (#x' = #x)) as [[= Hx]|Hx].
Ralf Jung's avatar
Ralf Jung committed
45
    - iIntros "H↦". iDestruct "Hclose" as "[_ Hclose]". subst.
46
      iMod ("Hclose" $! () with "H↦") as "HΦ". iIntros "!> HQ".
Ralf Jung's avatar
Ralf Jung committed
47
48
      wp_if. by iApply "HΦ".
    - iDestruct "Hclose" as "[Hclose _]". iIntros "H↦".
49
50
      iMod ("Hclose" with "H↦") as "AU". iIntros "!> HQ".
      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
67
68
69
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.
    iMod (inv_alloc nroot _ (x':Z, l  #x')%I with "[Hl]") as "#?"; first eauto.
    (* FIXME: I am only usign persistent stuff, so I should be allowed
       to move this to the persisten context even without the additional □. *)
70
71
72
    iAssert ( WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd".
    { iAlways. wp_apply (incr_spec with "[]"); first iEmpIntro. clear x.
      iApply (aupd_intro with "[]"); try iEmpIntro; [done|apply _|]. iIntros "!# _".
73
74
75
76
77
78
79
      iInv nroot as (x) ">H↦" "Hclose".
      iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
      iExists _. iFrame. iSplit.
      { iIntros "H↦". iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"); last done.
        iNext. iExists _. iFrame. }
      iIntros (_) "H↦". iMod "Hclose2" as "_".
      iMod ("Hclose" with "[-]"); last done. iNext. iExists _. iFrame. }
80
81
82
    wp_apply wp_par.
    - iAssumption.
    - iAssumption.
83
84
85
86
    - iIntros (??) "_ !>". done.
  Qed.

End increment_client.