Library mcertikos.mm.ALHGen
This file provide the contextual refinement proof between MALOp layer and MAL layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import LAsm.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import MALT.
Require Import MALH.
Require Import AbstractDataType.
Require Import OracleATHRel.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import LAsm.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import MALT.
Require Import MALH.
Require Import AbstractDataType.
Require Import OracleATHRel.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Section Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATAOps := (cdata (cdata_ops := malh_data_ops) RData).
Notation LDATAOps := (cdata (cdata_ops := malt_data_ops) RData).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATAOps := (cdata (cdata_ops := malh_data_ops) RData).
Notation LDATAOps := (cdata (cdata_ops := malt_data_ops) RData).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Record relate_RData (f:meminj) (hadt: RData) (ladt: RData) :=
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
AC_re: AC hadt = AC ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
ATC_re: ATC hadt = ATC ladt;
nps_re: nps hadt = nps ladt;
init_re: init hadt = init ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
lock_re: ∀ i,
ZMap.get i (lock hadt) = ZMap.get i (lock ladt);
pperm_re: pperm hadt = pperm ladt;
com1_re: com1 hadt = com1 ladt;
console_re: console hadt = console ladt;
console_concrete_re: console_concrete hadt = console_concrete ladt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr ladt = in_intr hadt;
drv_serial_re: drv_serial hadt = drv_serial ladt;
multi_oracle_re: relate_ATH_Oracle_Pool (multi_oracle hadt) (multi_oracle ladt);
multi_log_re: relate_ATH_Log_Pool (multi_log hadt) (multi_log ladt);
AT_log_re:
∀ l,
ZMap.get 0 (multi_log hadt) = MultiDef l →
CalAT_log_real l = Some (AT ladt)
}.
Inductive match_RData: stencil → RData → mem → meminj → Prop :=
| MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.
Local Hint Resolve MATCH_RDATA.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := nil
}.
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
AC_re: AC hadt = AC ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
ATC_re: ATC hadt = ATC ladt;
nps_re: nps hadt = nps ladt;
init_re: init hadt = init ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
lock_re: ∀ i,
ZMap.get i (lock hadt) = ZMap.get i (lock ladt);
pperm_re: pperm hadt = pperm ladt;
com1_re: com1 hadt = com1 ladt;
console_re: console hadt = console ladt;
console_concrete_re: console_concrete hadt = console_concrete ladt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr ladt = in_intr hadt;
drv_serial_re: drv_serial hadt = drv_serial ladt;
multi_oracle_re: relate_ATH_Oracle_Pool (multi_oracle hadt) (multi_oracle ladt);
multi_log_re: relate_ATH_Log_Pool (multi_log hadt) (multi_log ladt);
AT_log_re:
∀ l,
ZMap.get 0 (multi_log hadt) = MultiDef l →
CalAT_log_real l = Some (AT ladt)
}.
Inductive match_RData: stencil → RData → mem → meminj → Prop :=
| MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.
Local Hint Resolve MATCH_RDATA.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := nil
}.
Prove that after taking one step, the refinement relation still holds
Lemma relate_incr:
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
eapply relate_incr; eauto.
Qed.
End Rel_Property.
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
eapply relate_incr; eauto.
Qed.
End Rel_Property.
Section PASSTHROUGH_RPIM.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
Qed.
Lemma fstore_exist:
∀ s habd habd´ labd i v f,
fstore0_spec i v habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, fstore0_spec i v labd = Some labd´ ∧ relate_AbData s f habd´ labd´.
Proof.
unfold fstore0_spec; intros.
revert H. pose proof H0 as HR.
inv H0. subrewrite. subdestruct.
exploit flatmem_store_exists; eauto.
Qed.
Require Import TacticsForTesting.
Lemma H_CalLock_exists:
∀ l l´
(Hre: relate_ATH_Log l l´),
∃ n, H_CalLock l´ = Some (n, LEMPTY, None).
Proof.
Local Transparent H_CalLock.
simpl.
induction l; simpl; intros;
inv Hre; simpl; eauto.
exploit IHl; eauto.
intros (n & HCal).
inv Hrelate_event.
simpl; rewrite HCal.
repeat rewrite zeq_true. unfold local_lock_bound.
repeat rewrite zeq_true. eauto.
Qed.
Lemma H_CalLock_wait_exists:
∀ i n l l´
(Hre: relate_ATH_Log l l´)
(Hn: n ≠ O),
∃ a, H_CalLock (TEVENT i (TSHARED OPULL) :: TEVENT i (TTICKET (WAIT_LOCK n)) :: l´) = Some a.
Proof.
intros.
exploit H_CalLock_exists; eauto.
intros (n0 & Hcal).
simpl. rewrite Hcal. rewrite zeq_true.
destruct n; eauto.
elim Hn; trivial.
Qed.
Lemma CalAT_eq:
∀ l l´ a a´
(Hre: relate_ATH_Log l l´)
(Hcal: CalAT_log_real l = Some a)
(Hget: GetSharedAT l´ = Some a´),
a´ = a.
Proof.
destruct l; intros; simpl.
- inv Hre. inv Hget.
- inv Hre. inv Hrelate_event.
rewrite Hcal in Hrelate_e. inv Hrelate_e.
simpl in Hget. inv Hget. trivial.
Qed.
Lemma CalAT_eq_None:
∀ l l´
(Hre: relate_ATH_Log l l´)
(Hget: GetSharedAT l´ = None),
l = nil ∧ l´ = nil.
Proof.
destruct l; intros; simpl; trivial.
- inv Hre. eauto.
- inv Hre. inv Hrelate_event.
simpl in Hget. inv Hget.
Qed.
Local Opaque H_CalLock.
Lemma lock_gss:
∀ l l´,
(∀ i0, ZMap.get i0 l = ZMap.get i0 l´) →
(ZMap.get 0 l = LockFalse) →
(∀ i0,
ZMap.get i0 l = ZMap.get i0 (ZMap.set 0 LockFalse l´)).
Proof.
intros. destruct (zeq i0 0); subst.
- rewrite ZMap.gss. trivial.
- rewrite ZMap.gso; eauto.
Qed.
Lemma list_append_rewrite´:
∀ {A: Type} l (a b c d: A),
a :: b :: c :: d :: l = (a::b::c::d:: nil) ++ l.
Proof.
intros.
repeat rewrite <- app_comm_cons. trivial.
Qed.
Lemma relate_ATH_Log_palloc:
∀ c i a l l´
(Hre: relate_ATH_Log l l´)
(Hcal: CalAT_log_real (TEVENT c (TSHARED (OPALLOCE i)) :: l) = Some a),
relate_ATH_Log
(TEVENT c (TSHARED (OPALLOCE i)) :: l)
(TEVENT c (TTICKET REL_LOCK)
:: TEVENT c (TSHARED (OATE a))
:: TEVENT c (TSHARED OPULL)
:: TEVENT c (TTICKET (WAIT_LOCK local_lock_bound)) :: l´).
Proof.
intros.
rewrite list_append_rewrite´.
econstructor; eauto.
econstructor; eauto.
Qed.
Lemma index2Z_neq:
∀ i ofs r,
i ≠ 0 →
index2Z i ofs = Some r →
r ≠ 0.
Proof.
intros. functional inversion H0.
functional inversion H3; subst.
- omega.
- unfold ID_AT_range in ×. omega.
- unfold lock_TCB_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma palloc_exist:
∀ habd habd´ labd i id s f
(Hhigh: MALH.high_level_invariant habd),
lpalloc_spec id habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc´_spec id labd = Some (labd´, i) ∧ relate_AbData s f habd´ labd´.
Proof.
unfold lpalloc_spec, palloc´_spec, palloc_aux_spec,
acquire_lock_AT_spec, release_lock_AT_spec in *; intros.
revert H. pose proof H0 as HR.
inv H0. subrewrite. simpl.
rewrite <- lock_re0.
d4 subdestruct_one.
destruct (ZMap.get 0 (multi_log habd)) eqn:Hlog; contra_inv; eauto.
pose proof multi_log_re0 as Hlogre.
inv Hlogre. rewrite Hlog in Hrel_eq. inv Hrel_eq.
subdestruct_one.
assert (Hrel: relate_ATH_Log (ZMap.get 0 (multi_oracle habd) (CPU_ID labd) l ++ l)
(ZMap.get 0 (multi_oracle labd) (CPU_ID labd) l2 ++ l2)).
{
inv multi_oracle_re0. inv Hrel_o_eq.
eapply Hrel_o_log; eauto.
}
exploit (H_CalLock_wait_exists (CPU_ID labd) local_lock_bound); eauto.
{
unfold local_lock_bound. omega.
}
intros (a & ->).
destruct (GetSharedAT (ZMap.get 0 (multi_oracle labd) (CPU_ID labd) l2 ++ l2)) eqn:HAT; simpl; subrewrite´.
- subdestruct_one.
+ subdestruct_one.
exploit CalAT_eq; eauto. intros Heq. subst.
subdestruct; inv HQ; subrewrite´.
× repeat rewrite ZMap.gss.
assert (Hcal0: CalAT_log_real
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE i))
:: ZMap.get 0 (multi_oracle habd) (CPU_ID labd) l ++ l) =
Some (ZMap.set i (ATValid true ATNorm) a1)).
{
unfold CalAT_log_real in ×. simpl.
rewrite Hdestruct5.
destruct a0 as (Hi & Hget & Hrange).
rewrite zeq_false; [| omega].
rewrite Hget. trivial.
}
assert (Hrel´: relate_ATH_Log
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE i))
:: ZMap.get 0 (multi_oracle habd) (CPU_ID labd) l ++ l)
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd)
(TSHARED (OATE (ZMap.set i (ATValid true ATNorm) a1)))
:: TEVENT (CPU_ID labd) (TSHARED OPULL)
:: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get 0 (multi_oracle labd) (CPU_ID labd) l2 ++ l2)).
{
eapply relate_ATH_Log_palloc; eauto.
}
exploit H_CalLock_exists; eauto.
intros (n0 & ->).
repeat rewrite ZMap.set2.
refine_split´; eauto.
econstructor; simpl; eauto.
{
eapply lock_gss; eauto.
}
{
constructor; eauto.
- intros.
assert (Hneq: r ≠ 0) by (eapply index2Z_neq; eauto).
repeat rewrite ZMap.gso; eauto.
- repeat rewrite ZMap.gss.
constructor; eauto.
}
{
rewrite ZMap.gss. intros. inv H0. trivial.
}
× repeat rewrite ZMap.gss.
assert (Hcal0: CalAT_log_real
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE 0))
:: ZMap.get 0 (multi_oracle habd) (CPU_ID labd) l ++ l)
= Some a1).
{
unfold CalAT_log_real in ×. simpl.
rewrite Hdestruct5. trivial.
}
assert (Hrel´: relate_ATH_Log
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE 0))
:: ZMap.get 0 (multi_oracle habd) (CPU_ID labd) l ++ l)
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd)
(TSHARED (OATE a1))
:: TEVENT (CPU_ID labd) (TSHARED OPULL)
:: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get 0 (multi_oracle labd) (CPU_ID labd) l2 ++ l2)).
{
eapply relate_ATH_Log_palloc; eauto.
}
exploit H_CalLock_exists; eauto.
intros (n0 & ->).
repeat rewrite ZMap.set2.
refine_split´; eauto.
econstructor; simpl; eauto.
{
eapply lock_gss; eauto.
}
{
constructor; eauto.
- intros.
assert (Hneq: r ≠ 0) by (eapply index2Z_neq; eauto).
repeat rewrite ZMap.gso; eauto.
- repeat rewrite ZMap.gss.
constructor; eauto.
}
{
rewrite ZMap.gss. intros. inv H0. trivial.
}
+ inv HQ. subrewrite´.
repeat rewrite ZMap.gss.
assert (Hcal0: CalAT_log_real
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE 0))
:: ZMap.get 0 (multi_oracle habd) (CPU_ID labd) l ++ l)
= Some a0).
{
inv Hhigh.
unfold valid_AT_log_pool_H in ×.
specialize (valid_AT_log_pool_inv _ Hlog).
unfold valid_AT_oracle_pool_H, valid_AT_oracle_H in ×.
specialize (valid_AT_oracle_pool_inv _ (CPU_ID labd) valid_AT_log_pool_inv).
destruct valid_AT_oracle_pool_inv as (a1 & Hcal).
unfold CalAT_log_real in ×. simpl. unfold lock_AT_start in ×.
rewrite Hcal.
exploit CalAT_eq; eauto.
intros Heq. rewrite Heq; trivial.
}
assert (Hrel´: relate_ATH_Log
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE 0))
:: ZMap.get 0 (multi_oracle habd) (CPU_ID labd) l ++ l)
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd)
(TSHARED (OATE a0))
:: TEVENT (CPU_ID labd) (TSHARED OPULL)
:: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get 0 (multi_oracle labd) (CPU_ID labd) l2 ++ l2)).
{
eapply relate_ATH_Log_palloc; eauto.
}
exploit H_CalLock_exists; eauto.
intros (n0 & ->).
repeat rewrite ZMap.set2.
refine_split´; eauto.
econstructor; simpl; eauto.
{
eapply lock_gss; eauto.
}
{
constructor; eauto.
- intros.
assert (Hneq: r ≠ 0) by (eapply index2Z_neq; eauto).
repeat rewrite ZMap.gso; eauto.
- repeat rewrite ZMap.gss.
constructor; eauto.
}
{
rewrite ZMap.gss. intros. inv H0. trivial.
}
- specialize (AT_log_re0 _ refl_equal).
exploit CalAT_eq_None; eauto.
intros (Hl_nil & Hl2_nil). rewrite Hl_nil, Hl2_nil in ×.
eapply app_eq_nil in Hl_nil; eauto.
destruct Hl_nil as (Hlnil0 & Hlnil1); subst; simpl in ×.
subdestruct_one.
+ unfold CalAT_log_real in AT_log_re0. pose proof AT_log_re0 as AT_log_re1.
inv AT_log_re1. clear H1.
subrewrite´. subdestruct; inv HQ; subrewrite´; repeat rewrite ZMap.gss.
× assert (Hcal0: CalAT_log_real (TEVENT (CPU_ID labd) (TSHARED (OPALLOCE i)) :: nil) =
Some (ZMap.set i (ATValid true ATNorm) (real_AT (ZMap.init ATUndef)))).
{
unfold CalAT_log_real in ×. simpl.
destruct a0 as (Hi & Hget & Hrange).
rewrite zeq_false; [| omega].
rewrite Hget. trivial.
}
assert (Hrel´: relate_ATH_Log
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE i)) :: nil)
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd)
(TSHARED
(OATE
(ZMap.set i (ATValid true ATNorm)
(real_AT (ZMap.init ATUndef)))))
:: TEVENT (CPU_ID labd) (TSHARED OPULL)
:: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: nil)).
{
eapply relate_ATH_Log_palloc; eauto.
}
exploit H_CalLock_exists; eauto.
intros (n0 & ->).
repeat rewrite ZMap.set2.
refine_split´; eauto.
econstructor; simpl; eauto.
{
eapply lock_gss; eauto.
}
{
constructor; eauto.
- intros.
assert (Hneq: r ≠ 0) by (eapply index2Z_neq; eauto).
repeat rewrite ZMap.gso; eauto.
- repeat rewrite ZMap.gss.
constructor; eauto.
}
{
rewrite ZMap.gss. intros. inv H0. trivial.
}
× assert (Hrel´: relate_ATH_Log
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE 0)) :: nil)
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OATE (AT labd)))
:: TEVENT (CPU_ID labd) (TSHARED OPULL)
:: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: nil)).
{
eapply relate_ATH_Log_palloc; eauto.
}
exploit H_CalLock_exists; eauto.
intros (n0 & ->).
repeat rewrite ZMap.set2.
refine_split´; eauto.
econstructor; simpl; eauto.
{
eapply lock_gss; eauto.
}
{
constructor; eauto.
- intros.
assert (Hneq: r ≠ 0) by (eapply index2Z_neq; eauto).
repeat rewrite ZMap.gso; eauto.
- repeat rewrite ZMap.gss.
constructor; eauto.
}
{
rewrite ZMap.gss. intros. inv H0. trivial.
}
+ inv HQ. subrewrite´.
repeat rewrite ZMap.gss.
assert (Hcal0: CalAT_log_real
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE 0)) :: nil)
= Some (AT labd)).
{
rewrite <- AT_log_re0.
unfold CalAT_log_real. simpl. trivial.
}
assert (Hrel´: relate_ATH_Log
(TEVENT (CPU_ID labd) (TSHARED (OPALLOCE 0)) :: nil)
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd)
(TSHARED (OATE (AT labd)))
:: TEVENT (CPU_ID labd) (TSHARED OPULL)
:: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: nil)).
{
eapply relate_ATH_Log_palloc; eauto.
}
exploit H_CalLock_exists; eauto.
intros (n0 & ->).
repeat rewrite ZMap.set2.
refine_split´; eauto.
econstructor; simpl; eauto.
{
eapply lock_gss; eauto.
}
{
constructor; eauto.
- intros.
assert (Hneq: r ≠ 0) by (eapply index2Z_neq; eauto).
repeat rewrite ZMap.gso; eauto.
- repeat rewrite ZMap.gss.
constructor; eauto.
}
{
rewrite ZMap.gss. intros. inv H0. trivial.
}
Qed.
Lemma get_at_c_exist:
∀ habd labd i n f,
get_at_c_spec i habd = Some n
→ relate_RData f habd labd
→ get_at_c_spec i labd = Some n.
Proof.
unfold get_at_c_spec; intros until f; exist_simpl; inv HR´.
Qed.
Lemma set_at_c_exist:
∀ habd habd´ labd i z f,
set_at_c0_spec i z habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, set_at_c0_spec i z labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold set_at_c0_spec; intros until f; exist_simpl; inv HR´.
Qed.
Require Import CalTicketLock.
Lemma real_lock_pb_correct:
∀ n l l´,
(∀ i0,
ZMap.get i0 l = ZMap.get i0 l´) →
(∀ i0,
ZMap.get i0 (real_lock_pb n l) =
ZMap.get i0 (real_lock_pb n l´)).
Proof.
induction n; simpl; eauto. intros.
destruct (zeq i0 (Z.of_nat n)); subst.
- repeat rewrite ZMap.gss; trivial.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_lock_correct:
∀ l l´,
(∀ i0,
ZMap.get i0 l = ZMap.get i0 l´) →
(∀ i0,
ZMap.get i0 (real_lock l) =
ZMap.get i0 (real_lock l´)).
Proof.
intros.
unfold real_lock.
eapply real_lock_pb_correct; eauto.
Qed.
Lemma real_multi_log_pb_correct:
∀ n l l´,
relate_ATH_Log_Pool l l´ →
relate_ATH_Log_Pool (real_multi_log_pb n l) (real_multi_log_pb n l´).
Proof.
induction n; simpl; eauto. intros.
exploit IHn; eauto. intros Hn. inv Hn.
econstructor.
- intros.
destruct (zeq r (Z.of_nat n)); subst.
+ repeat rewrite ZMap.gss; trivial.
+ repeat rewrite ZMap.gso; eauto.
- destruct (zeq 0 (Z.of_nat n)); subst.
+ rewrite e. repeat rewrite ZMap.gss; trivial.
constructor. constructor.
+ repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_multi_log_correct:
∀ l l´,
relate_ATH_Log_Pool l l´ →
relate_ATH_Log_Pool (real_multi_log l) (real_multi_log l´).
Proof.
intros.
unfold real_multi_log.
eapply real_multi_log_pb_correct; eauto.
Qed.
Lemma real_multi_log_0:
∀ l,
ZMap.get 0 (real_multi_log l) = MultiDef nil.
Proof.
intros.
unfold real_multi_log.
change 0 with (Z.of_nat O).
rewrite real_multi_log_pb_in; trivial.
unfold lock_range, ID_AT_range, ID_TCB_range, ID_SC_range.
simpl. xomega.
Qed.
Lemma mem_init_exist:
∀ habd habd´ labd i f
(Hhigh: MALT.high_level_invariant labd),
lmem_init_spec i habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mem_init_spec i labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold mem_init_spec, lmem_init_spec; intros.
revert H. pose proof H0 as HR.
inv H0. subrewrite. simpl.
subdestruct; inv HQ; simpl.
refine_split´; eauto. inv HR.
econstructor; simpl;
match goal with
| |- context[ZMap.get] ⇒ idtac
| _ ⇒ trivial
end.
- eapply real_lock_correct; eauto.
- eapply real_multi_log_correct; eauto.
- intros.
erewrite real_multi_log_0 in H. inv H.
unfold CalAT_log_real. simpl.
inv Hhigh. exploit init_AT; eauto.
intros (Hat & _). rewrite Hat. trivial.
Qed.
Section ACQUIRE_SIM.
Lemma Shared2ID1_neq:
∀ i p,
Shared2ID1 i = Some p →
i ≠ 0.
Proof.
intros. functional inversion H; red; intros HF; inv HF.
Qed.
Lemma acquire_lock_exist:
∀ s i ofs bound habd habd´ labd f p l,
acquire_lock_spec1 bound i ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_lock_spec1 bound i ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ Shared2ID1 i = Some p.
Proof.
unfold acquire_lock_spec; intros.
inv H0. revert H; subrewrite. subdestruct.
- inv HQ.
subrewrite´.
pose proof multi_log_re0 as multi_log_re´.
inv multi_log_re0. exploit Hre_neq; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq. rewrite <- Heq.
rewrite Hdestruct4.
erewrite <- lock_re0. rewrite Hdestruct2.
pose proof multi_oracle_re0 as multi_oracle_re´.
inv multi_oracle_re0. exploit Hrel_o_neq; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq´. rewrite <- Heq´.
rewrite Hdestruct5.
refine_split´; trivial.
econstructor; eauto; simpl.
× intros. destruct (zeq i0 z); subst.
{ repeat rewrite ZMap.gss. trivial. }
{ repeat rewrite ZMap.gso; eauto. }
× econstructor; eauto.
{
intros. exploit Hre_neq; eauto.
destruct (zeq r z); subst.
- repeat rewrite ZMap.gss.
intros Heq1. trivial.
- repeat rewrite ZMap.gso; eauto.
}
{
assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
}
× assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Require Import LAsmModuleSemAux.
Lemma acquire_lock_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem (acquire_lock_spec1))
(id ↦ primcall_acquire_lock_compatsem (acquire_lock_spec1)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_lock_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
simpl. eapply Hst.
econstructor; eauto ; try congruence.
- constructor.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
erewrite Mem.nextblock_storebytes; eauto.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
simpl. trivial.
econstructor; eauto ; try congruence.
-
eapply acquire_lock_match; eauto.
-
subst rs´. val_inject_simpl.
}
Qed.
End ACQUIRE_SIM.
Section RELEASE_SIM.
Lemma release_lock_exist:
∀ s i ofs e habd habd´ labd f,
release_lock_spec1 i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ (∃ labd´, release_lock_spec1 i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´).
Proof.
unfold release_lock_spec; intros.
inv H0. revert H; subrewrite. subdestruct.
inv HQ.
subrewrite´.
pose proof multi_log_re0 as multi_log_re´.
inv multi_log_re0. exploit Hre_neq; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq. rewrite <- Heq.
rewrite Hdestruct3.
erewrite <- lock_re0. rewrite Hdestruct4.
rewrite Hdestruct5.
refine_split´; trivial.
econstructor; eauto; simpl.
- intros. destruct (zeq i0 z); subst.
{ repeat rewrite ZMap.gss. trivial. }
{ repeat rewrite ZMap.gso; eauto. }
- econstructor; eauto.
{
intros. exploit Hre_neq; eauto.
destruct (zeq r z); subst.
- repeat rewrite ZMap.gss.
intros Heq1. trivial.
- repeat rewrite ZMap.gso; eauto.
}
{
assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
}
- assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma release_lock_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_release_lock_compatsem release_lock (release_lock_spec1))
(id ↦ primcall_release_lock_compatsem release_lock (release_lock_spec1)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_lock_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
subst rs´. val_inject_simpl.
Qed.
End RELEASE_SIM.
Section PAGE_COPY_SIM.
Lemma page_copy0_exist:
∀ s habd habd´ labd index i from f,
page_copy0_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy0_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy0_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
subrewrite´.
pose proof multi_log_re0 as multi_log_re´.
inv multi_log_re0. exploit Hre_neq; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
intros Heq. rewrite <- Heq.
rewrite Hdestruct6.
rewrite <- (lock_re0 z).
rewrite Hdestruct7.
exploit page_copy_aux_exists; eauto.
intros.
rewrite H.
rewrite Hdestruct10.
refine_split´; try trivial.
econstructor; simpl; auto.
rewrite ikern_re0; auto.
rewrite ihost_re0; auto.
- constructor; intros.
intros. destruct (zeq r z); subst.
{ repeat rewrite ZMap.gss; auto. }
{ repeat rewrite ZMap.gso; eauto. }
{
assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
}
- assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy0_match:
∀ s d d´ m index i from f,
page_copy0_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy0_spec; intros.
subdestruct.
inv H. inv H0.
econstructor; eauto.
Qed.
Lemma page_copy0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy0_spec)
(id ↦ gensem page_copy0_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy0_exist; eauto 1.
exploit page_copy0_match; eauto 1.
intros.
destruct H0 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Lemma page_copy_back0_exist:
∀ s habd habd´ labd index i to f,
page_copy_back0_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back0_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back0_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
subrewrite´.
pose proof multi_log_re0 as multi_log_re´.
inv multi_log_re0. exploit Hre_neq; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
intros Heq. rewrite <- Heq.
rewrite Hdestruct6.
rewrite Hdestruct7.
exploit page_copy_back_aux_exists; eauto.
intros.
destruct H as (lh´ & H & Hrel).
rewrite H.
refine_split´; try trivial.
econstructor; simpl; auto.
rewrite ikern_re0; auto.
rewrite ihost_re0; auto.
Qed.
Lemma page_copy_back´0_match:
∀ s d d´ m index i to f,
page_copy_back0_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back0_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_back0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back0_spec)
(id ↦ gensem page_copy_back0_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy_back0_exist; eauto 1.
exploit page_copy_back0_match; eauto 1.
intros.
destruct H0 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
End PAGE_COPY_BACK_SIM.
Lemma passthrough_correct:
sim (crel RData RData) malh malt.
Proof.
sim_oplus.
- apply fload´_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit fstore_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
- apply page_copy0_sim.
- apply page_copy_back0_sim.
- apply vmxinfo_get_sim.
- apply setPG0_sim.
- apply setCR30_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
match_external_states_simpl.
erewrite get_at_c_exist; eauto.
reflexivity.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit set_at_c_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
-
layer_sim_simpl.
constructor.
split; simpl in *; trivial; repeat constructor.
intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2
HWB _ Hlow Hhigh Hhigh´ H Hι Hmd.
compatsim_simpl_inv_match H Hmd (@match_AbData).
exploit mem_init_exist; eauto 1; intros [labd´ [HP HM]].
refine_split;
match goal with
| |- inject_incr ?f _ ⇒ apply inject_incr_refl
| |- val_inject _ _ _ ⇒ econstructor
| _ ⇒ idtac
end.
+ econstructor.
econstructor.
econstructor. eapply HP.
+ econstructor; eauto. constructor.
- apply container_get_parent_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply container_split_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply release_lock_sim.
- apply acquire_lock_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply trapin_sim.
- apply trapout0_sim.
- apply hostin_sim.
- apply hostout_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End PASSTHROUGH_RPIM.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.