Commit 98005202 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

incomplete

parent 2c5a6373
......@@ -78,7 +78,7 @@ Section MSQueue.
else #0.
Section proof.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (frac_authR natR)}.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR locO)))}.
Context (P : Z iProp Σ).
......@@ -89,12 +89,15 @@ Section MSQueue.
end)%I.
Definition queue_inv_s (q: loc): iProp Σ :=
( s t: loc, q (#s, #t) L: list (prod loc Z), queue_inv s t L)%I.
( s t: loc, q {1/2} (#s, #t) L: list (prod loc Z), queue_inv s t L)%I.
Definition queueN : namespace := nroot .@ "queue".
Definition Queue (l : loc): iProp Σ :=
( q: loc, l = q inv queueN (queue_inv_s q))%I.
Definition Consumer (q: loc) := ( (h t: loc) (γ: gname), q {1/2} (#h, #t) own γ ( (Excl' h)))%I.
Definition Producer (q: loc) := ( (h t: loc) (γ: gname), q {1/2} (#h, #t) own γ ( (Excl' t)))%I.
Lemma newQueue_spec:
{{{ True }}}
(newQueue #())
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment