Commit 9a182da8 authored by Robbert Krebbers's avatar Robbert Krebbers

Make some names more consistent.

parent 88c9a1e0
From iris_logrel.F_mu_ref_par Require Export fundamental_binary. From iris_logrel.F_mu_ref_par Require Export fundamental_binary.
Inductive ctx_item := Inductive ctx_item :=
| CTX_Lam | CTX_Rec
| CTX_AppL (e2 : expr) | CTX_AppL (e2 : expr)
| CTX_AppR (e1 : expr) | CTX_AppR (e1 : expr)
(* Products *) (* Products *)
...@@ -42,7 +42,7 @@ Inductive ctx_item := ...@@ -42,7 +42,7 @@ Inductive ctx_item :=
Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr := Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
match ctx with match ctx with
| CTX_Lam => Lam e | CTX_Rec => Rec e
| CTX_AppL e2 => App e e2 | CTX_AppL e2 => App e e2
| CTX_AppR e1 => App e1 e | CTX_AppR e1 => App e1 e
| CTX_PairL e2 => Pair e e2 | CTX_PairL e2 => Pair e e2
...@@ -80,8 +80,8 @@ Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K. ...@@ -80,8 +80,8 @@ Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K.
(** typed ctx *) (** typed ctx *)
Inductive typed_ctx_item : Inductive typed_ctx_item :
ctx_item list type type list type type Prop := ctx_item list type type list type type Prop :=
| TP_CTX_Lam Γ τ τ' : | TP_CTX_Rec Γ τ τ' :
typed_ctx_item CTX_Lam (TArrow τ τ' :: τ :: Γ) τ' Γ (TArrow τ τ') typed_ctx_item CTX_Rec (TArrow τ τ' :: τ :: Γ) τ' Γ (TArrow τ τ')
| TP_CTX_AppL Γ e2 τ τ' : | TP_CTX_AppL Γ e2 τ τ' :
typed Γ e2 τ typed Γ e2 τ
typed_ctx_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ' typed_ctx_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ'
...@@ -211,22 +211,22 @@ Section bin_log_related_under_typed_ctx. ...@@ -211,22 +211,22 @@ Section bin_log_related_under_typed_ctx.
- inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. intros H3 Δ HΔ. - inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. intros H3 Δ HΔ.
specialize (IHK _ _ _ _ e e' H1 H2 Hx2 H3). specialize (IHK _ _ _ _ e e' H1 H2 Hx2 H3).
inversion Hx1; subst; simpl. inversion Hx1; subst; simpl.
+ eapply bin_log_related_Lam; eauto; + eapply bin_log_related_rec; eauto;
match goal with match goal with
H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H) H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H)
end. end.
+ eapply bin_log_related_App; eauto using binary_fundamental. + eapply bin_log_related_app; eauto using binary_fundamental.
+ eapply bin_log_related_App; eauto using binary_fundamental. + eapply bin_log_related_app; eauto using binary_fundamental.
+ eapply bin_log_related_Pair; eauto using binary_fundamental. + eapply bin_log_related_pair; eauto using binary_fundamental.
+ eapply bin_log_related_Pair; eauto using binary_fundamental. + eapply bin_log_related_pair; eauto using binary_fundamental.
+ eapply bin_log_related_Fst; eauto. + eapply bin_log_related_fst; eauto.
+ eapply bin_log_related_Snd; eauto. + eapply bin_log_related_snd; eauto.
+ eapply bin_log_related_InjL; eauto. + eapply bin_log_related_injl; eauto.
+ eapply bin_log_related_InjR; eauto. + eapply bin_log_related_injr; eauto.
+ match goal with + match goal with
H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst
end. end.
eapply bin_log_related_Case; eapply bin_log_related_case;
eauto using binary_fundamental; eauto using binary_fundamental;
match goal with match goal with
H : _ |- _ => eapply (typed_n_closed _ _ _ H) H : _ |- _ => eapply (typed_n_closed _ _ _ H)
...@@ -234,7 +234,7 @@ Section bin_log_related_under_typed_ctx. ...@@ -234,7 +234,7 @@ Section bin_log_related_under_typed_ctx.
+ match goal with + match goal with
H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst
end. end.
eapply bin_log_related_Case; eapply bin_log_related_case;
eauto using binary_fundamental; eauto using binary_fundamental;
try match goal with try match goal with
H : _ |- _ => eapply (typed_n_closed _ _ _ H) H : _ |- _ => eapply (typed_n_closed _ _ _ H)
...@@ -245,7 +245,7 @@ Section bin_log_related_under_typed_ctx. ...@@ -245,7 +245,7 @@ Section bin_log_related_under_typed_ctx.
+ match goal with + match goal with
H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst
end. end.
eapply bin_log_related_Case; eapply bin_log_related_case;
eauto using binary_fundamental; eauto using binary_fundamental;
try match goal with try match goal with
H : _ |- _ => eapply (typed_n_closed _ _ _ H) H : _ |- _ => eapply (typed_n_closed _ _ _ H)
...@@ -253,22 +253,22 @@ Section bin_log_related_under_typed_ctx. ...@@ -253,22 +253,22 @@ Section bin_log_related_under_typed_ctx.
match goal with match goal with
H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H) H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H)
end. end.
+ eapply bin_log_related_If; eauto using typed_ctx_typed, binary_fundamental. + eapply bin_log_related_if; eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_If; eauto using typed_ctx_typed, binary_fundamental. + eapply bin_log_related_if; eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_If; eauto using typed_ctx_typed, binary_fundamental. + eapply bin_log_related_if; eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_nat_bin_op; + eapply bin_log_related_nat_binop;
eauto using typed_ctx_typed, binary_fundamental. eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_nat_bin_op; + eapply bin_log_related_nat_binop;
eauto using typed_ctx_typed, binary_fundamental. eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_Fold; eauto. + eapply bin_log_related_fold; eauto.
+ eapply bin_log_related_Unfold; eauto. + eapply bin_log_related_unfold; eauto.
+ eapply bin_log_related_TLam; eauto with typeclass_instances. + eapply bin_log_related_tlam; eauto with typeclass_instances.
+ eapply bin_log_related_TApp; eauto. + eapply bin_log_related_tapp; eauto.
+ eapply bin_log_related_Fork; eauto. + eapply bin_log_related_fork; eauto.
+ eapply bin_log_related_Alloc; eauto. + eapply bin_log_related_alloc; eauto.
+ eapply bin_log_related_Load; eauto. + eapply bin_log_related_load; eauto.
+ eapply bin_log_related_Store; eauto using binary_fundamental. + eapply bin_log_related_store; eauto using binary_fundamental.
+ eapply bin_log_related_Store; eauto using binary_fundamental. + eapply bin_log_related_store; eauto using binary_fundamental.
+ eapply bin_log_related_CAS; eauto using binary_fundamental. + eapply bin_log_related_CAS; eauto using binary_fundamental.
+ eapply bin_log_related_CAS; eauto using binary_fundamental. + eapply bin_log_related_CAS; eauto using binary_fundamental.
+ eapply bin_log_related_CAS; eauto using binary_fundamental. + eapply bin_log_related_CAS; eauto using binary_fundamental.
......
...@@ -3,27 +3,27 @@ From iris_logrel.F_mu_ref_par Require Export examples.lock. ...@@ -3,27 +3,27 @@ From iris_logrel.F_mu_ref_par Require Export examples.lock.
From iris_logrel.F_mu_ref_par Require Import soundness_binary. From iris_logrel.F_mu_ref_par Require Import soundness_binary.
Definition CG_increment (x : expr) : expr := Definition CG_increment (x : expr) : expr :=
Lam (Store x.[ren (+ 2)] (BinOp Add ( 1) (Load x.[ren (+ 2)]))). Rec (Store x.[ren (+ 2)] (BinOp Add ( 1) (Load x.[ren (+ 2)]))).
Definition CG_locked_increment (x l : expr) : expr := Definition CG_locked_increment (x l : expr) : expr :=
with_lock (CG_increment x) l. with_lock (CG_increment x) l.
Definition CG_locked_incrementV (x l : expr) : val := Definition CG_locked_incrementV (x l : expr) : val :=
with_lockV (CG_increment x) l. with_lockV (CG_increment x) l.
Definition counter_read (x : expr) : expr := Lam (Load x.[ren (+2)]). Definition counter_read (x : expr) : expr := Rec (Load x.[ren (+2)]).
Definition counter_readV (x : expr) : val := LamV (Load x.[ren (+2)]). Definition counter_readV (x : expr) : val := RecV (Load x.[ren (+2)]).
Definition CG_counter_body (x l : expr) : expr := Definition CG_counter_body (x l : expr) : expr :=
Pair (CG_locked_increment x l) (counter_read x). Pair (CG_locked_increment x l) (counter_read x).
Definition CG_counter : expr := Definition CG_counter : expr :=
App App
(Lam $ App (Lam (CG_counter_body (Var 1) (Var 3))) (Rec $ App (Rec (CG_counter_body (Var 1) (Var 3)))
(Alloc ( 0))) (Alloc ( 0)))
newlock. newlock.
Definition FG_increment (x : expr) : expr := Definition FG_increment (x : expr) : expr :=
Lam $ App Rec $ App
(Lam $ (Rec $
(* try increment *) (* try increment *)
If (CAS x.[ren (+4)] (Var 1) (BinOp Add ( 1) (Var 1))) If (CAS x.[ren (+4)] (Var 1) (BinOp Add ( 1) (Var 1)))
Unit (* increment succeeds we return unit *) Unit (* increment succeeds we return unit *)
...@@ -32,7 +32,7 @@ Definition FG_increment (x : expr) : expr := ...@@ -32,7 +32,7 @@ Definition FG_increment (x : expr) : expr :=
Definition FG_counter_body (x : expr) : expr := Definition FG_counter_body (x : expr) : expr :=
Pair (FG_increment x) (counter_read x). Pair (FG_increment x) (counter_read x).
Definition FG_counter : expr := Definition FG_counter : expr :=
App (Lam (FG_counter_body (Var 1))) (Alloc ( 0)). App (Rec (FG_counter_body (Var 1))) (Alloc ( 0)).
Section CG_Counter. Section CG_Counter.
Context `{cfgSG Σ, heapIG Σ}. Context `{cfgSG Σ, heapIG Σ}.
...@@ -63,13 +63,13 @@ Section CG_Counter. ...@@ -63,13 +63,13 @@ Section CG_Counter.
={E}=> j fill K (Unit) x ↦ₛ (v (S n)). ={E}=> j fill K (Unit) x ↦ₛ (v (S n)).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hx Hj]]". unfold CG_increment. iIntros {HNE} "[#Hspec [Hx Hj]]". unfold CG_increment.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_load _ _ j (K ++ [StoreRCtx (LocV _); BinOpRCtx _ (v _)]) iPvs (step_load _ _ j (K ++ [StoreRCtx (LocV _); BinOpRCtx _ (v _)])
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
rewrite ?fill_app. simpl. rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial. iFrame "Hspec Hj"; trivial.
rewrite ?fill_app. simpl. rewrite ?fill_app. simpl.
iPvs (step_nat_bin_op _ _ j (K ++ [StoreRCtx (LocV _)]) iPvs (step_nat_binop _ _ j (K ++ [StoreRCtx (LocV _)])
_ _ _ with "[Hj]") as "Hj"; eauto. _ _ _ with "[Hj]") as "Hj"; eauto.
rewrite ?fill_app. simpl. rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial. simpl. iFrame "Hspec Hj"; trivial. simpl.
...@@ -164,7 +164,7 @@ Section CG_Counter. ...@@ -164,7 +164,7 @@ Section CG_Counter.
={E}=> j fill K ( n) x ↦ₛ (v n). ={E}=> j fill K ( n) x ↦ₛ (v n).
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iPvs (step_lam _ _ j K _ Unit with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
asimpl. asimpl.
iPvs (step_load _ _ j K with "[Hj Hx]") as "[Hj Hx]"; eauto. iPvs (step_load _ _ j K with "[Hj Hx]") as "[Hj Hx]"; eauto.
{ by iFrame "Hspec Hj". } { by iFrame "Hspec Hj". }
...@@ -260,24 +260,24 @@ Section CG_Counter. ...@@ -260,24 +260,24 @@ Section CG_Counter.
{ iDestruct (interp_env_length with "HΓ") as %[=]. } { iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_counter CG_counter]. iClear "HΓ". cbn -[FG_counter CG_counter].
rewrite ?empty_env_subst /CG_counter /FG_counter. rewrite ?empty_env_subst /CG_counter /FG_counter.
iPvs (steps_newlock _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]") iPvs (steps_newlock _ _ j (K ++ [AppRCtx (RecV _)]) _ with "[Hj]")
as {l} "[Hj Hl]"; eauto. as {l} "[Hj Hl]"; eauto.
{ rewrite fill_app /=. by iFrame. } { rewrite fill_app /=. by iFrame. }
rewrite fill_app /=. rewrite fill_app /=.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite CG_locked_increment_subst /=. asimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=. rewrite counter_read_subst /=.
iPvs (step_alloc _ _ j (K ++ [AppRCtx (LamV _)]) _ _ _ _ with "[Hj]") iPvs (step_alloc _ _ j (K ++ [AppRCtx (RecV _)]) _ _ _ _ with "[Hj]")
as {cnt'} "[Hj Hcnt']"; eauto. as {cnt'} "[Hj Hcnt']"; eauto.
{ rewrite fill_app; simpl. by iFrame. } { rewrite fill_app; simpl. by iFrame. }
rewrite fill_app; simpl. rewrite fill_app; simpl.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite CG_locked_increment_subst /=. asimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=. rewrite counter_read_subst /=.
Unshelve. Unshelve.
all: try match goal with |- to_val _ = _ => auto using to_of_val end. all: try match goal with |- to_val _ = _ => auto using to_of_val end.
all: trivial. all: trivial.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]); iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|]. iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {cnt} "Hcnt /=". iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {cnt} "Hcnt /=".
iPvsIntro. iPvsIntro.
...@@ -288,7 +288,7 @@ Section CG_Counter. ...@@ -288,7 +288,7 @@ Section CG_Counter.
iPvs (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial. iPvs (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
{ iNext; iExact "Hinv". } { iNext; iExact "Hinv". }
(* splitting increment and read *) (* splitting increment and read *)
iApply wp_lam; trivial. iNext. asimpl. iApply wp_rec; trivial. iNext. asimpl.
rewrite counter_read_subst /=. rewrite counter_read_subst /=.
iApply wp_value; simpl. iApply wp_value; simpl.
{ by rewrite counter_read_to_val. } { by rewrite counter_read_to_val. }
...@@ -301,19 +301,19 @@ Section CG_Counter. ...@@ -301,19 +301,19 @@ Section CG_Counter.
rewrite CG_locked_increment_of_val /=. rewrite CG_locked_increment_of_val /=.
destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=. destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=.
iLöb as "Hlat". iLöb as "Hlat".
iApply wp_lam; trivial. asimpl. iNext. iApply wp_rec; trivial. asimpl. iNext.
(* fine-grained reads the counter *) (* fine-grained reads the counter *)
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]); iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|]. iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv> counterN as {n} "[Hl [Hcnt Hcnt']]". iInv> counterN as {n} "[Hl [Hcnt Hcnt']]".
iApply wp_load; [|iFrame "Hheap"]. solve_ndisj. iApply wp_load; [|iFrame "Hheap"]. solve_ndisj.
iIntros "> {$Hcnt} Hcnt". iPvsIntro. iIntros "> {$Hcnt} Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|]. iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_lam; trivial. asimpl. iNext. iApply wp_rec; trivial. asimpl. iNext.
(* fine-grained performs increment *) (* fine-grained performs increment *)
iApply (@wp_bind _ _ _ [IfCtx _ _; CasRCtx (LocV _) (NatV _)]); iApply (@wp_bind _ _ _ [IfCtx _ _; CasRCtx (LocV _) (NatV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|]. iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iApply wp_nat_bin_op; simpl. iApply wp_nat_binop; simpl.
iNext. iPvsIntro. iNext. iPvsIntro.
iApply (@wp_bind _ _ _ [IfCtx _ _]); iApply (@wp_bind _ _ _ [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|]. iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
...@@ -343,7 +343,7 @@ Section CG_Counter. ...@@ -343,7 +343,7 @@ Section CG_Counter.
iDestruct "Heq" as "[% %]"; destruct v; simplify_eq/=. iDestruct "Heq" as "[% %]"; destruct v; simplify_eq/=.
Transparent counter_read. Transparent counter_read.
unfold counter_read at 2. unfold counter_read at 2.
iApply wp_lam; trivial. simpl. iApply wp_rec; trivial. simpl.
iNext. iInv> counterN as {n} "[Hl [Hcnt Hcnt']]". iNext. iInv> counterN as {n} "[Hl [Hcnt Hcnt']]".
iPvs (steps_counter_read with "[Hj Hcnt']") as "[Hj Hcnt']". iPvs (steps_counter_read with "[Hj Hcnt']") as "[Hj Hcnt']".
{ solve_ndisj. } { solve_ndisj. }
......
...@@ -3,19 +3,19 @@ From iris_logrel.F_mu_ref_par Require Export rules_binary typing. ...@@ -3,19 +3,19 @@ From iris_logrel.F_mu_ref_par Require Export rules_binary typing.
Definition newlock : expr := Alloc ( false). Definition newlock : expr := Alloc ( false).
Definition acquire : expr := Definition acquire : expr :=
Lam (If (CAS (Var 1) ( false) ( true)) (Unit) (App (Var 0) (Var 1))). Rec (If (CAS (Var 1) ( false) ( true)) (Unit) (App (Var 0) (Var 1))).
Definition release : expr := Lam (Store (Var 1) ( false)). Definition release : expr := Rec (Store (Var 1) ( false)).
Definition with_lock (e : expr) (l : expr) : expr := Definition with_lock (e : expr) (l : expr) : expr :=
Lam Rec
(App (Lam (App (Lam (App (Lam (Var 3)) (App release l.[ren (+6)]))) (App (Rec (App (Rec (App (Rec (Var 3)) (App release l.[ren (+6)])))
(App e.[ren (+4)] (Var 3)))) (App e.[ren (+4)] (Var 3))))
(App acquire l.[ren (+2)]) (App acquire l.[ren (+2)])
). ).
Definition with_lockV (e l : expr) : val := Definition with_lockV (e l : expr) : val :=
LamV RecV
(App (Lam (App (Lam (App (Lam (Var 3)) (App release l.[ren (+6)]))) (App (Rec (App (Rec (App (Rec (Var 3)) (App release l.[ren (+6)])))
(App e.[ren (+4)] (Var 3)))) (App e.[ren (+4)] (Var 3))))
(App acquire l.[ren (+2)]) (App acquire l.[ren (+2)])
). ).
...@@ -93,7 +93,7 @@ Section proof. ...@@ -93,7 +93,7 @@ Section proof.
={E}=> j fill K Unit l ↦ₛ (v true). ={E}=> j fill K Unit l ↦ₛ (v true).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hl Hj]]". unfold acquire. iIntros {HNE} "[#Hspec [Hl Hj]]". unfold acquire.
iPvs (step_lam _ _ j K with "[Hj]") as "Hj"; eauto. done. iPvs (step_rec _ _ j K with "[Hj]") as "Hj"; eauto. done.
iPvs (step_cas_suc _ _ j (K ++ [IfCtx _ _]) iPvs (step_cas_suc _ _ j (K ++ [IfCtx _ _])
_ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial. _ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
rewrite ?fill_app. simpl. rewrite ?fill_app. simpl.
...@@ -114,7 +114,7 @@ Section proof. ...@@ -114,7 +114,7 @@ Section proof.
={E}=> j fill K Unit l ↦ₛ (v false). ={E}=> j fill K Unit l ↦ₛ (v false).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hl Hj]]". unfold release. iIntros {HNE} "[#Hspec [Hl Hj]]". unfold release.
iPvs (step_lam _ _ j K with "[Hj]") as "Hj"; eauto; try done. iPvs (step_rec _ _ j K with "[Hj]") as "Hj"; eauto; try done.
iPvs (step_store _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto. iPvs (step_store _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
iFrame "Hspec Hj"; trivial. iFrame "Hspec Hj"; trivial.
iPvsIntro. iFrame "Hj Hl"; trivial. iPvsIntro. iFrame "Hj Hl"; trivial.
...@@ -133,26 +133,26 @@ Section proof. ...@@ -133,26 +133,26 @@ Section proof.
={E}=> j fill K (# v) Q l ↦ₛ (v false). ={E}=> j fill K (# v) Q l ↦ₛ (v false).
Proof. Proof.
iIntros {HNE H1 H2} "[#Hspec [HP [Hl Hj]]]". iIntros {HNE H1 H2} "[#Hspec [HP [Hl Hj]]]".
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite H1. asimpl. rewrite H1.
iPvs (steps_acquire _ _ j (K ++ [AppRCtx (LamV _)]) iPvs (steps_acquire _ _ j (K ++ [AppRCtx (RecV _)])
_ _ with "[Hj Hl]") as "[Hj Hl]"; eauto. _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
rewrite fill_app; simpl. rewrite fill_app; simpl.
iFrame "Hspec Hj"; trivial. iFrame "Hspec Hj"; trivial.
rewrite fill_app; simpl. rewrite fill_app; simpl.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite H1. asimpl. rewrite H1.
iPvs (H2 (K ++ [AppRCtx (LamV _)]) with "[Hj HP]") as "[Hj HQ]"; eauto. iPvs (H2 (K ++ [AppRCtx (RecV _)]) with "[Hj HP]") as "[Hj HQ]"; eauto.
rewrite ?fill_app /=. rewrite ?fill_app /=.
iFrame "Hspec HP"; trivial. iFrame "Hspec HP"; trivial.
rewrite ?fill_app /=. rewrite ?fill_app /=.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. asimpl.
iPvs (steps_release _ _ j (K ++ [AppRCtx (LamV _)]) _ _ with "[Hj Hl]") iPvs (steps_release _ _ j (K ++ [AppRCtx (RecV _)]) _ _ with "[Hj Hl]")
as "[Hj Hl]"; eauto. as "[Hj Hl]"; eauto.
rewrite ?fill_app /=. by iFrame. rewrite ?fill_app /=. by iFrame.
rewrite ?fill_app /=. rewrite ?fill_app /=.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iPvsIntro; by iFrame. asimpl. iPvsIntro; by iFrame.
Unshelve. Unshelve.
all: try match goal with |- to_val _ = _ => auto using to_of_val end. all: try match goal with |- to_val _ = _ => auto using to_of_val end.
......
...@@ -7,17 +7,17 @@ Definition CG_StackType τ := ...@@ -7,17 +7,17 @@ Definition CG_StackType τ :=
(* Coarse-grained push *) (* Coarse-grained push *)
Definition CG_push (st : expr) : expr := Definition CG_push (st : expr) : expr :=
Lam (Store Rec (Store
(st.[ren (+2)]) (Fold (InjR (Pair (Var 1) (Load st.[ren (+ 2)]))))). (st.[ren (+2)]) (Fold (InjR (Pair (Var 1) (Load st.[ren (+ 2)]))))).
Definition CG_locked_push (st l : expr) := with_lock (CG_push st) l. Definition CG_locked_push (st l : expr) := with_lock (CG_push st) l.
Definition CG_locked_pushV (st l : expr) : val := with_lockV (CG_push st) l. Definition CG_locked_pushV (st l : expr) : val := with_lockV (CG_push st) l.
Definition CG_pop (st : expr) : expr := Definition CG_pop (st : expr) : expr :=
Lam (Case (Unfold (Load st.[ren (+ 2)])) Rec (Case (Unfold (Load st.[ren (+ 2)]))
(InjL Unit) (InjL Unit)
( (
App (Lam (InjR (Fst (Var 2)))) App (Rec (InjR (Fst (Var 2))))
(Store st.[ren (+ 3)] (Snd (Var 0))) (Store st.[ren (+ 3)] (Snd (Var 0)))
) )
). ).
...@@ -25,35 +25,35 @@ Definition CG_pop (st : expr) : expr := ...@@ -25,35 +25,35 @@ Definition CG_pop (st : expr) : expr :=
Definition CG_locked_pop (st l : expr) := with_lock (CG_pop st) l. Definition CG_locked_pop (st l : expr) := with_lock (CG_pop st) l.
Definition CG_locked_popV (st l : expr) : val := with_lockV (CG_pop st) l. Definition CG_locked_popV (st l : expr) : val := with_lockV (CG_pop st) l.
Definition CG_snap (st l : expr) := with_lock (Lam (Load st.[ren (+2)])) l. Definition CG_snap (st l : expr) := with_lock (Rec (Load st.[ren (+2)])) l.
Definition CG_snapV (st l : expr) : val := with_lockV (Lam (Load st.[ren (+2)])) l. Definition CG_snapV (st l : expr) : val := with_lockV (Rec (Load st.[ren (+2)])) l.
Definition CG_iter (f : expr) : expr := Definition CG_iter (f : expr) : expr :=
Lam (Case (Unfold (Var 1)) Rec (Case (Unfold (Var 1))
Unit Unit
( (
App (Lam (App (Var 3) (Snd (Var 2)))) App (Rec (App (Var 3) (Snd (Var 2))))
(App f.[ren (+3)] (Fst (Var 0))) (App f.[ren (+3)] (Fst (Var 0)))
) )
). ).
Definition CG_iterV (f : expr) : val := Definition CG_iterV (f : expr) : val :=
LamV (Case (Unfold (Var 1)) RecV (Case (Unfold (Var 1))
Unit Unit
( (
App (Lam (App (Var 3) (Snd (Var 2)))) App (Rec (App (Var 3) (Snd (Var 2))))
(App f.[ren (+3)] (Fst (Var 0))) (App f.[ren (+3)] (Fst (Var 0)))
) )
). ).
Definition CG_snap_iter (st l : expr) : expr := Definition CG_snap_iter (st l : expr) : expr :=
Lam (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)). Rec (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)).
Definition CG_stack_body (st l : expr) : expr := Definition CG_stack_body (st l : expr) : expr :=
Pair (Pair (CG_locked_push st l) (CG_locked_pop st l)) Pair (Pair (CG_locked_push st l) (CG_locked_pop st l))
(CG_snap_iter st l). (CG_snap_iter st l).
Definition CG_stack : expr := Definition CG_stack : expr :=
TLam (App (Lam (App (Lam (CG_stack_body (Var 1) (Var 3))) TLam (App (Rec (App (Rec (CG_stack_body (Var 1) (Var 3)))
(Alloc (Fold (InjL Unit))))) newlock). (Alloc (Fold (InjL Unit))))) newlock).
Section CG_Stack. Section CG_Stack.
...@@ -82,7 +82,7 @@ Section CG_Stack. ...@@ -82,7 +82,7 @@ Section CG_Stack.
={E}=> j fill K Unit st ↦ₛ FoldV (InjRV (PairV w v)). ={E}=> j fill K Unit st ↦ₛ FoldV (InjRV (PairV w v)).
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. asimpl.
iPvs (step_load _ _ j (K ++ [StoreRCtx (LocV _); FoldCtx; iPvs (step_load _ _ j (K ++ [StoreRCtx (LocV _); FoldCtx;
InjRCtx; PairRCtx _]) InjRCtx; PairRCtx _])
...@@ -179,7 +179,7 @@ Section CG_Stack. ...@@ -179,7 +179,7 @@ Section CG_Stack.
={E}=> j fill K (InjR (# w)) st ↦ₛ v. ={E}=> j fill K (InjR (# w)) st ↦ₛ v.
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. asimpl.
iPvs (step_load _ _ j (K ++ [CaseCtx _ _; UnfoldCtx])