Commit a570abc2 authored by Ike Mulder's avatar Ike Mulder
Browse files

K42 lock verification now working nicely.

parent b58aa6b1
Pipeline #64043 failed with stage
in 7 minutes and 31 seconds
......@@ -3,7 +3,7 @@ From diaframe.heap_lang Require Import stepping_tacs.
From iris.algebra Require Import agree frac excl auth.
From diaframe.lib Require Import loc_map own_hints.
From diaframe.examples.comparison Require Import k42_lock.
From diaframe.examples.wip Require Import k42_lock.
Set Default Proof Using "Type".
Definition wait_for_succ' : val :=
......@@ -71,53 +71,20 @@ Section spec.
Existing Instance wait_on_spec.
Existing Instance wait_on_spec'.
Global Instance acquire_with_spec R (lk : val) (n : loc) γh γm γe :
Global Program Instance acquire_with_spec R (lk : val) (n : loc) γh γm γe :
SPEC {{ is_lock γh γm γe R lk free_node γm n }}
acquire_with' lk #n
{{ RET #(); R free_node γm n locked γh γe R }}.
Proof.
iStepsS.
- iSmash. (* lock was not held *)
- iRight. (* lock is held and has waiters *)
iStepS. iRight.
iStepsS. iLeft.
iStepsS.
* iRight. (* succesful detachment *)
iStepS. iRevert "H20 H18". (* reintroduce to detect more equalities *)
iSmash.
* iLeft.
iStepsS. iRight.
iSmash.
- iLeft. (* lock is held, no waiters *)
iStepS. iRight.
iStepS. iRight.
iStepsS. iLeft.
iStepsS.
* iRight.
iStepS. iRevert "H19 H17".
iSmash.
* iLeft.
iStepsS. iRight.
iSmash.
Qed.
Global Program Instance acquire_spec R (lk : val) (n : loc) γh γm γe :
SPEC {{ is_lock γh γm γe R lk }}
acquire' lk
{{ RET #(); R locked γh γe R }}.
Global Instance release_spec R γh γm γe (lk : val) :
Global Program Instance release_spec R γh γm γe (lk : val) :
SPEC {{ is_lock γh γm γe R lk R locked γh γe R }}
release' lk
{{ RET #(); emp }}.
Proof.
iStepsS.
- iRevert "H13"; iStepS.
- iSmash.
- iSmash.
- iRevert "H15"; iStepS.
- iSmash.
Qed.
End spec.
......
......@@ -106,156 +106,9 @@ Definition k42_lockΣ : gFunctors := #[
loc_mapΣ (option gname)
].
From diaframe Require Import env_utils introduce_hyp namer_tacs.
From iris.proofmode Require Import environments.
Section mergable_env.
Context {PROP : bi}.
Class MergableEnv (Δ : envs PROP) (P : PROP) (M : PROP) :=
mergable_env : (of_envs Δ) P M.
Global Instance mergable_env_base Δ P :
BiAffine PROP
MergableEnv Δ P True | 999.
Proof. rewrite /MergableEnv; eauto. Qed.
Lemma mergable_env_cons Δ P C mi p P2 P3 M PR :
BiAffine PROP
TCNoBackTrack (TCAnd
(MergablePersist P C)
(FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2))
MergableEnv (envs_option_delete true mi p Δ) P M
MakeAnd M P3 PR
MergableEnv Δ P PR.
(* TODO: can this be done for nonaffine? *)
Proof.
rewrite /MergablePersist /MergableEnv /MakeAnd => HA [[HCP HΔ]].
apply (ficext_satisfies) in HΔ as HC.
apply (findinextcontext_spec true) in HΔ.
rewrite HΔ => {HΔ}.
rewrite -assoc => HΔ <-.
iIntros "(HP2 & HΔ & HP)".
rewrite bi.intuitionistically_and.
iSplit.
iApply HΔ. iFrame.
iApply HCP => //. iFrame.
Qed.
Lemma tac_introduce_hyp_merge_env j Δ P1 a P1' Δ' R P3 :
MergableEnv Δ P1 P3
TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
(TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1))
(envs_add_fresh a j P1' Δ = Some Δ')
envs_entails Δ' $ IntroduceHyp ( P3)%I R
envs_entails Δ $ IntroduceHyp P1 R.
Proof.
rewrite envs_entails_eq /IntroduceHyp => HΔ HP1p' HΔ' HΔR.
iIntros "HΔ' HP1".
assert (P1 ?a P1') as HP1_ent.
{ revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
unfold bi_intuitionistically.
rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //. }
iAssert ( P3)%I as "#HP3"; last first. (* 'iEnough' *)
{ rewrite (envs_add_fresh_sound Δ) //.
rewrite HP1_ent.
iSpecialize ("HΔ'" with "HP1").
by iApply (HΔR with "HΔ'"). }
iCombine "HΔ' HP1" as "H".
rewrite HΔ.
eauto.
Qed.
Class MergableEnv2 (Δ : envs PROP) (P : PROP) (M : PROP) :=
mergable_env2 : (of_envs Δ) P <pers> M.
Global Instance mergable_env2_base Δ P :
(* BiAffine PROP →*)
MergableEnv2 Δ P True | 999.
Proof. rewrite /MergableEnv2; eauto. Qed.
Lemma mergable_env2_cons Δ P C mi p P2 P3 M PR :
TCNoBackTrack (TCAnd
(MergablePersist P C)
(FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2))
MergableEnv2 (envs_option_delete true mi p Δ) P M
MakeAnd M P3 PR
MergableEnv2 Δ P PR.
(* TODO: can this be done for nonaffine? *)
Proof.
rewrite /MergablePersist /MergableEnv2 /MakeAnd => [[[HCP HΔ]]].
apply (ficext_satisfies) in HΔ as HC.
apply (findinextcontext_spec true) in HΔ.
rewrite HΔ => {HΔ}.
rewrite -assoc => HΔ <-.
iIntros "(HP2 & HΔ & HP)".
iApply bi.persistently_and_2. iSplit.
iClear "HP2".
iApply HΔ. iFrame. iClear "HΔ".
iApply bi.intuitionistically_into_persistently_1.
iApply HCP => //. iFrame.
Qed.
Lemma tac_introduce_hyp_merge_env2 j Δ P1 a P1' Δ' R P3 :
MergableEnv2 Δ P1 P3
TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
(TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1))
(envs_add_fresh a j P1' Δ = Some Δ')
envs_entails Δ' $ IntroduceHyp ( P3)%I R
envs_entails Δ $ IntroduceHyp P1 R.
Proof.
rewrite envs_entails_eq /IntroduceHyp => HΔ HP1p' HΔ' HΔR.
iIntros "HΔ' HP1".
assert (P1 ?a P1') as HP1_ent.
{ revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
unfold bi_intuitionistically.
rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //. }
iAssert (<pers> P3)%I as "#HP3"; last first. (* 'iEnough' *)
{ rewrite (envs_add_fresh_sound Δ) //.
rewrite HP1_ent.
iSpecialize ("HΔ'" with "HP1").
by iApply (HΔR with "HΔ'"). }
iCombine "HΔ' HP1" as "H".
rewrite HΔ.
eauto.
Qed.
End mergable_env.
Global Hint Extern 100 (MergableEnv _ _ _) =>
solve [eapply mergable_env_cons;
[ iSolveTC
| iSolveTC
| cbn [envs_option_delete envs_delete env_delete ident_beq string_beq ascii_beq beq];
iSolveTC
| iSolveTC
]] : typeclass_instances.
Ltac introduceHypStep namer_tac ::=
first
[notypeclasses refine (tac_introduce_hyp_premise_emp _ _ _ )
|notypeclasses refine (tac_introduce_hyp_premise_sep _ _ _ _ _ _ _); [ iSolveTC | ]
|notypeclasses refine (tac_introduce_hyp_premise_exist _ _ _ _ _ _); [ iSolveTC | simpl]
|notypeclasses refine (tac_introduce_hyp_premise_or _ _ _ _ _ _ _ _ ); [ iSolveTC | simpl | simpl]
|notypeclasses refine (tac_introduce_hyp_premise_modal _ _ _ _ _ _ _ _ _ _);
[iSolveTC | iSolveTC | simpl; iSolveTC | ]
(* rules below this do actual introduction of separation logic premises *)
|notypeclasses refine (tac_introduce_hyp_premise_pure _ _ _ _ _ _ _ _);
[ iSolveTC | iSolveTC | simpl; simplifySolveSepPureHyp ]
|notypeclasses refine (tac_introduce_hyp_merge_consume _ _ _ _ _ _ _ _ _ _);
[iSolveTC | register_delete namer_tac; simpl ]
| lazymatch goal with
| |- envs_entails ?Δ (IntroduceHyp ?P _) =>
let j := namer_tac NameTac.GetName Δ P in first
[notypeclasses refine (tac_introduce_hyp_merge_env j _ _ _ _ _ _ _ _ _ _ _ );
[iSolveTC | iSolveTC | reflexivity | ]
|notypeclasses refine (tac_introduce_hyp_not_mergable j _ _ _ _ _ _ _ _ _);
[iSolveTC | reflexivity | ] ]
end].
Local Obligation Tactic := program_smash_verify.
Program Instance subG_k42_lockΣ {Σ} : subG k42_lockΣ Σ k42_lockG Σ.
Global Program Instance subG_k42_lockΣ {Σ} : subG k42_lockΣ Σ k42_lockG Σ.
Section spec.
Context `{!heapGS Σ, k42_lockG Σ}.
......@@ -308,21 +161,17 @@ Section spec.
).
Definition is_lock γh γm γe R v : iProp Σ :=
(lk : loc), v = #lk global_reg γm inv N_node (head_inv γh γe lk R) inv N (lock_inv γh γm γe lk R).
(lk : loc), v = #lk global_reg γm inv N (lock_inv γh γm γe lk R) inv N_node (head_inv γh γe lk R).
Global Program Instance own_frac_or_as_forall l γ R :
IntoForallCareful (own γ (to_agree l, 1%Qp) R)%I (λ (q : Qp), own γ (to_agree l, q) - ( own γ (to_agree l, q) R))%I.
Global Instance own_frac_or_as_forall l γ R :
AtomIntoForall (own γ (to_agree l, 1%Qp) R)%I (λ (q : Qp), own γ (to_agree l, q) - ( own γ (to_agree l, q) R))%I.
Proof. rewrite /AtomIntoForall /IntoForallCareful. do 3 iStepS. iFrame. Qed.
Global Instance new_lock_spec :
Global Program Instance new_lock_spec :
SPEC {{ True }}
new_lock #() (* note that global_reg is not a difficult premise, since one has ⊢ |={E}=> ∃ γm, global_reg γm *)
{{ (lk : val), RET lk; ( R γm, R global_reg γm ={}= γe γh, is_lock γh γm γe R lk) }}.
Proof.
do 20 iStepS.
iMod (own_alloc (Excl ())) as "[%γ Hγ]" => //.
iSmash.
Qed.
(* having global_reg γm on the left side of the fupd means multiple mcs_locks can share the same global_reg γm,
(* having global_reg γm on the left side of the fupd means multiple k42_locks can share the same global_reg γm,
which means free_nodes can be used in any of these locks, as desired. *)
Global Program Instance new_node_spec :
......@@ -339,7 +188,7 @@ Section spec.
rewrite /MergablePersist /SolveSepSideCondition => p Pin Pout [-> [Hv ->]].
rewrite bi.intuitionistically_if_elim.
destruct (decide (l1 = l2)) as [-> | Hneq]; iStepsS.
Qed. (* this is not enough since it does not enforce matching with all hypotheses *)
Qed.
Program Instance enqueue_node_spec (lk n : loc) γh γm γe R :
SPEC {{ inv N (lock_inv γh γm γe lk R) (n + 1) NONEV loc_map_elem γm n (DfracOwn 1) None }}
......@@ -373,56 +222,15 @@ Section spec.
wait_for_succ #l
{{ (n' : loc) γ, RET #(); own γh ( (Excl' true, ε)) own γ (to_agree (n', false), 1/2)%Qp own γh ({#1/2} (Excl' true, Excl' (Some (n', γ)))) inv N_signal (head_signal_loc γh n' γ R) }}.
Global Program Instance free_node_exist_atom γm n :
AtomIntoExist (free_node γm n) [tele_pair val; val]
(λ v1 v2, n v1 (n + 1) v2 loc_map_elem γm n (DfracOwn 1) None)%I.
Definition locked γh γe R : iProp Σ :=
own γe (Excl ())
(own γh ( (Excl' true, ε))
(s : loc) γ, own γh ( (Excl' false, Excl' (Some (s, γ)))) own γ (to_agree (s, false), 1/2)%Qp inv N_signal (signal_loc γh γe s γ R)).
(* TODO: what to do with these? *)
Instance find_local_upd_excl' {O : ofe} a1 a2 a :
@FindLocalUpdate (optionUR (exclR O)) (Excl' a1) (Excl' a2) (Excl' a) (Excl' a2) True | 100.
Proof. move => Hx1. by apply option_local_update, exclusive_local_update. Qed.
Instance find_local_upd_excl2' {O : ofe} a1 :
@FindLocalUpdate (optionUR (exclR O)) (Excl' a1) (Excl' a1) ε ε True | 90.
Proof. move => Hx1. done. Qed.
Global Instance acquire_with_spec R (lk : val) (n : loc) γh γm γe :
Global Program Instance acquire_with_spec R (lk : val) (n : loc) γh γm γe :
SPEC {{ is_lock γh γm γe R lk free_node γm n }}
acquire_with lk #n
{{ RET #(); R free_node γm n locked γh γe R }}.
Proof.
iStepsS.
- iSmash. (* lock was not held *)
- iRight. (* lock is held and has waiters *)
iStepS. iRight.
iStepsS.
* iRight. (* no successor has registered *)
iStepsS. iLeft.
iStepsS.
+ iRight. (* still no registered successor: succesful detachment *)
iStepS. iRevert "H20 H18". (* reintroduce to detect more equalities *)
iSmash.
+ iSmash. (* a successor has registred in the mean time; wait till propagation and store in lk + 1 *)
* iSmash.
- iLeft. (* lock is held, no waiters *)
iStepS. iRight.
iStepS. iRight.
iStepsS.
* iRight.
iStepsS. iLeft.
iStepsS.
+ iRight.
iStepS. iRevert "H19 H17".
iSmash.
+ iSmash.
* iSmash.
Qed.
Global Program Instance acquire_spec R (lk : val) (n : loc) γh γm γe :
SPEC {{ is_lock γh γm γe R lk }}
......
......@@ -1656,11 +1656,13 @@ Section validity.
apply auth_auth_dfrac_op_validN in Hac as [Hac _].
by apply dfracown1_invalid_op in Hac.
Qed.
Global Instance frag_coalloc {A : ucmra} (a a' a'' : A) :
CoAllocate a (Some a') (* not really a restriction, since A is a ucmra*)
Global Instance frag_coalloc {A : ucmra} (a a' a'' : A) ma :
CoAllocate a ma (* not really a restriction, since A is a ucmra*)
TCEq ma (Some a')
IsOp a'' a a'
CoAllocate ( a) (Some $ a'' a').
Proof.
move => + Hma. rewrite Hma => {ma Hma}.
rewrite /IsOp => HCoAlloc Ha''.
split.
{ destruct HCoAlloc as [Hab Habc].
......
......@@ -152,6 +152,7 @@ Ltac trySolvePure ::=
| |- ( ( _)) => by apply auth_auth_valid
| |- ( (F _)) => by apply frac_auth_auth_valid
| |- ( ( _)) => by apply auth_frag_valid
| |- _ => progress eauto with nocore solve_pure_add
(* | |- _ => fast_done *)
......
Supports Markdown
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