Commit ef98c180 authored by Dan Frumin's avatar Dan Frumin

Merge branch 'atomic_rules' into 'master'

Strengthen some rules.

See merge request lgg/iris-c-monad!2
parents 527f0f23 39e98fa6
......@@ -225,9 +225,10 @@ Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val :=
Definition c_pre_bin_op (op : cbin_op) : val := λ: "x" "y",
(* all binds should be non-sequenced *)
"lv" ←ᶜ ("x" ||| "y");;
"ov" ←ᶜ ∗ᶜ (c_ret (Fst "lv"));;
c_ret (Fst "lv") = c_bin_op op (c_ret "ov") (c_ret (Snd "lv"));;
c_ret "ov".
c_atomic (λ: <>,
"ov" ←ᶜ ∗ᶜ (c_ret (Fst "lv"));;
c_ret (Fst "lv") = c_bin_op op (c_ret "ov") (c_ret (Snd "lv"));;
c_ret "ov").
Notation "e1 +=ᶜ e2" := (c_pre_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 +∗=ᶜ e2" := (c_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope.
......@@ -267,15 +268,16 @@ Section proofs.
Qed.
Lemma cwp_free R Φ e :
CWP e @ R {{ v, cl ws, v = cloc_to_val cl
block_info cl true (length ws) cl C ws Φ #() }} -
CWP e @ R {{ v, R ={}= cl ws, v = cloc_to_val cl
block_info cl true (length ws) cl C ws R Φ #() }} -
CWP free(e) @ R {{ Φ }}.
Proof.
iIntros "H".
cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures.
iApply cwp_bind. iApply (cwp_wand with "H"). clear v.
iIntros (v). iDestruct 1 as (cl ws ->) "(Hinfo & Hcl & HΦ)". cwp_pures.
iIntros (v) "H". cwp_pures.
iApply cwp_atomic_env. iIntros (env) "Henv HR". wp_pures.
iMod ("H" with "HR") as (cl ws ->) "(Hinfo & Hcl & $ & HΦ)". cwp_pures.
rewrite cloc_to_val_eq. wp_pures.
iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
iAssert i : nat, is_Some (ws !! i) (cl + i) locked_locs σ⌝%I as %Hlocked.
......@@ -302,7 +304,7 @@ Section proofs.
wp_op. iSplit; first done. iNext; wp_pures.
iApply ("IH" with "[%] Hlocks HΨ"). lia. }
wp_apply ("Hcheck" with "[//]"); iIntros "Hlock". wp_pures. wp_store.
iIntros "!> {$HΦ $HR}". iExists X, _.
iIntros "!> {$HΦ}". iExists X, _.
iFrame "Hlock". iSplit; last by iApply "Hclose".
iPureIntro; intros w Hw. destruct (HX _ Hw) as (cl'&Hcl&Hin).
exists cl'; split; first done. apply locked_locs_free_heap; first done.
......@@ -315,8 +317,8 @@ Section proofs.
Lemma cwp_store R Φ Ψ1 Ψ2 e1 e2 :
CWP e1 @ R {{ Ψ1 }} -
CWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - cl w,
v1 = cloc_to_val cl cl C w (cl C[LLvl] v2 - Φ v2)) -
( v1 v2, Ψ1 v1 - Ψ2 v2 - R ={}= cl w,
v1 = cloc_to_val cl cl C w (cl C[LLvl] v2 ={}= R Φ v2)) -
CWP e1 = e2 @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
......@@ -325,9 +327,9 @@ Section proofs.
cwp_lam. cwp_pures.
iApply cwp_bind. iApply (cwp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>". cwp_pures.
iDestruct ("HΦ" with "H1 H2") as (cl w ->) "[Hl HΦ]".
iApply cwp_atomic_env.
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
iMod ("HΦ" with "H1 H2 HR") as (cl w ->) "[Hl HΦ]".
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1.
iDestruct (mapsto_offset_non_neg with "Hl") as %?.
assert ((#(cloc_base cl), #(cloc_offset cl))%V X) as HclX.
......@@ -341,22 +343,24 @@ Section proofs.
wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
iApply wp_fupd. wp_store.
iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
iMod ("HΦ" with "Hl") as "HΦ".
iIntros "!> !>". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
iExists ({[(#(cloc_base cl), #(cloc_offset cl))%V]} X), _.
iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver.
Qed.
Lemma cwp_load_exists_frac R Φ e :
CWP e @ R {{ v, cl q w, v = cloc_to_val cl
cl C{q} w (cl C{q} w - Φ w) }} -
CWP e @ R {{ v, R ={}= cl q w, v = cloc_to_val cl
cl C{q} w (cl C{q} w ={}= R Φ w) }} -
CWP ∗ᶜe @ R {{ Φ }}.
Proof.
iIntros "H".
cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures.
iApply cwp_bind. iApply (cwp_wand with "H"). clear v.
iIntros (v). iDestruct 1 as (cl q w ->) "[Hl HΦ]". cwp_pures.
iDestruct (mapsto_offset_non_neg with "Hl") as %?.
iIntros (v) "H". cwp_pures.
iApply cwp_atomic_env. iIntros (env) "Henv HR".
iMod ("H" with "HR") as (cl q w ->) "[Hl HΦ]".
iDestruct (mapsto_offset_non_neg with "Hl") as %?.
iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv.
assert ((#(cloc_base cl), #(cloc_offset cl))%V X) as HclX.
......@@ -368,20 +372,22 @@ Section proofs.
wp_op. iSplit; first done. iNext; wp_seq.
wp_load; wp_match.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
iApply wp_fupd.
wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
iExists X, _. by iFrame.
iMod ("HΦ" with "Hl") as "[$ $]".
iIntros "!> !>". iExists X, _. by iFrame.
Qed.
Lemma cwp_load R Φ q e :
CWP e @ R {{ v, cl w, v = cloc_to_val cl
cl C{q} w (cl C{q} w - Φ w) }} -
CWP e @ R {{ v, R ={}= cl w, v = cloc_to_val cl
cl C{q} w (cl C{q} w ={}= R Φ w) }} -
CWP ∗ᶜe @ R {{ Φ }}.
Proof.
iIntros "H". iApply cwp_load_exists_frac.
cwp_apply (cwp_wand with "H").
iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
iIntros (v). iIntros "H HR".
iMod ("H" with "HR") as (cl w ->) "[H1 H2]". eauto 100 with iFrame.
Qed.
(** Helper lemma *)
......@@ -642,11 +648,11 @@ Section proofs.
Lemma cwp_pre_bin_op R Φ Ψ1 Ψ2 e1 e2 op :
CWP e1 @ R {{ Ψ1 }} - CWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 -
( v1 v2, Ψ1 v1 - Ψ2 v2 - R ={}=
cl v w, v1 = cloc_to_val cl
cl C v
cbin_op_eval op v v2 = Some w
(cl C[LLvl] w - Φ v)) -
(cl C[LLvl] w ={}= R Φ v)) -
CWP c_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 He2 HΦ".
......@@ -654,10 +660,12 @@ Section proofs.
cwp_apply (cwp_wp with "He1"); iIntros (a1) "Ha1". cwp_lam; cwp_pures.
iApply cwp_bind. iApply (cwp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". cwp_pures.
iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
iApply cwp_atomic. iIntros "HR !>".
iExists True%I. iSplitR; first done. cwp_lam. cwp_pures.
iMod ("HΦ" with "Hv1 Hv2 HR") as (cl v w ->) "(Hl & % & HΦ)".
iApply cwp_bind. iApply cwp_load. iApply cwp_ret. iApply wp_value.
iExists cl, v; iFrame. iSplit; first done.
iIntros "Hl". cwp_pures. iApply cwp_bind.
iIntros "HR !>". iExists cl, v; iFrame. iSplit; first done.
iIntros "Hl !>". cwp_pures. iApply cwp_bind.
iApply (cwp_store _ _
(λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
- cwp_proj. iApply cwp_ret; by wp_value_head.
......@@ -665,8 +673,9 @@ Section proofs.
try (try cwp_proj; iApply cwp_ret; by wp_value_head).
iIntros (? ? -> ->); eauto.
- iIntros (? ? -> ->).
iExists _, _; iFrame. iSplit; first done.
iIntros "?". cwp_seq. iApply cwp_ret; iApply wp_value. by iApply "HΦ".
iIntros "HR !>". iExists _, _; iFrame. iSplit; first done.
iIntros "Hcl !>". cwp_seq. iMod ("HΦ" with "Hcl") as "[$ HΦ]".
iApply cwp_ret; iApply wp_value. eauto.
Qed.
End proofs.
......
......@@ -226,8 +226,8 @@ Section forward_spec.
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iApply cwp_load. iApply (cwp_wand with "H1"); iIntros (v1) "[-> Hm]".
iDestruct ("H2" with "Hm") as "[Hm2 Hi]".
iExists _, _. iFrame "Hi". iSplit; first by eauto.
iIntros "Hi"; iSplit; first done.
iIntros "$ !>". iExists _, _. iFrame "Hi". iSplit; first by eauto.
iIntros "Hi !>"; iSplit; first done.
iApply denv_insert_interp; eauto with iFrame.
- (* assign *)
destruct (forward_aux _ _ _ _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
......@@ -244,8 +244,8 @@ Section forward_spec.
iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
{ iApply denv_merge_interp; eauto with iFrame. }
iExists _, _. iFrame "Hi". iSplit; first by eauto.
iIntros "Hi"; iSplit; first done.
iIntros "$ !>". iExists _, _. iFrame "Hi". iSplit; first by eauto.
iIntros "Hi !>"; iSplit; first done.
iApply denv_insert_interp; eauto 10 with iFrame.
- (* bin op *)
destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
......@@ -272,11 +272,11 @@ Section forward_spec.
{ iApply denv_delete_full_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H"); iIntros "[[H1 H2] H]".
iApply (cwp_pre_bin_op with "H1 H2").
iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
iIntros (v1 v2) "[-> Hm1] [-> Hm2] $ !>".
iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
{ iApply denv_merge_interp; eauto with iFrame. }
iExists _, _, _. iFrame "Hi". repeat (iSplit; first by eauto).
iIntros "Hi"; iSplit; first done.
iIntros "Hi !>"; iSplit; first done.
iApply denv_insert_interp; eauto 10 with iFrame.
- (* un op *)
destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
......
......@@ -514,7 +514,7 @@ Section vcg_spec.
{ iApply ("IH" with "[] [] Hm H"); eauto. }
iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]".
iDestruct (vcg_load_correct with "Hm H") as (cl q w ?) "[Hi H]"; eauto.
iExists _, _, _; iSplit; first done. iIntros "{$Hi} Hi".
iIntros "$ !>". iExists _, _, _; iSplit; first done. iIntros "{$Hi} Hi".
by iApply vcg_continuation_mono; last by iApply "H".
- (* assign *)
destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
......@@ -528,7 +528,7 @@ Section vcg_spec.
eauto using denv_wf_mono, dval_wf_mono.
{ iApply denv_merge_interp; eauto using denv_wf_mono.
iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
iExists _, _; iSplit; first done. iIntros "{$Hi} Hi".
iIntros "$ !>". iExists _, _; iSplit; first done. iIntros "{$Hi} Hi !>".
rewrite (dval_interp_mono E E'); eauto.
by iApply vcg_continuation_mono; last by iApply "H".
+ iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
......@@ -540,7 +540,7 @@ Section vcg_spec.
{ iApply denv_merge_interp; eauto using denv_wf_mono.
iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
rewrite (dval_interp_mono E E'); eauto.
iExists _, _; iSplit; first done. iIntros "{$Hi} Hi".
iIntros "$ !>". iExists _, _; iSplit; first done. iIntros "{$Hi} Hi !>".
by iApply vcg_continuation_mono; last by iApply "H".
- (* bin op *)
destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
......@@ -579,8 +579,9 @@ Section vcg_spec.
{ iApply denv_merge_interp; eauto using denv_wf_mono.
iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
rewrite (dval_interp_mono E E'); eauto.
iIntros "$ !>".
iExists _, _, _. iFrame "Hi". repeat (iSplit; first done).
iIntros "Hi". by iApply vcg_continuation_mono; last by iApply "H".
iIntros "Hi !>". by iApply vcg_continuation_mono; last by iApply "H".
+ iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
iApply (cwp_pre_bin_op with "H1 [H Hm']").
{ iApply ("IH" with "[] [] Hm' H"); eauto. }
......@@ -590,8 +591,9 @@ Section vcg_spec.
{ iApply denv_merge_interp; eauto using denv_wf_mono.
iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
rewrite (dval_interp_mono E E'); eauto.
iIntros "$ !>".
iExists _, _, _. iFrame "Hi". repeat (iSplit; first done).
iIntros "Hi". by iApply vcg_continuation_mono; last by iApply "H".
iIntros "Hi !>". by iApply vcg_continuation_mono; last by iApply "H".
- (* un op *)
iApply cwp_un_op. iApply (cwp_wand with "[-]").
{ iApply ("IH" with "[] [] Hm H"); eauto. }
......
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