counter.v 5.5 KB
Newer Older
1
2
(* This file contains a formalization of the monotone counter, but with an
explicit contruction of the monoid, as we have also done in the proof mode
Ralf Jung's avatar
Ralf Jung committed
3
4
paper. This should simplify explaining and understanding what is happening.
A version that uses the authoritative monoid and natural number monoid
5
6
7
8
under max can be found in `heap_lang/lib/counter.v`. *)
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Export hoare.
9
From iris.proofmode Require Import tactics.
10
11
12
13
From iris.heap_lang Require Import proofmode notation.
Import uPred.

Definition newcounter : val := λ: <>, ref #0.
14
15
Definition incr : val :=
  rec: "incr" "l" :=
16
    let: "n" := !"l" in
17
    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
18
19
20
21
22
23
24
25
26
27
Definition read : val := λ: "l", !"l".

(** The CMRA we need. *)
Inductive M := Auth : nat  M | Frag : nat  M | Bot.

Section M.
  Arguments cmra_op _ !_ !_/.
  Arguments op _ _ !_ !_/.
  Arguments core _ _ !_/.

28
  Canonical Structure M_C : ofeT := leibnizC M.
29
30
31
32
33
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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

  Instance M_valid : Valid M := λ x, x  Bot.
  Instance M_op : Op M := λ x y,
    match x, y with
    | Auth n, Frag j | Frag j, Auth n => if decide (j  n)%nat then Auth n else Bot
    | Frag i, Frag j => Frag (max i j)
    | _, _ => Bot
    end.
  Instance M_pcore : PCore M := λ x,
    Some match x with Auth j | Frag j => Frag j | _ => Bot end.
  Instance M_empty : Empty M := Frag 0.

  Definition M_ra_mixin : RAMixin M.
  Proof.
    apply ra_total_mixin; try solve_proper || eauto.
    - intros [n1|i1|] [n2|i2|] [n3|i3|];
        repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n1|i1|] [n2|i2|]; repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n|i|]; repeat (simpl; case_decide); f_equal/=; lia.
    - by intros [n|i|].
    - intros [n1|i1|] y [[n2|i2|] ?]; exists (core y); simplify_eq/=;
        repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n1|i1|] [n2|i2|]; simpl; by try case_decide.
  Qed.
  Canonical Structure M_R : cmraT := discreteR M M_ra_mixin.
  Definition M_ucmra_mixin : UCMRAMixin M.
  Proof.
    split; try (done || apply _).
    intros [?|?|]; simpl; try case_decide; f_equal/=; lia.
  Qed.
  Canonical Structure M_UR : ucmraT := discreteUR M M_ra_mixin M_ucmra_mixin.

  Global Instance frag_persistent n : Persistent (Frag n).
  Proof. by constructor. Qed.
  Lemma auth_frag_valid j n :  (Auth n  Frag j)  (j  n)%nat.
  Proof. simpl. case_decide. done. by intros []. Qed.
  Lemma auth_frag_op (j n : nat) : (j  n)%nat  Auth n = Auth n  Frag j.
  Proof. intros. by rewrite /= decide_True. Qed.

  Lemma M_update n : Auth n ~~> Auth (S n).
  Proof.
    apply cmra_discrete_update=>-[m|j|] /= ?; repeat case_decide; done || lia.
  Qed.
End M.

Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
75
76
77
Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
Instance subG_counterΣ {Σ} : subG counterΣ Σ  counterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
78
79
80
81
82
83

Section proof.
Context `{!heapG Σ, !counterG Σ}.
Implicit Types l : loc.

Definition I (γ : gname) (l : loc) : iProp Σ :=
84
  ( c : nat, l  #c  own γ (Auth c))%I.
85
86

Definition C (l : loc) (n : nat) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
87
  ( N γ, heapN  N  heap_ctx  inv N (I γ l)  own γ (Frag n))%I.
88
89
90
91
92
93
94

(** The main proofs. *)
Global Instance C_persistent l n : PersistentP (C l n).
Proof. apply _. Qed.

Lemma newcounter_spec N :
  heapN  N 
Ralf Jung's avatar
Ralf Jung committed
95
  heap_ctx  {{ True }} newcounter #() {{ v,  l, v = #l  C l 0 }}.
96
Proof.
97
  iIntros (?) "#Hh !# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
98
  iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
99
  rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
100
  iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
101
  { iIntros "!>". iExists 0%nat. by iFrame. }
102
  iModIntro. rewrite /C; eauto 10.
103
104
Qed.

105
Lemma incr_spec l n :
Ralf Jung's avatar
Ralf Jung committed
106
  {{ C l n }} incr #l {{ v, v = #()  C l (S n) }}.
107
108
109
110
Proof.
  iIntros "!# Hl /=". iLöb as "IH". wp_rec.
  iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
  wp_bind (! _)%E; iInv N as (c) "[Hl Hγ]" "Hclose".
111
112
  wp_load. iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
  iModIntro. wp_let. wp_op.
113
114
115
  wp_bind (CAS _ _ _). iInv N as (c') ">[Hl Hγ]" "Hclose".
  destruct (decide (c' = c)) as [->|].
  - iCombine "Hγ" "Hγf" as "Hγ".
116
    iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
117
    iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
118
    rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
119
    wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]").
120
    { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
121
    iModIntro. wp_if. rewrite {3}/C; eauto 10.
122
  - wp_cas_fail; first (intros [=]; abstract omega).
123
124
    iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
    iModIntro. wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
125
126
127
Qed.

Lemma read_spec l n :
Ralf Jung's avatar
Ralf Jung committed
128
  {{ C l n }} read #l {{ v,  m : nat, v = #m  n  m  C l m }}.
129
130
Proof.
  iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
131
  rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
132
  iDestruct (own_valid γ (Frag n  Auth c) with "[-]") as % ?%auth_frag_valid.
133
134
  { iApply own_op. by iFrame. }
  rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
135
136
  iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
  iModIntro; rewrite /C; eauto 10 with omega.
137
138
Qed.
End proof.
Ralf Jung's avatar
Ralf Jung committed
139
140

Global Opaque newcounter incr read.