Commit 90734cf0 authored by Ralf Jung's avatar Ralf Jung

newchan -> newbarrier

parent 17736977
Pipeline #188 passed with stage
From heap_lang Require Export substitution notation. From heap_lang Require Export substitution notation.
Definition newchan : val := λ: "", ref '0. Definition newbarrier : val := λ: "", ref '0.
Definition signal : val := λ: "x", "x" <- '1. Definition signal : val := λ: "x", "x" <- '1.
Definition wait : val := Definition wait : val :=
rec: "wait" "x" := if: !"x" = '1 then '() else "wait" "x". rec: "wait" "x" := if: !"x" = '1 then '() else "wait" "x".
Instance newchan_closed : Closed newchan. Proof. solve_closed. Qed. Instance newbarrier_closed : Closed newbarrier. Proof. solve_closed. Qed.
Instance signal_closed : Closed signal. Proof. solve_closed. Qed. Instance signal_closed : Closed signal. Proof. solve_closed. Qed.
Instance wait_closed : Closed wait. Proof. solve_closed. Qed. Instance wait_closed : Closed wait. Proof. solve_closed. Qed.
\ No newline at end of file
...@@ -2,7 +2,7 @@ From barrier Require Import proof. ...@@ -2,7 +2,7 @@ From barrier Require Import proof.
From program_logic Require Import auth sts saved_prop hoare ownership. From program_logic Require Import auth sts saved_prop hoare ownership.
Import uPred. Import uPred.
Definition client := (let: "b" := newchan '() in wait "b")%L. Definition client := (let: "b" := newbarrier '() in wait "b")%L.
Section client. Section client.
Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace). Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace).
...@@ -12,7 +12,7 @@ Section client. ...@@ -12,7 +12,7 @@ Section client.
heapN N heap_ctx heapN || client {{ λ _, True }}. heapN N heap_ctx heapN || client {{ λ _, True }}.
Proof. Proof.
intros ?. rewrite /client. intros ?. rewrite /client.
ewp eapply (newchan_spec heapN N True%I); last done. ewp eapply (newbarrier_spec heapN N True%I); last done.
apply sep_intro_True_r; first done. apply sep_intro_True_r; first done.
apply forall_intro=>l. apply wand_intro_l. rewrite right_id. apply forall_intro=>l. apply wand_intro_l. rewrite right_id.
wp_let. etrans; last eapply wait_spec. wp_let. etrans; last eapply wait_spec.
......
...@@ -118,12 +118,12 @@ Proof. ...@@ -118,12 +118,12 @@ Proof.
Qed. Qed.
(** Actual proofs *) (** Actual proofs *)
Lemma newchan_spec (P : iProp) (Φ : val iProp) : Lemma newbarrier_spec (P : iProp) (Φ : val iProp) :
heapN N heapN N
(heap_ctx heapN l, recv l P send l P - Φ (LocV l)) (heap_ctx heapN l, recv l P send l P - Φ (LocV l))
|| newchan '() {{ Φ }}. || newbarrier '() {{ Φ }}.
Proof. Proof.
intros HN. rewrite /newchan. wp_seq. intros HN. rewrite /newbarrier. wp_seq.
rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj. rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l. apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
rewrite !assoc. apply pvs_wand_r. rewrite !assoc. apply pvs_wand_r.
......
...@@ -12,7 +12,7 @@ Local Notation iProp := (iPropG heap_lang Σ). ...@@ -12,7 +12,7 @@ Local Notation iProp := (iPropG heap_lang Σ).
Lemma barrier_spec (heapN N : namespace) : Lemma barrier_spec (heapN N : namespace) :
heapN N heapN N
recv send : loc iProp -n> iProp, recv send : loc iProp -n> iProp,
( P, heap_ctx heapN {{ True }} newchan '() {{ λ v, l, v = LocV l recv l P send l P }}) ( P, heap_ctx heapN {{ True }} newbarrier '() {{ λ v, l, v = LocV l recv l P send l P }})
( l P, {{ send l P P }} signal (LocV l) {{ λ _, True }}) ( l P, {{ send l P P }} signal (LocV l) {{ λ _, True }})
( l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ( l P, {{ recv l P }} wait (LocV l) {{ λ _, P }})
( l P Q, {{ recv l (P Q) }} Skip {{ λ _, recv l P recv l Q }}) ( l P Q, {{ recv l (P Q) }} Skip {{ λ _, recv l P recv l Q }})
...@@ -22,7 +22,7 @@ Proof. ...@@ -22,7 +22,7 @@ Proof.
exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)). exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
split_and?; simpl. split_and?; simpl.
- intros P. apply: always_intro. apply impl_intro_r. - intros P. apply: always_intro. apply impl_intro_r.
rewrite -(newchan_spec heapN N P) // always_and_sep_r. rewrite -(newbarrier_spec heapN N P) // always_and_sep_r.
apply sep_mono_r, forall_intro=>l; apply wand_intro_l. apply sep_mono_r, forall_intro=>l; apply wand_intro_l.
by rewrite right_id -(exist_intro l) const_equiv // left_id. by rewrite right_id -(exist_intro l) const_equiv // left_id.
- intros l P. apply ht_alt. by rewrite -signal_spec right_id. - intros l P. apply ht_alt. by rewrite -signal_spec right_id.
......
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