blob: f7e08868b3155b09e4f8cde38ab28d8069f80d32 (
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import notation proofmode.
From lmpmc Require Import util.
(* Doing this split because I don't know how to otherwise get a nice
closed proof. *)
Record fin_queue_hl :=
FinQueueHl
{ new : val;
enqueue : val;
finalize : val;
try_dequeue : val;}.
Record fin_queue_iris {Σ} `{!heapGS Σ} (hl : fin_queue_hl) :=
FinQueueIris
{ (** If [⊢ queue_repr ℓ vs mfin], then there is a queue at [ℓ]
which currently holds the values [vs], and possibly a final
value [mfin]. The dequeue and enqueue operations work in
FIFO fashion, with [head vs] (if any) representing the next
value that would be dequeued by a [try_dequeue ℓ] operation.
Only non-finalized queues can be enqueued in. Non-finalized queues
can be finalized using the [finalize ℓ v] operation, which sets
[mfin] to [v]. Subsequent [try_dequeue ℓ] operations then first
dequeue the remainder of [vs]; when [vs] is empty, they return [mfin]
(but, critically, do not unset it). *)
queue_repr : loc → list val → option val → iProp Σ;
#[global] queue_repr_timeless ℓ vs mfin :: Timeless (queue_repr ℓ vs mfin);
(** If [⊢ queue_fin ℓ v], then the queue at [ℓ] has been
finalized and all elements except for the final element [v]
have been dequeued.
Queues that enter this state never leave this state; this
allows [queue_fin ℓ v] to be a persistent proposition. *)
queue_fin : loc → val → iProp Σ;
#[global] queue_fin_persistent ℓ v :: Persistent (queue_fin ℓ v);
#[global] queue_fin_timeless ℓ v :: Timeless (queue_fin ℓ v);
queue_fin_obtain ℓ fin : queue_repr ℓ [] (Some fin) -∗ queue_fin ℓ fin;
queue_fin_agree ℓ vs fin mfin :
queue_fin ℓ fin -∗
queue_repr ℓ vs mfin -∗
⌜vs = []⌝ ∗ ⌜mfin = Some fin⌝;
new_spec :
{{{ True }}}
hl.(new) #()
{{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] None }}};
enqueue_spec (ℓ_q : loc) (data : val) :
⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
hl.(enqueue) #ℓ_q data @ ∅
<<{ queue_repr ℓ_q (vs ++ [data]) None | RET #() }>>;
finalize_spec (ℓ_q : loc) (data : val) :
⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
hl.(finalize) #ℓ_q data @ ∅
<<{ queue_repr ℓ_q vs (Some data) | RET #() }>>;
try_dequeue_spec (ℓ_q : loc) :
⊢ <<{ ∀∀ vs mfin, queue_repr ℓ_q vs mfin }>>
hl.(try_dequeue) #ℓ_q @ ∅
<<{ queue_repr ℓ_q (tail vs) mfin
| RET (if head vs is Some v then InjLV v else InjRV (val_opt_hl mfin)) }>>;
}.
#[global] Arguments fin_queue_iris _ {_} _ : assert.
|
