Commit a1f6b809 authored by Michael Sammler's avatar Michael Sammler
Browse files

Parametrize Omega by the thread_id

This change is required for the dataraces since there Omega needs to
refer to the current thread id. In particular, Omega should refer to a
different thread_id after forking (which is not possible without this
change).
parent c5db9733
......@@ -27,7 +27,7 @@ Section data_race.
)%E.
Lemma remove_store_and_load_sim π:
sim_ectx val_rel π remove_store_and_load_opt remove_store_and_load val_rel.
sim_ectx (const val_rel) π remove_store_and_load_opt remove_store_and_load val_rel.
Proof.
iIntros (v_t v_s) "Hrel". sim_pures.
......@@ -75,7 +75,7 @@ Section data_race.
)%E.
Lemma reg_promote_loop_sim π f:
sim_ectx val_rel π (reg_promote_loop_opt f) (reg_promote_loop f) val_rel.
sim_ectx (const val_rel) π (reg_promote_loop_opt f) (reg_promote_loop f) val_rel.
Proof.
iIntros (v_t v_s) "Hrel". sim_pures.
......@@ -119,7 +119,7 @@ Section data_race.
)%E.
Lemma hoist_load_sim π:
sim_ectx val_rel π hoist_load_opt hoist_load val_rel.
sim_ectx (const val_rel) π hoist_load_opt hoist_load val_rel.
Proof.
iIntros (v_t v_s) "Hrel". sim_pures.
......
......@@ -8,7 +8,7 @@ From simuliris.simplang Require heap_bij.
Module fix_bi.
Section a.
Context `{sheapGS Σ}.
Context `{sheapGS Σ} (π : thread_id).
Program Instance : sheapInv Σ := {|
sheap_inv _ _ _ _ _ := True%I;
|}.
......@@ -18,44 +18,46 @@ Proof. done. Qed.
Definition val_rel (v1 v2 : val) : iProp Σ := (v1 = v2)%I.
Lemma test_load l l2 π :
Local Notation "et '⪯' es {{ Φ }}" := (et {π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es [{ Φ }]" := (et {π, const val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
Lemma test_load l l2 :
l t #4 - l2 s #4 -
((! #l)%E {π, val_rel} ! #l2 {{ val_rel }}).
((! #l)%E ! #l2 {{ val_rel }}).
Proof.
iIntros "H H1". target_load. source_load. sim_val. eauto.
Qed.
Lemma test_store l l2 π :
Lemma test_store l l2 :
l t #4 - l2 s #4 -
((#l <- #42)%E {π, val_rel} #l2 <- #1337 {{ val_rel }}).
((#l <- #42)%E #l2 <- #1337 {{ val_rel }}).
Proof.
iIntros "H H1". target_store. source_store. sim_val. eauto.
Qed.
(* FIXME: fix precedences for ⪯ to make the parantheses unnecessary *)
Lemma test_alloc π :
(Alloc #2 ;; #()) {π, val_rel} (Alloc #4;;#()) {{ val_rel }}.
Lemma test_alloc :
(Alloc #2 ;; #()) (Alloc #4;;#()) {{ val_rel }}.
Proof.
target_alloc l1 as "H" "_".
source_alloc l2 as "H2" "_".
(*to_sim. *)
(*target_pures. source_pures. *)
sim_pures; sim_val.
eauto.
Qed.
Lemma test_free l l2 π :
Lemma test_free l l2 :
l t #42 - l2 s #1337 - l t 1 - l2 s 1 -
Free #l {π, val_rel} Free #l2 {{ val_rel }}.
Free #l Free #l2 {{ val_rel }}.
Proof.
iIntros "H1 H2 H3 H4".
target_free. source_free. sim_val. eauto.
Qed.
(* FIXME: if we remove the parantheses around the first element, parsing is broken *)
Lemma test_freeN l l2 π :
Lemma test_freeN l l2 :
l t [(#42); #99] - l2 s [(#1337); #420; #666] - l t 2 - l2 s 3 -
FreeN #2 #l {π, val_rel} FreeN #3 #l2 {{ val_rel }}.
FreeN #2 #l FreeN #3 #l2 {{ val_rel }}.
Proof.
iIntros "H1 H2 H3 H4".
target_free; first done. source_free; first done. sim_val. eauto.
......@@ -65,48 +67,50 @@ End fix_bi.
Module bij_test.
Import heap_bij.
Context `{sbijG Σ}.
Context `{sbijG Σ} (π : thread_id).
Local Notation "et '⪯' es {{ Φ }}" := (et {π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es [{ Φ }]" := (et {π, const val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
Lemma test_load l l2 π:
Lemma test_load l l2:
l t #4 - l2 s #4 -
((! #l)%E {π, val_rel} ! #l2 {{ val_rel }}).
((! #l)%E ! #l2 {{ val_rel }}).
Proof.
iIntros "H H1". target_load. source_load. sim_val. eauto.
Qed.
Lemma test_store l l2 π:
Lemma test_store l l2:
l t #4 - l2 s #4 -
((#l <- #42)%E {π, val_rel} #l2 <- #1337 {{ val_rel }}).
((#l <- #42)%E #l2 <- #1337 {{ val_rel }}).
Proof.
iIntros "H H1". target_store. source_store. sim_val. eauto.
Qed.
Lemma test_insert l l2 π:
Lemma test_insert l l2:
l t #4 - l2 s #4 - l t 1 - l2 s 1 -
((#l <- #42)%E {π, val_rel} #l2 <- #42 {{ val_rel }}).
((#l <- #42)%E #l2 <- #42 {{ val_rel }}).
Proof.
iIntros "H H1 H2 H3".
iApply (sim_bij_insert _ _ l l2 with "H2 H3 H H1 "); first done; iIntros "Hb".
iApply (sim_bij_store with "Hb []"); first done. by sim_val.
Qed.
Lemma test_bij_store (l_t l_s : loc) π :
Lemma test_bij_store (l_t l_s : loc) :
l_t h l_s -
(#l_t <- #42)%E {π, val_rel} (#l_s <- #42)%E {{ val_rel }}.
(#l_t <- #42)%E (#l_s <- #42)%E {{ val_rel }}.
Proof.
iIntros "H". sim_store; first done. by sim_val.
Qed.
Lemma test_bij_load (l_t l_s : loc) π:
Lemma test_bij_load (l_t l_s : loc):
l_t h l_s -
! #l_t {π, val_rel} ! #l_s {{ val_rel }}.
! #l_t ! #l_s {{ val_rel }}.
Proof.
iIntros "H". sim_load v_t v_s as "Ha"; sim_val. done.
Qed.
Lemma test_bij_free (l_t l_s : loc) π:
Lemma test_bij_free (l_t l_s : loc):
l_t h l_s -
Free #l_t {π, val_rel} Free #l_s {{ val_rel }}.
Free #l_t Free #l_s {{ val_rel }}.
Proof.
iIntros "#H". sim_free; sim_val. done.
Qed.
......
......@@ -41,7 +41,8 @@ Section reorder.
iApply (sim_bij_insert with "Ha1_t Ha2_s Hl1_t Hl2_s Hv1"); iIntros "#Hbij_1".
iApply (sim_bij_insert with "Ha2_t Ha1_s Hl2_t Hl1_s Hv2"); iIntros "#Hbij_2".
iApply sim_call; [done | done | simpl; by eauto ].
iApply sim_wand; [ iApply sim_call; [done | done | simpl; by eauto ] |].
iIntros (??) "$".
Qed.
End reorder.
......@@ -33,7 +33,7 @@ Inductive val_rel_pure : val → val → Prop :=
Local Hint Constructors val_rel_pure : core.
Definition val_rel v1 v2 : iProp Σ := (val_rel_pure v1 v2)%I.
Local Notation "et '⪯' es {{ Φ }}" := (et {π, val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es {{ Φ }}" := (et {π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Definition mul2_source :=
(λ: "x",
......@@ -84,6 +84,7 @@ Lemma client_sim (n : Z) :
Proof.
iIntros "Htarget Hsource Hinj1_t".
target_call. target_call. source_call. sim_pures.
iApply sim_call; eauto.
iApply sim_wand; [ iApply sim_call; [done..|]; eauto |].
eauto.
Qed.
End fix_bi.
......@@ -4,14 +4,17 @@ From simuliris.simulation Require Import slsls lifting.
From simuliris.simplang Require Import log_rel.
Section fix_bi.
Context `{sbijG Σ}.
Context `{sbijG Σ} (π : thread_id).
Local Notation "et '⪯' es {{ Φ }}" := (et {π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es [{ Φ }]" := (et {π, const val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
Definition loop_test n : expr :=
let: "n" := Alloc #n in
While (#0 < ! "n") ("n" <- ! "n" - #1).
Lemma loop (n : nat) π :
loop_test n {π, val_rel} #() {{ val_rel }}.
Lemma loop (n : nat) :
loop_test n #() {{ val_rel }}.
Proof.
rewrite /loop_test.
target_alloc l as "Hl" "_". sim_pures.
......@@ -49,8 +52,8 @@ Section fix_bi.
+ by assert ((n0 - S n) * m + m = (n0 - n) * m)%Z as -> by lia.
Qed.
Lemma mul_sim (n m : nat) π :
mul_loop #n #m {π, val_rel} #n * #m {{ val_rel }}.
Lemma mul_sim (n m : nat) :
mul_loop #n #m #n * #m {{ val_rel }}.
Proof.
rewrite /mul_loop.
sim_pures. target_alloc l_n as "Hln" "Ha_n". target_alloc l_acc as "Hlacc" "Ha_acc".
......@@ -88,7 +91,7 @@ Section fix_bi.
"rec" @s input_rec -
log_rel input_loop (Call ##"rec" #true).
Proof.
iIntros "#Hs". log_rel. iIntros "!#" (π).
iIntros "#Hs". log_rel. iIntros "!#" (π').
rewrite /input_loop. target_alloc lc_t as "Hlc_t" "_". sim_pures.
iApply (sim_while_rec _ _ _ _ _ _ (λ v_s, v_t, val_rel v_t v_s lc_t t v_t)%I with "[Hlc_t] Hs").
{ iExists #true. eauto. }
......@@ -108,7 +111,7 @@ Section fix_bi.
"rec" @t input_rec -
log_rel (Call ##"rec" #true) input_loop.
Proof.
iIntros "#Hs". log_rel. iIntros "!#" (π).
iIntros "#Hs". log_rel. iIntros "!#" (π').
rewrite /input_loop. source_alloc lc_s as "Hlc_s" "Ha_s". sim_pures.
iApply (sim_rec_while _ _ _ _ _ _ (λ v_t, v_s, val_rel v_t v_s lc_s s v_s)%I with "[Hlc_s] Hs").
{ iExists #true. eauto. }
......
......@@ -253,8 +253,8 @@ Section fix_heap.
Global Instance : sheapInvConst.
Proof. done. Qed.
Local Notation "et '⪯' es {{ Φ }}" := (et {π, val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es [{ Φ }]" := (et {π, val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es {{ Φ }}" := (et {π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es [{ Φ }]" := (et {π, const val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
Lemma sim_bij_load_sc l_t l_s Φ :
l_t h l_s -
......@@ -633,7 +633,7 @@ Section sim.
Import bi.
Local Notation "et '⪯' es {{ Φ }}" := (et {π, val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es {{ Φ }}" := (et {π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Implicit Types
(K_t K_s : ectx)
......@@ -652,10 +652,10 @@ Section sim.
( v_t v_s,
match envs_app true (Esnoc Enil j (val_rel v_t v_s)) Δ with
| Some Δ' =>
envs_entails Δ' (sim_expr val_rel Φ π (fill K_t (Val v_t)) (fill K_s (Val v_s)))
envs_entails Δ' (sim_expr (const val_rel) Φ π (fill K_t (Val v_t)) (fill K_s (Val v_s)))
| None => False
end)
envs_entails Δ (sim_expr val_rel Φ π (fill K_t (Load o (LitV l_t))) (fill K_s (Load o (LitV l_s))))%I.
envs_entails Δ (sim_expr (const val_rel) Φ π (fill K_t (Load o (LitV l_t))) (fill K_s (Load o (LitV l_s))))%I.
Proof using val_rel_pers.
rewrite envs_entails_eq=> ? Hi.
rewrite -sim_expr_bind. eapply wand_apply; first exact: sim_bij_load.
......@@ -671,8 +671,8 @@ Section sim.
Lemma tac_bij_store Δ i K_t K_s b l_t l_s v_t' v_s' o Φ :
envs_lookup i Δ = Some (b, l_t h l_s)%I
envs_entails Δ (val_rel v_t' v_s')
envs_entails Δ (sim_expr val_rel Φ π (fill K_t (Val $ LitV LitUnit)) (fill K_s (Val $ LitV LitUnit)))
envs_entails Δ (sim_expr val_rel Φ π (fill K_t (Store o (LitV l_t) (Val v_t'))) (fill K_s (Store o (LitV l_s) (Val v_s')))).
envs_entails Δ (sim_expr (const val_rel) Φ π (fill K_t (Val $ LitV LitUnit)) (fill K_s (Val $ LitV LitUnit)))
envs_entails Δ (sim_expr (const val_rel) Φ π (fill K_t (Store o (LitV l_t) (Val v_t'))) (fill K_s (Store o (LitV l_s) (Val v_s')))).
Proof using val_rel_pers.
rewrite envs_entails_eq => HΔ.
rewrite (persistent_persistently_2 (val_rel _ _)).
......@@ -691,8 +691,8 @@ Section sim.
*)
Lemma tac_bij_freeN Δ i K_t K_s b l_t l_s n Φ :
envs_lookup i Δ = Some (b, l_t h l_s)%I
envs_entails (envs_delete true i b Δ) (sim_expr val_rel Φ π (fill K_t (Val $ LitV LitUnit)) (fill K_s (Val $ LitV LitUnit)))
envs_entails Δ (sim_expr val_rel Φ π (fill K_t (FreeN (Val $ LitV $ LitInt n) (LitV l_t))) (fill K_s (FreeN (Val $ LitV $ LitInt n) (LitV l_s)))).
envs_entails (envs_delete true i b Δ) (sim_expr (const val_rel) Φ π (fill K_t (Val $ LitV LitUnit)) (fill K_s (Val $ LitV LitUnit)))
envs_entails Δ (sim_expr (const val_rel) Φ π (fill K_t (FreeN (Val $ LitV $ LitInt n) (LitV l_t))) (fill K_s (FreeN (Val $ LitV $ LitInt n) (LitV l_s)))).
Proof using val_rel_pers.
rewrite envs_entails_eq => Hl HΔ.
rewrite -sim_expr_bind. rewrite (envs_lookup_sound _ _ _ _ Hl).
......
......@@ -145,7 +145,7 @@ Section refl.
{ iApply (subst_map_rel_weaken with "[$]"). set_solver. }
iIntros (v_t2 v_s2) "#Hv2".
discr_source; first by apply call_not_val. val_discr_source "Hv2".
iApply sim_call; done.
iApply sim_wand; [ by iApply sim_call|]. iIntros (??) "$".
Qed.
Lemma log_rel_unop e_t e_s o :
......
......@@ -65,12 +65,12 @@ Section open_rel.
Definition log_rel e_t e_s : iProp Σ :=
π (map : gmap string (val * val)),
subst_map_rel (free_vars e_t free_vars e_s) map -
subst_map (fst <$> map) e_t {π, val_rel} subst_map (snd <$> map) e_s {{ val_rel }}.
subst_map (fst <$> map) e_t {π, const val_rel} subst_map (snd <$> map) e_s {{ val_rel }}.
Lemma log_rel_closed e_t e_s :
free_vars e_t =
free_vars e_s =
log_rel e_t e_s ( π, e_t {π, val_rel} e_s {{ val_rel }}).
log_rel e_t e_s ( π, e_t {π, const val_rel} e_s {{ val_rel }}).
Proof.
intros Hclosed_t Hclosed_s. iSplit.
- iIntros "#Hrel !#" (π). iSpecialize ("Hrel" $! π ).
......
......@@ -115,7 +115,7 @@ Implicit Types l : loc.
Implicit Types f : fname.
Implicit Types π : thread_id.
Context (Ω : val val iProp Σ) (π : thread_id).
Context (Ω : thread_id val val iProp Σ) (π : thread_id).
Local Notation "et '⪯' es [{ Φ }]" := (et {π, Ω} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
(** Program for target *)
......@@ -432,7 +432,7 @@ Qed.
Lemma sim_call e_t e_s v_t v_s f :
to_val e_t = Some v_t
to_val e_s = Some v_s
Ω v_t v_s - Call (## f) e_t {π, Ω} Call (## f) e_s {{ Ω }}.
Ω π v_t v_s - Call (## f) e_t {π, Ω} Call (## f) e_s {{ Ω π }}.
Proof.
intros <-%of_to_val <-%of_to_val.
(* FIXME use lifting lemma for this *)
......@@ -446,7 +446,7 @@ Qed.
(** fork *)
Lemma sim_fork e_t e_s Ψ `{!sheapInvConst} :
#() #() [{ Ψ }] -
( π', e_t {π', Ω} e_s [{ lift_post Ω }]) -
( π', e_t {π', Ω} e_s [{ lift_post (Ω π') }]) -
Fork e_t Fork e_s [{ Ψ }].
Proof.
iIntros "Hval Hsim". iApply sim_lift_head_step_both.
......
......@@ -12,7 +12,7 @@ From iris.prelude Require Import options.
Section sim.
Context `{!sheapGS Σ} `{sheapInv Σ}.
Context (Ω : val val iProp Σ) (π : thread_id).
Context (Ω : thread_id val val iProp Σ) (π : thread_id).
Local Notation "et '⪯' es {{ Φ }}" := (et {π, Ω} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
Local Notation "et '⪯' es [{ Φ }]" := (et {π, Ω} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
......
......@@ -11,7 +11,7 @@ Section meta_level_simulation.
Context {PROP : bi}.
Context {Λ : language}.
Context (Ω : val Λ val Λ PROP).
Context (Ω : thread_id val Λ val Λ PROP).
Context {s : simulirisG PROP Λ}.
Context {PROP_bupd : BiBUpd PROP}.
Context {PROP_affine : BiAffine PROP}.
......@@ -24,7 +24,7 @@ Section meta_level_simulation.
(* we pull out the simulation to a meta-level simulation,
the set V tracks which threads are already values in both target and source *)
Definition msim (T_t: tpool Λ) (σ_t: state Λ) (T_s: tpool Λ) (σ_s: state Λ) (V: gset nat) :=
sat (state_interp p_t σ_t p_s σ_s T_s i, i V v_t v_s, T_t !! i = Some (of_val v_t) T_s !! i = Some (of_val v_s) [ list] ie_t; e_s T_t;T_s, gsim_expr Ω (lift_post Ω) i e_t e_s).
sat (state_interp p_t σ_t p_s σ_s T_s i, i V v_t v_s, T_t !! i = Some (of_val v_t) T_s !! i = Some (of_val v_s) [ list] ie_t; e_s T_t;T_s, gsim_expr Ω (lift_post (Ω i)) i e_t e_s).
Lemma msim_length T_t T_s σ_t σ_s V:
msim T_t σ_t T_s σ_s V length T_t = length T_s.
......@@ -79,7 +79,7 @@ Section meta_level_simulation.
v_t v_s,
T_t !! i = Some (of_val v_t)
T_s !! i = Some (of_val v_s)
sat (state_interp p_t σ_t p_s σ_s T_s Ω v_t v_s).
sat (state_interp p_t σ_t p_s σ_s T_s Ω i v_t v_s).
Proof.
intros Hel Hsafe Hsim. rewrite /msim in Hsim. eapply sat_mono in Hsim.
- eapply sat_bupd in Hsim.
......@@ -266,7 +266,7 @@ Section meta_level_simulation.
pool_steps p_s T_s σ_s J T_s' σ_s'
msim T_t' σ_t' T_s' σ_s' U
( i v_t, T_t' !! i = Some (of_val v_t)
v_s, T_s' !! i = Some (of_val v_s) sat (state_interp p_t σ_t' p_s σ_s' T_s' Ω v_t v_s)).
v_s, T_s' !! i = Some (of_val v_s) sat (state_interp p_t σ_t' p_s σ_s' T_s' Ω i v_t v_s)).
Proof.
(* first we exectute the simulation to v_t *)
intros Hsim Hstuck Htgt; eapply msim_steps in Hsim as (T_s' & σ_s' & J1 & Hsrc & Hsim); [|eauto..].
......@@ -304,7 +304,7 @@ End meta_level_simulation.
Section adequacy_statement.
Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
Context {Λ : language}.
Context (Ω : val Λ val Λ PROP).
Context (Ω : thread_id val Λ val Λ PROP).
Context {s : simulirisG PROP Λ}.
Context {sat: PROP Prop} {Sat: Satisfiable sat}.
Arguments sat _%I.
......@@ -320,9 +320,9 @@ Section adequacy_statement.
sat (local_rel Ω p_t p_s
( σ_t σ_s, I σ_t σ_s - state_interp p_t σ_t p_s σ_s [of_call main u])
progs_are p_t p_s
Ω u u)
Ω 0 u u)
(* post *)
( v_t v_s σ_t σ_s T_s, sat (state_interp p_t σ_t p_s σ_s T_s Ω v_t v_s) O v_t v_s)
( π v_t v_s σ_t σ_s T_s, sat (state_interp p_t σ_t p_s σ_s T_s Ω π v_t v_s) O v_t v_s)
B p_t p_s.
Proof.
intros Hpre Hpost σ_t σ_s HI Hsafe.
......@@ -352,7 +352,7 @@ Section adequacy_statement_alt.
Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
Context {Λ : language}.
Context (Ω : val Λ val Λ PROP).
Context (Ω : thread_id val Λ val Λ PROP).
Context {s : simulirisG PROP Λ}.
Context {sat: PROP Prop} {Sat: Satisfiable sat}.
Arguments sat _%I.
......@@ -373,16 +373,16 @@ Section adequacy_statement_alt.
(* The programs are in the state *)
progs_are p_t p_s
(* The "unit" argument to main is related *)
Ω u u
Ω 0 u u
(* Logically related values are observationally related *)
v_s v_t, Ω v_t v_s - O v_t v_s)
π v_s v_t, Ω π v_t v_s - O v_t v_s)
B p_t p_s.
Proof.
intros Hsat. eapply sat_frame_intro in Hsat; last first.
{ iIntros "(H1 & H2 & H3 & H4 & F)". iSplitL "F"; first iExact "F".
iCombine "H1 H2 H3 H4" as "H". iExact "H". }
eapply (@adequacy PROP _ _ _ _ _ _ (sat_frame _) _); first apply Hsat.
intros v_t v_s σ_t σ_s T_s Hsat_post. eapply sat_elim, sat_mono, Hsat_post.
intros π v_t v_s σ_t σ_s T_s Hsat_post. eapply sat_elim, sat_mono, Hsat_post.
iIntros "(H & _ & Hval)". by iApply "H".
Qed.
......
......@@ -25,7 +25,7 @@ Implicit Types
(D: gmap nat nat)
(i j k: nat)
(σ_s σ_t σ : state Λ)
(Ω: val Λ val Λ PROP).
(Ω: thread_id val Λ val Λ PROP).
(* Language Setup *)
Notation "P '.(tgt)'" := (P.*1) (at level 5).
......@@ -184,7 +184,7 @@ Qed.
*)
Definition gsim_expr_all Ω π (P: list (expr Λ * expr Λ)) := ([ list] ip P, gsim_expr Ω (lift_post Ω) (π + i) (fst p) (snd p))%I.
Definition gsim_expr_all Ω π (P: list (expr Λ * expr Λ)) := ([ list] ip P, gsim_expr Ω (lift_post (Ω (π + i))) (π + i) (fst p) (snd p))%I.
Notation must_step_all Ω π := (must_step (gsim_expr_all Ω π)).
......@@ -252,19 +252,19 @@ Proof.
Qed.
Definition gsim_expr_all_wo Ω π P O :=
([ list] k p P, if (decide (k O)) then emp else gsim_expr Ω (lift_post Ω) (π + k) (fst p) (snd p))%I.
([ list] k p P, if (decide (k O)) then emp else gsim_expr Ω (lift_post (Ω (π + k))) (π + k) (fst p) (snd p))%I.
Lemma gsim_expr_all_to_wo Ω P π:
gsim_expr_all Ω π P gsim_expr_all_wo Ω π P .
Proof.
rewrite /gsim_expr_all /gsim_expr_all_wo. f_equiv.
intros k [e_t e_s]. destruct (decide (k )); set_solver.
intros k [e_t e_s]. case_decide; set_solver.
Qed.
Lemma gsim_expr_all_wo_split Ω P O i e_t e_s π:
P !! i = Some (e_t, e_s)
i O
gsim_expr_all_wo Ω π P O (gsim_expr Ω (lift_post Ω) (π + i) e_t e_s gsim_expr_all_wo Ω π P (O {[i]}))%I.
gsim_expr_all_wo Ω π P O (gsim_expr Ω (lift_post (Ω (π + i))) (π + i) e_t e_s gsim_expr_all_wo Ω π P (O {[i]}))%I.
Proof.
intros Hlook Hel. rewrite /gsim_expr_all_wo.
rewrite (big_sepL_delete _ _ i); last done.
......@@ -299,7 +299,7 @@ Proof.
intros Hlt; rewrite /gsim_expr_all_wo /gsim_expr_all.
rewrite big_sepL_app. f_equiv. f_equiv.
intros k [e_t e_s]; simpl.
destruct (decide) as [Hel|]; last done.
case_decide as Hel; last done.
eapply Hlt in Hel.
change (length P1 + k) with (length (P1: list (expr Λ * expr Λ)) + k) in Hel.
lia.
......@@ -318,8 +318,8 @@ Lemma gsim_expr_target_step_unfold Ω T i p_t p_s σ_t σ_s e_t e_s e_t' σ_t' e
prim_step p_t e_t σ_t e_t' σ_t' efs_t
pool_safe p_s T σ_s
state_interp p_t σ_t p_s σ_s T -
gsim_expr Ω (lift_post Ω) i e_t e_s ==
e_s' σ_s' efs_s I, gsim_expr Ω (lift_post Ω) i e_t' e_s' state_interp p_t σ_t' p_s σ_s' (<[i := e_s']> T ++ efs_s)
gsim_expr Ω (lift_post (Ω i)) i e_t e_s ==
e_s' σ_s' efs_s I, gsim_expr Ω (lift_post (Ω i)) i e_t' e_s' state_interp p_t σ_t' p_s σ_s' (<[i := e_s']> T ++ efs_s)
pool_steps p_s T σ_s I (<[i := e_s']> T ++ efs_s) σ_s' length efs_t = length efs_s gsim_expr_all Ω (length T) (zip efs_t efs_s).
Proof.
intros Hlook Hprim Hsafe. iIntros "SI Hsim". rewrite gsim_expr_unfold.
......@@ -355,7 +355,7 @@ Proof.
replace ( {[i]}: gset nat) with ({[i]}: gset nat) by set_solver.
iDestruct "Hall" as "[Hsim Hall]".
rewrite gsim_expr_eq global_greatest_def_unfold.
iApply (global_least_def_strong_ind _ (λ Ψ π e_t e_s, P D, P !! i = Some (e_t, e_s) - i = π⌝ - O threads P.(tgt) - gsim_expr_all_wo Ω 0 P {[i]} - ( e_t e_s, Ψ e_t e_s - lift_post Ω e_t e_s) - must_step_all Ω 0 P O D)%I with "[] Hsim [] [] [] Hall"); eauto.
iApply (global_least_def_strong_ind _ (λ Ψ π e_t e_s, P D, P !! i = Some (e_t, e_s) - i = π⌝ - O threads P.(tgt) - gsim_expr_all_wo Ω 0 P {[i]} - ( e_t e_s, Ψ e_t e_s - lift_post (Ω i) e_t e_s) - must_step_all Ω 0 P O D)%I with "[] Hsim [] [] [] Hall"); eauto.
{ intros n ?? Heq ???. repeat f_equiv. by apply Heq. }
clear P D Hsub e_t e_s Hlook. iModIntro. iIntros (Ψ π e_t e_s) "Hsim".
iIntros (P D Hlook ? Hsub) "Hall Hpost". subst π.
......
......@@ -33,7 +33,7 @@ Section fix_lang.
(** Global simulation relation with stuttering *)
Section sim_def.
Context (val_rel : val Λ val Λ PROP).
Context (val_rel : thread_id val Λ val Λ →<