blob: 0ea3a4a316a391fbfbd447e034bb1eeedf763501 (
about) (
plain) (
blame)
1
2
3
4
5
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
41
42
43
44
45
46
47
48
49
|
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import notation proofmode.
From lmpmc Require Import util.
Record lmpmc_queue_hl :=
LmpmcQueueHl
{ new : val;
enqueue : val;
try_dequeue : val;
link : val;
}.
Record lmpmc_queue_iris {Σ} `{!heapGS Σ} (hl : lmpmc_queue_hl) :=
LmpmcQueueIris
{ queue_repr : loc → loc → list val → iProp Σ;
#[global] queue_repr_timeless ℓ_deq ℓ_enq vs :: Timeless (queue_repr ℓ_deq ℓ_enq vs);
new_spec :
{{{ True }}}
hl.(new) #()
{{{ (ℓ_deq ℓ_enq : loc), RET (#ℓ_deq, #ℓ_enq); queue_repr ℓ_deq ℓ_enq [] }}};
enqueue_spec (ℓ_enq : loc) (data : val) :
⊢ <<{ ∀∀ ℓ_deq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
hl.(enqueue) #ℓ_enq data @ ∅
<<{ queue_repr ℓ_deq ℓ_enq (cvs ++ [data]) | RET #() }>>;
try_dequeue_spec (ℓ_deq : loc) :
⊢ <<{ ∀∀ ℓ_enq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
hl.(try_dequeue) #ℓ_deq @ ∅
<<{ queue_repr ℓ_deq ℓ_enq (tail cvs) | RET (val_opt_hl (head cvs)) }>>;
(** Linking two queues:
* _______________ _______________
* / Q1 \ / Q2 \
* ℓ_deq1 ... ℓ_enq1 <> ℓ_deq2 ... ℓ_enq2
* \ \ link op args / /
* \ \____________/ /
* \ Q1 <> Q2 /
* \______________________________/
*)
link_spec (ℓ_enq1 ℓ_deq2 : loc) :
⊢ <<{ ∀∀ (b : bool) ℓ_deq1 ℓ_enq2 cvs1 cvs2, queue_repr ℓ_deq1 ℓ_enq1 cvs1 ∗
if b then queue_repr ℓ_deq2 ℓ_enq2 cvs2 else ⌜ℓ_deq1 = ℓ_deq2 ∧ ℓ_enq1 = ℓ_enq2⌝ }>>
hl.(link) #ℓ_enq1 #ℓ_deq2 @ ∅
<<{ if b then queue_repr ℓ_deq1 ℓ_enq2 (cvs1 ++ cvs2) else True | RET #() }>>;
}.
#[global] Arguments lmpmc_queue_iris _ {_} _ : assert.
|
