treiber.v 6 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2
From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre atomic.
Zhen Zhang's avatar
Zhen Zhang committed
3 4
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
5
From iris.algebra Require Import frac auth gmap csum.
Zhen Zhang's avatar
Zhen Zhang committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40

Definition new_stack: val := λ: <>, ref (ref NONE).

Definition push: val :=
  rec: "push" "s" "x" :=
      let: "hd" := !"s" in
      let: "s'" := ref SOME ("x", "hd") in
      if: CAS "s" "hd" "s'"
        then #()
        else "push" "s" "x".

Definition pop: val :=
  rec: "pop" "s" :=
      let: "hd" := !"s" in
      match: !"hd" with
        SOME "cell" =>
        if: CAS "s" "hd" (Snd "cell")
          then SOME (Fst "cell")
          else "pop" "s"
      | NONE => NONE
      end.

Definition iter: val :=
  rec: "iter" "hd" "f" :=
      match: !"hd" with
        NONE => #()
      | SOME "cell" => "f" (Fst "cell") ;; "iter" (Snd "cell") "f"
      end.

Section proof.
  Context `{!heapG Σ} (N: namespace).

  Fixpoint is_list (hd: loc) (xs: list val) : iProp Σ :=
    match xs with
    | [] => ( q, hd { q } NONEV)%I
41
    | x :: xs => ( (hd': loc) q, hd { q } SOMEV (x, #hd')  is_list hd' xs)%I
Zhen Zhang's avatar
Zhen Zhang committed
42 43 44
    end.

  Lemma dup_is_list :  xs hd,
45
    is_list hd xs  is_list hd xs  is_list hd xs.
Zhen Zhang's avatar
Zhen Zhang committed
46 47
  Proof.
    induction xs as [|y xs' IHxs'].
48
    - iIntros (hd) "Hs".
Zhen Zhang's avatar
Zhen Zhang committed
49
      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
50
    - iIntros (hd) "Hs". simpl.
Zhen Zhang's avatar
Zhen Zhang committed
51 52 53 54 55 56
      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hs')".
      iDestruct (IHxs' with "[Hs']") as "[Hs1 Hs2]"; first by iFrame.
      iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
  Qed.

  Lemma uniq_is_list:
57
     xs ys hd, is_list hd xs  is_list hd ys  xs = ys.
Zhen Zhang's avatar
Zhen Zhang committed
58 59 60 61
  Proof.
    induction xs as [|x xs' IHxs'].
    - induction ys as [|y ys' IHys'].
      + auto.
62
      + iIntros (hd) "(Hxs & Hys)".
Zhen Zhang's avatar
Zhen Zhang committed
63 64
        simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
        iExFalso. iDestruct "Hxs" as (?) "Hhd'".
Robbert Krebbers's avatar
Robbert Krebbers committed
65
        (* FIXME: If I dont use the @ here and below through this file, it loops. *)
66
        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
Zhen Zhang's avatar
Zhen Zhang committed
67
    - induction ys as [|y ys' IHys'].
68
      + iIntros (hd) "(Hxs & Hys)".
Zhen Zhang's avatar
Zhen Zhang committed
69 70 71
        simpl.
        iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
        iDestruct "Hys" as (?) "Hhd'".
72
        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
73
      + iIntros (hd) "(Hxs & Hys)".
Zhen Zhang's avatar
Zhen Zhang committed
74 75
        simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
        iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
76
        iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
Zhen Zhang's avatar
Zhen Zhang committed
77 78 79 80
        subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
        by subst.
  Qed.

81
  Definition is_stack (s: loc) xs: iProp Σ := ( hd: loc, s  #hd  is_list hd xs)%I.
Zhen Zhang's avatar
Zhen Zhang committed
82

Ralf Jung's avatar
Ralf Jung committed
83
  Global Instance is_list_timeless xs hd: Timeless (is_list hd xs).
Zhen Zhang's avatar
Zhen Zhang committed
84 85
  Proof. generalize hd. induction xs; apply _. Qed.

Ralf Jung's avatar
Ralf Jung committed
86
  Global Instance is_stack_timeless xs hd: Timeless (is_stack hd xs).
Zhen Zhang's avatar
Zhen Zhang committed
87 88 89
  Proof. generalize hd. induction xs; apply _. Qed.

  Lemma new_stack_spec:
Ralf Jung's avatar
Ralf Jung committed
90
    {{{ True }}} new_stack #() {{{ s, RET #s; is_stack s [] }}}.
Zhen Zhang's avatar
Zhen Zhang committed
91
  Proof.
Ralf Jung's avatar
Ralf Jung committed
92
    iIntros (Φ) "_ HΦ". wp_lam.
Zhen Zhang's avatar
Zhen Zhang committed
93 94 95 96 97 98 99
    wp_bind (ref NONE)%E. wp_alloc l as "Hl".
    wp_alloc l' as "Hl'".
    iApply "HΦ". rewrite /is_stack. iExists l.
    iFrame. by iExists 1%Qp.
  Qed.
  
  Lemma push_atomic_spec (s: loc) (x: val) :
Ralf Jung's avatar
Ralf Jung committed
100 101 102
    <<<  (xs : list val), is_stack s xs >>>
      push #s x @ 
    <<< is_stack s (x::xs), RET #() >>>.
Zhen Zhang's avatar
Zhen Zhang committed
103
  Proof.
Ralf Jung's avatar
Ralf Jung committed
104
    iApply wp_atomic_intro. unfold is_stack.
Ralf Jung's avatar
Ralf Jung committed
105
    iIntros (Φ) "HP". iLöb as "IH". wp_rec.
Zhen Zhang's avatar
Zhen Zhang committed
106
    wp_let. wp_bind (! _)%E.
Ralf Jung's avatar
Ralf Jung committed
107 108 109
    iMod "HP" as (xs) "[Hxs [Hvs' _]]".
    iDestruct "Hxs" as (hd) "[Hs Hhd]".
    wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by eauto with iFrame.
110
    iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
111
    wp_bind (CAS _ _ _)%E.
Ralf Jung's avatar
Ralf Jung committed
112 113
    iMod "HP" as (xs') "[Hxs' Hvs']".
    iDestruct "Hxs'" as (hd') "[Hs' Hhd']".
Robbert Krebbers's avatar
Robbert Krebbers committed
114
    destruct (decide (hd = hd')) as [->|Hneq].
Zhen Zhang's avatar
Zhen Zhang committed
115
    * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
Ralf Jung's avatar
Ralf Jung committed
116
      iMod ("Hvs'" with "[-]") as "HQ".
Ralf Jung's avatar
Ralf Jung committed
117
      { by eauto with iFrame. }
118
      iModIntro. wp_if. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
119 120
    * wp_cas_fail.
      iDestruct "Hvs'" as "[Hvs' _]".
Ralf Jung's avatar
Ralf Jung committed
121
      iMod ("Hvs'" with "[-]") as "HP"; first by eauto with iFrame.
122
      iModIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
123 124
  Qed.

Ralf Jung's avatar
Ralf Jung committed
125 126
  Lemma pop_atomic_spec (s: loc) :
    <<<  (xs : list val), is_stack s xs >>>
Ralf Jung's avatar
Ralf Jung committed
127
      pop #s @ 
Ralf Jung's avatar
Ralf Jung committed
128 129
    <<< match xs with [] => is_stack s []
                | x::xs' => is_stack s xs' end,
Ralf Jung's avatar
Ralf Jung committed
130
    RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
Zhen Zhang's avatar
Zhen Zhang committed
131
  Proof.
Ralf Jung's avatar
Ralf Jung committed
132
    iApply wp_atomic_intro. unfold is_stack.
Ralf Jung's avatar
Ralf Jung committed
133
    iIntros (Φ) "HP". iLöb as "IH". wp_rec.
Zhen Zhang's avatar
Zhen Zhang committed
134
    wp_bind (! _)%E.
Ralf Jung's avatar
Ralf Jung committed
135 136
    iMod "HP" as (xs) "[Hxs Hvs']".
    iDestruct "Hxs" as (hd) "[Hs Hhd]".
Robbert Krebbers's avatar
Robbert Krebbers committed
137
    destruct xs as [|y' xs'].
Zhen Zhang's avatar
Zhen Zhang committed
138 139
    - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
      iDestruct "Hhd" as (q) "[Hhd Hhd']".
Ralf Jung's avatar
Ralf Jung committed
140
      iMod ("Hvs'" with "[-Hhd]") as "HQ".
Ralf Jung's avatar
Ralf Jung committed
141
      { eauto with iFrame. }
Ralf Jung's avatar
Ralf Jung committed
142
      iModIntro. wp_let. wp_load. wp_pures.
143
      eauto.
Zhen Zhang's avatar
Zhen Zhang committed
144 145 146
    - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
      iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
      wp_load. iDestruct "Hvs'" as "[Hvs' _]".
147
      iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
Ralf Jung's avatar
Ralf Jung committed
148
      { eauto with iFrame. }
149
      iModIntro. wp_let. wp_load. wp_match. wp_proj.
150
      wp_bind (CAS _ _ _).
Ralf Jung's avatar
Ralf Jung committed
151 152
      iMod "HP" as (xs'') "[Hxs'' Hvs']".
    iDestruct "Hxs''" as (hd'') "[Hs'' Hhd'']".
Robbert Krebbers's avatar
Robbert Krebbers committed
153
      destruct (decide (hd = hd'')) as [->|Hneq].
Zhen Zhang's avatar
Zhen Zhang committed
154
      + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
Ralf Jung's avatar
Ralf Jung committed
155
        destruct xs'' as [|x'' xs''].
Ralf Jung's avatar
Ralf Jung committed
156 157 158 159 160
        { simpl. iDestruct "Hhd''" as (?) "H".
          iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?. }
        simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
        iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=]. subst.
        iMod ("Hvs'" with "[-]") as "HQ".
Ralf Jung's avatar
Ralf Jung committed
161
        { eauto with iFrame.  }
Ralf Jung's avatar
Ralf Jung committed
162
        iModIntro. wp_if. wp_pures. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
163
      + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
Ralf Jung's avatar
Ralf Jung committed
164
        iMod ("Hvs'" with "[-]") as "HP"; first by eauto with iFrame.
165
        iModIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
166 167
  Qed.
End proof.