Commit 2966b4da authored by Robbert Krebbers's avatar Robbert Krebbers

Solve atomic also using reification/vm_compute.

I also reverted 7952bca4 since there is no need for atomic to be a
boolean predicate anymore. Moreover, I introduced a hint database
fsaV for solving side-conditions related to FSAs, in particular,
side-conditions related to expressions being atomic.
parent db3512f7
Pipeline #2283 passed with stage
......@@ -274,16 +274,16 @@ Inductive head_step : expr → state → expr → state → option (expr) → Pr
head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
(** Atomic expressions *)
Definition atomic (e: expr) : bool :=
Definition atomic (e: expr) :=
match e with
| Alloc e => bool_decide (is_Some (to_val e))
| Load e => bool_decide (is_Some (to_val e))
| Store e1 e2 => bool_decide (is_Some (to_val e1) is_Some (to_val e2))
| Alloc e => is_Some (to_val e)
| Load e => is_Some (to_val e)
| Store e1 e2 => is_Some (to_val e1) is_Some (to_val e2)
| CAS e0 e1 e2 =>
bool_decide (is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2))
is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2)
(* Make "skip" atomic *)
| App (Rec _ _ (Lit _)) (Lit _) => true
| _ => false
| App (Rec _ _ (Lit _)) (Lit _) => True
| _ => False
end.
(** Basic properties about the language *)
......
......@@ -49,11 +49,12 @@ Lemma inc_spec l j (Φ : val → iProp) :
Proof.
iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
iDestruct "Hl" as (N γ) "(% & #? & #Hγ & Hγf)".
wp_focus (! _)%E; iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
wp_focus (! _)%E.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv.
wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
wp_let; wp_op.
wp_focus (CAS _ _ _); iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
wp_let; wp_op. wp_focus (CAS _ _ _).
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv.
destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
- wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
......@@ -74,7 +75,8 @@ Lemma read_spec l j (Φ : val → iProp) :
WP read #l {{ Φ }}.
Proof.
iIntros "[Hc HΦ]". iDestruct "Hc" as (N γ) "(% & #? & #Hγ & Hγf)".
rewrite /read. wp_let. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
rewrite /read. wp_let.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=".
wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
{ iPureIntro; apply mnat_local_update; abstract lia. }
......
......@@ -64,7 +64,7 @@ Proof.
wp_apply wp_fork. iSplitR "Hf".
- iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
iInv N as (v') "[Hl _]"; first wp_done.
iInv N as (v') "[Hl _]".
wp_store. iPvsIntro. iSplit; [iNext|done].
iExists (SOMEV v). iFrame. eauto.
Qed.
......
......@@ -163,6 +163,23 @@ Proof.
induction e; simpl; repeat case_decide;
f_equal; auto using is_closed_nil_subst, is_closed_of_val, eq_sym.
Qed.
Definition atomic (e : expr) :=
match e with
| Alloc e => bool_decide (is_Some (to_val e))
| Load e => bool_decide (is_Some (to_val e))
| Store e1 e2 => bool_decide (is_Some (to_val e1) is_Some (to_val e2))
| CAS e0 e1 e2 =>
bool_decide (is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2))
(* Make "skip" atomic *)
| App (Rec _ _ (Lit _)) (Lit _) => true
| _ => false
end.
Lemma atomic_correct e : atomic e heap_lang.atomic (to_expr e).
Proof.
destruct e; simpl; repeat (case_match; try done);
naive_solver eauto using to_val_is_Some.
Qed.
End W.
Ltac solve_closed :=
......@@ -187,6 +204,19 @@ Ltac solve_to_val :=
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end.
Ltac solve_atomic :=
try match goal with
| |- context E [language.atomic ?e] =>
let X := context E [atomic e] in change X
end;
match goal with
| |- atomic ?e =>
let e' := W.of_expr e in change (atomic (W.to_expr e'));
apply W.atomic_correct; vm_compute; exact I
end.
Hint Extern 0 (atomic _) => solve_atomic : fsaV.
Hint Extern 0 (language.atomic _) => solve_atomic : fsaV.
(** Substitution *)
Ltac simpl_subst :=
csimpl;
......
......@@ -16,8 +16,6 @@ Ltac wp_done :=
| |- is_Some (to_val _) => solve_to_val
| |- to_val _ = Some _ => solve_to_val
| |- language.to_val _ = Some _ => solve_to_val
| |- Is_true (atomic _) => rewrite /= ?to_of_val; fast_done
| |- Is_true (language.atomic _) => rewrite /= ?to_of_val; fast_done
| _ => fast_done
end.
......
......@@ -11,7 +11,7 @@ Class EctxLanguage (expr val ectx state : Type) := {
empty_ectx : ectx;
comp_ectx : ectx ectx ectx;
fill : ectx expr expr;
atomic : expr bool;
atomic : expr Prop;
head_step : expr state expr state option expr Prop;
to_of_val v : to_val (of_val v) = Some v;
......
......@@ -9,7 +9,7 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
of_val : val expr;
to_val : expr option val;
fill_item : ectx_item expr expr;
atomic : expr bool;
atomic : expr Prop;
head_step : expr state expr state option expr Prop;
to_of_val v : to_val (of_val v) = Some v;
......
......@@ -6,7 +6,7 @@ Structure language := Language {
state : Type;
of_val : val expr;
to_val : expr option val;
atomic : expr bool;
atomic : expr Prop;
prim_step : expr state expr state option expr Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v of_val v = e;
......
......@@ -243,6 +243,9 @@ Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
fsa_frame_r E P Φ : (fsa E Φ P) fsa E (λ a, Φ a P)
}.
(* Used to solve side-conditions related to [fsaV] *)
Create HintDb fsaV.
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
Implicit Types Φ Ψ : A iProp Λ Σ.
......
......@@ -38,7 +38,7 @@ Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
eapply tac_inv_fsa with _ _ _ _ N H _ _;
[let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P
|try fast_done (* atomic *)
|trivial with fsaV
|solve_ndisj
|iAssumption || fail "iInv: invariant" N "not found"
|env_cbv; reflexivity
......@@ -64,7 +64,7 @@ Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
[let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P
|try fast_done (* atomic *)
|trivial with fsaV
|solve_ndisj
|iAssumption || fail "iOpenInv: invariant" N "not found"
|let P := match goal with |- TimelessP ?P => P end in
......
......@@ -38,7 +38,7 @@ Tactic Notation "iSts" constr(H) "as"
end;
[let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
apply _ || fail "iSts: cannot viewshift in goal" P
|try fast_done (* atomic *)
|auto with fsaV
|iAssumptionCore || fail "iSts:" H "not found"
|iAssumption || fail "iSts: invariant not found"
|solve_ndisj
......
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