-
Notifications
You must be signed in to change notification settings - Fork 1
/
spec_abs.v
132 lines (116 loc) · 3.89 KB
/
spec_abs.v
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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
From stdpp Require Import namespaces.
From gpfsl.logic Require Import logatom.
From gpfsl.examples.queue Require Export event spec_abs_graph.
Require Import iris.prelude.options.
Local Open Scope Z_scope.
Implicit Type (Q : queue) (N : namespace).
(** * Abstract State Specs, similar to Cosmo style. *)
(** Queue predicates *)
Definition isQueueT Σ : Type := namespace → gname → loc → vProp Σ.
Definition QueueT Σ : Type := gname → loc → queue → vProp Σ.
(** Operation specs *)
Definition new_queue_spec' {Σ} `{!noprolG Σ}
(new_queue : val) (isQueue : isQueueT Σ) (Queue : QueueT Σ) : Prop :=
∀ N tid,
{{{ True }}}
new_queue [] @ tid; ⊤
{{{ γq (q: loc), RET #q; isQueue N γq q ∗ Queue γq q [] }}}.
Definition enqueue_spec' {Σ} `{!noprolG Σ}
(enqueue : val) (isQueue : isQueueT Σ) (Queue : QueueT Σ) : Prop :=
∀ N (DISJ: N ## histN) (q : loc) tid γq (V : view) (v : Z) (Posx: 0 < v),
(* PRIVATE PRE *)
⊒V -∗ isQueue N γq q -∗
(* PUBLIC PRE *)
<<< ∀ Q, ▷ Queue γq q Q >>>
enqueue [ #q ; #v] @ tid; ↑N
<<< ∃ V' Q',
(* PUBLIC POST *)
▷ Queue γq q Q' ∗
⊒V' ∗
⌜ V ⊑ V' ∧ Q' = Q ++ [(v, V')] ⌝,
(* RETURN VALUE AT COMMITTING POINT *)
RET #☠, emp >>>
.
Definition dequeue_spec' {Σ} `{!noprolG Σ}
(dequeue : val) (isQueue : isQueueT Σ) (Queue : QueueT Σ) : Prop :=
∀ N (DISJ: N ## histN) (q : loc) tid γq V,
(* PRIVATE PRE *)
⊒V -∗ isQueue N γq q -∗
(* PUBLIC PRE *)
<<< ∀ Q, ▷ Queue γq q Q >>>
dequeue [ #q] @ tid; ↑N
<<< ∃ (v: Z) V' Q',
(* PUBLIC POST *)
▷ Queue γq q Q' ∗
⊒V' ∗
⌜ ( (* EMPTY case *)
( Q' = Q ∧ v = 0 )
∨ (* successful case *)
( Q = (v, V') :: Q' ∧ 0 < v ) ) ⌝,
(* RETURN VALUE AT COMMITTING POINT *)
RET #v, emp >>>
.
Definition try_enq_spec' {Σ} `{!noprolG Σ}
(try_enq : val) (isQueue : isQueueT Σ) (Queue : QueueT Σ) : Prop :=
∀ N (DISJ: N ## histN) (q : loc) tid γq (V : view) (v : Z) (Posx: 0 < v),
(* PRIVATE PRE *)
⊒V -∗ isQueue N γq q -∗
(* PUBLIC PRE *)
<<< ∀ Q, ▷ Queue γq q Q >>>
try_enq [ #q ; #v] @ tid; ↑N
<<< ∃ (b: bool) V' Q',
(* PUBLIC POST *)
▷ (Queue γq q Q') ∗
⊒V' ∗
⌜ V ⊑ V' ∧
if b is false then
Q' = Q
else
Q' = Q ++ [(v, V')] ⌝,
(* RETURN VALUE AT COMMITTING POINT *)
RET #b, emp >>>
.
Definition try_deq_spec' {Σ} `{!noprolG Σ}
(try_deq : val) (isQueue : isQueueT Σ) (Queue : QueueT Σ) : Prop :=
∀ N (DISJ: N ## histN) (q : loc) tid γq V,
(* PRIVATE PRE *)
⊒V -∗ isQueue N γq q -∗
<<< (* PUBLIC PRE *)
∀ Q, ▷ (Queue γq q Q) >>>
try_deq [ #q] @ tid; ↑N
<<< ∃ (v: Z) V' Q',
(* PUBLIC POST *)
▷ (Queue γq q Q') ∗
⊒V' ∗
⌜ (* FAIL case *)
( ( Q' = Q ∧ v < 0 )
∨ (* EMPTY case *)
( Q' = Q ∧ v = 0 )
∨ (* successful case *)
( Q = (v, V') :: Q' ∧ 0 < v ) ) ⌝,
(* RETURN VALUE AT COMMITTING POINT *)
RET #v, emp >>>
.
Record queue_spec {Σ} `{!noprolG Σ} := QueueSpec {
(* operations *)
new_queue : val;
enqueue : val;
dequeue : val;
try_enq : val;
try_deq : val;
(* predicates *)
isQueue : isQueueT Σ;
Queue : QueueT Σ;
(** predicates properties *)
Queue_Timeless : ∀ γq q Q, Timeless (Queue γq q Q);
Queue_Objective : ∀ γq q Q, Objective (Queue γq q Q);
isQueue_Persistent :
∀ N γq q, Persistent (isQueue N γq q);
(* operations specs *)
new_queue_spec : new_queue_spec' new_queue isQueue Queue;
enqueue_spec : enqueue_spec' enqueue isQueue Queue;
dequeue_spec : dequeue_spec' dequeue isQueue Queue;
try_enq_spec : try_enq_spec' try_enq isQueue Queue;
try_deq_spec : try_deq_spec' try_deq isQueue Queue;
}.
Arguments queue_spec _ {_}.