Commit 41bd7cb2 authored by Robbert Krebbers's avatar Robbert Krebbers

More barrier clean up.

parent 3f8273a4
This diff is collapsed.
......@@ -5,22 +5,19 @@ Import uPred.
Definition client := (let: "b" := newchan '() in wait "b")%L.
Section client.
Context {Σ : iFunctorG} `{!heapG Σ} `{!barrierG Σ}.
Context (N : namespace) (heapN : namespace).
Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Lemma client_safe :
heapN N heap_ctx heapN || client {{ λ _, True }}.
Proof.
intros ?. rewrite /client.
ewp eapply (newchan_spec N heapN True%I); last done.
ewp eapply (newchan_spec heapN N True%I); last done.
apply sep_intro_True_r; first done.
apply forall_intro=>l. apply wand_intro_l. rewrite right_id.
wp_let. etrans; last eapply wait_spec.
apply sep_mono_r. apply wand_intro_r. eauto.
apply sep_mono_r, wand_intro_r. eauto.
Qed.
End client.
Section ClosedProofs.
......@@ -33,7 +30,7 @@ Section ClosedProofs.
{ (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
by move=>? _. }
apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
rewrite -(client_safe (nroot .@ "Heap" ) (nroot .@ "Barrier" )) //.
rewrite -(client_safe (nroot .@ "Barrier") (nroot .@ "Heap")) //.
(* This, too, should be automated. *)
by apply ndot_ne_disjoint.
Qed.
......
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