spec_graph.v 17.6 KB
Newer Older
1
From stdpp Require Import namespaces.
Hai Dang's avatar
Hai Dang committed
2

3
From gpfsl.logic Require Import logatom.
Hai Dang's avatar
Hai Dang committed
4
From gpfsl.examples.graph Require Export spec.
Hai Dang's avatar
Hai Dang committed
5

6
Require Import iris.prelude.options.
Hai Dang's avatar
Hai Dang committed
7

Hai Dang's avatar
Hai Dang committed
8
9
Local Open Scope Z_scope.

Hai Dang's avatar
Hai Dang committed
10
(** Queue events *)
Hai Dang's avatar
Hai Dang committed
11
Inductive qevent := Enq (v : Z) | Deq (v : Z) | EmpDeq (* | FAIL_DEQ *).
Hai Dang's avatar
Hai Dang committed
12
Notation dummy_qevt := (Enq 0).
Hai Dang's avatar
Hai Dang committed
13

Hai Dang's avatar
Hai Dang committed
14
15
16
17
18
19
Instance qevent_eq_dec : EqDecision qevent.
Proof. solve_decision. Defined.
Instance qevent_countable : Countable qevent.
Proof.
  refine (
    inj_countable'
20
21
22
      (λ e, match e with
            | Enq v => (1, v)
            | Deq v => (2, v)
23
            | EmpDeq => (3, 0) end)
24
25
26
27
      (λ x, match x with
            | (1, v) => Enq v
            | (2, v) => Deq v
            | _ => EmpDeq end) _);
Hai Dang's avatar
Hai Dang committed
28
29
    by intros [].
Qed.
Hai Dang's avatar
Hai Dang committed
30

31
32
Local Notation graph := (graph qevent).
Implicit Type (G : graph) (M : logView).
Hai Dang's avatar
Hai Dang committed
33

34
35
Definition unmatched_enq G eid : Prop :=
  ( v : Z, ge_event <$> (G.(Es) !! eid) = Some (Enq v)) 
Hai Dang's avatar
Hai Dang committed
36
    ( id, (eid, id)  G.(so)).
Hai Dang's avatar
Hai Dang committed
37
38
39
40

(** Queue predicates *)
Definition is_enqueue e v : Prop := e = Enq v.
Definition is_dequeue e v : Prop := e = Deq v.
41
42
Definition is_maybe_dequeue e : Prop :=
  match e with | Enq _ => False | _ => True end.
Hai Dang's avatar
Hai Dang committed
43

Hai Dang's avatar
Hai Dang committed
44
Definition QueueLocalT Σ : Type :=
45
  namespace  gname  loc  graph  logView  vProp Σ.
Hai Dang's avatar
Hai Dang committed
46
Definition QueueInvT Σ : Type :=
47
  gname  graph  vProp Σ.
Hai Dang's avatar
Hai Dang committed
48
49


