increment.v 3.81 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
8
9
10
11
12
Set Default Proof Using "Type".

(** Show taht implementing fetch-and-add on top of CAS preserves logical
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
29
30
31
32
                  (λ v _, #v).
  Proof.
    iIntros (Φ) "AUpd". iLöb as "IH". wp_let.
    wp_apply load_spec.
    (* Prove the atomic shift for load *)
    iDestruct "AUpd" as (F P) "(HF & HP & #AShft)".
Robbert Krebbers's avatar
Robbert Krebbers committed
33
    iExists F, P. iFrame. iIntros "!#" (E ?) "HP".
Ralf Jung's avatar
Ralf Jung committed
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
    iMod ("AShft" with "[%] HP") as (x) "[H↦ Hclose]"; first done.
    iModIntro. iExists (#x, 1%Qp). iFrame. iSplit.
    { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
    iIntros (_) "H↦". iDestruct "Hclose" as "[Hclose _]".
    iMod ("Hclose" with "H↦") as "HP". iIntros "!> HF".
    clear dependent E.
    (* Now go on *)
    wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
    wp_apply cas_spec.
    (* Prove the atomic shift for CAS *)
    iExists F, P. iFrame. iIntros "!# * % HP".
    iMod ("AShft" with "[%] HP") as (x') "[H↦ Hclose]"; first done.
    iModIntro. iExists #x'. iFrame. iSplit.
    { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
    iIntros (_). destruct (decide (#x' = #x)) as [[= Hx]|Hx].
    - iIntros "H↦". iDestruct "Hclose" as "[_ Hclose]". subst.
      iMod ("Hclose" $! () with "H↦") as "HΦ". iIntros "!> HF".
      wp_if. by iApply "HΦ".
    - iDestruct "Hclose" as "[Hclose _]". iIntros "H↦".
      iMod ("Hclose" with "H↦") as "HP". iIntros "!> HF".
      wp_if. iApply "IH". iExists F, P. iFrame. done.
  Qed.

End increment.

59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
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 □. *)
    iAssert ( atomic_update (λ (v: Z), l  #v)
                           (λ v (_:()), l  #(v + 1))
                            
                           (λ _ _, True))%I as "#Aupd".
    { iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
79
      iIntros "!#" (E) "% _".
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
      assert (E = ) as -> by set_solver.
      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. }
    wp_apply (wp_par (λ _, True)%I (λ _, True)%I).
    - wp_apply incr_spec. iAssumption. (* FIXME: without giving the
      postconditions above, this diverges. *)
    - wp_apply incr_spec. iAssumption.
    - iIntros (??) "_ !>". done.
  Qed.

End increment_client.