treiber_stack.v 4.81 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
2
3
4
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Zhen Zhang's avatar
Zhen Zhang committed
5
6
From iris.algebra Require Import upred upred_big_op.
From iris.tests Require Import atomic.
Zhen Zhang's avatar
Zhen Zhang committed
7

Zhen Zhang's avatar
Zhen Zhang committed
8
Definition new_stack: val := λ: <>, ref (ref NONE).
Zhen Zhang's avatar
Zhen Zhang committed
9

Zhen Zhang's avatar
Zhen Zhang committed
10
11
12
Definition push: val :=
  rec: "push" "s" "x" :=
      let: "hd" := !"s" in
Zhen Zhang's avatar
Zhen Zhang committed
13
      let: "s'" := ref SOME ("x", "hd") in
Zhen Zhang's avatar
Zhen Zhang committed
14
      if: CAS "s" "hd" "s'"
Zhen Zhang's avatar
Zhen Zhang committed
15
        then #()
Zhen Zhang's avatar
Zhen Zhang committed
16
        else "push" "s" "x".
Zhen Zhang's avatar
Zhen Zhang committed
17

Zhen Zhang's avatar
Zhen Zhang committed
18
19
20
Definition pop: val :=
  rec: "pop" "s" :=
      let: "hd" := !"s" in
Zhen Zhang's avatar
Zhen Zhang committed
21
      match: !"hd" with
Zhen Zhang's avatar
Zhen Zhang committed
22
        SOME "pair" =>
Zhen Zhang's avatar
Zhen Zhang committed
23
        if: CAS "s" "hd" (Snd "pair")
Zhen Zhang's avatar
Zhen Zhang committed
24
          then SOME (Fst "pair")
Zhen Zhang's avatar
Zhen Zhang committed
25
          else "pop" "s"
Zhen Zhang's avatar
Zhen Zhang committed
26
27
28
      | NONE => NONE
      end.

Zhen Zhang's avatar
Zhen Zhang committed
29
30
31
Section proof.
  Context `{!heapG Σ} (N: namespace) (R: val  iProp Σ) `{ v, TimelessP (R v)}.

Zhen Zhang's avatar
Zhen Zhang committed
32
  Fixpoint is_stack' (hd: loc) (xs: list val) : iProp Σ :=
Zhen Zhang's avatar
Zhen Zhang committed
33
    match xs with
Zhen Zhang's avatar
Zhen Zhang committed
34
35
    | [] => ( q, hd { q } NONEV)%I
    | x :: xs => ( (hd': loc) q, hd { q } SOMEV (x, #hd')   R x  is_stack' hd' xs)%I
Zhen Zhang's avatar
Zhen Zhang committed
36
37
    end.

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

Zhen Zhang's avatar
Zhen Zhang committed
40
  Definition is_some_stack (s: loc): iProp Σ := ( xs, is_stack s xs)%I.
