Library mcertikos.conlib.conmclib.Concurrent_Linking_Additional_Prop
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import Smallstep.
Require Import CommonTactic.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
Require Import AuxStateDataType.
Section WITHORACLE2.
Context `{op: OracleProp (ret:= event) (log := Log) (log_len := list_Len)}.
Definition valid_oracle (A: ZSet) (o: Oracle) :=
∀ l e,
oget A l o = Some e →
A (event_source e) = false
∧ (match l with
| EYIELD i :: l´ ⇒ ∃ j, e = EBACK j
| _ ⇒ True
end).
Lemma valid_oracle_append_o:
∀ A o1 o2 (Hdis: domain_disjoint o1 o2),
valid_oracle A o1 →
valid_oracle A o2 →
valid_oracle A (append_o o1 o2).
Proof.
unfold valid_oracle; intros.
eapply append_o_or in H1; trivial.
destruct H1.
- eauto.
- destruct H1 as (? & ?). eauto.
Qed.
Lemma valid_oracle_empty:
∀ A,
valid_oracle A empty_o.
Proof.
unfold valid_oracle; intros.
rewrite empty_o_empty in H. congruence.
Qed.
Lemma valid_oracle_u_back:
∀ i l j i´,
valid_oracle core_set (uoracle i (EYIELD j :: l) (EBACK i´)).
Proof.
unfold valid_oracle; intros.
eapply uoracle_some_imply in H.
destruct H as (Hcore & Hl0 & He); subst.
simpl. split; eauto 2.
eapply sched_valid; eauto.
Qed.
End WITHORACLE2.
Section ORACLE_REFINES_HARDWARE.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset := hdset)}.
Context `{pmap: PartialMap}.
Inductive match_local: Z → Z → private_state → local_state → Prop :=
| MATCH_LOCAL_NEQ: ∀ curid i ps b
(Hmatch_program_eq: curid = i → b = true)
(Hmatch_program_neq: curid ≠ i → b = false),
match_local curid i ps (LState ps b)
.
Inductive match_state: hstate → state → Prop :=
| MATCH_STATE: ∀ curid l psp lsp
(Hlsp: ∀ i ps,
pget i psp = Some ps →
∃ ls, pget i lsp = Some ls
∧ match_local curid i ps ls),
match_state (HState curid psp l) (State curid lsp l).
Definition hardware_prop (s s´: hstate) (t:trace):=
∀ os
(Hmatch_state: match_state s os),
∃ o os´,
(∀ init_o (Hdis: domain_disjoint o init_o),
valid_oracle core_set init_o →
plus oracle_step (append_o o init_o) os t os´)
∧ match_state s´ os´
∧ valid_oracle core_set o
∧ domain o (RZSet (state_log_len os) (state_log_len os´)).
Lemma one_step_oracle_refines_hardware:
∀ start s s´ t
(Hone: hardware_step start s t s´),
hardware_prop s s´ t.
Proof.
unfold hardware_prop; intros.
inv Hone. inv Hmatch_state.
pose proof Hget_local as Hdomain.
eapply (pget_some lsp) in Hget_local. destruct Hget_local as (ps0 & Hget_local).
destruct (Hlsp _ _ Hget_local) as (ols & Hols & Hmatch_local).
inv Hmatch_local. specialize (Hmatch_program_eq refl_equal).
∃ (uoracle curid (EYIELD curid :: l) (EBACK curid´)).
destruct (Hlsp _ _ Hget_local´) as (ols´ & Hols´ & Hmatch_local).
inv Hmatch_local.
destruct (zeq curid curid´); subst.
{
rewrite Hget_local in Hget_local´.
inv Hget_local´. rewrite Hols in Hols´. inv Hols´.
refine_split´.
{
intros.
eapply plus_two.
{
eapply oracle_exec_step_yield_pos; eauto; try omega.
eapply append_o_left; trivial.
eapply uoracle_eq; eauto.
}
{
eapply oracle_exec_step_progress; eauto.
rewrite pgss; trivial.
}
{ trivial. }
}
{
constructor. intros.
destruct (zeq i curid´); subst.
{
rewrite pgss in *; trivial.
rewrite pgss in H; trivial.
inv H.
refine_split´; trivial.
constructor; eauto.
}
{
rewrite pgso in H; auto.
repeat rewrite pgso; auto.
}
}
{
eapply valid_oracle_u_back.
}
{
simpl. eapply domain_uoracle_append1.
}
}
{
specialize (Hmatch_program_neq0 n).
refine_split´.
{
intros.
eapply plus_two.
{
eapply oracle_exec_step_yield_pos; eauto; try omega.
eapply append_o_left; eauto.
eapply uoracle_eq; eauto.
}
{
eapply oracle_exec_step_progress; eauto. subst.
rewrite pgso; eauto.
}
{ trivial. }
}
{
constructor. intros.
destruct (zeq i curid´); subst.
{
eapply (pget_some_domain lsp) in Hget_local´.
rewrite pgss in *; trivial.
rewrite pgss in H; trivial.
inv H.
refine_split´; trivial.
constructor; eauto.
}
{
rewrite pgso in H; auto.
rewrite pgso; auto.
destruct (zeq i curid); subst.
{
rewrite pgss; trivial. rewrite Hget_local in H. inv H.
refine_split´; trivial.
econstructor; eauto.
}
{
rewrite pgso; auto.
specialize (Hlsp _ _ H).
destruct Hlsp as (ls´ & Hls´ & Hmatch).
refine_split´; eauto.
inv Hmatch. econstructor; eauto.
}
}
}
{
eapply valid_oracle_u_back.
}
{
simpl. eapply domain_uoracle_append1.
}
}
Qed.
End ORACLE_REFINES_HARDWARE.
Section ENV_REFINES_ENV.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset:= hdset)}.
Context `{pmap: PartialMap}.
Variable start_core: Z.
Variable cpuid : Z.
Hypothesis valid_cpuid: core_set cpuid = true.
Hypothesis est_curid_in_core_set: ∀ st, core_set (est_curid core_set st) = true.
Inductive match_estate: estate (A := s_set cpuid) → (estate (A:= core_set)) → Prop :=
| MATCH_ESTATE: ∀ curid l lsp´ lsp,
pget cpuid lsp´ = pget cpuid lsp →
curid = get_curid_from_log start_core l →
lastEvTy l ≠ Some YIELDTY →
match_estate (EState curid lsp´ l) (EState curid lsp l).
Lemma valid_oracle_u_back_single:
∀ i l j i´,
valid_oracle (s_set cpuid) (uoracle i (EYIELD j :: l) (EBACK i´)).
Proof.
unfold valid_oracle; intros.
eapply uoracle_some_imply in H.
destruct H as (Hcore & Hl0 & He); subst.
simpl. split; eauto 2.
assert (core_set sched_id = false).
{ eapply sched_valid; eauto. }
case_eq (s_set cpuid sched_id); intros; subst; auto.
apply s_set_in_imply in H0.
rewrite <- H0 in H.
rewrite valid_cpuid in H; inv H.
Qed.
Lemma domain_uoracle_append_2ev:
∀ l cid z e e´,
domain (uoracle cid (e::l) z) (RZSet (list_Len l) (list_Len (e´::e::l))).
Proof.
intros. eapply domain_weak.
eapply domain_uoracle.
unfold list_Len. simpl.
eapply subset_RZSet.
xomega.
xomega.
Qed.
Lemma domain_uoracle_one:
∀ cid l ev z,
domain (uoracle cid l z) (RZSet (list_Len l) (list_Len (ev :: l))).
Proof.
intros.
assert (list_Len (ev :: l) = list_Len l + 1).
{ unfold list_Len; simpl.
xomega. }
rewrite H.
eapply domain_uoracle.
Qed.
Lemma sched_cpu_neq:
sched_id ≠ cpuid.
Proof.
assert (core_set sched_id = false).
{ eapply sched_valid; eauto. }
case_eq (zeq cpuid sched_id).
- intros; subst.
rewrite valid_cpuid in H.
inv H.
- intros.
auto.
Qed.
Lemma valid_oracle_add:
∀ ev tid i l,
lastEvTy l ≠ Some YIELDTY →
event_source ev ≠ tid →
valid_oracle (s_set tid) (uoracle i l ev).
Proof.
unfold valid_oracle; intros.
eapply uoracle_some_imply in H1.
destruct H1 as (Hcore & Hl0 & He); subst.
simpl. split; eauto 2.
eapply s_set_not_in.
auto.
destruct l0; auto.
simpl in H.
destruct e; auto.
simpl in H; elim H; auto.
Qed.
Lemma domain_disjoint_diff_len:
∀ curid curid´ l ev ev´ ev´´,
domain_disjoint (uoracle curid (ev :: l) (ev´)) (uoracle curid´ l (ev´´)).
Proof.
intros.
unfold domain_disjoint.
unfold domain.
∃ (s_set (list_Len (ev :: l))).
∃ (s_set (list_Len l)).
refine_split.
- intros.
eapply uoracle_neq.
left.
intro contra.
subst.
assert (Hr_contra: s_set (list_Len (ev:: l)) (list_Len (ev::l)) = true) by eapply s_set_in.
rewrite Hr_contra in Hr.
inv Hr.
- intros.
eapply uoracle_neq.
left.
intro contra.
subst.
assert (Hr_contra: s_set (list_Len l) (list_Len l) = true) by eapply s_set_in.
rewrite Hr_contra in Hr.
inv Hr.
- unfold disjoint_set.
intros; split; intros.
+ unfold list_Len in *; simpl.
eapply s_set_in_imply in H.
eapply s_set_not_in.
intro contra.
rewrite <- contra in H.
simpl in H.
xomega.
+ unfold list_Len in *; simpl.
eapply s_set_in_imply in H.
eapply s_set_not_in.
intro contra.
rewrite <- contra in H.
simpl in H.
xomega.
Qed.
Lemma one_step_single_env_refines_full_env:
∀ hw_o (Hvalid: valid_oracle core_set hw_o) curid curid´ lsp lsp0 lsp´ l l´ t
(Hone: env_step hw_o (EState (A:= core_set) curid lsp l) t (EState (A:= core_set) curid´ lsp´ l´))
(Hmatch: match_estate (EState (A := s_set cpuid) curid lsp0 l) (EState (A := core_set) curid lsp l)),
∃ si_o lsp0´,
(∀ init_o,
domain_disjoint si_o init_o →
valid_oracle (s_set cpuid) init_o →
star env_step (append_o si_o init_o) (EState (A := (s_set cpuid)) curid lsp0 l) t
(EState (A:= s_set cpuid) curid´ lsp0´ l´))
∧ match_estate (EState (A:= s_set cpuid) curid´ lsp0´ l´) (EState (A:= core_set) curid´ lsp´ l´)
∧ valid_oracle (s_set cpuid) si_o
∧ domain si_o (RZSet (list_Len l) (list_Len l´)).
Proof.
intros.
inv Hone; inv Hmatch.
- case_eq (zeq (get_curid_from_log start_core l) cpuid); intros.
+ subst.
∃ empty_o.
∃ (pset (get_curid_from_log start_core l) (LState ps´ true) lsp0).
refine_split.
× intros.
eapply star_one.
econstructor; eauto.
rewrite H3; auto.
× constructor.
{ rewrite e.
repeat rewrite pgss; auto.
rewrite e in valid_cpuid; auto.
rewrite s_set_in; auto. }
{ inversion Hlocal; subst; simpl; auto. }
{ inversion Hlocal; subst; simpl; try auto; intro contra; inv contra. }
× eapply valid_oracle_empty.
× eapply domain_empty.
+ assert (Hnone: pget (get_curid_from_log start_core l) lsp0 = None).
{ eapply pget_none.
eapply s_set_not_in; auto. }
inv Hlocal.
× ∃ (uoracle cpuid l (EACQ (get_curid_from_log start_core l) id)).
∃ lsp0.
refine_split; intros.
{ eapply star_one.
eapply env_exec_step_skip; simpl; eauto.
eapply append_o_left; auto.
eapply uoracle_eq.
rewrite s_set_in; auto. }
{ constructor; auto.
rewrite pgso; auto.
simpl; intro contra; inv contra. }
{ eapply valid_oracle_add; auto. }
{ simpl.
eapply domain_uoracle_one. }
× ∃ (uoracle cpuid l (EREL (get_curid_from_log start_core l) id d)).
∃ lsp0.
refine_split; intros.
{ eapply star_one.
eapply env_exec_step_skip; simpl; eauto.
eapply append_o_left; auto.
eapply uoracle_eq.
rewrite s_set_in; auto. }
{ constructor; auto.
rewrite pgso; auto.
simpl; intro contra; inv contra. }
{ eapply valid_oracle_add; auto. }
{ simpl.
eapply domain_uoracle_one. }
× ∃ empty_o.
∃ lsp0.
refine_split; intros.
{ eapply star_refl. }
{ econstructor; eauto.
rewrite pgso; eauto. }
{ eapply valid_oracle_empty. }
{ eapply domain_empty. }
× ∃ (uoracle cpuid l (EATOMIC (get_curid_from_log start_core l) id e)).
∃ lsp0.
refine_split; intros.
{ eapply star_one.
eapply env_exec_step_skip; simpl; eauto.
eapply append_o_left; auto.
eapply uoracle_eq.
rewrite s_set_in; auto. }
{ constructor; auto.
rewrite pgso; auto.
simpl; intro contra; inv contra. }
{ eapply valid_oracle_add; auto. }
{ simpl.
eapply domain_uoracle_one. }
- case_eq (zeq cpuid (get_curid_from_log start_core l)).
+ ∃ (uoracle (get_curid_from_log start_core l)
(EYIELD (get_curid_from_log start_core l) :: l) (EBACK curid´)).
∃ (pset (get_curid_from_log start_core l) (LState ps false) lsp0).
refine_split.
× intros.
eapply star_one.
{ eapply env_exec_step_yield_pos; eauto; try omega.
- rewrite <- e.
rewrite H3.
auto.
rewrite e.
auto.
- eapply append_o_left; trivial.
eapply uoracle_eq; eauto.
rewrite e.
apply s_set_in.
}
× constructor.
{ rewrite <- e.
repeat rewrite pgss; auto.
apply s_set_in. }
{ unfold get_curid_from_log; simpl; auto. }
{ simpl; intro contra; inv contra. }
× constructor.
eapply valid_oracle_u_back_single; eauto.
eapply uoracle_some_imply in H0.
destruct H0 as (? & ? & ?); auto.
subst; simpl.
∃ curid´; auto.
× apply domain_uoracle_append_2ev.
+ ∃ (append_o (uoracle cpuid (EYIELD (get_curid_from_log start_core l) :: l) (EBACK curid´))
((uoracle cpuid l) (EYIELD (get_curid_from_log start_core l)))).
∃ lsp0.
assert (Htwo_disj: domain_disjoint (uoracle cpuid (EYIELD (get_curid_from_log start_core l) :: l)
(EBACK curid´))
(uoracle cpuid l (EYIELD (get_curid_from_log start_core l)))).
{ eapply domain_disjoint_diff_len; eauto. }
assert (Hfirst_o: oget (s_set cpuid) l
(append_o (uoracle cpuid (EYIELD (get_curid_from_log start_core l) :: l)
(EBACK curid´))
(uoracle cpuid l (EYIELD (get_curid_from_log start_core l))))
= Some (EYIELD (get_curid_from_log start_core l))).
{ rewrite append_o_commutativity_disjoint; auto.
eapply append_o_left; auto.
apply domain_disjoint_commutativity; auto.
eapply uoracle_eq.
rewrite s_set_in; auto. }
assert (Hsecond_o: oget (s_set cpuid) (EYIELD (get_curid_from_log start_core l)::l)
(append_o (uoracle cpuid (EYIELD (get_curid_from_log start_core l) :: l)
(EBACK curid´))
(uoracle cpuid l (EYIELD (get_curid_from_log start_core l))))
= Some (EBACK curid´)).
{ eapply append_o_left; auto.
eapply uoracle_eq.
rewrite s_set_in; auto. }
refine_split.
× intros.
eapply star_two.
{ eapply env_exec_step_skip; eauto; try omega.
- eapply pget_none.
apply s_set_not_in; auto.
- eapply append_o_left; trivial.
eauto. }
{ assert (Hback_id: (back_id (get_curid_from_log start_core l)
(EYIELD (get_curid_from_log start_core l))) = sched_id).
{ unfold back_id; auto. }
rewrite Hback_id.
assert (pget sched_id lsp0 = None).
{ generalize sched_cpu_neq; intros.
eapply pget_none.
eapply s_set_not_in.
auto. }
eapply env_exec_step_skip; eauto; try omega.
- eapply append_o_left; trivial. }
{ auto. }
× constructor.
{ rewrite pgso; auto. }
{ simpl; auto. }
{ simpl; intro contra; inv contra. }
× constructor.
{ eapply append_o_or in H0; eauto.
destruct H0.
- eapply uoracle_some_imply in H0; eauto.
destruct H0 as (_ & ? & ?); subst.
simpl.
eapply s_set_not_in.
generalize sched_valid.
intros.
case_eq (zeq cpuid sched_id); intros; auto.
subst.
rewrite valid_cpuid in H0; inv H0.
- destruct H0.
eapply uoracle_some_imply in H1; eauto.
destruct H1 as (_ & ? & ?); subst.
simpl.
eapply s_set_not_in.
auto. }
{ eapply append_o_or in H0; eauto.
destruct H0.
- eapply uoracle_some_imply in H0; eauto.
destruct H0 as (_ & ? & ?); subst.
∃ curid´; auto.
- destruct H0.
eapply uoracle_some_imply in H1; eauto.
destruct H1 as (_ & ? & ?); subst.
destruct l0; auto.
destruct e; simpl in H5; auto.
elim H5; auto. }
× rewrite append_o_commutativity_disjoint; eauto.
eapply domain_trans; eauto.
{ apply domain_disjoint_commutativity; auto. }
{ instantiate (1:= list_Len (EYIELD (get_curid_from_log start_core l) :: l)).
unfold list_Len; simpl.
xomega. }
{ unfold list_Len; simpl.
xomega. }
simpl; eapply domain_uoracle_one.
simpl; eapply domain_uoracle_one.
- assert (Htotal: core_set (get_curid_from_log start_core l) = true).
{ generalize (est_curid_in_core_set (EState (A:= core_set) (get_curid_from_log start_core l) lsp´ l)).
intros; simpl in H; auto. }
eapply pget_none_domain in Hget_local.
rewrite Hget_local in Htotal.
inv Htotal.
Qed.
End ENV_REFINES_ENV.
Section REORDER_REFINES_SPLIT.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{op1: OracleProp (ret:= Log) (log:= Log) (log_len := list_Len) (zset_op:= zset_op)
(hdset := hdset)}.
Context `{hdsem: HardSemantics (hdset:= hdset)}.
Context `{pmap: PartialMap}.
Context `{fair: Fairness}.
Inductive match_ostate: srstate → rstate → Prop :=
| MATCH_OSTATE: ∀ l ps al,
match_ostate (SRState ps l al) (RState ps l).
Lemma CalOwner_valid:
∀ e z l id
(Hvalid_s : s_set z (event_source e) = false)
(Hcal: CalOwner (e :: l) id = OWN z),
CalOwner l id = OWN z.
Proof.
intros. simpl in Hcal. destruct e; trivial.
- destruct (zeq id id0); subst; trivial.
destruct (CalOwner l id0); trivial.
inv Hcal. simpl in Hvalid_s.
rewrite s_set_in in Hvalid_s. inv Hvalid_s.
- destruct (zeq id id0); subst; trivial.
destruct (CalOwner l id0); trivial.
destruct (zeq i from); subst; trivial. inv Hcal.
Qed.
Lemma AbsYieldBack_CalOwner:
∀ n tid l al o l´ id
(Hback: AbsYieldBack n tid l al o = Some l´)
(Hcal1: CalOwner (l´ ++ l) id = OWN tid)
(Hvalid: valid_oracle (s_set tid) o),
CalOwner (al ++ l) id = OWN tid.
Proof.
induction n; intros; try (inv Hback; fail).
simpl in Hback. pose proof Hvalid as Hvalid´. unfold valid_oracle in Hvalid.
destruct (oget (s_set tid) (al ++ l) o) eqn:Hget; contra_inv.
specialize (Hvalid _ _ Hget).
destruct Hvalid as (Hvalid_s & Hvalid_e).
destruct (back_id_option e) eqn: Hid; contra_inv.
- destruct (zeq tid z); subst.
+ inv Hback. rewrite <- app_comm_cons in Hcal1.
eapply CalOwner_valid; eauto.
+ exploit IHn; eauto. intros Hcal2.
rewrite <- app_comm_cons in Hcal2.
eapply CalOwner_valid; eauto.
- exploit IHn; eauto. intros Hcal2.
rewrite <- app_comm_cons in Hcal2.
eapply CalOwner_valid; eauto.
Qed.
Definition valid_option_oracle_source (l: Log) (tid: Z) :=
∀ e (Hin: In e l),
log_event_source e ≠ Some tid.
Definition valid_option_oracle (tid: Z) (o: Oracle) :=
∀ l (rl: Log),
oget (s_set tid) l o = Some rl →
valid_option_oracle_source rl tid.
Lemma valid_option_oracle_empty:
∀ tid,
valid_option_oracle tid empty_o.
Proof.
unfold valid_option_oracle; intros.
rewrite empty_o_empty in H. congruence.
Qed.
Lemma valid_option_oracle_u:
∀ tid l l´
(Hsource: valid_option_oracle_source l´ tid),
valid_option_oracle tid (uoracle tid l l´).
Proof.
intros.
unfold valid_option_oracle; intros.
eapply uoracle_some_imply in H.
destruct H as (Hset & ? & ?); subst. trivial.
Qed.
Lemma valid_option_oracle_u_source_split:
∀ tid l1 l2
(Hvalid1: valid_option_oracle_source l1 tid)
(Hvalid2: valid_option_oracle_source l2 tid),
valid_option_oracle_source (l1 ++ l2) tid.
Proof.
unfold valid_option_oracle_source. intros.
eapply in_app_or in Hin.
destruct Hin as [Hin´|Hin´].
- eapply Hvalid1; eauto.
- eapply Hvalid2; eauto.
Qed.
Lemma valid_option_oracle_u_source_append:
∀ tid e l
(Hvalid1: log_event_source e ≠ Some tid)
(Hvalid2: valid_option_oracle_source l tid),
valid_option_oracle_source (e::l) tid.
Proof.
unfold valid_option_oracle_source. intros.
inv Hin; eauto.
Qed.
Lemma AbsYieldBack_valid_option_oracle:
∀ n tid l l´ al o
(Hback: AbsYieldBack n tid l al o = Some l´)
(hvalid_al: valid_option_oracle_source al tid)
(Hvalid: valid_oracle (s_set tid) o),
valid_option_oracle_source l´ tid.
Proof.
induction n; intros; try (inv Hback; fail).
simpl in Hback. pose proof Hvalid as Hvalid´. unfold valid_oracle in Hvalid.
destruct (oget (s_set tid) (al ++ l) o) eqn:Hget; contra_inv.
specialize (Hvalid _ _ Hget).
destruct Hvalid as (Hvalid_s & Hvalid_e).
destruct (back_id_option e) eqn: Hid; contra_inv.
- destruct (zeq tid z); subst.
+ inv Hback. eapply valid_option_oracle_u_source_append; eauto.
destruct e; inv Hid; simpl. congruence.
+ eapply IHn; eauto.
eapply valid_option_oracle_u_source_append; eauto.
destruct e; inv Hid; simpl. congruence.
- eapply IHn; eauto.
eapply valid_option_oracle_u_source_append; eauto.
eapply s_set_not_in_imply in Hvalid_s.
destruct e; simpl in Hvalid_s; inv Hid; simpl; try congruence.
Qed.
Lemma valid_option_oracle_source_nil:
∀ tid,
valid_option_oracle_source nil tid.
Proof.
unfold valid_option_oracle_source. intros. inv Hin.
Qed.
Definition srstate_log_len (s: srstate) :=
match s with
| SRState _ l al ⇒ list_Len l
end.
Lemma domain_uoracle_append2:
∀ l l´ l´´ l´´´ cid z e,
domain (uoracle cid l z) (RZSet (list_Len l) (list_Len (l´´´ ++ l´´ ++ e :: l´ ++ l))).
Proof.
intros. eapply domain_weak.
eapply domain_uoracle.
unfold list_Len. simpl.
eapply subset_RZSet.
repeat (erewrite app_length; simpl). simpl. xomega.
repeat (erewrite app_length; simpl). simpl. xomega.
Qed.
Lemma one_step_reorder_refines_split:
∀ tid o (Hvalid: valid_oracle (s_set tid) o) ps l al ps´ l´ al´ s0 t
(Hone: single_split_step tid o (SRState ps l al) t (SRState ps´ l´ al´))
(Hcal: ∀ id, CalOwner (al ++ l) id = OWN tid → CalOwner l id = OWN tid)
(Hmatch: match_ostate (SRState ps l al) s0)
(Hvalid1: valid_option_oracle_source al tid),
∃ o´ s0´,
(∀ init_o,
domain_disjoint o´ init_o →
valid_option_oracle tid init_o →
plus (single_reorder_step tid) (append_o o´ init_o) s0 t s0´)
∧ match_ostate (SRState ps´ l´ al´) s0´
∧ (∀ id, CalOwner (al´ ++ l´) id = OWN tid → CalOwner l´ id = OWN tid)
∧ valid_option_oracle tid o´
∧ valid_option_oracle_source al´ tid
∧ domain o´ (RZSet (list_Len l) (list_Len l´)).
Proof.
intros. inv Hmatch. inv Hone.
-
assert (Hcal´: ∀ id,
CalOwner (l2 ++ (EYIELD tid :: al) ++ l´) id = OWN tid
→ CalOwner l´ id = OWN tid).
{
intros. eapply Hcal.
eapply AbsYieldBack_CalOwner in Hl1; simpl in *; eauto.
}
∃ empty_o.
refine_split´; trivial.
+ intros. eapply plus_one.
eapply single_exec_step_progress_reorder_local; eauto.
+ econstructor.
+ rewrite <- app_assoc. trivial.
+ eapply valid_option_oracle_empty; eauto.
+ eapply valid_option_oracle_u_source_split.
× eapply AbsYieldBack_valid_option_oracle; eauto.
eapply valid_option_oracle_source_nil.
× eapply valid_option_oracle_u_source_append; eauto.
simpl. congruence.
+ eapply domain_empty; eauto.
-
∃ (uoracle tid l (l2 ++ EYIELD tid :: al)).
refine_split´; trivial.
+ intros. eapply plus_one.
eapply single_exec_step_progress_reorder_log; eauto.
× eapply append_o_left; eauto.
eapply uoracle_eq.
eapply s_set_in.
× rewrite <- app_assoc.
rewrite <- app_comm_cons.
eapply Hlocal.
+ rewrite <- app_assoc.
rewrite <- app_comm_cons.
econstructor.
+ eapply valid_option_oracle_u.
eapply valid_option_oracle_u_source_split.
× eapply AbsYieldBack_valid_option_oracle; eauto.
eapply valid_option_oracle_source_nil.
× eapply valid_option_oracle_u_source_append; eauto.
simpl. congruence.
+ eapply valid_option_oracle_source_nil.
+ eapply domain_uoracle_append2; eauto.
Qed.
End REORDER_REFINES_SPLIT.
Section SEPARATE_REFINES_REORDER.
Context `{op: OracleProp (ret:= Log) (log:= Log) (log_len := list_Len)}.
Context `{op1: OracleProp (ret:= separate_log_type)
(log:= Z × separate_log_type × ident)
(zset_op := zset_op) (hdset := hdset)}.
Context `{hdsem: HardSemantics (hdset := hdset)}.
Context `{pmap: PartialMap}.
Context `{fair: Fairness}.
Definition Oracle0 := Oracle (OracleProp := op).
Definition Oracle1 := Oracle (OracleProp := op1).
Fixpoint remove_cache_event (l: Log) (tid: Z) :=
match l with
| nil ⇒ nil
| e :: l´ ⇒
if zeq tid (event_source e) then l
else remove_cache_event l´ tid
end.
Inductive match_logs: Z → separate_log → Log → Prop :=
| MATCH_LOG: ∀ tid gl sl
(Hatomic: ∀ id l0 l1,
ZMap.get id gl = l0 →
log_get_atomic sl id = l1 →
separate_log_type_2_log l0 id = (remove_cache_event l1 tid)),
match_logs tid gl sl.
Inductive match_spstate: Z → sp_state → rstate → Prop :=
| MATCH_SPSTATE: ∀ tid gl sl ps
(Hlog: match_logs tid gl sl),
match_spstate tid (SPState ps gl) (RState ps sl).
Definition match_oracle_separate (tid: Z) (o1: Oracle1) (o0: Oracle0):=
∀ id e A sl sl´ gl l l0
(Hget0: oget A sl o0 = Some sl´)
(Hlog: match_logs tid gl sl)
(Hl: ZMap.get id gl = l)
(Hsl: log_get_atomic (sl´ ++ sl) id = l0),
∃ l´,
oget A (id, l, e) o1 = Some l´
∧ separate_log_type_2_log (l´ ++ l) id = l0.
Lemma CalOwner_atomic_log:
∀ l id,
CalOwner (log_get_atomic (l) id) id = CalOwner l id.
Proof.
induction l; simpl; intros; trivial.
destruct a; eauto; simpl.
- destruct (zeq id id0); subst; eauto.
simpl. rewrite zeq_true. erewrite IHl; eauto.
- destruct (zeq id id0); subst; eauto.
simpl. rewrite zeq_true. erewrite IHl; eauto.
- destruct (zeq id id0); subst; eauto.
Qed.
Lemma log_get_atomic_simpl:
∀ l id,
log_get_atomic (log_get_atomic l id) id = log_get_atomic l id.
Proof.
induction l; simpl; intros; trivial.
destruct a; simpl; eauto.
- destruct (zeq id id0); subst; eauto.
simpl. rewrite zeq_true. erewrite IHl; eauto.
- destruct (zeq id id0); subst; eauto.
simpl. rewrite zeq_true. erewrite IHl; eauto.
- destruct (zeq id id0); subst; eauto.
simpl. rewrite zeq_true. erewrite IHl; eauto.
Qed.
Lemma remove_cache_gss:
∀ l´ l id tid
(Horacle: ∀ e, In e l´ → event_source e ≠ tid),
remove_cache_event (log_get_atomic (l´ ++ l) id) tid
= remove_cache_event (log_get_atomic l id) tid.
Proof.
induction l´; trivial; simpl; intros.
destruct a; eauto; destruct (zeq id id0); subst;
eauto; simpl; rewrite zeq_false; eauto;
intro HF; subst; exploit Horacle; eauto.
Qed.
Lemma match_logs_gss:
∀ gl l´ sl sl´ tid id e1 e2
(He: separate_event_2_event e1 id = e2)
(Hsource: event_source e2 = tid)
(Hmatch: match_logs tid gl sl)
(Hsep: separate_log_type_2_log (l´ ++ ZMap.get id gl) id
= (log_get_atomic (sl´ ++ sl) id))
(Horacle: ∀ e, In e sl´ → event_source e ≠ tid),
match_logs tid (ZMap.set id (e1 :: l´ ++ ZMap.get id gl) gl)
(e2 :: sl´ ++ sl).
Proof.
intros. econstructor; intros. subst.
destruct (zeq id id0); subst.
- set (separate_event_2_event e1 id0) as e2 in ×.
assert (Heq: remove_cache_event (log_get_atomic (e2 :: sl´ ++ sl) id0)
(event_source e2)
= e2 :: log_get_atomic (sl´ ++ sl) id0).
{
destruct e1; subst; repeat (simpl; rewrite zeq_true); trivial.
}
rewrite Heq.
rewrite ZMap.gss.
simpl. subrewrite´.
- set (separate_event_2_event e1 id) as e2 in ×.
rewrite ZMap.gso; auto. inv Hmatch.
exploit (Hatomic id0); eauto. intros HP.
assert (Heq: log_get_atomic (e2 :: sl´ ++ sl) id0 = log_get_atomic (sl´ ++ sl) id0).
{
destruct e1; subst e2; simpl; rewrite zeq_false; auto.
}
rewrite Heq.
rewrite remove_cache_gss; eauto.
Qed.
Definition valid_oracle´ (tid: Z) (o: Oracle0) :=
∀ l l´,
oget (s_set tid) l o = Some l´ →
(∀ e, In e l´ → event_source e ≠ tid).
Lemma one_step_separate_refines_reorder:
∀ tid o1 o2 s s0 s´ t
(Hone: single_reorder_step (op := op) tid o1 s t s´)
(Hmatch: match_spstate tid s0 s)
(Horacle: match_oracle_separate tid o2 o1)
(Hvalid: valid_oracle´ tid o1),
∃ s0´,
plus (single_separate_step (op := op1) tid) o2 s0 t s0´
∧ match_spstate tid s0´ s´.
Proof.
intros. inv Hone; inv Hmatch.
-
refine_split´; trivial.
+
eapply plus_one. constructor; eauto.
+ econstructor. trivial.
-
inv Hlocal.
+ exploit (Horacle id); eauto.
intros (l´ & Hget & Hma).
refine_split´; trivial.
×
eapply plus_one.
eapply single_exec_step_progress_separate_log; eauto.
eapply separate_local_exec_step_acq; eauto.
erewrite CalOwner_atomic_log; eauto.
× simpl. econstructor. simpl.
eapply match_logs_gss; eauto; try constructor.
+ exploit (Horacle id); eauto.
intros (l´ & Hget & Hma).
refine_split´; trivial.
×
eapply plus_one.
eapply single_exec_step_progress_separate_log; eauto.
eapply separate_local_exec_step_rel; eauto.
erewrite CalOwner_atomic_log; eauto.
× simpl. econstructor. simpl.
eapply match_logs_gss; eauto; try constructor.
+ exploit (Horacle id); eauto.
intros (l´ & Hget & Hma).
refine_split´; trivial.
×
eapply plus_one.
eapply single_exec_step_progress_separate_log; eauto.
eapply separate_local_exec_step_atomic; eauto.
eapply atomic_step_valid; eauto.
erewrite log_get_atomic_simpl. trivial.
× simpl. econstructor. simpl.
eapply match_logs_gss; eauto; try constructor.
Qed.
End SEPARATE_REFINES_REORDER.