Commit a0de8ddf authored by Dan Frumin's avatar Dan Frumin

A more reasonable CAS rule

parent dc623f25
...@@ -450,20 +450,22 @@ Section properties. ...@@ -450,20 +450,22 @@ Section properties.
to_val e1 = Some v1 to_val e1 = Some v1
to_val e2 = Some v2 to_val e2 = Some v2
(|={E1,E2}=> v', l ↦ᵢ v' (|={E1,E2}=> v', l ↦ᵢ v'
(v' v1 - (l ↦ᵢ v' - {E2,E1;Δ;Γ} fill K #false log t : τ)) (v' v1 - (l ↦ᵢ v' - {E2,E1;Δ;Γ} fill K #false log t : τ))
(v' = v1 - (l ↦ᵢ v2 - {E2,E1;Δ;Γ} fill K #true log t : τ))) (v' = v1 - (l ↦ᵢ v2 - {E2,E1;Δ;Γ} fill K #true log t : τ)))
- {E1,E1;Δ;Γ} fill K (CAS #l e1 e2) log t : τ. - {E1,E1;Δ;Γ} fill K (CAS #l e1 e2) log t : τ.
Proof. Proof.
iIntros (??) "Hlog". iIntros (??) "Hlog".
iApply bin_log_related_wp_atomic_l; auto. iApply bin_log_related_wp_atomic_l; auto.
iMod "Hlog" as (v') "[Hl [Hlog_fail Hlog_suc]]". iModIntro. iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
destruct (decide (v' = v1)). destruct (decide (v' = v1)).
- (* CAS successful *) subst. - (* CAS successful *) subst.
iApply (wp_cas_suc with "Hl"); eauto. iApply (wp_cas_suc with "Hl"); eauto.
iSpecialize ("Hlog_suc" with "[]"); eauto. iDestruct "Hlog" as "[_ Hlog]".
iSpecialize ("Hlog" with "[]"); eauto.
- (* CAS failed *) - (* CAS failed *)
iApply (wp_cas_fail with "Hl"); eauto. iApply (wp_cas_fail with "Hl"); eauto.
iSpecialize ("Hlog_fail" with "[]"); eauto. iDestruct "Hlog" as "[Hlog _]".
iSpecialize ("Hlog" with "[]"); eauto.
Qed. Qed.
Lemma bin_log_related_cas_fail_l Δ Γ E1 E2 K l e1 e2 v1 v2 t τ : Lemma bin_log_related_cas_fail_l Δ Γ E1 E2 K l e1 e2 v1 v2 t τ :
......
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