Hai Dang's avatar
Hai Dang committed
50
(** Operation specs *)
51
Definition new_queue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Hai Dang's avatar
Hai Dang committed
52
  (new_queue : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
53
   N tid,
Hai Dang's avatar
Hai Dang committed
54
  {{{ True }}}
Hai Dang's avatar
Hai Dang committed
55
    new_queue [] @ tid; 
56
  {{{ γg (q: loc), RET #q; QueueLocal N γg q    QueueInv γg  }}}.
Hai Dang's avatar
Hai Dang committed
57

58
Definition enqueue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
59
60
  (enqueue : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
   N (DISJ: N ## histN) (q : loc) tid γg G1 M (V : view) (v : Z) (Posx: 0 < v),
61
  (* PRIVATE PRE *)
62
  V - QueueLocal N γg q G1 M - (* G1 is a snapshot of the graph, locally observed by M *)
Hai Dang's avatar
Hai Dang committed
63
  (* PUBLIC PRE *)
64
  <<<  G,  QueueInv γg G >>>
65
    enqueue [ #q ; #v] @ tid; N
66
  <<<  V' G' (enqId : event_id) enq Venq M',
67
      (* PUBLIC POST *)
68
       QueueInv γg G' 
69
      V'  @{V'} QueueLocal N γg q G' M' 
70
       G  G'  M  M' 
71
        V  Venq.(dv_in)  Venq.(dv_wrt) = V' 
Hai Dang's avatar
Hai Dang committed
72
        (* enq is a new enqueue event with which G' strictly extends G *)
73
        is_enqueue enq v 
74
75
        enqId = length G.(Es) 
        G'.(Es) = G.(Es) ++ [mkGraphEvent enq Venq M'] 
76
        G'.(so) = G.(so)  G'.(com) = G.(com) 
Hai Dang's avatar
Hai Dang committed
77
        enqId  M' (* << M' may also acquire more events that
78
79
          come with the Enqueue (acquired by reading the Head pointer). *) 
        enqId  M ,
Hai Dang's avatar
Hai Dang committed
80
      (* RETURN VALUE AT COMMITTING POINT *)
Hai Dang's avatar
Hai Dang committed
81
      RET #, emp >>>
Hai Dang's avatar
Hai Dang committed
82
  .
Hai Dang's avatar
Hai Dang committed
83

84
Definition dequeue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
85
86
  (dequeue : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
   N (DISJ: N ## histN) (q : loc) tid γg G1 M V,
87
  (* PRIVATE PRE *)
88
  V - QueueLocal N γg q G1 M -
Hai Dang's avatar
Hai Dang committed
89
  (* PUBLIC PRE *)
90
  <<<  G,  QueueInv γg G >>>
91
    dequeue [ #q] @ tid; N
92
  <<<  (v: Z) V' G' enqId deqId enq deq Vdeq M',
93
      (* PUBLIC POST *)
94
       QueueInv γg G' 
95
      V'  @{V'} QueueLocal N γg q G' M' 
96
       G  G'  M  M' 
97
        V  Vdeq.(dv_in)  Vdeq.(dv_comm) = V' 
98
99
        ( (* EMPTY case *)
          (v = 0  deq = EmpDeq 
100
101
            deqId = length G.(Es) 
            G'.(Es) = G.(Es) ++ [mkGraphEvent deq Vdeq M'] 
102
            G'.(so) = G.(so)  G'.(com) = G.(com) 
103
            {[deqId]}  M  M'  deqId  M)
104
         (* successful case *)
105
106
          (0 < v  is_enqueue enq v  is_dequeue deq v 
          deqId = length G.(Es) 
107
          ( id, (enqId, id)  G.(so)) 
108
          G'.(Es) = G.(Es) ++ [mkGraphEvent deq Vdeq M'] 
Hai Dang's avatar
Hai Dang committed
109
110
          G'.(so) = {[(enqId, deqId)]}  G.(so) 
          G'.(com) = {[(enqId, deqId)]}  G.(com) 
111
112
          enqId  M'  deqId  M'  deqId  M 
           eV, G.(Es) !! enqId = Some eV  eV.(ge_event) = enq  eV.(ge_lview)  M') ) ,
113
      (* RETURN VALUE AT COMMITTING POINT *)
Hai Dang's avatar
Hai Dang committed
114
      RET #v, emp >>>
Hai Dang's avatar
Hai Dang committed
115
116
117
  .


118
Definition try_enq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
119
120
  (try_enq : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
   N (DISJ: N ## histN) (q : loc) tid γg G1 M (V : view) (v : Z) (Posx: 0 < v),
Hai Dang's avatar
Hai Dang committed
121
  (* PRIVATE PRE *)
122
  V - QueueLocal N γg q G1 M -
Hai Dang's avatar
Hai Dang committed
123
  (* PUBLIC PRE *)
124
  <<<  G,  QueueInv γg G >>>
125
    try_enq [ #q ; #v] @ tid; N
126
  <<<  (b: bool) V' G' (enqId : event_id) enq Venq M',
Hai Dang's avatar
Hai Dang committed
127
      (* PUBLIC POST *)
128
       (QueueInv γg G') 
129
      V'  @{V'} QueueLocal N γg q G' M' 
130
       G  G'  M  M' 
131
        V  Venq.(dv_in)  Venq.(dv_wrt) = V' 
Hai Dang's avatar
Hai Dang committed
132
          if b is false then
133
            G' = G
Hai Dang's avatar
Hai Dang committed
134
135
136
          else
            (* enq is a new enqueue event with which G' strictly extends G *)
            is_enqueue enq v 
137
138
            enqId = length G.(Es) 
            G'.(Es) = G.(Es) ++ [mkGraphEvent enq Venq M'] 
Hai Dang's avatar
Hai Dang committed
139
            G'.(so) = G.(so)  G'.(com) = G.(com) 
140
            enqId  M'  enqId  M ,
Hai Dang's avatar
Hai Dang committed
141
      (* RETURN VALUE AT COMMITTING POINT *)
Hai Dang's avatar
Hai Dang committed
142
      RET #b, emp >>>
Hai Dang's avatar
Hai Dang committed
143
144
  .

145
Definition try_deq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
146
147
  (try_deq : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
   N (DISJ: N ## histN) (q : loc) tid γg G1 M V,
Hai Dang's avatar
Hai Dang committed
148
  (* PRIVATE PRE *)
149
  V - QueueLocal N γg q G1 M -
Hai Dang's avatar
Hai Dang committed
150
  <<< (* PUBLIC PRE *)
151
       G,  (QueueInv γg G) >>>
152
    try_deq [ #q] @ tid; N
153
  <<<  (v: Z) V' G' enqId deqId enq deq Vdeq M',
Hai Dang's avatar
Hai Dang committed
154
      (* PUBLIC POST *)
155
       (QueueInv γg G') 
156
      V'  @{V'} QueueLocal N γg q G' M' 
157
       G  G'  M  M' 
158
        V  Vdeq.(dv_in)  Vdeq.(dv_comm) = V' 
Hai Dang's avatar
Hai Dang committed
159
          (* FAIL case *)
160
        ((v < 0  G' = G)
Hai Dang's avatar
Hai Dang committed
161
162
         (* EMPTY case *)
          (v = 0  deq = EmpDeq 
163
164
            deqId = length G.(Es) 
            G'.(Es) = G.(Es) ++ [mkGraphEvent deq Vdeq M'] 
Hai Dang's avatar
Hai Dang committed
165
            G'.(so) = G.(so)  G'.(com) = G.(com) 
166
            {[deqId]}  M  M'  deqId  M)
Hai Dang's avatar
Hai Dang committed
167
         (* successful case *)
168
169
          (0 < v  is_enqueue enq v  is_dequeue deq v 
          deqId = length G.(Es) 
Hai Dang's avatar
Hai Dang committed
170
          ( id, (enqId, id)  G.(so)) 
171
          G'.(Es) = G.(Es) ++ [mkGraphEvent deq Vdeq M'] 
Hai Dang's avatar
Hai Dang committed
172
173
          G'.(so) = {[(enqId, deqId)]}  G.(so) 
          G'.(com) = {[(enqId, deqId)]}  G.(com) 
174
175
          enqId  M'  deqId  M'  deqId  M 
           eV, G.(Es) !! enqId = Some eV  eV.(ge_event) = enq  eV.(ge_lview)  M') ) ,
Hai Dang's avatar
Hai Dang committed
176
      (* RETURN VALUE AT COMMITTING POINT *)
Hai Dang's avatar
Hai Dang committed
177
      RET #v, emp >>>
Hai Dang's avatar
Hai Dang committed
178
179
  .

Hai Dang's avatar
Hai Dang committed
180
(** Bundling of specs *)
181
Record core_queue_spec {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
182
  {QueueConsistent : graph  Prop} := QueueSpec {
Hai Dang's avatar
Hai Dang committed
183
184
185
186
187
  (* operations *)
  new_queue : val;
  enqueue : val;
  dequeue : val;
  (* predicates *)
Hai Dang's avatar
Hai Dang committed
188
189
  QueueLocal : QueueLocalT Σ;
  QueueInv : QueueInvT Σ;
Hai Dang's avatar
Hai Dang committed
190
  (** predicates properties *)
191
192
193
  QueueInv_Timeless :  γg G, Timeless (QueueInv γg G);
  QueueInv_Objective :  γg G, Objective (QueueInv γg G);
  QueueInv_QueueConsistent :  γg G, QueueInv γg G   QueueConsistent G ;
Hai Dang's avatar
Hai Dang committed
194
  QueueInv_graph_master_acc :
195
196
     γg G, QueueInv γg G  graph_master γg (1/2) G 
                                (graph_master γg (1/2) G - QueueInv γg G);
197

Hai Dang's avatar
Hai Dang committed
198
  QueueLocal_graph_snap :
199
     N γg q G M, QueueLocal N γg q G M  graph_snap γg G M;
Hai Dang's avatar
Hai Dang committed
200
  QueueLocal_Persistent :
201
202
     N γg q G M, Persistent (QueueLocal N γg q G M);

Hai Dang's avatar
Hai Dang committed
203
204
  (* operations specs *)
  new_queue_spec : new_queue_spec' new_queue QueueLocal QueueInv;
205
206
  enqueue_spec : enqueue_spec' enqueue QueueLocal QueueInv;
  dequeue_spec : dequeue_spec' dequeue QueueLocal QueueInv;
Hai Dang's avatar
Hai Dang committed
207
}.
Hai Dang's avatar
Hai Dang committed
208

209
210
211
212
213
214
215
216
217
218
219
220
221
222
Arguments core_queue_spec _ {_ _} _.

Record extended_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
  (QueueConsistent : graph  Prop) := ExtendedQueueSpec {
  extended_core_spec :> core_queue_spec Σ QueueConsistent ;
  (* extra operations *)
  try_enq : val;
  try_deq : val;
  (* operations specs *)
  try_enq_spec :
    try_enq_spec' try_enq extended_core_spec.(QueueLocal) extended_core_spec.(QueueInv);
  try_deq_spec :
    try_deq_spec' try_deq extended_core_spec.(QueueLocal) extended_core_spec.(QueueInv);
}.
Hai Dang's avatar
Hai Dang committed
223

224
225
226
227
228
229
230
231
(* only enqueue positive values *)
Definition queue_positive_value G : Prop :=
   e eV (v: Z), G.(Es) !! e = Some eV  eV.(ge_event) = Enq v  0 < v.

(** (2) com relates matching enqueue and dequeu events *)
Definition queue_matches_value G : Prop :=
   e d, (e, d)  G.(com)  (e < d)%nat 
     eV dV (v : Z), G.(Es) !! e = Some eV  G.(Es) !! d = Some dV 
232
233
234
      eV.(ge_event) = Enq v  dV.(ge_event) = Deq v 
      (* so is synchronizing at commit points *)
      eV.(ge_view).(dv_comm)  dV.(ge_view).(dv_comm).
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261

(** (4) every unmatched dequeue returns empty *)
Definition queue_unmatched_deq_empty G : Prop :=
   e eV, G.(Es) !! e = Some eV 
    is_maybe_dequeue eV.(ge_event) 
    e  (elements G.(com)).*2 
    eV.(ge_event) = EmpDeq.

(** (5) a dequeue with a previous unmatched enqueue cannot return empty. *)
Definition queue_empty_unmatched_enq G : Prop :=
   d dV, G.(Es) !! d = Some dV  dV.(ge_event) = EmpDeq 
     e, e  dV.(ge_lview)  ¬ unmatched_enq G e.
(* A stronger version *)
Definition queue_empty_unmatched_enq_strong G : Prop :=
   d dV, G.(Es) !! d = Some dV  dV.(ge_event) = EmpDeq 
     e v eV, G.(Es) !! e = Some eV  eV.(ge_event) = Enq v 
      e  dV.(ge_lview)   de, (e, de)  G.(com)  de  dV.(ge_lview).

(* This encodes enough properties for xo so that we can show xo
  to be the total (linearization) order similar to that of Yacovet's (7ii).
  This task can be done in the linearizability step.

  This is a strong property. We can also weaken it to just require (e1,e2) ∈ hb,
  instead of (e1,e2) ∈ xo.
  See more weakenings below.

  On the other hand, we can also strengthen it further by changing the
Hai Dang's avatar
Hai Dang committed
262
  conclusion from [(d1,d2) ∈ xo] to [(d1,d2) ∈ eco]. *)
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
Definition queue_FIFO_strong G : Prop :=
   e1 v1 eV1 e2 d2,
    G.(Es) !! e1 = Some eV1  eV1.(ge_event) = Enq v1 
    (e2, d2)  G.(com)  (* if e2 is already dequeued *)
    (e1  e2)%nat  (* and e1 is before e2 in xo--- (e1,e2) ∈ xo *)
    (* then e1 must also have been dequeued with d1, which,
    by [queue_matches_value], should also come before d2 in xo. *)
     d1, (d1  d2)%nat  (e1, d1)  G.(com). (* (d1, d2) ∈ xo ∧ (e1, d1) ∈ com *)

(* A weakening that is not so weak *)
Definition queue_FIFO G : Prop :=
   e1 eV1 v1 e2 d2 eV2,
    G.(Es) !! e1 = Some eV1  eV1.(ge_event) = Enq v1 
    (e2, d2)  G.(com)   (* (e2, d2) ∈ com *)
    G.(Es) !! e2 = Some eV2 
    e1  eV2.(ge_lview)  (* (e1,e2) ∈ eco *)
     d1, (e1,d1)  G.(com)  (* (e1, d1) ∈ com *)
     dV1, G.(Es) !! d1 = Some dV1 
    e1  e2  d2  dV1.(ge_lview) (* (d2, d1) ∉ eco *)
  .

(* Alternatively, if e2 as an enqueue that has been dequeued but also observed
Hai Dang's avatar
Hai Dang committed
285
286
  an enqueue e1, then e1 must also have been dequeued.
  This encodes the Yacovet's condition [com^-1; lhb; com; lhb is irreflexive]. *)
287
288
289
290
291
292
293
294
295
Definition queue_FIFO_weak G :=
   e1 d1 dV1 e2 d2 eV2,
    (e1, d1)  G.(com)  (e2, d2)  G.(com) 
    e1  e2  (* e1 and e2 are distinct *)
    G.(Es) !! d1 = Some dV1  G.(Es) !! e2 = Some eV2 
    e1  eV2.(ge_lview)  (* (e1, e2) ∈ eco *)
    d2  dV1.(ge_lview)   (* (d2,d1) ∉ eco *)
  .

296
297
298
(** * Basic Queue Consistency *)
Record BasicQueueConsistent G : Prop := mkBasicQueueConsistent {
  bsq_cons_enq_non_zero : (* 0 is used for Empty Dequeue *)
299
    queue_positive_value G ;
Hai Dang's avatar
Hai Dang committed
300
  (* (1)-(7) Weak queue spec from POPL'19 Library Correctness paper *)
Hai Dang's avatar
Hai Dang committed
301
    (* (1) at most 1 Constructor event: we currently don't have initialization events *)
302
  bsq_cons_matches :
Hai Dang's avatar
Hai Dang committed
303
    (* (2) There can only be so edges between matching enqueues and dequeues *)
304
    queue_matches_value G ;
305
  bsq_cons_com_functional :
Hai Dang's avatar
Hai Dang committed
306
    (* (3) com and com^-1 are functional: *)
307
    functional_pair G.(com) ;
308
  bsq_cons_unmatched_dequeue_empty :
309
310
    (* (4) every unmatched dequeue returns empty  *)
      queue_unmatched_deq_empty G ;
311
  bsq_cons_non_empty :
312
313
314
    (* (5) a dequeue with a previous unmatched enqueue cannot return empty.
    But we can prove a stronger property: *)
    queue_empty_unmatched_enq_strong G ;
315
  bsq_cons_so_com :
Hai Dang's avatar
Hai Dang committed
316
317
    (* (6) so and com agree *)
    G.(so) = G.(com) ;
318
  bsq_cons_FIFO_a :
319
    (* xo must agree with logview-inclusion. *)
320
321
    graph_xo_eco G.(Es) ;
  bsq_cons_FIFO_b :
Hai Dang's avatar
Hai Dang committed
322
    (* (7b) "If we know that e1 happens before e2, then it is impossible that d2
Hai Dang's avatar
Hai Dang committed
323
            happens before d1."
Hai Dang's avatar
Hai Dang committed
324
      Here, e1 happens-before e2 would mean that e2 has seen e1, i.e.
325
326
      (e1,e2) ∈ eco ∧ e1 ≠ e2. *)
    queue_FIFO G ;
Hai Dang's avatar
Hai Dang committed
327
328
}.

329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
(** * Weak Consistency *)
Record WeakQueueConsistent G : Prop := mkWeakQueueConsistent {
  wkq_cons_write : (* all non-empty events are writes *)
    graph_event_is_writing G.(Es) (. EmpDeq) ;
  wkq_cons_enqueue_release : (* enqueue is releasing *)
    graph_event_is_releasing G.(Es) (λ eg,  v, eg = Enq v) ;
  wkq_cons_dequeue_acquire : (* dequeue is acquiring *)
    graph_event_is_acquiring G.(Es) (λ eg,  v, eg = Deq v) ;

  wkq_bsq_cons :> BasicQueueConsistent G;
}.

(** * Strong Consistency *)
Record StrongQueueConsistent G : Prop := mkStrongQueueConsistent {
  strq_cons_relacq : (* the message view is the same as the commiter's view *)
    graph_event_is_relacq G.(Es) (λ _, True) ;

  strq_wkq_cons :> WeakQueueConsistent G ;

  strq_cons_FIFO_b :
  (* (7b) stronger FIFO *)
    queue_FIFO_strong G ;
}.

(** A strong queue spec *)
Definition strong_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
  := extended_queue_spec Σ StrongQueueConsistent.

357
(** A Weak queue spec *)
358
Definition weak_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
359
  := core_queue_spec Σ WeakQueueConsistent.
Hai Dang's avatar
Hai Dang committed
360

361
362
363
(** Basic queue spec *)
Definition basic_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
  := core_queue_spec Σ BasicQueueConsistent.
Hai Dang's avatar
Hai Dang committed
364

365
(** Strong implies Weak *)
Hai Dang's avatar
Hai Dang committed
366
Program Definition strong_weak_queue_spec
367
368
  {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
  (sq : strong_queue_spec Σ) : weak_queue_spec Σ :=
Hai Dang's avatar
Hai Dang committed
369
  {|
Hai Dang's avatar
Hai Dang committed
370
    QueueInv_Timeless         := sq.(QueueInv_Timeless);
Hai Dang's avatar
Hai Dang committed
371
372
373
374
375
376
377
378
379
    QueueInv_Objective        := sq.(QueueInv_Objective);
    QueueInv_graph_master_acc := sq.(QueueInv_graph_master_acc);
    QueueLocal_graph_snap     := sq.(QueueLocal_graph_snap) ;
    QueueLocal_Persistent     := sq.(QueueLocal_Persistent) ;
    new_queue_spec            := sq.(new_queue_spec) ;
    enqueue_spec              := sq.(enqueue_spec) ;
    dequeue_spec              := sq.(dequeue_spec) ;
  |}.
Next Obligation.
Hai Dang's avatar
Hai Dang committed
380
  iIntros "* QI".
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
  by iDestruct (sq.(QueueInv_QueueConsistent) with "QI") as %SC%strq_wkq_cons.
Qed.

(** Weak implies Basic *)
Program Definition weak_basic_queue_spec
  {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
  (wq : weak_queue_spec Σ) : basic_queue_spec Σ :=
  {|
    QueueInv_Timeless         := wq.(QueueInv_Timeless);
    QueueInv_Objective        := wq.(QueueInv_Objective);
    QueueInv_graph_master_acc := wq.(QueueInv_graph_master_acc);
    QueueLocal_graph_snap     := wq.(QueueLocal_graph_snap) ;
    QueueLocal_Persistent     := wq.(QueueLocal_Persistent) ;
    new_queue_spec            := wq.(new_queue_spec) ;
    enqueue_spec              := wq.(enqueue_spec) ;
    dequeue_spec              := wq.(dequeue_spec) ;
  |}.
Next Obligation.
  iIntros "* QI".
  by iDestruct (wq.(QueueInv_QueueConsistent) with "QI") as %SC%wkq_bsq_cons.
Hai Dang's avatar
Hai Dang committed
401
Qed.
Hai Dang's avatar
Hai Dang committed
402
403

(** Some properties *)
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
Lemma BasicQueueConsistent_empty : BasicQueueConsistent .
Proof. done. Qed.

Lemma WeakQueueConsistent_empty : WeakQueueConsistent .
Proof. constructor; [done..|apply BasicQueueConsistent_empty]. Qed.

Lemma StrongQueueConsistent_empty : StrongQueueConsistent .
Proof. constructor; [done|apply WeakQueueConsistent_empty|done]. Qed.

Lemma queue_FIFO_strong_FIFO G :
  graph_xo_eco G.(Es)  functional_pair G.(com) 
  queue_FIFO_strong G  queue_FIFO G.
Proof.
  intros EC FP F e1 eV1 v1 e2 d2 eV2 Eqe1 Eqv1 InCo Eqe2 Ine2.
  specialize (F _ _ _ _ _ Eqe1 Eqv1 InCo (EC _ _ _ Eqe2 Ine2))
    as (d1 & Le12 & InCo1).
  exists d1. split; [done|].
  intros dV1 Eqd1 NEq Ind1. apply NEq.
  assert (d2 = d1) as ->.
  { apply (anti_symm le); [|done]. apply (EC _ _ _ Eqd1 Ind1). }
  destruct FP as [_ F2]. by apply (F2 _ _ InCo1 InCo eq_refl).
Qed.

Lemma BasicQueueConsistent_FIFO_weak G :
  BasicQueueConsistent G  queue_FIFO_weak G.
Proof.
  destruct 1 as [_ CON2 [CON3a CON3b] CON4 CON5 CON6 CON7a CON7b].
  intros e1 d1 dV1 e2 d2 eV2 InG1 InG2 NEq Eqd1 Eq2 Ine1 Ind2.
  destruct (CON2 _ _ InG1) as [Lt1 (eV1 & dV1' & v1 & Eqe1 & Eqd1' & Eqv1 & ?)].
  rewrite Eqd1 in Eqd1'; inversion Eqd1'; clear Eqd1'; subst dV1'.
  specialize (CON7b _ _ _ _ _ _ Eqe1 Eqv1 InG2 Eq2 Ine1) as (d1' & Ind1' & CASE).
  assert (Eqd := CON3a _ _ InG1 Ind1' eq_refl). simpl in Eqd. subst d1'.
  destruct (CON2 _ _ InG2) as [Lt2 (eV2' & dV2 & v2 & Eqe2 & Eqd2 & ?)].
  rewrite Eq2 in Eqe2; inversion Eqe2; clear Eqe2; subst eV2'.
  assert (LE1 := CON7a _ _ _ Eq2 Ine1).
  assert (LE2 := CON7a _ _ _ Eqd1 Ind2).
  by apply (CASE _ Eqd1 NEq).
Qed.

443
444
445
Lemma unmatched_enq_mono G G' eid :
  G  G'  is_Some (G.(Es) !! eid) 
  unmatched_enq G' eid  unmatched_enq G eid.
Hai Dang's avatar
Hai Dang committed
446
Proof.
447
448
449
  intros LeG' [? Eq] [[v Eq'] FA].
  destruct (G'.(Es) !! eid) as [[? V]|] eqn:Eq''; [|done]. simpl in Eq'.
  rewrite (prefix_lookup _ _ _ _ Eq) in Eq''; [|apply LeG']. simplify_eq.
Hai Dang's avatar
Hai Dang committed
450
451
452
453
  split.
  - exists v. by rewrite Eq.
  - intros e' ?. apply (FA e'); by apply LeG'.
Qed.