Library mcertikos.ticketlog.HTicketLockOpGen
This file provide the contextual refinement proof between MALInit layer and MALOp 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 AbstractDataType.
Require Import LAsmModuleSemAux.
Require Import TacticsForTesting.
Require Import DeviceStateDataType.
Require Import CalTicketLock.
Require Import ListLemma2.
Require Import StarvationFreedomTicketLock.
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 AbstractDataType.
Require Import LAsmModuleSemAux.
Require Import TacticsForTesting.
Require Import DeviceStateDataType.
Require Import CalTicketLock.
Require Import ListLemma2.
Require Import StarvationFreedomTicketLock.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mqticketlockop_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mqticketlockop_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
MM_re: MM hadt = MM ladt;
MMSize_re: MMSize hadt = MMSize 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;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
init_re: init hadt = init ladt;
buffer_re: buffer hadt = buffer ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
ticket_oracle_re: relate_ticket_oracle_pool (multi_oracle hadt) (multi_oracle ladt);
ticket_log_re: relate_ticket_log_pool (multi_log hadt) (multi_log ladt);
lock_re: lock hadt = lock ladt;
com1_re: com1 ladt = com1 hadt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
saved_intr_flags_re: saved_intr_flags ladt = saved_intr_flags hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr hadt = in_intr ladt;
tf_re: tfs_inj f (tf hadt) (tf ladt)
}.
Inductive match_RData: stencil → HDATA → 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);
MM_re: MM hadt = MM ladt;
MMSize_re: MMSize hadt = MMSize 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;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
init_re: init hadt = init ladt;
buffer_re: buffer hadt = buffer ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
ticket_oracle_re: relate_ticket_oracle_pool (multi_oracle hadt) (multi_oracle ladt);
ticket_log_re: relate_ticket_log_pool (multi_log hadt) (multi_log ladt);
lock_re: lock hadt = lock ladt;
com1_re: com1 ladt = com1 hadt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
saved_intr_flags_re: saved_intr_flags ladt = saved_intr_flags hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr hadt = in_intr ladt;
tf_re: tfs_inj f (tf hadt) (tf ladt)
}.
Inductive match_RData: stencil → HDATA → 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.
eapply tfs_inj_incr; 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.
eapply tfs_inj_incr; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
eapply relate_incr; eauto.
Qed.
End Rel_Property.
Section OneStep_Forward_Relation.
Section FRESH_PRIM.
Lemma wait_lock_exist:
∀ habd habd´ labd bound n ofs f
(Hhigh: MQTicketLockOp.high_level_invariant labd),
wait_hlock_spec bound n ofs habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, wait_qlock_spec bound n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold wait_hlock_spec, wait_qlock_spec; intros until f. intro.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
subrewrite´.
intros HQ; subdestruct; inv HQ.
inv ticket_log_re0. specialize (Hrelate_ticket_log_type _ _ _ Hdestruct1).
rewrite Hdestruct3 in Hrelate_ticket_log_type. inv Hrelate_ticket_log_type.
assert (He: ∃ x,
Q_CalLock
(TEVENT (CPU_ID labd)
(TTICKET (INC_TICKET (Z.to_nat bound)))
:: ZMap.get z (multi_oracle labd)
(CPU_ID labd) l0 ++ l0) = Some x).
{
exploit MQTicketLockOp.valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
eapply Q_CalLock_INC_TICKET_exists´; eauto.
- eapply MQTicketLockOp.valid_multi_oracle_pool_inv; eauto.
- eapply valid_last_pool_inv; eauto.
- eapply valid_last_pool_inv; eauto.
- exploit valid_qlock_pool_status_inv; eauto. rewrite Hdestruct2.
intros (HP &_). eapply HP. trivial.
}
destruct He as (x & HCal).
destruct x as ((((self_c, other_c), b), q), tq0).
rewrite HCal.
Local Transparent Q_CalLock.
assert (Heq: ∃ q´ tq0´,
q = q´ ++ ((CPU_ID labd)) :: nil
∧ tq0 = tq0´ ++ ((Z.to_nat bound)) :: nil
∧ ¬ In (CPU_ID labd) q´
∧ ∃ lother_c lb,
Q_CalLock (ZMap.get z (multi_oracle labd)(CPU_ID labd) l0 ++ l0)
= Some (self_c, lother_c, lb, q´, tq0´)).
{
simpl in HCal.
subdestruct; inv HCal.
- ∃ nil, nil.
refine_split´; trivial.
simpl. intros HF; inv HF.
- ∃ (z0 :: l4), (n0 :: l2).
refine_split´; trivial.
intros HF. inv HF.
+ elim n3. trivial.
+ elim n4; trivial.
}
Local Opaque Q_CalLock.
destruct Heq as (q´ & tq0´ & ? & ? & Hnotin & Hlcal); subst.
assert (He: ∃ l´,
Q_CalWait (CalWaitTime (tq0´ ++ Z.to_nat bound :: nil)) (CPU_ID labd)
(TEVENT (CPU_ID labd)
(TTICKET (INC_TICKET (Z.to_nat bound)))
:: ZMap.get z (multi_oracle labd)
(CPU_ID labd) l0 ++ l0)
(ZMap.get z (multi_oracle labd)) = Some l´).
{
eapply starvation_freedom; eauto.
- eapply Q_CalLock_q_length_same in HCal.
repeat rewrite app_length in HCal. simpl in HCal. xomega.
- unfold CalWaitTime.
eapply decrease_number_lt_Wait; eauto.
+ eapply Q_CalLock_other_c; eauto.
+ destruct Hlcal as (lother_c & lb & Hlcal).
eapply Q_CalLock_self_c; eauto.
- eapply MQTicketLockOp.valid_multi_oracle_pool_inv; eauto.
- destruct Hlcal as (lother_c & lb & Hlcal).
eapply Q_CalLock_INC_TICKET_status; eauto.
- intros. inv H0.
+ inv H1. eapply MQTicketLockOp.CPU_ID_range; eauto.
+ eapply in_app_or in H1. inv H1.
× eapply MQTicketLockOp.valid_multi_oracle_pool_inv; eauto.
× eapply MQTicketLockOp.valid_last_pool_inv; eauto.
- eapply MQTicketLockOp.CPU_ID_range; eauto.
}
destruct He as (l´ & HWait).
rewrite HWait.
inv ticket_oracle_re0. specialize (Hrelate_ticket_oracle _ _ _ Hdestruct1).
pose proof Hrelate_ticket_oracle as Hrelate_ticket_oracle´.
inv Hrelate_ticket_oracle.
specialize (Hrelate_ticket_oracle_res (CPU_ID labd) _ _ _ _ Hrelate_ticket_log
_ _ _ _ _ _ HCal HWait).
destruct Hrelate_ticket_oracle_res as (tq´ & Hrelate).
assert (He: ∃ tq0´, tq´ = (Z.to_nat bound) :: tq0´).
{
exploit Q_CalLock_q_length_same; eauto. intros Hlen.
repeat rewrite app_length in Hlen. simpl in Hlen.
exploit CalWait_exists; eauto.
intros (self_c0 & other_c0 & q & tq0 & HCal1).
exploit Q_CalLock_relate_log_eq; eauto. intro; subst.
exploit CalWait_exists_log; eauto.
{ eapply MQTicketLockOp.valid_multi_oracle_pool_inv; eauto. }
intros (l´0 & ? & Hp); subst.
rewrite <- (app_nil_l ((CPU_ID labd) :: q)) in HCal1.
exploit CalLock_length; try eapply HCal; eauto.
{ omega. }
intros (tq´ & tq1 & Heq & Hlen1); subst.
destruct tq´.
- refine_split´; simpl; trivial.
- inv Hlen1.
}
destruct He as (tq0´´ & He); subst.
assert (Hhold:
∃ x, Q_CalLock (TEVENT (CPU_ID labd) (TTICKET HOLD_LOCK) :: l´) = Some x).
{
eapply Q_CalLock_HOLD_LOCK_exists; eauto.
}
destruct Hhold as (x & ->).
refine_split´; trivial.
constructor; simpl; inv HR´; try eassumption; trivial.
eapply relate_ticket_log_pool_gss; eauto.
econstructor; trivial.
simpl. rewrite Hrelate. trivial.
Qed.
Lemma wait_lock_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem wait_hlock_spec)
(id ↦ gensem wait_qlock_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit wait_lock_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
Lemma pass_lock_exist:
∀ habd habd´ labd n ofs f
(Hhigh: MQTicketLockOp.high_level_invariant labd),
pass_hlock_spec n ofs habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, pass_qlock_spec n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold pass_hlock_spec, pass_qlock_spec; intros until f. intro.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
subrewrite´.
intros HQ; subdestruct; inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct1).
rewrite Hdestruct2 in Hrelate_ticket_log_type. inv Hrelate_ticket_log_type.
assert (He: ∃ x,
Q_CalLock (TEVENT (CPU_ID labd) (TTICKET INC_NOW) :: l0) = Some x).
{
exploit MQTicketLockOp.valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
exploit valid_qlock_pool_status_inv; eauto. rewrite Hdestruct4.
intros (_ & HP). specialize (HP _ eq_refl).
destruct HP as (q´ & HP & Hhold & Hnin); subst.
eapply Q_CalLock_INC_NOW_exists; eauto.
}
destruct He as (x & Hcal).
rewrite Hcal.
refine_split´; simpl; trivial.
constructor; simpl; inv HR´; trivial.
destruct x as ((((self_c, other_c), b), q), tq0).
eapply Q_CalLock_relate_log_exists in Hcal.
destruct Hcal as (l´ & Hcal).
eapply relate_ticket_log_pool_REL; eauto.
Qed.
Lemma pass_lock_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem pass_hlock_spec)
(id ↦ gensem pass_qlock_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pass_lock_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
Lemma acquire_shared_exist:
∀ habd habd´ labd (Hhigh: MQTicketLockOp.high_level_invariant labd)
n ofs i l f,
acquire_shared_spec0 n ofs habd = Some (habd´, i, l)
→ relate_RData f habd labd
→ ∃ labd´, acquire_shared1_spec0 n ofs labd = Some (labd´, i, l) ∧ relate_RData f habd´ labd´
∧ Shared2ID0 n = Some i.
Proof.
unfold acquire_shared_spec, acquire_shared1_spec. intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
d8 subdestruct_one. inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct1).
rewrite Hdestruct5 in Hrelate_ticket_log_type.
inv Hrelate_ticket_log_type.
exploit relate_log_shared; eauto.
intros Heq. rewrite <- Heq. clear Heq.
inv Hhigh.
exploit valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
assert (Hs: ∃ x, Q_CalLock (TEVENT (CPU_ID labd) (TSHARED OPULL) :: l) = Some x).
{
destruct p0. destruct p.
eapply Q_CalLock_TSHARED_exists; eauto.
}
destruct Hs as (x & ->).
exploit cal_qlock_pool_status_inv; eauto.
rewrite Hdestruct3. intros (Hvalid &_).
rewrite Hvalid; trivial.
refine_split; eauto.
inv HR´; constructor; eauto. simpl.
eapply relate_ticket_log_pool_shared; eauto.
Qed.
Lemma acquire_shared_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_shared_compatsem acquire_shared_spec0)
(id ↦ primcall_acquire_shared_compatsem acquire_shared1_spec0).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_shared_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; eauto.
econstructor; eauto ; try congruence.
-
constructor.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. red; intros. inv H.
-
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; eauto.
econstructor; eauto ; try congruence.
-
constructor.
-
subst rs´.
val_inject_simpl.
}
Qed.
Lemma release_shared_exist:
∀ habd habd´ labd n ofs e f
(Hhigh: MQTicketLockOp.high_level_invariant labd),
release_shared_spec0 n ofs e habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, release_shared1_spec0 n ofs e labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold release_shared_spec, release_shared1_spec. intros until f. intro.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct. inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct2).
rewrite Hdestruct5 in Hrelate_ticket_log_type.
inv Hrelate_ticket_log_type.
exploit MQTicketLockOp.valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
repeat destruct p0.
assert (Hs: ∃ x, Q_CalLock (TEVENT (CPU_ID labd) (TSHARED (OMEME e)) :: l0) = Some x).
{
eapply Q_CalLock_TSHARED_exists; eauto.
}
destruct Hs as (x & ->).
exploit cal_qlock_pool_status_inv; eauto.
rewrite Hdestruct3. intros (_ & Hvalid).
rewrite Hvalid; trivial. rewrite zeq_true.
refine_split; eauto.
inv HR´; constructor; eauto. simpl.
eapply relate_ticket_log_pool_shared; eauto.
Qed.
Lemma release_shared_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_release_lock_compatsem id release_shared_spec0)
(id ↦ primcall_release_lock_compatsem id release_shared1_spec0).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_shared_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;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; try eapply H7; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
- 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 ; try congruence.
constructor.
-
subst rs´.
val_inject_simpl.
Qed.
Lemma relate_log_buffer:
∀ l1 l0 tq
(Hre: HTicketLockOpGenDef.relate_log l1 = Some (l0, tq)),
GetSharedBuffer l0 = GetSharedBuffer l1.
Proof.
induction l1; simpl; intros.
- inv Hre. trivial.
- subdestruct; inv Hre; simpl; eauto.
destruct e0; eauto.
Qed.
Lemma page_copy_exist:
∀ s habd habd´ labd (Hhigh: MQTicketLockOp.high_level_invariant labd)
index i from f,
page_copy´_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy´´_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy´´_spec, page_copy´_spec.
intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
d11 subdestruct_one. inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct4).
rewrite Hdestruct5 in Hrelate_ticket_log_type.
inv Hrelate_ticket_log_type.
exploit page_copy_aux_exists; eauto.
intros HCopy´.
rewrite HCopy´.
inv Hhigh.
exploit valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
assert (Hs: ∃ x, Q_CalLock (TEVENT (CPU_ID labd) (TSHARED (OBUFFERE l0)) :: l1) = Some x).
{
destruct p. destruct p.
eapply Q_CalLock_TSHARED_exists; eauto.
}
destruct Hs as (x & ->).
refine_split; eauto.
inv HR´; constructor; eauto. simpl.
eapply relate_ticket_log_pool_shared; eauto.
Qed.
Lemma page_copy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy´_spec)
(id ↦ gensem page_copy´´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_exist; eauto 1. intros [labd´ [HP HM]].
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.
- repeat econstructor; eauto ; try congruence.
- constructor.
Qed.
Lemma page_copy_back_exist:
∀ s habd habd´ labd (Hhigh: MQTicketLockOp.high_level_invariant labd)
index i to f,
page_copy_back´_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back´_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back´_spec.
intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct. inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct4).
rewrite Hdestruct5 in Hrelate_ticket_log_type.
inv Hrelate_ticket_log_type.
exploit relate_log_buffer; eauto.
intros Heq. rewrite <- Heq. clear Heq. rewrite Hdestruct6.
exploit page_copy_back_aux_exists; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´.
refine_split; eauto.
inv HR´; constructor; eauto.
Qed.
Lemma page_copy_back_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back´_spec)
(id ↦ gensem page_copy_back´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_back_exist; eauto 1. intros [labd´ [HP HM]].
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.
- repeat econstructor; eauto ; try congruence.
- constructor.
Qed.
Lemma ticket_lock_init_exist:
∀ habd habd´ labd n f,
ticket_lock_init0_spec n habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, ticket_lock_init0_spec n labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold ticket_lock_init0_spec; intros until f; exist_simpl.
eapply real_ticket_relate; eauto.
Qed.
Lemma ticket_lock_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ticket_lock_init0_spec)
(id ↦ gensem ticket_lock_init0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ticket_lock_init_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End FRESH_PRIM.
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 passthrough_correct:
sim (crel HDATA LDATA) mhticketlockop mqticketlockop.
Proof.
unfold mhticketlockop.
unfold mhticketlockop_fresh.
unfold mqticketlockop.
unfold mqticketlockop_fresh.
eapply oplus_sim_monotonic.
eapply lower_bound.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy_sim.
- apply page_copy_back_sim.
- apply vmxinfo_get_sim.
- apply setPG_sim.
- apply setCR3_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
- apply get_CPU_ID_sim.
- apply release_shared_sim.
- apply acquire_shared_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply ticket_lock_init_sim.
- apply pass_lock_sim.
- apply wait_lock_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply serial_irq_check_sim.
- apply iret_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_irq_current_sim.
- apply ic_intr_sim.
- apply save_context_sim.
- apply restore_context_sim.
- apply local_irq_save_sim.
- apply local_irq_restore_sim.
- apply serial_in_sim.
- apply serial_out_sim.
- apply serial_hw_intr_sim.
- apply ioapic_read_sim.
- apply ioapic_write_sim.
- apply lapic_read_sim.
- apply lapic_write_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End PASSTHROUGH_RPIM.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.
Section FRESH_PRIM.
Lemma wait_lock_exist:
∀ habd habd´ labd bound n ofs f
(Hhigh: MQTicketLockOp.high_level_invariant labd),
wait_hlock_spec bound n ofs habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, wait_qlock_spec bound n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold wait_hlock_spec, wait_qlock_spec; intros until f. intro.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
subrewrite´.
intros HQ; subdestruct; inv HQ.
inv ticket_log_re0. specialize (Hrelate_ticket_log_type _ _ _ Hdestruct1).
rewrite Hdestruct3 in Hrelate_ticket_log_type. inv Hrelate_ticket_log_type.
assert (He: ∃ x,
Q_CalLock
(TEVENT (CPU_ID labd)
(TTICKET (INC_TICKET (Z.to_nat bound)))
:: ZMap.get z (multi_oracle labd)
(CPU_ID labd) l0 ++ l0) = Some x).
{
exploit MQTicketLockOp.valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
eapply Q_CalLock_INC_TICKET_exists´; eauto.
- eapply MQTicketLockOp.valid_multi_oracle_pool_inv; eauto.
- eapply valid_last_pool_inv; eauto.
- eapply valid_last_pool_inv; eauto.
- exploit valid_qlock_pool_status_inv; eauto. rewrite Hdestruct2.
intros (HP &_). eapply HP. trivial.
}
destruct He as (x & HCal).
destruct x as ((((self_c, other_c), b), q), tq0).
rewrite HCal.
Local Transparent Q_CalLock.
assert (Heq: ∃ q´ tq0´,
q = q´ ++ ((CPU_ID labd)) :: nil
∧ tq0 = tq0´ ++ ((Z.to_nat bound)) :: nil
∧ ¬ In (CPU_ID labd) q´
∧ ∃ lother_c lb,
Q_CalLock (ZMap.get z (multi_oracle labd)(CPU_ID labd) l0 ++ l0)
= Some (self_c, lother_c, lb, q´, tq0´)).
{
simpl in HCal.
subdestruct; inv HCal.
- ∃ nil, nil.
refine_split´; trivial.
simpl. intros HF; inv HF.
- ∃ (z0 :: l4), (n0 :: l2).
refine_split´; trivial.
intros HF. inv HF.
+ elim n3. trivial.
+ elim n4; trivial.
}
Local Opaque Q_CalLock.
destruct Heq as (q´ & tq0´ & ? & ? & Hnotin & Hlcal); subst.
assert (He: ∃ l´,
Q_CalWait (CalWaitTime (tq0´ ++ Z.to_nat bound :: nil)) (CPU_ID labd)
(TEVENT (CPU_ID labd)
(TTICKET (INC_TICKET (Z.to_nat bound)))
:: ZMap.get z (multi_oracle labd)
(CPU_ID labd) l0 ++ l0)
(ZMap.get z (multi_oracle labd)) = Some l´).
{
eapply starvation_freedom; eauto.
- eapply Q_CalLock_q_length_same in HCal.
repeat rewrite app_length in HCal. simpl in HCal. xomega.
- unfold CalWaitTime.
eapply decrease_number_lt_Wait; eauto.
+ eapply Q_CalLock_other_c; eauto.
+ destruct Hlcal as (lother_c & lb & Hlcal).
eapply Q_CalLock_self_c; eauto.
- eapply MQTicketLockOp.valid_multi_oracle_pool_inv; eauto.
- destruct Hlcal as (lother_c & lb & Hlcal).
eapply Q_CalLock_INC_TICKET_status; eauto.
- intros. inv H0.
+ inv H1. eapply MQTicketLockOp.CPU_ID_range; eauto.
+ eapply in_app_or in H1. inv H1.
× eapply MQTicketLockOp.valid_multi_oracle_pool_inv; eauto.
× eapply MQTicketLockOp.valid_last_pool_inv; eauto.
- eapply MQTicketLockOp.CPU_ID_range; eauto.
}
destruct He as (l´ & HWait).
rewrite HWait.
inv ticket_oracle_re0. specialize (Hrelate_ticket_oracle _ _ _ Hdestruct1).
pose proof Hrelate_ticket_oracle as Hrelate_ticket_oracle´.
inv Hrelate_ticket_oracle.
specialize (Hrelate_ticket_oracle_res (CPU_ID labd) _ _ _ _ Hrelate_ticket_log
_ _ _ _ _ _ HCal HWait).
destruct Hrelate_ticket_oracle_res as (tq´ & Hrelate).
assert (He: ∃ tq0´, tq´ = (Z.to_nat bound) :: tq0´).
{
exploit Q_CalLock_q_length_same; eauto. intros Hlen.
repeat rewrite app_length in Hlen. simpl in Hlen.
exploit CalWait_exists; eauto.
intros (self_c0 & other_c0 & q & tq0 & HCal1).
exploit Q_CalLock_relate_log_eq; eauto. intro; subst.
exploit CalWait_exists_log; eauto.
{ eapply MQTicketLockOp.valid_multi_oracle_pool_inv; eauto. }
intros (l´0 & ? & Hp); subst.
rewrite <- (app_nil_l ((CPU_ID labd) :: q)) in HCal1.
exploit CalLock_length; try eapply HCal; eauto.
{ omega. }
intros (tq´ & tq1 & Heq & Hlen1); subst.
destruct tq´.
- refine_split´; simpl; trivial.
- inv Hlen1.
}
destruct He as (tq0´´ & He); subst.
assert (Hhold:
∃ x, Q_CalLock (TEVENT (CPU_ID labd) (TTICKET HOLD_LOCK) :: l´) = Some x).
{
eapply Q_CalLock_HOLD_LOCK_exists; eauto.
}
destruct Hhold as (x & ->).
refine_split´; trivial.
constructor; simpl; inv HR´; try eassumption; trivial.
eapply relate_ticket_log_pool_gss; eauto.
econstructor; trivial.
simpl. rewrite Hrelate. trivial.
Qed.
Lemma wait_lock_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem wait_hlock_spec)
(id ↦ gensem wait_qlock_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit wait_lock_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
Lemma pass_lock_exist:
∀ habd habd´ labd n ofs f
(Hhigh: MQTicketLockOp.high_level_invariant labd),
pass_hlock_spec n ofs habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, pass_qlock_spec n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold pass_hlock_spec, pass_qlock_spec; intros until f. intro.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
subrewrite´.
intros HQ; subdestruct; inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct1).
rewrite Hdestruct2 in Hrelate_ticket_log_type. inv Hrelate_ticket_log_type.
assert (He: ∃ x,
Q_CalLock (TEVENT (CPU_ID labd) (TTICKET INC_NOW) :: l0) = Some x).
{
exploit MQTicketLockOp.valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
exploit valid_qlock_pool_status_inv; eauto. rewrite Hdestruct4.
intros (_ & HP). specialize (HP _ eq_refl).
destruct HP as (q´ & HP & Hhold & Hnin); subst.
eapply Q_CalLock_INC_NOW_exists; eauto.
}
destruct He as (x & Hcal).
rewrite Hcal.
refine_split´; simpl; trivial.
constructor; simpl; inv HR´; trivial.
destruct x as ((((self_c, other_c), b), q), tq0).
eapply Q_CalLock_relate_log_exists in Hcal.
destruct Hcal as (l´ & Hcal).
eapply relate_ticket_log_pool_REL; eauto.
Qed.
Lemma pass_lock_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem pass_hlock_spec)
(id ↦ gensem pass_qlock_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pass_lock_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
Lemma acquire_shared_exist:
∀ habd habd´ labd (Hhigh: MQTicketLockOp.high_level_invariant labd)
n ofs i l f,
acquire_shared_spec0 n ofs habd = Some (habd´, i, l)
→ relate_RData f habd labd
→ ∃ labd´, acquire_shared1_spec0 n ofs labd = Some (labd´, i, l) ∧ relate_RData f habd´ labd´
∧ Shared2ID0 n = Some i.
Proof.
unfold acquire_shared_spec, acquire_shared1_spec. intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
d8 subdestruct_one. inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct1).
rewrite Hdestruct5 in Hrelate_ticket_log_type.
inv Hrelate_ticket_log_type.
exploit relate_log_shared; eauto.
intros Heq. rewrite <- Heq. clear Heq.
inv Hhigh.
exploit valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
assert (Hs: ∃ x, Q_CalLock (TEVENT (CPU_ID labd) (TSHARED OPULL) :: l) = Some x).
{
destruct p0. destruct p.
eapply Q_CalLock_TSHARED_exists; eauto.
}
destruct Hs as (x & ->).
exploit cal_qlock_pool_status_inv; eauto.
rewrite Hdestruct3. intros (Hvalid &_).
rewrite Hvalid; trivial.
refine_split; eauto.
inv HR´; constructor; eauto. simpl.
eapply relate_ticket_log_pool_shared; eauto.
Qed.
Lemma acquire_shared_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_shared_compatsem acquire_shared_spec0)
(id ↦ primcall_acquire_shared_compatsem acquire_shared1_spec0).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_shared_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; eauto.
econstructor; eauto ; try congruence.
-
constructor.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. red; intros. inv H.
-
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; eauto.
econstructor; eauto ; try congruence.
-
constructor.
-
subst rs´.
val_inject_simpl.
}
Qed.
Lemma release_shared_exist:
∀ habd habd´ labd n ofs e f
(Hhigh: MQTicketLockOp.high_level_invariant labd),
release_shared_spec0 n ofs e habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, release_shared1_spec0 n ofs e labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold release_shared_spec, release_shared1_spec. intros until f. intro.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct. inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct2).
rewrite Hdestruct5 in Hrelate_ticket_log_type.
inv Hrelate_ticket_log_type.
exploit MQTicketLockOp.valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
repeat destruct p0.
assert (Hs: ∃ x, Q_CalLock (TEVENT (CPU_ID labd) (TSHARED (OMEME e)) :: l0) = Some x).
{
eapply Q_CalLock_TSHARED_exists; eauto.
}
destruct Hs as (x & ->).
exploit cal_qlock_pool_status_inv; eauto.
rewrite Hdestruct3. intros (_ & Hvalid).
rewrite Hvalid; trivial. rewrite zeq_true.
refine_split; eauto.
inv HR´; constructor; eauto. simpl.
eapply relate_ticket_log_pool_shared; eauto.
Qed.
Lemma release_shared_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_release_lock_compatsem id release_shared_spec0)
(id ↦ primcall_release_lock_compatsem id release_shared1_spec0).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_shared_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;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; try eapply H7; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
- 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 ; try congruence.
constructor.
-
subst rs´.
val_inject_simpl.
Qed.
Lemma relate_log_buffer:
∀ l1 l0 tq
(Hre: HTicketLockOpGenDef.relate_log l1 = Some (l0, tq)),
GetSharedBuffer l0 = GetSharedBuffer l1.
Proof.
induction l1; simpl; intros.
- inv Hre. trivial.
- subdestruct; inv Hre; simpl; eauto.
destruct e0; eauto.
Qed.
Lemma page_copy_exist:
∀ s habd habd´ labd (Hhigh: MQTicketLockOp.high_level_invariant labd)
index i from f,
page_copy´_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy´´_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy´´_spec, page_copy´_spec.
intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
d11 subdestruct_one. inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct4).
rewrite Hdestruct5 in Hrelate_ticket_log_type.
inv Hrelate_ticket_log_type.
exploit page_copy_aux_exists; eauto.
intros HCopy´.
rewrite HCopy´.
inv Hhigh.
exploit valid_qlock_pool_inv; eauto.
unfold valid_qlock.
intros (self_c & other_c & b & q & tq0 & Hcal).
assert (Hs: ∃ x, Q_CalLock (TEVENT (CPU_ID labd) (TSHARED (OBUFFERE l0)) :: l1) = Some x).
{
destruct p. destruct p.
eapply Q_CalLock_TSHARED_exists; eauto.
}
destruct Hs as (x & ->).
refine_split; eauto.
inv HR´; constructor; eauto. simpl.
eapply relate_ticket_log_pool_shared; eauto.
Qed.
Lemma page_copy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy´_spec)
(id ↦ gensem page_copy´´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_exist; eauto 1. intros [labd´ [HP HM]].
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.
- repeat econstructor; eauto ; try congruence.
- constructor.
Qed.
Lemma page_copy_back_exist:
∀ s habd habd´ labd (Hhigh: MQTicketLockOp.high_level_invariant labd)
index i to f,
page_copy_back´_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back´_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back´_spec.
intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct. inv HQ.
inv ticket_log_re0.
specialize (Hrelate_ticket_log_type _ _ _ Hdestruct4).
rewrite Hdestruct5 in Hrelate_ticket_log_type.
inv Hrelate_ticket_log_type.
exploit relate_log_buffer; eauto.
intros Heq. rewrite <- Heq. clear Heq. rewrite Hdestruct6.
exploit page_copy_back_aux_exists; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´.
refine_split; eauto.
inv HR´; constructor; eauto.
Qed.
Lemma page_copy_back_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back´_spec)
(id ↦ gensem page_copy_back´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_back_exist; eauto 1. intros [labd´ [HP HM]].
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.
- repeat econstructor; eauto ; try congruence.
- constructor.
Qed.
Lemma ticket_lock_init_exist:
∀ habd habd´ labd n f,
ticket_lock_init0_spec n habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, ticket_lock_init0_spec n labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold ticket_lock_init0_spec; intros until f; exist_simpl.
eapply real_ticket_relate; eauto.
Qed.
Lemma ticket_lock_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ticket_lock_init0_spec)
(id ↦ gensem ticket_lock_init0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ticket_lock_init_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End FRESH_PRIM.
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 passthrough_correct:
sim (crel HDATA LDATA) mhticketlockop mqticketlockop.
Proof.
unfold mhticketlockop.
unfold mhticketlockop_fresh.
unfold mqticketlockop.
unfold mqticketlockop_fresh.
eapply oplus_sim_monotonic.
eapply lower_bound.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy_sim.
- apply page_copy_back_sim.
- apply vmxinfo_get_sim.
- apply setPG_sim.
- apply setCR3_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
- apply get_CPU_ID_sim.
- apply release_shared_sim.
- apply acquire_shared_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply ticket_lock_init_sim.
- apply pass_lock_sim.
- apply wait_lock_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply serial_irq_check_sim.
- apply iret_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_irq_current_sim.
- apply ic_intr_sim.
- apply save_context_sim.
- apply restore_context_sim.
- apply local_irq_save_sim.
- apply local_irq_restore_sim.
- apply serial_in_sim.
- apply serial_out_sim.
- apply serial_hw_intr_sim.
- apply ioapic_read_sim.
- apply ioapic_write_sim.
- apply lapic_read_sim.
- apply lapic_write_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End PASSTHROUGH_RPIM.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.