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

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

Definition push: val :=
  rec: "push" "s" "x" :=
      let: "hd" := !"s" in
Robbert Krebbers's avatar
Robbert Krebbers committed
12
      let: "s'" := ref (SOME ("x", "hd")) in
Zhen Zhang's avatar
Zhen Zhang committed
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
      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
    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.
111
    wp_bind (CmpXchg _ _ _)%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].
115
    * wp_cmpxchg_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
      { simpl. by eauto 10 with iFrame. }
118 119
      iModIntro. wp_pures. eauto.
    * wp_cmpxchg_fail.
Zhen Zhang's avatar
Zhen Zhang committed
120
      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_pures. 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
    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 (CmpXchg _ _ _).
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].
154
      + wp_cmpxchg_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.  }
162 163
        iModIntro. wp_pures. eauto.
      + wp_cmpxchg_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_pures. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
166 167
  Qed.
End proof.