Library mcertikos.mcslock.MCSLockIntroGenPassthrough
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Section Refinement.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section release_sahred0_sim.
Lemma release_shared0_match:
∀ s i ofs e d d´ m f,
release_shared0_spec0 i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_shared0_spec; intros. subdestruct.
inv H. inv H0; constructor; simpl.
inv Hlog. econstructor; eauto.
intros.
destruct (zeq z lock_index); subst.
- rewrite ZMap.gss.
specialize (HMCSLock _ Hvalid).
mcslock_destruct HMCSLock.
refine_split; eauto.
rewrite Hdestruct3 in Hm.
inv Hm.
econstructor; eauto.
Transparent CalMCSLock.
simpl.
rewrite Hcal; auto.
- rewrite ZMap.gso; auto.
Qed.
Lemma release_shared0_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id (release_shared0_spec0))
(id ↦ primcall_release_lock_compatsem id (release_shared0_spec0)).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit (release_shared0_exist (valid_arg:= Shared2ID0)); 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.
eapply release_shared0_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
End release_sahred0_sim.
Section PAGE_COPY_SIM.
Lemma page_copy´´´_match:
∀ s d d´ m index i from f,
page_copy´´´_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy´´´_spec; intros.
subdestruct; inv H.
inv H0. constructor. simpl.
inv Hlog. econstructor; eauto.
intros.
destruct (zeq z lock_index); subst.
- rewrite ZMap.gss.
specialize (HMCSLock _ Hvalid).
mcslock_destruct HMCSLock.
refine_split; eauto.
rewrite Hdestruct5 in Hm.
inv Hm.
econstructor; eauto.
Transparent CalMCSLock.
simpl.
rewrite Hcal; auto.
- rewrite ZMap.gso; auto.
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.
-
eapply page_copy´´´_match; eauto.
Qed.
End PAGE_COPY_SIM.
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) mmcslockintro_passthrough mcurid.
Proof.
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 bootloader0_sim.
- apply get_CPU_ID_sim.
- apply release_shared0_sim.
- assert (Hp: match_impl_multi_log_one acquire_shared0_log_update_match_mcs).
{
constructor.
intros.
destruct H.
destruct Hlog.
constructor.
econstructor; eauto.
intros.
generalize (HMCSLock _ Hvalid).
intros HMCSLock´.
mcslock_destruct HMCSLock´.
destruct (Decision.decide (lock_index = z)); subst.
- inv Hm.
+ rewrite H0 in H2; inv H2.
+ simpl.
rewrite ZMap.gss.
rewrite H0 in H2; clear H0.
inversion H2; clear H2; subst.
exploit H1; eauto; intros.
destruct H as (la´ & np´ & tq´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ & bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ & Hcal´ & Ha1 & Ha2 & Ha3 & Ha4 & Ha5 & Ha6 & Ha7 & Ha8 & ?).
destruct H as (Hb1 & Hb2 & Hb3 & Hb4 & Hb5 & Hb6 & Hb7 & Hb8 & Hb9 & Hb10 & Hb11 & Hb12 & Hb13 & Hb14 & Hb15 & Hb16 & Hb17).
∃ (Vint (Int.repr la´)), (Vint (Int.repr (BooltoZ bs0´))), (Vint (Int.repr ne0´)), (Vint (Int.repr (BooltoZ bs1´))), (Vint (Int.repr ne1´)), (Vint (Int.repr (BooltoZ bs2´))), (Vint (Int.repr ne2´)), (Vint (Int.repr (BooltoZ bs3´))), (Vint (Int.repr ne3´)), (Vint (Int.repr (BooltoZ bs4´))), (Vint (Int.repr ne4´)), (Vint (Int.repr (BooltoZ bs5´))), (Vint (Int.repr ne5´)), (Vint (Int.repr (BooltoZ bs6´))), (Vint (Int.repr ne6´)), (Vint (Int.repr (BooltoZ bs7´))), (Vint (Int.repr ne7´)).
refine_split; try eauto;
[ rewrite <- Hb1; auto | rewrite <- Hb2; auto | rewrite <- Hb3; auto | rewrite <- Hb4; auto | rewrite <- Hb5; auto |rewrite <- Hb6; auto | rewrite <- Hb7; auto | rewrite <- Hb8; auto | rewrite <- Hb9; auto | rewrite <- Hb10; auto | rewrite <- Hb11; auto | rewrite <- Hb12; auto | rewrite <- Hb13; auto | rewrite <- Hb14; auto | rewrite <- Hb15; auto | rewrite <- Hb16; auto | rewrite <- Hb17; auto | econstructor; eauto].
- refine_split; eauto.
simpl; rewrite ZMap.gso by eauto.
eassumption.
}
apply (acquire_shared0_mcs_sim (valid_id_args:= Shared2ID_valid0)).
intros; inv H; [eauto | inv H0].
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_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 WITHMEM.
End Refinement.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section release_sahred0_sim.
Lemma release_shared0_match:
∀ s i ofs e d d´ m f,
release_shared0_spec0 i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_shared0_spec; intros. subdestruct.
inv H. inv H0; constructor; simpl.
inv Hlog. econstructor; eauto.
intros.
destruct (zeq z lock_index); subst.
- rewrite ZMap.gss.
specialize (HMCSLock _ Hvalid).
mcslock_destruct HMCSLock.
refine_split; eauto.
rewrite Hdestruct3 in Hm.
inv Hm.
econstructor; eauto.
Transparent CalMCSLock.
simpl.
rewrite Hcal; auto.
- rewrite ZMap.gso; auto.
Qed.
Lemma release_shared0_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id (release_shared0_spec0))
(id ↦ primcall_release_lock_compatsem id (release_shared0_spec0)).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit (release_shared0_exist (valid_arg:= Shared2ID0)); 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.
eapply release_shared0_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
End release_sahred0_sim.
Section PAGE_COPY_SIM.
Lemma page_copy´´´_match:
∀ s d d´ m index i from f,
page_copy´´´_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy´´´_spec; intros.
subdestruct; inv H.
inv H0. constructor. simpl.
inv Hlog. econstructor; eauto.
intros.
destruct (zeq z lock_index); subst.
- rewrite ZMap.gss.
specialize (HMCSLock _ Hvalid).
mcslock_destruct HMCSLock.
refine_split; eauto.
rewrite Hdestruct5 in Hm.
inv Hm.
econstructor; eauto.
Transparent CalMCSLock.
simpl.
rewrite Hcal; auto.
- rewrite ZMap.gso; auto.
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.
-
eapply page_copy´´´_match; eauto.
Qed.
End PAGE_COPY_SIM.
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) mmcslockintro_passthrough mcurid.
Proof.
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 bootloader0_sim.
- apply get_CPU_ID_sim.
- apply release_shared0_sim.
- assert (Hp: match_impl_multi_log_one acquire_shared0_log_update_match_mcs).
{
constructor.
intros.
destruct H.
destruct Hlog.
constructor.
econstructor; eauto.
intros.
generalize (HMCSLock _ Hvalid).
intros HMCSLock´.
mcslock_destruct HMCSLock´.
destruct (Decision.decide (lock_index = z)); subst.
- inv Hm.
+ rewrite H0 in H2; inv H2.
+ simpl.
rewrite ZMap.gss.
rewrite H0 in H2; clear H0.
inversion H2; clear H2; subst.
exploit H1; eauto; intros.
destruct H as (la´ & np´ & tq´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ & bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ & Hcal´ & Ha1 & Ha2 & Ha3 & Ha4 & Ha5 & Ha6 & Ha7 & Ha8 & ?).
destruct H as (Hb1 & Hb2 & Hb3 & Hb4 & Hb5 & Hb6 & Hb7 & Hb8 & Hb9 & Hb10 & Hb11 & Hb12 & Hb13 & Hb14 & Hb15 & Hb16 & Hb17).
∃ (Vint (Int.repr la´)), (Vint (Int.repr (BooltoZ bs0´))), (Vint (Int.repr ne0´)), (Vint (Int.repr (BooltoZ bs1´))), (Vint (Int.repr ne1´)), (Vint (Int.repr (BooltoZ bs2´))), (Vint (Int.repr ne2´)), (Vint (Int.repr (BooltoZ bs3´))), (Vint (Int.repr ne3´)), (Vint (Int.repr (BooltoZ bs4´))), (Vint (Int.repr ne4´)), (Vint (Int.repr (BooltoZ bs5´))), (Vint (Int.repr ne5´)), (Vint (Int.repr (BooltoZ bs6´))), (Vint (Int.repr ne6´)), (Vint (Int.repr (BooltoZ bs7´))), (Vint (Int.repr ne7´)).
refine_split; try eauto;
[ rewrite <- Hb1; auto | rewrite <- Hb2; auto | rewrite <- Hb3; auto | rewrite <- Hb4; auto | rewrite <- Hb5; auto |rewrite <- Hb6; auto | rewrite <- Hb7; auto | rewrite <- Hb8; auto | rewrite <- Hb9; auto | rewrite <- Hb10; auto | rewrite <- Hb11; auto | rewrite <- Hb12; auto | rewrite <- Hb13; auto | rewrite <- Hb14; auto | rewrite <- Hb15; auto | rewrite <- Hb16; auto | rewrite <- Hb17; auto | econstructor; eauto].
- refine_split; eauto.
simpl; rewrite ZMap.gso by eauto.
eassumption.
}
apply (acquire_shared0_mcs_sim (valid_id_args:= Shared2ID_valid0)).
intros; inv H; [eauto | inv H0].
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_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 WITHMEM.
End Refinement.