MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

pipeline.v 9.12 KB
Newer Older
1
2
From iris.algebra Require Import excl_auth csum numbers list.
From iris.base_logic Require Import invariants.
3
4
5
From cosmo.base Require Import base Zlist lattice_cmra.
From cosmo.program_logic Require Export proofmode atomic.
From cosmo.examples Require bounded_queue.
6
7
8
9
10
11
12

Set Default Proof Using "Type".
Open Scope Z.

(** Implementation **)

(* This must NOT be a value since it may be open. *)
13
(* Beware that this notation captures the variables "_for", "_i", "_start" and "_stop". *)
14
15
16
17
18
19
20
21
22
Notation For iname start stop body :=
  ((let: "_stop" := stop in
    rec: "_for" "_i" :=
      if: "_i"  "_stop" then
        let: iname := "_i" in
        body ;; "_for" ("_i" + #1)
      else
        #()
   ) start)%E.
23
24
25
26
27
28
29
30
31

Notation "'for:' i 'from' e1 'to' e2 'do' e3 'enddo'" := (For i e1%E e2%E e3%E)
  (at level 200, e1, e2, e3 at level 200,
   format "'[' 'for:'  i  'from'  e1  'to'  e2  'do'  '/  ' e3  '/' 'enddo' ']'") : expr_scope.

Section pipeline.

Context (capacity : nat) (capacity_min : capacity  1).

32
33
(*
   ICFP21: Here is a simple client code that makes uses of the data structure
34
   defined in bounded_queue.v. It corresponds to the code listings in Figure 11
35
36
37
   of the paper.
 *)

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
Definition pipeline : val := λ: "f" "g" "xs",
  let: "q" := (bounded_queue.make capacity) #() in
  let: "n" := Length "xs" in
  Fork (
    for: "i" from #0 to "n" - #1 do
      let: "x" := Read NonAtomic "xs" "i" in
      let: "y" := "f" "x" in
      (bounded_queue.enqueue capacity) "q" "y"
    enddo
  ) ;;
  let: "zs" := Alloc NonAtomic "n" #() in
  for: "i" from #0 to "n" - #1 do
    let: "y" := (bounded_queue.dequeue capacity) "q" in
    let: "z" := "g" "y" in
    Write NonAtomic "zs" "i" "z"
  enddo ;;
  "zs".

(** Specification **)

Class pipelineG Σ := {
  (* the shared queue: *)
  pipelineG_queue :> (bounded_queue.queueG capacity capacity_min) Σ ;
  (* both cursors: *)
  pipelineG_cur :> inG Σ (excl_authR natO) ;
}.

Section Spec.

67
  Context `{!cosmoG Σ, !pipelineG Σ}.
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

  Implicit Types (γqueue γcur_f γcur_g : gname) (q : val) (i cur_f cur_g : nat).
  Implicit Types (f g : val).
  Implicit Types (R : nat  val  vProp Σ).
  Implicit Types (xs_array zs_array : location).
  Implicit Types (x y z : val) (xs zs : list val).
  Implicit Types (V : view) (yV : val * view) (yVs : list (val * view)).

  Open Scope Z.

  Definition pipelineN : namespace :=
    nroot .@ "pipeline".

  Notation seq' a b := (seq a%nat (b - a)%nat).

83
84
  (*
    ICFP21: Here is the internal invariant of the pipeline, as described in
85
    Figure 13 of the paper.
86
87
88
89
90
91
    
    pipeline_proto is what the paper calls PipeInvInner.
    f_thread is what the paper calls PipeF.
    g_thread is what the paper calls PipeG.
   *)

92
  Definition pipeline_proto f g R xs γqueue γcur_f γcur_g : iProp Σ := (
93
94
     yVs cur_f cur_g Vt Vh,
        (bounded_queue.is_queue capacity capacity_min) γqueue Vt Vh yVs
95
96
97
98
       own γcur_f (E cur_f)
       own γcur_g (E cur_g)
       cur_g  cur_f
       length yVs = (cur_f - cur_g)%nat
99
       [ list] iyV  yVs, let '(y, V) := yV in
100
101
102
103
104
105
106
          WP g (Val y) {{ λ z, R (i + cur_g)%nat z }} V
  )%I.

  Definition f_thread f g R xs xs_array γcur_f cur_f : vProp Σ := (
      own γcur_f (E cur_f)
     xs_array * xs
     cur_f  length xs
107
     [ list] ix  drop cur_f xs,
108
109
110
111
112
113
114
115
        WP f (Val x) {{ λ y, WP g y {{ λ z, R (i + cur_f)%nat z }} }}
  )%I.

  Definition g_thread f g R xs zs_array zs γcur_g cur_g : vProp Σ := (
      own γcur_g (E cur_g)
     cur_g  length xs
     zs_array * zs
     length zs = length xs
116
     [ list] iz  take cur_g zs, R i z
117
118
  )%I.

119
  (*
120
    ICFP21: Here is the spec of the pipeline, as shown in Figure 12 of the paper,
121
122
123
    along with its proof.
  *)

124
125
126
127
  Theorem pipeline_spec f g R xs xs_array :
    {{{
        xs_array * xs
       has_length xs_array (length xs)
128
       [ list] ix  xs,
129
130
131
132
133
134
          WP f (Val x) {{ λ y, WP g y {{ λ z, R i z }} }}
    }}}
        pipeline f g #xs_array
    {{{ zs_array zs, RET #zs_array ;
        zs_array * zs
       length zs = length xs
135
       [ list] iz  zs, R i z
136
    }}}.
137
  Proof using All.
138
139
140
141
142
143
144
145
146
147
    iIntros (Φ) "(Hxs & Hlen & HR) HΦ".
    wp_lam; wp_let.
    wp_apply (bounded_queue.make_spec capacity capacity_min) ; first solve_monPred_in.
    iIntros (q γqueue) "[#Hqueue_inv Hqueue]".
    (* create ghost variables *)
    iMod (own_alloc (E 0%nat  E 0%nat)) as (γcur_f) "[Hγcur_f● Hγcur_f◯]".
    { by apply auth_both_valid_discrete. }
    iMod (own_alloc (E 0%nat  E 0%nat)) as (γcur_g) "[Hγcur_g● Hγcur_g◯]".
    { by apply auth_both_valid_discrete. }
    (* create invariant *)
148
    iMod (inv_alloc pipelineN _ (pipeline_proto f g R xs γqueue γcur_f γcur_g)
149
150
151
152
153
154
155
156
157
          with "[Hqueue Hγcur_f● Hγcur_g●]")  as "#I".
    { rewrite /pipeline_proto. repeat (iExists _). iFrame. by cbn. }
    (* fork *)
    wp_apply (wp_length with "Hlen").
    wp_apply (wp_fork with "[Hxs HR Hγcur_f◯]").
    {
      iAssert (f_thread f g R _ _ _ _) with "[$Hγcur_f◯ $Hxs HR]" as "F".
      { setoid_rewrite Nat.add_0_r. iFrame "HR". iPureIntro ; lia. }
      rewrite (_ : #0 = #0%nat) // ; set cur_f := 0%nat ; clearbody cur_f.
158
159
160
161
162
163
164
165
      iIntros "!>". wp_pures. iLöb as "IH" forall (cur_f).
      wp_pures. case_bool_decide; wp_pures; [|done].
      iDestruct "F" as "(Hγcur_f◯ & Hxs & _ & Hfwps)".
      wp_read_na_block as xs_cur_f EQxs. wp_pures.
      apply list_lookup_Z_Some_to_nat in EQxs. rewrite Nat2Z.id in EQxs.
      erewrite drop_S; [|done]. iDestruct "Hfwps" as "[Hfwp Hfwps]".
      wp_bind (f xs_cur_f). iApply (wp_wand with "Hfwp"). iIntros (y) "Hgwp". wp_pures.
      iDestruct (monPred_in_intro with "Hgwp") as (Vgwp) "[#HVgwp Hgwp]".
166
167
168
      iDestruct (bi.later_intro with "Hgwp") as "Hgwp". (* Make laterable. *)
      awp_apply (bounded_queue.enqueue_spec _ _ (pipelineN) with "Hqueue_inv HVgwp")
        without "Hfwps"; [solve_ndisj|] .
169
170
      iInv "I" as (yVs cur_f' cur_g Vt Vh) "(>Hq & >Hγcur_f● & >Hγcur_g● & >% & >% & Hgwps)".
      iDestruct (own_valid_2 with "Hγcur_f● Hγcur_f◯") as %->%excl_auth_agree_L.
171
172
      iAaccIntro with "Hq".
      { (* Abort *) iIntros "Hq !>". iFrame. iExists _, _, _, _, _. iFrame. auto. }
173
174
175
176
      (* Commit *)
      iIntros "[Hq _]".
      iMod (own_update_2 with "Hγcur_f● Hγcur_f◯") as "[Hγcur_f● Hγcur_f◯]".
      { apply (excl_auth_update _ _ (S cur_f)). }
177
      iSplitR "Hxs Hγcur_f◯".
178
      - iExists _, _, _, _, _. iFrame "Hγcur_f● Hγcur_g● Hq".
179
180
        rewrite big_sepL_app app_length /=
                (_ : (length yVs + 0 + cur_g = cur_f)%nat); [|lia].
181
        rewrite -embed_later /=. iFrame. auto with lia.
182
      - iIntros "!> Hfwps". wp_pures. rewrite (_ : cur_f + 1 = S cur_f); [|lia].
183
184
        iApply "IH". iFrame. iSplitR; [auto with lia|].
        by setoid_rewrite Nat.add_succ_comm.
185
186
187
188
189
    }
    {
      wp_alloc zs_array as "Hzs". iSpecialize ("HΦ" $! zs_array).
      iAssert (g_thread f g R xs _ _ _ _) with "[$Hγcur_g◯ $Hzs]" as "G".
      { rewrite /take/= replicate_length. iPureIntro ; lia. }
190
      generalize (replicate (Z.to_nat (length xs)) #())=>zs. wp_let.
191
      rewrite (_ : #0 = #0%nat) // ; set cur_g := 0%nat ; clearbody cur_g.
192
193
194
195
196
      wp_pures. iLöb as "IH" forall (cur_g zs).
      case_bool_decide; wp_pures; last first.
      { iApply "HΦ". iDestruct "G" as "(_ & % & $ & % & HR)". iFrame "%".
        rewrite take_ge //. lia. }
      iDestruct "G" as "(Hγcur_g◯ & _ & Hzs & % & HR)".
197
198
      awp_apply (bounded_queue.dequeue_spec _ _ (pipelineN) with "Hqueue_inv []")
        without "HR HΦ"; [solve_ndisj|by iApply monPred_in_bot|].
199
200
      iInv "I" as (yVs cur_f cur_g' Vt Vh) "(>Hq & >Hγcur_f● & >Hγcur_g● & >% & >% & Hgwps)".
      iDestruct (own_valid_2 with "Hγcur_g● Hγcur_g◯") as %->%excl_auth_agree_L.
201
      iAaccIntro with "Hq".
202
203
204
205
206
207
      { (* Abort *) iIntros "Hq". iFrame. iExists _, _, _, _, _. iFrame. auto. }
      (* Commit *)
      iIntros ([y Vy] yVs') "(-> & Hq & _ & #HVy) /=".
      iMod (own_update_2 with "Hγcur_g● Hγcur_g◯") as "[Hγcur_g● Hγcur_g◯]".
      { apply (excl_auth_update _ _ (S cur_g)). }
      iDestruct "Hgwps" as "[Hgwp Hgwps]".
208
      iModIntro. iSplitR "Hzs Hγcur_g◯ Hgwp".
209
210
211
212
      - iExists _, _, _, _, _. iFrame "Hq Hγcur_f● Hγcur_g●".
        do 2 (iSplitR; [iPureIntro; simpl in *; lia|]).
        do 2 iModIntro. iApply (big_sepL_impl with "Hgwps").
        iIntros "!>" (k [??] ?). rewrite Nat.add_succ_r. auto.
213
      - iIntros "[HR HΦ]". wp_pures. iDestruct (monPred_in_elim with "HVy Hgwp") as "Hgwp".
214
215
216
217
218
219
220
        wp_bind (g y). iApply (wp_wand with "Hgwp"). iIntros (z) "Hz". wp_pures.
        wp_write_na_block. wp_pures.
        rewrite (_ : cur_g + 1 = S cur_g); [|lia].
        iApply ("IH" with "HΦ"). iFrame.
        rewrite list_insert_Z_to_nat; [|lia]. rewrite Nat2Z.id.
        iSplitR; [iPureIntro; lia|]. iSplitR; [by rewrite insert_length|].
        erewrite take_S_r; [|apply list_lookup_insert; lia].
221
        rewrite big_sepL_app /= take_insert; [|done]. iFrame.
222
223
        rewrite take_length Min.min_l; [|lia]. by rewrite 2!right_id. }
  Qed.
224
End Spec.
225
End pipeline.