Commit f7f0423d authored by Dan Frumin's avatar Dan Frumin

fork rules for the relational interpretation

parent 2a4b76f7
......@@ -406,6 +406,7 @@ Definition is_atomic (e : expr) : Prop :=
| Load e => is_Some (to_val e)
| Store e1 e2 => is_Some (to_val e1) is_Some (to_val e2)
| CAS e0 e1 e2 => is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2)
| Fork _ => True
| _ => False
end.
......
......@@ -378,14 +378,15 @@ Section properties.
end;
try done.
Lemma bin_log_related_fork_l Γ E K (e t : expr) (τ : type)
Lemma bin_log_related_fork_l Γ E1 E2 K (e t : expr) (τ : type)
(Hclosed : Closed e) :
(WP e {{ _, True }}) -
{E,E;Γ} fill K (Lit Unit) log t : τ -
{E,E;Γ} fill K (Fork e) log t : τ.
(|={E1,E2}=> (WP e {{ _, True }})
{E2,E1;Γ} fill K (Lit Unit) log t : τ) -
{E1,E1;Γ} fill K (Fork e) log t : τ.
Proof.
iIntros "Hsafe Hlog".
iApply bin_log_related_wp_l.
iIntros "Hlog".
iApply bin_log_related_wp_atomic_l; auto.
iMod "Hlog" as "[Hsafe Hlog]". iModIntro.
iApply wp_fork. iNext. by iFrame "Hsafe".
Qed.
......@@ -702,6 +703,24 @@ Section properties.
done.
Qed.
Lemma bin_log_related_fork_r Γ E1 E2 K (e t : expr) (τ : type)
(Hmasked : nclose specN E1)
(Hclosed : Closed e) :
( i, i e -
{E1,E2;Γ} t log fill K (Lit Unit) : τ) -
{E1,E2;Γ} t log fill K (Fork e) : τ.
Proof.
iIntros "Hlog".
pose (Φ := (fun (v : val) => i, i e v = #()%V)%I).
iApply (bin_log_related_step_r Φ with "[]"); cbv[Φ].
{ iIntros (ρ j K') "#Hspec Hj".
tp_fork j as i "Hi".
iModIntro. iExists #()%V. iFrame. eauto.
}
iIntros (v). iDestruct 1 as (i) "[Hi %]"; subst.
by iApply "Hlog".
Qed.
Lemma bin_log_related_alloc_r Γ K E1 E2 e v t τ
(Hmasked : nclose specN E1)
(Heval : to_val e = Some v) :
......
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