Library mcertikos.conlib.conmclib.Concurrent_Linking_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.
Section ORACLE_REFINES_HARDWARE.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset := hdset)}.
Context `{pmap: PartialMap}.
Variable cpuid : Z.
Variable hw_o : Oracle (OracleProp := op).
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: state → hstate → Prop :=
| MATCH_STATE: ∀ curid l psp lsp
(Hlsp: ∀ i ps ls,
core_set i = true →
pget i psp = Some ps →
pget i lsp = Some ls →
match_local curid i ps ls),
lastEvTy l ≠ Some YIELDTY →
core_set curid = true →
valid_log cpuid l →
curid = get_curid_from_log cpuid l →
match_state (State curid lsp l) (HState curid psp l).
Hypothesis valid_cpuid: core_set cpuid = true.
Hypothesis valid_oracle_def: valid_oracle cpuid core_set hw_o.
Hypothesis relate_hw_step_hw_oracle:
∀ l curid lsp psp,
match_state (State curid lsp l) (HState curid psp l) →
∃ ev,
oget (OracleProp := op) core_set (EYIELD curid :: l) hw_o = Some ev ∧
∀ curid´´,
ev = EBACK curid´´ →
∀ curid´ ps st,
hardware_local_step curid´ (LView ps (EBACK curid´ :: EYIELD curid :: l)) st →
curid´ = curid´´.
Lemma one_step_hw_refines_oracle:
∀ s s´ t os
(Hone: hardware_step cpuid s t s´)
(Hmatch_state: match_state os s),
∃ os´,
plus oracle_step hw_o os t os´
∧ match_state os´ s´.
Proof.
intros.
inv Hone.
pose proof Hmatch_state as Hmatch_state´.
inv Hmatch_state.
assert (∃ ps_p, pget (get_curid_from_log cpuid l) lsp = Some ps_p).
{ eapply pget_some; eauto. }
destruct H as (ps_p & Hget_low).
assert (∃ ps_h, pget (get_curid_from_log cpuid l) lsp0 = Some ps_h).
{ eapply pget_some; eauto. }
destruct H as (ps_h´ & Hget_high).
destruct ps_h´.
assert (ps_p = p ∧ b = true).
{ exploit Hlsp; eauto.
intros.
inv H.
exploit Hmatch_program_eq; eauto. }
destruct H; subst.
assert (valid_log cpuid (EYIELD (get_curid_from_log cpuid l)::l)).
{ constructor; eauto.
simpl; refine_split; auto. }
exploit (relate_hw_step_hw_oracle l); eauto.
intros Ho_cond.
destruct Ho_cond as (ev & Ho1 & Ho2).
assert (∃ curid´´, ev = EBACK curid´´ ∧ core_set curid´´ = true).
{ unfold valid_oracle in valid_oracle_def.
eapply valid_oracle_def in Ho1; eauto.
destruct Ho1 as (_ & Ho1).
inv Ho1.
simpl in H8.
destruct ev; try (inv H8; fail).
destruct H8 as (H8 & _); elim H8; auto.
destruct H8.
∃ to; auto. }
destruct H0 as (curid´´ & Ha & Hb); subst.
exploit (Ho2 curid´´); eauto.
intros; subst.
assert (∃ ps´, pget curid´´ (pset (get_curid_from_log cpuid l) (LState p false) lsp0) = Some ps´).
{ case_eq (zeq curid´´ (get_curid_from_log cpuid l)); intros; subst.
- rewrite pgss; auto.
eexists; eauto.
- rewrite pgso; auto.
eapply pget_some; eauto. }
destruct H0 as (ps´´ & H0).
destruct ps´´.
assert (p0 = ps ∧ b = false).
{ case_eq (zeq curid´´ (get_curid_from_log cpuid l)); intros; subst.
- rewrite pgss in H0; auto.
inv H0.
rewrite Hget_local´ in Hget_low; auto.
inv Hget_low; auto.
- rewrite pgso in H0; auto.
exploit (Hlsp curid´´); eauto.
intros.
inv H3.
exploit Hmatch_program_neq; eauto. }
destruct H1; subst.
∃ (State curid´´ (pset curid´´ (LState ps´ true) (pset (get_curid_from_log cpuid l) (LState p false) lsp0))
(l´ ++ EBACK curid´´ :: EYIELD (get_curid_from_log cpuid l) :: l)).
split.
- eapply plus_two.
+ eapply oracle_exec_step_yield_pos; eauto.
+ eapply oracle_exec_step_progress; eauto.
+ auto.
- constructor; simpl; auto.
+ intros.
destruct ls.
assert (ps0 = p0).
{ case_eq (zeq i curid´´); intros; subst.
× rewrite pgss in H3; auto.
rewrite pgss in H6; auto.
inv H3; inv H6; auto.
× rewrite pgso in H3.
rewrite pgso in H6.
case_eq (zeq i (get_curid_from_log cpuid l)); intros; subst.
{ rewrite pgss in H6; auto.
rewrite Hget_low in H3.
inv H3; inv H6; auto. }
{ rewrite pgso in H6; auto.
exploit (Hlsp i); eauto.
intros.
inv H9; auto. }
auto.
auto. }
subst.
constructor.
intros; subst.
× rewrite pgss in H6; auto.
inv H6; auto.
× intros.
rewrite pgso in H6; auto.
case_eq (zeq (get_curid_from_log cpuid l) i); intros; subst.
{ rewrite pgss in H6; auto.
inv H6; auto. }
{ rewrite pgso in H3; auto.
rewrite pgso in H6; auto.
exploit (Hlsp i); eauto.
intros.
inv H9.
eapply Hmatch_program_neq; auto. }
+ inv Hlocal; simpl; auto; intro contra; inv contra.
+ assert (valid_log cpuid (EBACK curid´´ :: EYIELD (get_curid_from_log cpuid l) :: l)).
{ econstructor; simpl; eauto. }
inv Hlocal; simpl in *; auto.
× econstructor; eauto.
simpl; eauto.
× econstructor; eauto.
simpl; eauto.
× econstructor; eauto.
simpl; eauto.
+ inv Hlocal; simpl; auto.
Qed.
Lemma match_state_implies_one_step:
∀ curid lsp l curid´ hsp l´,
match_state (State curid lsp l) (HState curid´ hsp l´) →
∃ curid´´ lsp´ l´, star oracle_step hw_o (State curid lsp l) E0 (State curid´´ lsp´ l´) ∧
l´ = (EBACK curid´´)::(EYIELD curid)::l ∧
(∀ ps, pget curid lsp = Some (LState ps true) →
lsp´ = pset curid (LState ps false) lsp).
Proof.
intros.
assert (l´ = l) by (inv H; auto); subst.
assert (curid´ = curid) by (inv H; auto); subst.
assert (lastEvTy l ≠ Some YIELDTY) by (inv H; auto).
assert (core_set curid = true) by (inv H; eauto).
assert (valid_log cpuid (EYIELD (get_curid_from_log cpuid l)::l)).
{ inv H.
constructor; eauto.
simpl; refine_split; auto. }
assert (core_set (get_curid_from_log cpuid l) = true).
{ inv H; subst; auto. }
exploit (relate_hw_step_hw_oracle l); eauto; eauto.
intros.
destruct H4 as (ev & H4).
destruct H4 as (H4 & _).
assert (∃ ps, pget curid lsp = Some ps).
{ inv H; eapply pget_some; eauto. }
assert (∃ ps´, pget curid hsp = Some ps´).
{ inv H; eapply pget_some; eauto. }
destruct H5 as (ps & H5).
destruct H6 as (ps´ & H6).
destruct ps.
assert (p = ps´ ∧ b = true).
{ inv H.
exploit Hlsp; eauto.
intros; inv H.
exploit Hmatch_program_eq; eauto. }
destruct H7.
subst; rename ps´ into p.
assert (∃ curid´´, ev = EBACK curid´´).
{ unfold valid_oracle in valid_oracle_def.
assert (curid = get_curid_from_log cpuid l).
{ inv H; auto. }
rewrite <- H7 in H2.
generalize (valid_oracle_def (EYIELD curid :: l) ev H2 H4).
intros; simpl in ×.
destruct H8 as (H7a & H7b).
inv H7b.
simpl in H12.
destruct ev; try (inv H13; fail); [destruct H13 as (H13 & _); elim H13; auto |].
∃ to; auto. }
destruct H7 as (curid´´ & H7); subst.
∃ curid´´.
∃ (pset curid (LState p false) lsp).
∃ (EBACK curid´´ :: EYIELD curid :: l).
split.
- eapply star_one.
eapply oracle_exec_step_yield_pos; eauto.
- split; auto.
intros; auto.
rewrite H7 in H5; inv H5; auto.
Qed.
End ORACLE_REFINES_HARDWARE.
Section ENV_REFINES_ORACLE.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset := hdset)}.
Context `{pmap: PartialMap}.
Variable cpuid : Z.
Variable oracle: Oracle (OracleProp := op).
Hypothesis valid_oracle_def: valid_oracle cpuid core_set oracle.
Inductive match_estate: (estate (A:= core_set)) → state → Prop :=
| MATCH_ESTATE: ∀ curid l lsp,
core_set curid = true →
valid_log cpuid l →
lastEvTy l ≠ Some YIELDTY →
curid = get_curid_from_log cpuid l →
(∀ ps b tid, tid ≠ curid → pget tid lsp = Some (LState ps b) → b = false) →
(∀ ps b, pget curid lsp = Some (LState ps b) → b = false → ∃ e l´, l = e::l´ ∧ e = EBACK curid) →
match_estate (EState curid lsp l) (State curid lsp l).
Lemma one_step_env_refines_oracle:
∀ s s´ os t
(Hone: env_step oracle s t s´)
(Hmatch_state: match_estate s os),
∃ os´,
plus oracle_step oracle os t os´ ∧
match_estate s´ os´.
Proof.
intros.
inv Hmatch_state.
inv Hone.
- refine_split´.
+ eapply plus_one.
eapply oracle_exec_step_progress; eauto.
+ econstructor; auto.
× pose proof Hget_local as Hget_local´.
eapply H4 in Hget_local´; eauto.
destruct Hget_local´ as (e & l´´ & Htemp1 & Htemp2).
revert Htemp2; subst.
intros.
rewrite Htemp2.
remember (get_curid_from_log cpuid (e :: l´´)) as z.
clear Heqz; subst.
assert (core_set cpuid = true).
{ inv H0; auto. }
inv Hlocal; simpl; auto.
{ econstructor; eauto.
simpl; split; auto. }
{ econstructor; eauto.
simpl; split; auto. }
{ econstructor; eauto.
simpl; split; auto. }
× inv Hlocal; simpl; intro contra; inv contra.
elim H1; auto.
× inv Hlocal; simpl; auto.
× intros.
rewrite pgso in H5; auto.
eapply H3; eauto.
× intros.
rewrite pgss in H2; auto; simpl.
inv H2.
inv H8.
- refine_split´.
+ eapply plus_one.
eapply oracle_exec_step_yield_pos; eauto.
+ assert (core_set cpuid = true).
{ inv H0; auto. }
assert (valid_log cpuid (EYIELD (get_curid_from_log cpuid l) :: l)).
{ econstructor; eauto; simpl; auto. }
assert (valid_log cpuid (EBACK curid´ :: EYIELD (get_curid_from_log cpuid l) :: l)).
{ unfold valid_oracle in valid_oracle_def.
pose proof H0 as H0´.
eapply valid_oracle_def in Horacle; eauto.
destruct Horacle.
auto. }
assert (core_set curid´ = true).
{ inv H6.
simpl in H12; destruct H12; auto. }
econstructor; eauto.
× simpl.
intros contra; inv contra.
× intros.
case_eq (zeq tid (get_curid_from_log cpuid l)); intros; subst.
{ rewrite pgss in H9; auto; inv H9; auto. }
{ rewrite pgso in H9; auto.
eapply H3; eauto. }
- eapply pget_none_domain in Hget_local.
rewrite Hget_local in H.
inv H.
Qed.
End ENV_REFINES_ORACLE.
Section ENV_REFINES_ENV.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset := hdset)}.
Context `{pmap: PartialMap}.
Variable hw_oracle : Oracle (OracleProp := op).
Variable si_oracle : Oracle (OracleProp := op).
Variable cpuid : Z.
Inductive match_eestate: estate (A := s_set cpuid) → (estate (A:= core_set)) → Prop :=
| MATCH_EESTATE_S: ∀ curid l lsp´ lsp,
measure l = S O →
core_set curid = true →
valid_log cpuid l →
curid = get_curid_from_log cpuid l →
pget cpuid lsp´ = pget cpuid lsp →
(curid = cpuid →
∀ ps b, pget cpuid lsp = Some (LState ps b) → b = false → ∃ e l´, l = e::l´ ∧ e = EBACK curid) →
(∀ tid, tid ≠ curid → ∀ ps b, pget tid lsp = Some (LState ps b) → b = false) →
(curid ≠ cpuid → lastEvTy l = Some EBACKTY →
∀ ps b, pget curid lsp = Some (LState ps b) → b = false) →
(curid ≠ cpuid → lastEvTy l ≠ Some EBACKTY →
∀ ps b, pget curid lsp = Some (LState ps b) → b = true) →
match_eestate (EState curid lsp´ l) (EState curid lsp l)
| MATCH_EESTATE_O: ∀ curid curid´ l l´ lsp´ lsp,
measure l´ = O →
core_set (get_curid_from_log cpuid l) = true →
valid_log cpuid l´ →
l´ = (EYIELD curid)::l →
curid´ = sched_id →
curid = get_curid_from_log cpuid l →
pget cpuid lsp´ = pget cpuid lsp →
pget (get_curid_from_log cpuid l) lsp´ = None →
oget (hdset := hdset) (OracleProp := op) (s_set cpuid) l si_oracle = Some (EYIELD curid) →
(∀ tid, tid ≠ curid → ∀ ps b, pget tid lsp = Some (LState ps b) → b = false) →
(curid ≠ cpuid → ∀ ps b, pget curid lsp = Some (LState ps b) → b = false → lastEvTy l = Some EBACKTY) →
match_eestate (EState curid´ lsp´ l´) (EState curid lsp l).
Definition local_step_ev (ev : event) : option Log :=
match ev with
| EACQ _ _ ⇒ Some (ev::nil)
| EREL _ _ _ ⇒ Some (ev::nil)
| EATOMIC _ _ _ ⇒ Some (ev::nil)
| EYIELD _ ⇒ Some nil
| _ ⇒ None
end.
Hypothesis valid_cpuid: core_set cpuid = true.
Hypothesis valid_oracle_cond: valid_oracle cpuid (s_set cpuid) si_oracle.
Hypothesis relate_single_oracle_hw_oracle_def:
∀ l ev, valid_log cpuid l →
lastEvTy l = Some YIELDTY →
oget (hdset := hdset) (OracleProp := op) (s_set cpuid) l si_oracle = Some ev →
oget (hdset := hdset) (OracleProp := op) core_set l hw_oracle = Some ev.
Hypothesis relate_single_oracle_concrete_step_def:
∀ curid´ curid lsp´ lsp l´ l l_res ps ev,
match_eestate (EState curid´ lsp´ l´) (EState curid lsp l) →
get_curid_from_log cpuid l ≠ cpuid →
pget (get_curid_from_log cpuid l) lsp = Some (LState ps false) →
oget (hdset := hdset) (OracleProp := op) (s_set cpuid) l si_oracle = Some ev →
local_step_ev ev = Some l_res →
lastEvTy l = Some EBACKTY →
∃ ps´ : private_state,
hardware_local_step (get_curid_from_log cpuid l) (LView ps l) (LView ps´ l_res).
Lemma measure_s_implies_non_yield :
∀ l, measure l = S O → lastEvTy l≠ Some YIELDTY.
Proof.
intros.
unfold measure in H.
destruct l.
- intro contra.
simpl in contra.
inv contra.
- simpl in H.
destruct e; simpl in *; try (intro contra; inv contra).
inv H.
Qed.
Lemma measure_o_implies_last_yield_ev:
∀ l, measure l = O → ∃ curid ev l´, l = ev::l´ ∧ ev = EYIELD curid.
Proof.
intros.
unfold measure in H.
destruct l.
- simpl in H; inv H.
- simpl in H.
destruct e; try inv H.
∃ from, (EYIELD from), l.
tauto.
Qed.
Lemma oget_valid_yield:
∀ curid´ l e,
valid_log cpuid (EYIELD curid´ :: l) →
oget (s_set cpuid) (EYIELD curid´ :: l) si_oracle = Some e →
∃ curid´´, e = EBACK curid´´.
Proof.
intros.
unfold valid_oracle in valid_oracle_cond.
eapply valid_oracle_cond in H; eauto.
destruct H.
inv H1; eauto.
simpl in H7.
destruct e; simpl; try (inv H7; fail).
- destruct H7; elim H1; auto.
- esplit; eauto.
Qed.
Lemma oget_valid_noback:
∀ l to,
valid_log cpuid l →
oget (s_set cpuid) l si_oracle = Some (EBACK to) →
measure l = 1%nat →
False.
Proof.
intros.
unfold valid_oracle in valid_oracle_cond.
eapply valid_oracle_cond in H0; eauto.
destruct H0.
unfold measure in H1.
destruct l.
- inv H2.
simpl in H8.
destruct H8.
inv H2.
- inv H2.
simpl in H8.
destruct H8.
destruct e; simpl in *; try (inv H2; auto; fail).
inv H1.
Qed.
Lemma oracle_result_valid_log:
∀ l ev,
valid_log cpuid l →
oget (hdset := hdset) (OracleProp := op) (s_set cpuid) l si_oracle = Some ev →
valid_log cpuid (ev::l).
Proof.
intros.
unfold valid_oracle in valid_oracle_cond.
eapply valid_oracle_cond in H0; eauto; destruct H0; auto.
Qed.
Theorem single_env_step_refines_full_env_step:
∀ st t st´ st0
(Hone: env_step (A := s_set cpuid) si_oracle st t st´)
(Hmatch: match_eestate st st0),
(∃ st0´,
(plus (env_step (A := core_set))) hw_oracle st0 t st0´ ∧
match_eestate st´ st0´) ∨
((state_measure (s_set cpuid) st´ < state_measure (s_set cpuid) st)%nat ∧ t = E0 ∧
match_eestate st´ st0).
Proof.
intros.
inv Hone.
-
inv Hmatch.
+
assert ((get_curid_from_log cpuid l) = cpuid).
{ eapply pget_some_domain in Hget_local.
eapply s_set_in_imply in Hget_local; auto. }
assert (pget cpuid lsp0 = Some (LState ps false)).
{ rewrite <- H6.
rewrite <- Hget_local.
rewrite H.
auto. }
rewrite H.
revert H; subst; intros.
left.
∃ (EState (get_curid_from_log cpuid l)
(pset (get_curid_from_log cpuid l) (LState ps´ true) lsp0) (l´ ++ l)).
split.
× eapply plus_one.
rewrite H.
eapply env_exec_step_progress; eauto.
rewrite H in Hlocal; auto.
× rewrite H.
rewrite H in ×.
eapply MATCH_EESTATE_S.
{ inversion Hlocal; revert H; subst; intros; try (unfold measure; simpl; auto). }
{ auto. }
{ pose proof Hget_local as HEBACK.
rewrite <- H6 in H7.
eapply H7 in Hget_local; eauto.
destruct Hget_local as (ev & l´´ & Hget_locala & Hget_localb); revert H; subst; intros.
revert H; inv Hlocal; simpl; intros; try auto.
- econstructor; auto.
simpl; auto.
- econstructor; auto.
simpl; auto.
- econstructor; auto.
simpl; auto. }
{ inversion Hlocal; revert H; subst; intros; try (unfold measure; simpl; auto). }
{ repeat rewrite pgss; auto.
rewrite s_set_in; auto. }
{ intros.
rewrite pgss in H5; auto.
revert H; inv H5; auto.
inversion H13. }
{ intros.
rewrite pgso in H5; auto.
eapply H8; eauto. }
{ intros.
elim H1; auto. }
{ intros.
elim H1; auto. }
+
assert (sched_id ≠ cpuid).
{ assert (core_set sched_id = false).
{ eapply sched_valid. }
case_eq (zeq sched_id cpuid); intros; subst; auto.
rewrite H in valid_cpuid.
inv valid_cpuid. }
eapply pget_some_domain in Hget_local.
eapply s_set_in_imply in Hget_local.
elim H; auto.
-
pose proof Hmatch as Hmatch´.
inv Hmatch.
+
assert ((get_curid_from_log cpuid l) = cpuid).
{ eapply pget_some_domain in Hget_local.
eapply s_set_in_imply in Hget_local; auto. }
assert (pget cpuid lsp0 = Some (LState ps true)).
{ rewrite <- H6.
rewrite H in Hget_local.
auto. }
assert (Hvalid_with_yield: valid_log cpuid (EYIELD (get_curid_from_log cpuid l) :: l)).
{ econstructor; eauto.
simpl.
refine_split; auto.
unfold measure in H2; simpl.
subdestruct. }
assert (Hvalid_res: valid_log cpuid (EBACK curid´:: EYIELD (get_curid_from_log cpuid l) :: l)).
{ eapply oracle_result_valid_log; eauto. }
assert (Hvalid: core_set curid´ = true).
{ revert H; inv Hvalid_res.
simpl in H13.
destruct H13; auto. }
left.
∃ (EState curid´ (pset (get_curid_from_log cpuid l) (LState ps false) lsp0)
(EBACK curid´ :: EYIELD (get_curid_from_log cpuid l) :: l)).
split.
× eapply plus_one.
eapply env_exec_step_yield_pos; eauto.
rewrite H; auto.
× rewrite H.
eapply MATCH_EESTATE_S.
{ simpl; auto. }
{ auto. }
{ rewrite H in Hvalid_res.
auto. }
{ simpl; auto. }
{ repeat rewrite pgss; auto.
rewrite s_set_in; auto. }
{ intros.
∃ (EBACK curid´), (EYIELD cpuid::l); split; auto. }
{ intros.
case_eq (zeq tid cpuid); intros; revert H; subst; intros.
- rewrite pgss in H5; auto.
inversion H5; auto.
- rewrite pgso in H5; auto.
clear H9.
rewrite <- H in n.
eapply H8; eauto. }
{ intros.
rewrite pgso in H9; auto.
rewrite H in ×.
eapply H8 in H1; eauto. }
{ intros.
simpl in H5; auto. }
+
assert (sched_id ≠ cpuid).
{ assert (core_set sched_id = false).
{ eapply sched_valid. }
case_eq (zeq sched_id cpuid); intros; subst; auto.
rewrite H in valid_cpuid.
inv valid_cpuid. }
eapply pget_some_domain in Hget_local.
eapply s_set_in_imply in Hget_local.
elim H; auto.
-
pose proof Hmatch as Hmatch´.
inv Hmatch.
+
remember (EState (get_curid_from_log cpuid l) lsp0 l) as est0.
assert (Hget_low: ∃ ps´, pget (get_curid_from_log cpuid l) lsp0 = Some ps´).
{ subst.
eapply pget_some; auto. }
destruct Hget_low as (ps´ & Hget_low).
assert (Htid_neq: (get_curid_from_log cpuid l) ≠ cpuid).
{ case_eq (zeq (get_curid_from_log cpuid l) cpuid); intros; auto.
clear H.
revert e0; subst; intros.
rewrite e0 in ×.
rewrite Hget_low in H6.
rewrite Hget_local in H6.
inv H6. }
destruct ps´.
rename p into ps.
subst.
assert (Hvalid_res: valid_log cpuid (e::l)).
{ unfold valid_oracle in valid_oracle_cond.
eapply valid_oracle_cond; eauto. }
destruct e; simpl.
×
right.
rewrite H2.
unfold measure; simpl.
refine_split; auto.
constructor; eauto.
{ inv Hvalid_res.
simpl in H12.
destruct H12 as (_ & ? & _).
rewrite H; auto. }
{ assert (from = (get_curid_from_log cpuid l)).
{ inv Hvalid_res.
simpl in H12; destruct H12 as (_ & H12 & _); auto. }
rewrite <- H; auto. }
{ intros.
rewrite Hget_low in H0.
destruct b; inv H0; [ inv H12 | ].
assert (lastEvTy l = Some EBACKTY ∨ lastEvTy l ≠ Some EBACKTY).
{ destruct l; simpl; auto.
destruct e; simpl; auto.
- right; intro contra; inv contra.
- right; intro contra; inv contra.
- right; intro contra; inv contra.
- right; intro contra; inv contra. }
destruct H0; auto.
eapply H11 in Hget_low; eauto.
inv Hget_low. }
×
eapply oget_valid_noback in Horacle; eauto.
inv Horacle.
×
assert (HlastEvTy: lastEvTy l = Some EBACKTY).
{ inv Hvalid_res.
simpl in H12.
destruct l; try (inv H12; fail).
destruct e; try (inv H12; fail).
destruct H12; subst.
simpl; auto. }
assert (b = false).
{ eapply H10; eauto; subst. }
rewrite H in ×.
clear H.
assert (Hvalid_con_step:
∃ ps´, hardware_local_step (get_curid_from_log cpuid l) (LView ps l) (LView ps´ ((EACQ from id)::nil))).
{ assert (local_step_ev (EACQ from id) = Some ((EACQ from id)::nil)).
{ simpl; auto. }
eapply relate_single_oracle_concrete_step_def; eauto. }
destruct Hvalid_con_step as (ps´ & Hvalid_con_step).
left.
∃ (EState (get_curid_from_log cpuid l)
(pset (get_curid_from_log cpuid l) (LState ps´ true) lsp0)
(EACQ from id :: nil ++ l)).
split.
{ eapply plus_one.
eapply env_exec_step_progress with (oracle := hw_oracle) in Hvalid_con_step; eauto. }
{ econstructor.
- simpl; auto.
- auto.
- simpl; auto.
- simpl; auto.
inv Hvalid_res.
simpl in H12.
destruct l; try (inv H12; fail).
destruct e; try (inv H12; auto).
- rewrite pgso; auto.
- intros.
elim Htid_neq; auto.
- intros.
rewrite pgso in H0; auto.
eapply H8; eauto.
- intros.
simpl in H0; inv H0.
- intros.
rewrite pgss in H1; auto.
inv H1; auto. }
×
assert (HlastEvTy: lastEvTy l = Some EBACKTY).
{ inv Hvalid_res.
simpl in H12.
destruct l; try (inv H12; fail).
destruct e; try (inv H12; fail).
destruct H12; subst.
simpl; auto. }
assert (b = false).
{ eapply H10; eauto; subst. }
rewrite H in ×.
clear H.
assert (Hvalid_con_step:
∃ ps´, hardware_local_step (get_curid_from_log cpuid l) (LView ps l) (LView ps´ ((EREL from id d)::nil))).
{ assert (local_step_ev (EREL from id d) = Some ((EREL from id d)::nil)).
{ simpl; auto. }
eapply relate_single_oracle_concrete_step_def; eauto. }
destruct Hvalid_con_step as (ps´ & Hvalid_con_step).
left.
∃ (EState (get_curid_from_log cpuid l)
(pset (get_curid_from_log cpuid l) (LState ps´ true) lsp0)
(EREL from id d :: nil ++ l)).
split.
{ eapply plus_one.
eapply env_exec_step_progress with (oracle := hw_oracle) in Hvalid_con_step; eauto. }
{ econstructor.
- simpl; auto.
- auto.
- simpl; auto.
- simpl; auto.
inv Hvalid_res.
simpl in H12.
destruct l; try (inv H12; fail).
destruct e; try (inv H12; auto).
- rewrite pgso; auto.
- intros.
elim Htid_neq; auto.
- intros.
rewrite pgso in H0; auto.
eapply H8; eauto.
- intros.
simpl in H0; inv H0.
- intros.
rewrite pgss in H1; auto.
inv H1; auto. }
×
assert (HlastEvTy: lastEvTy l = Some EBACKTY).
{ inv Hvalid_res.
simpl in H12.
destruct l; try (inv H12; fail).
destruct e0; try (inv H12; fail).
destruct H12; subst.
simpl; auto. }
assert (b = false).
{ eapply H10; eauto; subst. }
rewrite H in ×.
clear H.
assert (Hvalid_con_step:
∃ ps´, hardware_local_step (get_curid_from_log cpuid l) (LView ps l) (LView ps´ ((EATOMIC from id e)::nil))).
{ assert (local_step_ev (EATOMIC from id e) = Some ((EATOMIC from id e)::nil)).
{ simpl; auto. }
eapply relate_single_oracle_concrete_step_def; eauto. }
destruct Hvalid_con_step as (ps´ & Hvalid_con_step).
left.
∃ (EState (get_curid_from_log cpuid l)
(pset (get_curid_from_log cpuid l) (LState ps´ true) lsp0)
(EATOMIC from id e :: nil ++ l)).
split.
{ eapply plus_one.
eapply env_exec_step_progress with (oracle := hw_oracle) in Hvalid_con_step; eauto. }
{ econstructor.
- simpl; auto.
- auto.
- simpl; auto.
- simpl; auto.
inv Hvalid_res.
simpl in H12.
destruct l; try (inv H12; fail).
destruct e0; try (inv H12; auto).
- rewrite pgso; auto.
- intros.
elim Htid_neq; auto.
- intros.
rewrite pgso in H0; auto.
eapply H8; eauto.
- intros.
simpl in H0; inv H0.
- intros.
rewrite pgss in H1; auto.
inv H1; auto. }
+
left.
exploit oget_valid_yield; eauto.
intros Hev.
destruct Hev as (curid´´, Hev); subst.
exploit measure_o_implies_last_yield_ev; eauto.
intros.
destruct H as (prev_curid & ev & l´ & ? & ?); subst.
inv H.
remember (EState (get_curid_from_log cpuid l´) lsp0 l´) as est0.
assert (Hget_low: ∃ ps´, pget (get_curid_from_log cpuid l´) lsp0 = Some ps´).
{ subst.
eapply pget_some; auto. }
destruct Hget_low as (ps´ & Hget_low); subst.
pose proof Hmatch´ as Hmatch´´.
assert (Hcpu_neq: cpuid ≠ get_curid_from_log cpuid l´).
{ intros contra.
rewrite <- contra in H9.
rewrite <- contra in Hget_low.
rewrite H8 in H9.
rewrite Hget_low in H9.
inv H9. }
assert (Hvalid_prev: valid_log cpuid l´).
{ inv H4; auto. }
assert (Hvalid_res: valid_log cpuid (EBACK curid´´ :: EYIELD (get_curid_from_log cpuid l´) :: l´)).
{ unfold valid_oracle in valid_oracle_cond.
eapply valid_oracle_cond in Horacle; eauto.
destruct Horacle; simpl in *; auto. }
assert (Hin_new: core_set curid´´ = true).
{ inv Hvalid_res.
simpl in H7.
destruct H7; auto. }
simpl in *; auto.
destruct ps´.
rename p into ps.
rename l´ into l.
destruct b.
{
∃ (EState curid´´ (pset (get_curid_from_log cpuid l) (LState ps false) lsp0)
(EBACK curid´´ :: EYIELD (get_curid_from_log cpuid l) :: l)).
split.
- eapply plus_one.
eapply env_exec_step_yield_pos; eauto.
- eapply MATCH_EESTATE_S.
+ simpl; auto.
+ auto.
+ auto.
+ simpl; auto.
+ rewrite pgso; auto.
+ intros.
subst.
∃ (EBACK cpuid), (EYIELD (get_curid_from_log cpuid l) :: l); auto.
+ intros.
case_eq (zeq tid (get_curid_from_log cpuid l)); intros; subst.
× rewrite pgss in H0; auto.
inv H0; auto.
× rewrite pgso in H0; auto.
eapply H12; eauto.
+ intros.
case_eq (zeq curid´´ (get_curid_from_log cpuid l)); intros; subst.
× rewrite pgss in H1; auto.
inv H1; auto.
× rewrite pgso in H1; auto.
eapply H12; eauto.
+ intros.
simpl in H0.
elim H0; auto. }
{
assert (lastEvTy l = Some EBACKTY).
{ eapply H13; eauto. }
assert (Hvalid_con_step:
∃ ps´, hardware_local_step (get_curid_from_log cpuid l) (LView ps l) (LView ps´ nil)).
{ assert (local_step_ev (EYIELD (get_curid_from_log cpuid l)) = Some nil).
{ simpl; auto. }
eapply relate_single_oracle_concrete_step_def; eauto. }
destruct Hvalid_con_step as (ps´ & Hvalid_con_step).
remember (EState (get_curid_from_log cpuid l) (pset (get_curid_from_log cpuid l) (LState ps´ true) lsp0) l) as est0´.
assert (Hone_step: env_step hw_oracle (EState (get_curid_from_log cpuid l) lsp0 l) E0 est0´).
{ subst; eapply env_exec_step_progress in Hvalid_con_step; eauto; simpl. }
remember (pset (get_curid_from_log cpuid l) (LState ps´ true) lsp0) as lsp0´.
∃ (EState curid´´ (pset (get_curid_from_log cpuid l) (LState ps´ false) lsp0´)
(EBACK curid´´ :: EYIELD (get_curid_from_log cpuid l) :: l)).
split.
{ eapply plus_two.
- eapply Hone_step.
- subst.
eapply env_exec_step_yield_pos; eauto.
rewrite pgss; auto.
- auto. }
{ eapply MATCH_EESTATE_S.
- simpl; auto.
- auto.
- auto.
- simpl; auto.
- subst.
rewrite pgso; eauto.
rewrite pgso; eauto.
- intros.
∃ (EBACK curid´´), (EYIELD (get_curid_from_log cpuid l) :: l); auto.
- intros.
case_eq (zeq tid (get_curid_from_log cpuid l)); intros; subst.
+ rewrite pgss in H1; auto.
inv H1; auto.
+ rewrite pgso in H1; auto.
rewrite pgso in H1; auto.
eapply H12; eauto.
- intros.
case_eq (zeq curid´´ (get_curid_from_log cpuid l)); intros; subst.
+ rewrite pgss in H5; auto; inv H5; auto.
+ rewrite pgso in H5; auto.
rewrite pgso in H5; auto.
eapply H12; eauto.
- intros.
simpl in H1.
elim H1; auto. } }
Qed.
End ENV_REFINES_ENV.
Section SINGLE_REFINES_ENV.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset := hdset)}.
Context `{pmap: PartialMap}.
Variable cur_cpuid : Z.
Inductive match_sstate: single_state → (estate (A:= s_set cur_cpuid)) → Prop :=
| MATCH_SSTATE: ∀ curid l lsp lv,
pget cur_cpuid lsp = Some lv →
match_sstate (SState curid lv l) (EState curid lsp l).
Lemma one_step_single_refines_env:
∀ o s s´ os t
(Hone: single_step cur_cpuid o s t s´)
(Hmatch_state: match_sstate s os),
∃ os´,
plus env_step o os t os´ ∧
match_sstate s´ os´.
Proof.
intros.
inv Hmatch_state.
inversion Hone; revert H1; subst; intros.
- rewrite <- H1 in ×.
clear H1.
set (lsp´ := pset cur_cpuid (LState ps´ true) lsp).
∃ (EState cur_cpuid lsp´ (l´ ++ l)).
split.
+ eapply plus_one.
eapply env_exec_step_progress; eauto.
+ econstructor.
unfold lsp´.
rewrite pgss; auto.
rewrite s_set_in; auto.
- rewrite <- H1 in ×.
set (lsp´ := pset cur_cpuid (LState ps false) lsp).
∃ (EState curid´ lsp´ (EBACK curid´ :: EYIELD cur_cpuid :: l)).
split.
+ eapply plus_one.
eapply env_exec_step_yield_pos; eauto.
+ econstructor.
unfold lsp´.
rewrite pgss; auto.
rewrite s_set_in; auto.
- assert (Hempty: pget curid lsp = None).
{ eapply pget_none.
rewrite s_set_not_in; auto. }
∃ (EState (back_id curid e) lsp (e::l)).
split.
+ eapply plus_one.
eapply env_exec_step_skip; eauto.
+ constructor; auto.
Qed.
End SINGLE_REFINES_ENV.
Section SINGLE_REFINES_BIG.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset:= hdset)}.
Context `{pmap: PartialMap}.
Context `{fair: Fairness}.
Variable tid : Z.
Variable si_o : Oracle.
Hypothesis valid_tid: core_set tid = true.
Hypothesis valid_oracle_hyp: valid_oracle tid (s_set tid) si_o.
Lemma tid_neq_sched_id : tid ≠ sched_id.
Proof.
intros contra.
subst.
assert (core_set sched_id = false).
{ eapply sched_valid; auto. }
rewrite H in valid_tid; inv valid_tid.
Qed.
Lemma star_step_get_env_log:
∀ n l res l´ ps curid
(Hneq: tid ≠ curid)
(Hback: AbsYieldBack n tid l res si_o = Some l´),
star (single_step tid) si_o (SState curid ps (res ++ l)) E0 (SState tid ps (l´ ++ l)).
Proof.
induction n; intros.
- inv Hback.
- simpl in Hback.
destruct (oget (s_set tid) (res ++ l) si_o) eqn:Hget; contra_inv.
destruct (back_id_option e) eqn: Hback_id; contra_inv.
{ destruct e; inv Hback_id.
destruct (zeq tid z); subst.
{ inv Hback.
eapply star_one.
eapply single_exec_step_skip; eauto.
trivial. }
{ eapply star_trans.
{ eapply star_one.
eapply single_exec_step_skip; eauto. }
{ rewrite app_comm_cons.
eapply IHn; eauto. }
{ trivial. } } }
{ eapply star_trans.
{ eapply star_one.
eapply single_exec_step_skip; eauto. }
{ rewrite app_comm_cons.
eapply IHn; eauto.
destruct e; inv Hback_id; simpl; trivial.
eauto using tid_neq_sched_id; auto. }
{ trivial. } }
Qed.
Definition match_bsstate (s_h: single_state) (s_l: single_state) : Prop :=
s_h = s_l ∧ match s_h with
| (SState tid (LState ps b) l) ⇒ valid_log tid l ∧
lastEvTy l ≠ Some YIELDTY ∧
tid = get_curid_from_log tid l ∧
(b = false → ∃ e l´, l = e::l´ ∧ e = EBACK tid)
end.
Lemma one_step_single_refines_big:
∀ s_h t s_h´ s_l
(Hone: single_big_step tid si_o s_h t s_h´)
(Hmatch: match_bsstate s_h s_l),
∃ s_l´,
plus (single_step tid) si_o s_l t s_l´ ∧
match_bsstate s_h´ s_l´.
Proof.
intros.
inv Hone; inv Hmatch.
-
refine_split´.
+ eapply plus_one.
eapply single_exec_step_progress; eauto.
+ constructor; eauto.
destruct H0 as (H0a & H0b & H0c & H0d).
exploit H0d; auto; clear H0d; intros.
destruct H as (ev & l´´ & Ha & Hb).
revert H0c; subst; intros.
split.
× clear H0c.
inv Hlocal; simpl; try auto.
{ econstructor; auto; simpl; auto. }
{ econstructor; auto; simpl; auto. }
{ econstructor; auto; simpl; auto. }
× split.
{ clear H0c.
inv Hlocal; simpl; auto; intro contra; inv contra. }
{ split.
- simpl in H0c; subst.
clear H0c.
inv Hlocal; simpl; auto.
- intro contra; inv contra. }
-
destruct H0 as (H01 & H02 & H03 & _).
destruct time_bound; try (inv Hl1; fail).
simpl in Hl1.
destruct (oget (s_set tid) (EYIELD tid :: l) si_o) eqn: Hget; contra_inv.
assert (valid_log tid (EYIELD tid::l)).
{ econstructor; eauto.
simpl; split; auto. }
pose proof valid_oracle_hyp as valid_oracle_hyp´.
unfold valid_oracle in valid_oracle_hyp.
specialize (valid_oracle_hyp _ _ H Hget).
destruct valid_oracle_hyp as (? & ?).
revert H03; inv H1; simpl in H7.
destruct e; simpl; try (inversion H7; fail).
+ destruct H7 as (H7 & _).
elim H7; auto.
+ destruct H7.
clear H2.
simpl in H0.
unfold back_id_option in Hl1.
intros.
∃ (SState tid (LState ps false) (l´ ++ EYIELD tid:: l)).
refine_split.
eapply plus_star_trans.
{
eapply plus_one.
eapply single_exec_step_yield_pos; eauto.
}
destruct (zeq tid to); revert H03; subst; intros.
{ revert H03; inv Hl1; econstructor. }
{
rewrite list_append_rewrite.
eapply star_step_get_env_log; eauto.
}
{ trivial. }
{ econstructor; eauto.
subdestruct.
+ inv Hl1; simpl; split.
× constructor; eauto; simpl; split; auto.
× split; [intro contra; inv contra | split; auto].
intros.
∃ (EBACK to), (EYIELD to :: l); eauto.
+ assert (valid_log tid (EBACK to::nil ++ EYIELD tid::l)).
{ unfold valid_oracle in valid_oracle_hyp´.
eapply valid_oracle_hyp´ in H6; eauto.
destruct H6; simpl; auto. }
split; [eapply YieldBack_satisfies_valid_log; eauto; simpl; auto |].
exploit YieldBack_valid_last_event; eauto; simpl; auto.
intros Htemp.
destruct Htemp as (ev & l_res´ & Ha & Hb & Hc); revert H03; subst; intros.
split; [ simpl; intros contra; inv contra | split; simpl; auto].
intros.
∃ (EBACK tid), (l_res´ ++ EYIELD tid::l).
split; auto. }
Qed.
End SINGLE_REFINES_BIG.
Section BIG_REFINES_BIG2.
Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset:= hdset)}.
Context `{pmap: PartialMap}.
Context `{fair: Fairness}.
Inductive match_rstate: Z → rstate → single_state → Prop :=
| MATCH_RSTATE: ∀ curid l ps,
match_rstate curid (RState ps l) (SState curid (LState ps true) l).
Lemma one_step_big_refines_big2:
∀ tid o s s0 s´ t
(Hone: single_big2_step tid o s t s´)
(Hmatch: match_rstate tid s s0),
∃ s0´,
plus (single_big_step tid) o s0 t s0´
∧ match_rstate tid s´ s0´.
Proof.
intros. inv Hone. inv Hmatch.
refine_split´; trivial.
-
eapply plus_two.
+
eapply single_exec_step_yield_pos_big; eauto.
+
eapply single_exec_step_progress_big; eauto.
+ trivial.
-
constructor; eauto.
Qed.
End BIG_REFINES_BIG2.
Section BIG2_REFINES_SPLIT.
Context `{op: OracleProp(ret:= event) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset:= hdset)}.
Context `{pmap: PartialMap}.
Context `{fair: Fairness}.
Inductive match_srstate: srstate → rstate → Prop :=
| MATCH_SRSTATE: ∀ al l l´ ps
(Hl´: l´ = al ++ l),
match_srstate (SRState ps l al) (RState ps l´).
Lemma single_local_imply_env:
∀ tid l ps ps´,
single_local_step tid (SView ps)
(SView ps´) →
hardware_local_step tid (LView ps l)
(LView ps´ nil).
Proof.
intros. inv H.
- eapply hardware_local_exec_step_private; eauto.
Qed.
Lemma single_log_imply_env:
∀ tid ps l l´ ps´,
single_log_step tid (LView ps l)
(LView ps´ l´) →
hardware_local_step tid (LView ps l)
(LView ps´ l´).
Proof.
intros. inv H.
- eapply hardware_local_exec_step_acq; eauto.
- eapply hardware_local_exec_step_rel; eauto.
- eapply hardware_local_exec_step_atomic; eauto.
Qed.
Lemma one_step_big2_refines_split:
∀ tid o s s0 s´ t
(Hone: single_split_step tid o s t s´)
(Hmatch: match_srstate s s0),
∃ s0´,
plus (single_big2_step tid) o s0 t s0´
∧ match_srstate s´ s0´.
Proof.
intros. inv Hone; inv Hmatch.
-
refine_split´; trivial.
+
eapply plus_one. constructor; eauto.
eapply single_local_imply_env; eauto.
+ simpl. econstructor. rewrite <- app_assoc.
trivial.
-
refine_split´; trivial.
+
eapply plus_one. econstructor; eauto.
eapply single_log_imply_env; eauto.
+ simpl. econstructor. simpl. trivial.
Qed.
End BIG2_REFINES_SPLIT.
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}.
Variable cpuid : Z.
Variable si_oracle : Oracle (OracleProp := op).
Variable re_oracle : Oracle (OracleProp := op1).
Inductive match_osstate: rstate → srstate → Prop :=
| MATCH_OSSTATE:
∀ l_h l_l ps_h ps_l al,
ps_h = ps_l → l_h = l_l →
valid_log cpuid (al ++ l_l) →
get_curid_from_log cpuid (al ++ l_l) = cpuid →
lastEvTy l_h ≠ Some YIELDTY →
(al = nil ∨ (∃ ev al´, al = ev::al´ ∧ ev = EBACK cpuid)) →
valid_cache_log_members cpuid al →
match_osstate (RState ps_h l_h) (SRState ps_l l_l al).
Hypothesis valid_oracle: valid_oracle cpuid (s_set cpuid) si_oracle.
Hypothesis YieldBack_consistence_with_reorder_o :
∀ ps_h l_h ps_l l_l al,
match_osstate (RState ps_h l_h) (SRState ps_l l_l al) →
valid_log cpuid (EYIELD cpuid::al ++ l_l) →
∃ l1, AbsYieldBack time_bound cpuid (EYIELD cpuid::al ++ l_l) nil si_oracle = Some l1 ∧
∀ l1´, oget (s_set cpuid) l_h re_oracle = Some l1´ →
l1´ = l1 ++ EYIELD cpuid :: al.
Lemma one_step_split_refines_reorder:
∀ s_h t s_h´ s_l
(Hone: single_reorder_step cpuid re_oracle s_h t s_h´)
(Hmatch: match_osstate s_h s_l),
∃ s_l´,
single_split_step cpuid si_oracle s_l t s_l´ ∧
match_osstate s_h´ s_l´.
Proof.
intros; inv Hone; pose proof Hmatch as Hmatch´.
- destruct s_l.
inversion Hmatch.
revert H7; subst; intros.
assert (Hvalid_l_w_yield: valid_log cpuid (EYIELD cpuid :: al ++ l0)).
{ econstructor; eauto.
- revert H7; inv H6; intros; auto.
- destruct H9; revert H7; subst; intros.
+ simpl.
simpl in H6.
simpl in H7.
refine_split; auto.
revert H7; inv H6; intros; auto.
+ destruct H as (ev´ & al´ & Ha & Hb).
revert H7; subst; intros.
simpl.
refine_split; auto.
× intro contra; inv contra.
× revert H7; inv H6; intros; auto. }
eapply YieldBack_consistence_with_reorder_o in Hmatch´; auto.
destruct Hmatch´ as (l1 & Hyield & _).
refine_split´.
+ eapply single_exec_step_progress_split_local; eauto.
+ constructor; eauto.
× rewrite app_assoc_reverse.
simpl.
eapply YieldBack_satisfies_valid_log; eauto.
simpl; auto.
× eapply YieldBack_valid_last_event in Hyield; simpl; eauto.
destruct Hyield as (ev & l_res´ & Ha & Hb & Hc).
revert H7; subst; intros.
simpl; auto.
× right.
eapply YieldBack_valid_last_event in Hyield; simpl; eauto.
destruct Hyield as (ev & l_res´ & Ha & Hb & Hc).
revert H7; subst; intros.
simpl.
refine_split´; eauto.
× unfold valid_cache_log_members.
intros.
eapply in_app_or in H.
destruct H.
{ eapply YieldBack_satisfies_valid_oracle_members in Hyield; eauto.
unfold valid_oracle_members; intros ? contra; inv contra. }
{ simpl in H.
destruct H.
- revert H7; subst.
intros.
simpl.
right; auto.
- unfold valid_cache_log_members in H10.
eapply H10 in H; eauto. }
- destruct s_l.
inversion Hmatch.
revert H7; subst; intros.
assert (Hvalid_l_w_yield: valid_log cpuid (EYIELD cpuid :: al ++ l1)).
{ econstructor; eauto.
- revert H7; inv H6; intros; auto.
- destruct H9; revert H7; subst; intros.
+ simpl.
simpl in H6.
simpl in H7.
refine_split; auto.
revert H7; inv H6; intros; auto.
+ destruct H as (ev´ & al´ & Ha & Hb).
revert H7; subst; intros.
simpl.
refine_split; auto.
× intro contra; inv contra.
× revert H7; inv H6; intros; auto. }
eapply YieldBack_consistence_with_reorder_o in Hmatch´; auto.
destruct Hmatch´ as (l2 & Hyield & Hyield_cond).
exploit Hyield_cond; eauto; clear Hyield_cond.
intros Htemp; revert H7; inv Htemp; intros.
assert ((l2 ++ EYIELD cpuid :: al) ++ l1 = l2 ++ EYIELD cpuid :: al ++ l1).
{ rewrite app_assoc_reverse; simpl; auto. }
rewrite H in Hlocal; clear H.
refine_split´.
+ eapply single_exec_step_progress_split_log; eauto.
+ assert (valid_log cpuid (l2 ++ EYIELD cpuid :: al ++ l1)).
{ eapply YieldBack_satisfies_valid_log; simpl; eauto.
simpl; auto. }
econstructor; eauto.
× rewrite app_assoc_reverse; simpl; auto.
× simpl.
eapply YieldBack_valid_last_event in Hyield; simpl; eauto.
destruct Hyield as (ev & l_res´ & Ha & Hb & Hc); revert H7; subst; intros; simpl.
clear H7.
inv Hlocal; simpl.
{ eapply valid_log_cons; eauto.
simpl; auto. }
{ eapply valid_log_cons; eauto.
simpl; auto. }
{ eapply valid_log_cons; eauto.
simpl; auto. }
× simpl.
clear H7.
inv Hlocal; simpl; eauto.
× clear H7; inv Hlocal; simpl; intros contra; inv contra.
× unfold valid_cache_log_members.
intros ? contra; inv contra.
Qed.
End REORDER_REFINES_SPLIT.
Section REORDER_REFINES_REORDER.
Context `{op: OracleProp (ret:= Log) (log:= Log) (log_len := list_Len)}.
Context `{hdsem: HardSemantics (hdset:= hdset)}.
Context `{pmap: PartialMap}.
Context `{fair: Fairness}.
Variable cpuid : Z.
Variable hi_re_o : Oracle (OracleProp := op).
Variable lo_re_o : Oracle (OracleProp := op).
Inductive match_rrstate: rstate → rstate → Prop :=
| MATCH_RRSTATE:
∀ l´ l ps,
l´ = reduce_log l →
match_rrstate (RState ps l´) (RState ps l).
Hypothesis relate_reorder_oracles :
∀ ps l,
match_rrstate (RState ps (reduce_log l)) (RState ps l) →
∀ l_h, oget (s_set cpuid) (reduce_log l) hi_re_o = Some l_h →
∃ l_l, oget (s_set cpuid) l lo_re_o = Some l_l ∧ l_h = reduce_log l_l.
Lemma one_step_reorder_refines_reorder:
∀ s t s´ s0
(Hone: single_reorder_step cpuid hi_re_o s t s´)
(Hmatch: match_rrstate s s0),
∃ s0´,
single_reorder_step cpuid lo_re_o s0 t s0´ ∧
match_rrstate s´ s0´.
Proof.
intros.
pose proof Hmatch as Hmatch´.
inv Hone.
- inv Hmatch.
refine_split´; econstructor; auto.
- inv Hmatch.
exploit relate_reorder_oracles; eauto; intros.
destruct H as (l_l & Ha & H_b).
subst.
rewrite <- reduce_log_split.
rewrite <- reduce_log_split in Hlocal.
exploit single_log_log_imply2; eauto; intros Hstep.
∃ (RState ps´ (l´ ++ l_l ++ l1)).
split; constructor; auto.
exploit single_log_log_imply3; eauto.
intros.
rewrite reduce_log_split.
rewrite reduce_log_split.
rewrite reduce_log_split.
rewrite <- H; auto.
Qed.
End REORDER_REFINES_REORDER.
Section SEPARATE_REFINES_REORDER.
Context `{re_op: OracleProp (ret:= Log) (log:= Log) (log_len := list_Len)}.
Context `{sep_op: 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}.
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.
Definition valid_log´ (l : Log) : Prop :=
l = reduce_log l.
Definition valid_oracle´ (tid: Z) (o : Oracle (OracleProp := re_op)) :=
∀ l l´,
valid_log´ l →
oget (s_set tid) l o = Some l´ →
(∀ e, In e l´ → event_source e ≠ tid) ∧
valid_log´ l´.
Hint Unfold valid_log´ valid_oracle´.
Variable cpuid : Z.
Variable sep_o : Oracle (OracleProp := sep_op).
Variable re_o : Oracle (OracleProp := re_op).
Inductive match_logs: Z → separate_log → Log → Prop :=
| MATCH_LOG:
∀ tid sep_l glob_l
(Hatomic: ∀ prim_id l_h l_l,
ZMap.get prim_id sep_l = l_h →
log_get_atomic glob_l prim_id = l_l →
separate_log_type_2_log l_h prim_id = (remove_cache_event l_l tid)),
match_logs tid sep_l glob_l.
Inductive match_spstate: Z → sp_state → rstate → Prop :=
| MATCH_SPSTATE:
∀ tid glob_l sep_l ps
(Hlow_cond: valid_log´ glob_l)
(Hlog: match_logs tid sep_l glob_l),
match_spstate tid (SPState ps sep_l) (RState ps glob_l).
Hypothesis valid_oracle´_def: valid_oracle´ cpuid re_o.
Hypothesis relate_separate_oracle_reorder_oracle_def:
∀ ps sep_l glob_l id id_l id_l´ e,
match_spstate cpuid (SPState ps sep_l) (RState ps glob_l) →
ZMap.get id sep_l = id_l → oget (OracleProp := sep_op) (s_set cpuid) (id, id_l, e) sep_o = Some id_l´ →
∃ glob_l´,
oget (OracleProp := re_op) (s_set cpuid) glob_l re_o = Some glob_l´ ∧
log_get_atomic (glob_l´ ++ glob_l) id = separate_log_type_2_log (id_l´ ++ id_l) id.
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 one_step_reorder_refines_separate:
∀ s s0 s´ t
(Hone: single_separate_step (op := sep_op) cpuid sep_o s t s´)
(Hmatch: match_spstate cpuid s s0),
∃ s0´,
single_reorder_step (op := re_op) cpuid re_o s0 t s0´
∧ match_spstate cpuid s´ s0´.
Proof.
intros.
pose proof Hmatch as Hmatch´.
inv Hone; inv Hmatch.
-
refine_split´; trivial.
+ constructor; eauto.
+ constructor; eauto.
-
inv Hlocal.
+
eapply relate_separate_oracle_reorder_oracle_def in Hmatch´; eauto.
destruct Hmatch´ as (glob_l´ & Hmatch_a & Hmatch_b).
rewrite <- Hmatch_b in Howner.
rewrite CalOwner_atomic_log in Howner.
refine_split´; trivial.
× eapply single_exec_step_progress_reorder_log; eauto.
eapply single_local_exec_step_acq; eauto.
× simpl.
econstructor.
{ unfold valid_oracle´ in ×.
eapply valid_oracle´_def in Hmatch_a; eauto.
destruct Hmatch_a.
unfold valid_log´ in ×.
simpl.
f_equal; auto.
rewrite reduce_log_split; auto.
set (temp:= reduce_log glob_l´ ++ reduce_log glob_l).
rewrite Hlow_cond, H0; unfold temp; auto. }
{ econstructor; eauto.
intros.
case_eq (zeq prim_id id); intros; subst.
- rewrite ZMap.gss; simpl.
rewrite zeq_true; simpl.
rewrite zeq_true; simpl.
f_equal; auto.
- rewrite ZMap.gso; simpl; auto.
rewrite zeq_false; simpl; auto.
rewrite remove_cache_gss; inv Hlog; auto.
unfold valid_oracle´ in ×.
eapply valid_oracle´_def in Hmatch_a; eauto.
destruct Hmatch_a; auto. }
+
eapply relate_separate_oracle_reorder_oracle_def in Hmatch´; eauto.
destruct Hmatch´ as (glob_l´ & Hmatch_a & Hmatch_b).
rewrite <- Hmatch_b in Howner.
rewrite CalOwner_atomic_log in Howner.
refine_split´; trivial.
× eapply single_exec_step_progress_reorder_log; eauto.
eapply single_local_exec_step_rel; eauto.
× simpl.
econstructor.
{ unfold valid_oracle´ in ×.
eapply valid_oracle´_def in Hmatch_a; eauto.
destruct Hmatch_a.
unfold valid_log´ in ×.
simpl.
f_equal; auto.
rewrite reduce_log_split; auto.
set (temp:= reduce_log glob_l´ ++ reduce_log glob_l).
rewrite Hlow_cond, H0; unfold temp; auto. }
{ econstructor; eauto.
intros.
case_eq (zeq prim_id id); intros; subst.
- rewrite ZMap.gss; simpl.
rewrite zeq_true; simpl.
rewrite zeq_true; simpl.
f_equal; auto.
- rewrite ZMap.gso; simpl; auto.
rewrite zeq_false; simpl; auto.
rewrite remove_cache_gss; inv Hlog; auto.
unfold valid_oracle´ in ×.
eapply valid_oracle´_def in Hmatch_a; eauto.
destruct Hmatch_a; auto. }
+
eapply relate_separate_oracle_reorder_oracle_def in Hmatch´; eauto.
destruct Hmatch´ as (glob_l´ & Hmatch_a & Hmatch_b).
rewrite <- Hmatch_b in Hatomic.
refine_split´.
× eapply single_exec_step_progress_reorder_log; eauto.
eapply single_local_exec_step_atomic; eauto.
eapply atomic_step_valid; eauto.
rewrite log_get_atomic_simpl; auto.
× simpl.
econstructor.
{ unfold valid_oracle´ in ×.
eapply valid_oracle´_def in Hmatch_a; eauto.
destruct Hmatch_a.
unfold valid_log´ in ×.
simpl.
f_equal; auto.
rewrite reduce_log_split; auto.
set (temp:= reduce_log glob_l´ ++ reduce_log glob_l).
rewrite Hlow_cond, H0; unfold temp; auto. }
{ econstructor; eauto.
intros.
case_eq (zeq prim_id id); intros; subst.
- rewrite ZMap.gss; simpl.
rewrite zeq_true; simpl.
rewrite zeq_true; simpl.
f_equal; auto.
- rewrite ZMap.gso; simpl; auto.
rewrite zeq_false; simpl; auto.
rewrite remove_cache_gss; inv Hlog; auto.
unfold valid_oracle´ in ×.
eapply valid_oracle´_def in Hmatch_a; eauto.
destruct Hmatch_a; auto. }
Qed.
End SEPARATE_REFINES_REORDER.