Zhen Zhang's avatar
Zhen Zhang committed
41
42
43
44
45

  Lemma new_stack_spec:
     (Φ: val  iProp Σ),
      heapN  N 
      heap_ctx  ( s, is_stack s [] - Φ #s)  WP new_stack #() {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
46
47
48
49
50
51
52
  Proof.
    iIntros (Φ HN) "[#Hh HΦ]". wp_seq.
    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.
Zhen Zhang's avatar
Zhen Zhang committed
53
54

  Definition push_triple (s: loc) (x: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
55
    atomic_triple (fun xs =>  R x  is_stack s xs)%I
Zhen Zhang's avatar
Zhen Zhang committed
56
57
58
59
60
61
62
63
                  (fun xs _ => is_stack s (x :: xs))
                  (nclose heapN)
                  
                  (push #s x).
  
  Lemma push_atomic_spec (s: loc) (x: val) :
    heapN  N  heap_ctx  push_triple s x.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
64
    iIntros (HN) "#?". rewrite /push_triple /atomic_triple.
Zhen Zhang's avatar
Zhen Zhang committed
65
66
67
68
    iIntros (P Q) "#Hvs".
    iLöb as "IH". iIntros "!# HP". wp_rec.
    wp_let. wp_bind (! _)%E.
    iVs ("Hvs" with "HP") as (xs) "[[Hx Hxs] [Hvs' _]]".
Zhen Zhang's avatar
Zhen Zhang committed
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
    simpl. iDestruct "Hxs" as (hd) "[Hs Hhd]".
    wp_load. iVs ("Hvs'" with "[Hx Hs Hhd]") as "HP".
    { rewrite /is_stack. iFrame. iExists hd. by iFrame. }
    iVsIntro. wp_let. wp_alloc l as "Hl". wp_let.
    wp_bind (CAS _ _ _)%E.
    iVs ("Hvs" with "HP") as (xs') "[[Hx Hxs] Hvs']".
    simpl. iDestruct "Hxs" as (hd') "[Hs Hhd']".
    destruct (decide (hd = hd')) as [->|Hneq].
    * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
      iVs ("Hvs'" $! #() with "[-]") as "HQ".
      {  iExists l. iFrame. iExists hd', 1%Qp. by iFrame. }
      iVsIntro. wp_if. iVsIntro. eauto.
    * wp_cas_fail.
      iDestruct "Hvs'" as "[Hvs' _]".
      iVs ("Hvs'" with "[-]") as "HP".
      {  iFrame. iExists hd'. by iFrame. }
      iVsIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
86
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
87
88
89

  Definition pop_triple (s: loc) :=
    atomic_triple (fun xs => is_stack s xs)%I
Zhen Zhang's avatar
Zhen Zhang committed
90
91
                  (fun xs ret => (ret = NONEV  xs = []  is_stack s []) 
                                 ( x, ret = SOMEV x   R x))%I (* FIXME: we can give a stronger one *)
Zhen Zhang's avatar
Zhen Zhang committed
92
93
94
                  (nclose heapN)
                  
                  (pop #s).
Zhen Zhang's avatar
Zhen Zhang committed
95
  
Zhen Zhang's avatar
Zhen Zhang committed
96
97
98
99
100
101
102
103
104
105
106
107
  Lemma pop_atomic_spec (s: loc) (x: val) :
    heapN  N  heap_ctx  pop_triple s.
  Proof.
    iIntros (HN) "#?".
    rewrite /pop_triple /atomic_triple.
    iIntros (P Q) "#Hvs".
    iLöb as "IH". iIntros "!# HP". wp_rec.
    wp_bind (! _)%E.
    iVs ("Hvs" with "HP") as (xs) "[Hxs Hvs']".
    destruct xs as [|y' xs'].
    - simpl. iDestruct "Hxs" as (hd) "[Hs Hhd]".
      wp_load. iDestruct "Hvs'" as "[_ Hvs']".
Zhen Zhang's avatar
Zhen Zhang committed
108
109
110
111
112
      iDestruct "Hhd" as (q) "[Hhd Hhd']".
      iVs ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
      { iLeft. iSplit=>//. iSplit=>//.
        iExists hd. iFrame. rewrite /is_stack'. eauto. }
      iVsIntro. wp_let. wp_load. wp_match.
Zhen Zhang's avatar
Zhen Zhang committed
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
      iVsIntro. by iExists [].
    - simpl. iDestruct "Hxs" as (hd) "[Hs Hhd]".
      simpl. iDestruct "Hhd" as (hd' q) "([Hhd Hhd'] & #Hy' & Hxs')".
      wp_load. iDestruct "Hvs'" as "[Hvs' _]".
      iVs ("Hvs'" with "[-Hhd]") as "HP".
      { iExists hd. iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
      iVsIntro. wp_let. wp_load. wp_match. wp_proj.
      wp_bind (CAS _ _ _). iVs ("Hvs" with "HP") as (xs) "[Hxs Hvs']".
      iDestruct "Hxs" as (hd'') "[Hs Hhd'']".
      destruct (decide (hd = hd'')) as [->|Hneq].
      + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
        iVs ("Hvs'" $! (SOMEV y') with "[]") as "HQ".
        { iRight. eauto. }
        iVsIntro. wp_if. wp_proj. eauto.
      + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
        iVs ("Hvs'" with "[-]") as "HP".
        { iExists hd''. by iFrame. }
        iVsIntro. wp_if. by iApply "IH".
  Qed.
      
Zhen Zhang's avatar
Zhen Zhang committed
133
134
End proof.