Commit 73584da3 authored by Ralf Jung's avatar Ralf Jung

fix for Iris with stuckness bit

parent 62d7e313
Pipeline #5884 passed with stage
in 14 minutes and 26 seconds
......@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
"coq-iris" { (= "dev.2017-11-24.0") | (= "dev") }
"coq-iris" { (= "dev.2017-12-07.2") | (= "dev") }
]
......@@ -19,7 +19,7 @@ Proof. solve_inG. Qed.
Definition lrust_adequacy Σ `{lrustPreG Σ} e σ φ :
( `{lrustG Σ}, True WP e {{ v, ⌜φ v }})
adequate e σ φ.
adequate NotStuck e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (own_alloc ( to_heap σ)) as (vγ) "Hvγ".
......
......@@ -28,7 +28,7 @@ Qed.
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
| |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
unify e' efoc;
eapply (tac_wp_pure K);
[simpl; apply _ (* PureExec *)
......@@ -54,7 +54,7 @@ Qed.
Tactic Notation "wp_eq_loc" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' => eapply (tac_wp_eq_loc K));
[apply _|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
| _ => fail "wp_pure: not a 'wp'"
......@@ -82,7 +82,7 @@ Ltac wp_bind_core K :=
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
| |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind_core K
end) || fail "wp_bind: cannot find" efoc "in" e
......@@ -169,7 +169,7 @@ End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
iPoseProofCore lem as false true (fun H =>
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
lazymatch iTypeOf H with
......@@ -181,7 +181,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc K _ _ _ H Hf))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
......@@ -209,7 +209,7 @@ Tactic Notation "wp_alloc" ident(l) :=
Tactic Notation "wp_free" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_free K))
|fail 1 "wp_free: cannot find 'Free' in" e];
......@@ -229,7 +229,7 @@ Tactic Notation "wp_free" :=
Tactic Notation "wp_read" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_read K))
|fail 1 "wp_read: cannot find 'Read' in" e];
......@@ -245,7 +245,7 @@ Tactic Notation "wp_read" :=
Tactic Notation "wp_write" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [apply _|..])
|fail 1 "wp_write: cannot find 'Write' in" e];
......
......@@ -295,7 +295,7 @@ Proof.
Qed.
Corollary adequate_nonracing e1 t2 σ1 σ2 φ :
adequate e1 σ1 φ
adequate NotStuck e1 σ1 φ
rtc step ([e1], σ1) (t2, σ2)
nonracing_threadpool t2 σ2.
Proof.
......
......@@ -153,7 +153,7 @@ Definition is_atomic (e: expr) : bool :=
bool_decide (is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2))
| _ => false
end.
Lemma is_atomic_correct e : is_atomic e Atomic (to_expr e).
Lemma is_atomic_correct e : is_atomic e Atomic WeaklyAtomic (to_expr e).
Proof.
intros He. apply ectx_language_atomic.
- intros σ e' σ' ef.
......@@ -195,11 +195,11 @@ Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
Ltac solve_atomic :=
match goal with
| |- Atomic ?e =>
let e' := W.of_expr e in change (Atomic (W.to_expr e'));
| |- Atomic ?s ?e =>
let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
apply W.is_atomic_correct; vm_compute; exact I
end.
Hint Extern 0 (Atomic _) => solve_atomic : typeclass_instances.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
(** Substitution *)
Ltac simpl_subst :=
......
......@@ -123,7 +123,7 @@ Section borrow.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iDestruct "Hown" as (l') "#[H↦b #Hown]".
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iApply (wp_step_fupd _ (__) with "[Hown Htok2]"); try done.
iApply (wp_step_fupd _ _ (__) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
......@@ -184,7 +184,7 @@ Section borrow.
iAssert (κ κ' κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']"; first solve_ndisj.
iApply (wp_step_fupd _ (__) with "[Hown Htok2]"); try done.
iApply (wp_step_fupd _ _ (__) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose''" with "Htok2") as "Htok2".
......
......@@ -292,7 +292,7 @@ Section typing.
iDestruct "Hϝ" as (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
rewrite /= left_id in EQ. subst κ'. simpl. wp_rec. wp_bind Endlft.
iSpecialize ("Hinh" with "Htk"). iClear "Hκs".
iApply (wp_mask_mono (lftN)); first done.
iApply (wp_mask_mono _ (lftN)); first done.
iApply (wp_step_fupd with "Hinh"); [solve_ndisj..|]. wp_seq.
iIntros "#Htok !>". wp_seq. iMod ("HκsI" with "Htok") as ">Hκs".
iApply ("Hk" with "Htl HL Hκs"). rewrite tctx_hasty_val. done.
......
......@@ -758,7 +758,7 @@ Section arc.
wp_bind (drop_arc _). iApply (drop_arc_spec with "[] [$Htok Hν]");
[by iDestruct "Hpersist" as "[$?]"|done|].
iNext. iIntros (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
iApply (wp_wand _ _ (λ _, ty_own (box (option ty)) tid [r])%I with "[Hdrop Hr]").
iApply (wp_wand _ _ _ (λ _, ty_own (box (option ty)) tid [r])%I with "[Hdrop Hr]").
{ destruct b; wp_if=>//. destruct r as [[]|]; try done.
(* FIXME: 'simpl' reveals a match here. Didn't we forbid that for ty_own? *)
rewrite {3}[option]lock. simpl. rewrite -{2 3}lock. (* FIXME: Tried using contextual pattern, did not work. *)
......@@ -816,7 +816,7 @@ Section arc.
iDestruct "Hrc'" as (γ ν) "[#Hpersist Htok]". wp_bind (drop_weak _).
iApply (drop_weak_spec with "[] [Htok]"); [by iDestruct "Hpersist" as "[$?]"|by auto|].
iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
iApply (wp_wand _ _ (λ _, True)%I with "[Hdrop]").
iApply (wp_wand _ _ _ (λ _, True)%I with "[Hdrop]").
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
wp_apply (wp_delete _ _ _ (_::_::vl) with "[-]"); [simpl;lia| |done].
......@@ -880,7 +880,7 @@ Section arc.
iMod ("Hend" with "[$H† Hrc']") as "Htok"; first by eauto.
iApply (drop_weak_spec with "Ha Htok").
iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
iApply (wp_wand _ _ (λ _, True)%I with "[Hdrop]").
iApply (wp_wand _ _ _ (λ _, True)%I with "[Hdrop]").
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
wp_apply (wp_delete _ _ _ (_::_::vl') with "[-]"); [simpl; lia| |done].
......
......@@ -190,7 +190,7 @@ Section ref_functions.
iExists ν. iFrame. iApply step_fupd_intro; first set_solver. iIntros "!>".
iSplitR; first done. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
wp_bind Endlft. iApply (wp_mask_mono (lftN)); first done.
wp_bind Endlft. iApply (wp_mask_mono _ (lftN)); first done.
iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq.
iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
......
......@@ -131,7 +131,7 @@ Section refmut_functions.
{ by destruct (exclusive_included (Cinl (Excl ())) st'). }
setoid_subst. iDestruct "INV" as (ν') "(Hνν' & H† & _)".
iDestruct "Hνν'" as %<-%(inj to_agree)%leibniz_equiv.
wp_bind Endlft. iApply (wp_mask_mono (lftN)); first done.
wp_bind Endlft. iApply (wp_mask_mono _ (lftN)); first done.
iApply (wp_step_fupd with "[H† Hν]");
[done| |iApply ("H†" with "Hν")|]; first set_solver.
wp_seq. iIntros "{Hb} Hb !>".
......
......@@ -168,7 +168,7 @@ Section typing_rules.
iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
iApply (wp_mask_mono (lftN)); first done.
iApply (wp_mask_mono _ (lftN)); first done.
iApply (wp_step_fupd with "Hend"). done. set_solver. wp_seq.
iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
......
......@@ -32,9 +32,9 @@ Section type_soundness.
( e, e t is_Some (to_val e) reducible e σ).
Proof.
intros Hmain Hrtc.
cut (adequate (main [exit_cont]%E) (λ _, True)).
cut (adequate NotStuck (main [exit_cont]%E) (λ _, True)).
{ split. by eapply adequate_nonracing.
intros. by eapply (adequate_safe (main [exit_cont]%E)). }
intros. by eapply (adequate_not_stuck _ (main [exit_cont]%E)). }
apply: lrust_adequacy=>?. iIntros "_".
iMod lft_init as (?) "#LFT". done.
iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
......
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