Library mcertikos.mcslock.QMCSLockOpGen
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 LAsmModuleSemAux.
Require Import TacticsForTesting.
Require Import ListLemma2.
Require Import ZSet.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import CalMCSLock.
Require Import INVLemmaQSLock.
Require Export MQMCSLockOp.
Require Export MMCSLockOp.
Require Import QMCSLockOpGenDef.
Require Import QMCSLockOpGenLemma.
Require Import ObjQLock.
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 LAsmModuleSemAux.
Require Import TacticsForTesting.
Require Import ListLemma2.
Require Import ZSet.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import CalMCSLock.
Require Import INVLemmaQSLock.
Require Export MQMCSLockOp.
Require Export MMCSLockOp.
Require Import QMCSLockOpGenDef.
Require Import QMCSLockOpGenLemma.
Require Import ObjQLock.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mqmcslockop_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mmcslockabsintro_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 `{mcs_oracle_prop: MCSOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mqmcslockop_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mmcslockabsintro_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;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
multi_log_re: multi_log hadt = multi_log 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;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
multi_log_re: multi_log hadt = multi_log 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 update_abd_log_rel : ∀ abid f habd labd l LOCK,
relate_RData f habd labd →
(multi_log habd) = (multi_log labd) →
relate_RData f
(habd {multi_log : ZMap.set abid (MultiDef l) (multi_log labd)})
{lock : ZMap.set abid LOCK (lock habd)}
(labd {multi_log : ZMap.set abid (MultiDef l) (multi_log labd)}).
Proof.
inversion 1.
constructor; auto.
Qed.
Lemma acquire_shared_exist:
∀ habd habd´ labd n ofs i l f,
acquire_shared1_mcs_spec0 n ofs habd = Some (habd´, i, l)
→ relate_RData f habd labd
→ ∃ labd´, acquire_shared0_spec0 n ofs labd = Some (labd´, i, l) ∧ relate_RData f habd´ labd´
∧ Shared2ID0 n = Some i.
Proof.
unfold acquire_shared0_spec, acquire_shared1_mcs_spec. intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct;
inv HQ; refine_split; eauto.
destruct (GetSharedMemEvent l0); trivial.
inv HR´; constructor; eauto.
Qed.
Lemma acquire_shared_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_shared_compatsem acquire_shared1_mcs_spec0)
(id ↦ primcall_acquire_shared_compatsem acquire_shared0_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 page_copy_exist:
∀ s habd habd´ labd index i from f,
mcs_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 mcs_page_copy´´_spec, page_copy´´´_spec.
intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct;
inv HQ; refine_split; eauto.
- exploit page_copy_aux_exists; eauto.
intros HCopy´.
rewrite HCopy´. trivial.
- inv HR´; constructor; eauto.
Qed.
Lemma page_copy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem mcs_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 release_shared_exist:
∀ habd habd´ labd n ofs e f,
release_shared1_mcs_spec0 n ofs e habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, release_shared0_spec0 n ofs e labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold release_shared0_spec, release_shared1_mcs_spec. intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct. inv HQ.
refine_split; eauto.
inv HR´; constructor; eauto.
Qed.
Lemma release_shared_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_release_lock_compatsem id release_shared1_mcs_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_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 mcs_pass_lock_exist:
∀ habd habd´ labd n ofs f
(HhighQ: MQMCSLockOp.high_level_invariant habd),
pass_qslock_spec n ofs habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_pass_lock_spec n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold mcs_pass_lock_spec, pass_qslock_spec.
intros until f.
intros HhighQ.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
subrewrite´.
destruct (ikern labd); [|intros; congruence].
destruct (ihost labd); [|intros; congruence].
destruct (index2Z n ofs) as [abid|] eqn: H_abid; [|intros; congruence].
inversion HhighQ.
inv relate_qs_mcs_log_inv.
specialize (Hrelate_qs_mcs_log_type _ _ _ H_abid).
inv relate_mcs_qs_oracle_inv.
specialize (Hrelate_qs_mcs_oracle _ _ _ H_abid).
rewrite multi_oracle_re0 in ×.
rewrite multi_log_re0 in ×.
specialize (valid_qs_oracle_pool_inv _ _ _ H_abid).
destruct valid_qs_oracle_pool_inv as [Hvalid_oracle _].
destruct (ZMap.get abid (multi_log labd)) as [|ll] eqn: H_l ;
intros Hpass_qlock; try congruence.
specialize (get_free_qslock_pool_inv _ _ _ _ H_abid H_l).
specialize (get_free_qslock_oracle_pool_inv _ _ _ H_abid).
specialize (cal_qslock_pool_status_inv _ _ _ _ H_abid H_l).
inversion Hrelate_qs_mcs_log_type; subst.
remember (ZMap.get abid (multi_oracle labd)) as o.
clear Heqo.
unfold correct_qslock_pool_status in valid_qslock_pool_status_inv.
specialize (valid_qslock_pool_status_inv _ _ _ _ H_abid H_l).
assert (CalValidBit ll = Some FreeToPull) as Hvalid.
{
unfold cal_qslock_status in cal_qslock_pool_status_inv.
destruct (ZMap.get abid (lock habd)); [congruence|].
destruct b; [congruence|].
destruct Hrelate_qs_mcs_log as [? ? H0].
inversion H0 as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq HCal_inv].
symmetry in HCal_inv.
destruct (cal_qslock_pool_status_inv _ _ _ _ _ _ HCal_inv) as [cal_qslock_pool_status_inv0 _].
auto.
}
pose (curid := CPU_ID labd).
inversion Hrelate_qs_mcs_oracle; subst.
pose (ll1 := o curid ll ++ ll).
change (o (CPU_ID labd) ll ++ ll) with ll1.
change (o (CPU_ID labd) ll ++ ll) with ll1 in Hpass_qlock.
assert (Hrelate_log1 : relate_qs_mcs_log ll1 ).
{ unfold ll1. apply Hrelate_mcs_qs_oracle_res; auto. }
destruct Hrelate_qs_mcs_log as [queue H_QCalMCS H_QCal].
assert (thread_has_lock curid queue) as Hhas_lock.
{
assert (Foo := CalLock_thread_has_lock queue).
inversion H_QCal
as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq H_QCal_inv].
symmetry in H_QCal_inv.
destruct (ZMap.get abid (lock habd)); [congruence|].
replace (CPU_ID habd) with (CPU_ID labd) in valid_qslock_pool_status_inv by congruence. unfold correct_qslock_status in valid_qslock_pool_status_inv.
specialize (valid_qslock_pool_status_inv self_c rel_c b qs tq slow H_QCal_inv).
destruct valid_qslock_pool_status_inv as [_ valid_qslock_pool_status_inv].
destruct b0; [inversion Hpass_qlock|].
assert (eq_refl: LockOwn false = LockOwn false) by reflexivity.
destruct (valid_qslock_pool_status_inv _ eq_refl) as [queue0 [Hvalid1 [Hvalid2 _]]] .
apply Foo with (queue0 := queue0); unfold curid; congruence.
}
destruct (ZMap.get abid (lock habd)); [congruence|].
destruct Hrelate_log1 as [queue1 H_QCalMCS1 H_QCal1].
assert (thread_has_lock curid queue1) as Hhas_lock1.
{
unfold ll1 in H_QCalMCS1.
apply other_threads_preserve_thread_has_lock with (l:=ll) (l´:=o curid ll) (q:=queue); auto.
intros k e.
apply Hvalid_oracle.
}
assert (CalValidBit ll1 = Some FreeToPull) as Hvalid1.
{
destruct b; [congruence|].
inversion H_QCal as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq HQCal_inv].
symmetry in HQCal_inv.
inversion Hhas_lock.
subst.
simpl in HQCal_inv.
inversion H_QCal1 as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 HQCal_inv1].
symmetry in HQCal_inv1.
inversion Hhas_lock1.
subst.
simpl in HQCal_inv1.
unfold ll1.
apply (other_threads_preserve_FreeToPull _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HQCal_inv HQCal_inv1); assumption.
}
clearbody ll1.
clear ll H_l valid_qslock_pool_status_inv get_free_qslock_pool_inv cal_qslock_pool_status_inv Hrelate_qs_mcs_log_type queue H_QCalMCS H_QCal Hhas_lock Hvalid.
inversion H_QCal1
as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 H_QCal_inv1].
symmetry in H_QCal_inv1.
destruct Hhas_lock1.
rewrite H_QCal_inv1 in Hpass_qlock.
rewrite Hqs1 in Hpass_qlock.
simpl in Hpass_qlock.
destruct (Q_CalMCSLock_completeness _ _ H_QCalMCS1) as [[old_tail1 la1] H_CalMCS1].
rewrite H_CalMCS1.
destruct (zeq old_tail1 (CPU_ID labd)) as [H_old_tail1 | H_old_tail1].
+ rewrite (Q_CalMCSLock_tail_AT_HEAD ll1 MCS_INSIDE (CPU_ID labd) bi q0 H_QCalMCS1 old_tail1 la1 bounds H_CalMCS1) in H_old_tail1.
subst.
simpl in ×.
destruct b; [inversion Hpass_qlock|].
destruct rel_c1 as [|rel_c1´]; [congruence|].
replace habd´
with (habd {multi_log: ZMap.set abid
(MultiDef (TEVENT (CPU_ID labd) (TTICKET (CAS_TAIL true)) :: ll1))
(multi_log habd)}
{lock: ZMap.set abid LockFalse (lock habd)})
by congruence.
eexists; split; [reflexivity|].
rewrite multi_log_re0.
apply update_abd_log_rel.
assumption.
assumption.
+ assert (q0 ≠ nil).
{
pose (Q_CalMCSLock_tail_AT_HEAD ll1 MCS_INSIDE curid bi q0 H_QCalMCS1 old_tail1 la1 bounds H_CalMCS1).
tauto.
}
destruct q0 as [|[s j bj] q00]; [congruence|].
simpl in Hpass_qlock.
pose (ll2 := (TEVENT curid (TTICKET (CAS_TAIL false)) :: ll1)).
assert (Q_CalMCSLock ll2 ((QT MCS_INSIDE curid bi) :: (QT s j bj) :: q00)) as H_QCalMCS2
by (unfold ll2; apply Q_CalMCSLock_CAS_TAIL_false; auto).
assert (relate_qs_mcs_log ll2) as Hrelate_log2.
{
apply RELATE_QS_MCS_LOG with (q := (QT MCS_INSIDE curid bi) :: (QT s j bj) :: q00).
auto.
unfold ll2.
Transparent QS_CalLock.
simpl.
Opaque QS_CalLock.
rewrite H_QCal_inv1.
rewrite Hqs1, Hb1, Htq1.
simpl.
rewrite zeq_true.
destruct b; [inversion Hpass_qlock|].
destruct rel_c1 as [|rel_c´]; [congruence|].
apply QSTATE_OF_QMCSLOCKSTATE.
reflexivity.
reflexivity.
rewrite Hslow1; reflexivity.
reflexivity.
}
assert (CalValidBit ll2 = Some FreeToPull) as Hvalid2 by (simpl; rewrite Hvalid1; reflexivity).
change (TEVENT (CPU_ID labd) (TTICKET (CAS_TAIL false)) :: ll1) with ll2.
change (TEVENT (CPU_ID labd) (TTICKET (CAS_TAIL false)) :: ll1) with ll2 in Hpass_qlock.
clearbody ll2.
destruct b; [inversion Hpass_qlock|].
destruct rel_c1 as [|rel_c´]; [congruence|].
destruct (QS_CalWaitRel CalPassLockLoopTime (CPU_ID labd) j ll2 o) as [ll´|] eqn:H_CalWaitRel;
[|congruence].
destruct (pass_lock_CalWaitRel curid j o Hvalid_oracle Hrelate_qs_mcs_oracle CalPassLockLoopTime ll2 ll´ _
H_QCalMCS2 H_CalWaitRel Hrelate_log2) as [H1_ll´ [H2_ll´ [HCal´ _]]].
{ apply THREAD_HAS_LOCK_NEXT. }
{ assumption. }
fold curid. rewrite H1_ll´.
inversion H2_ll´ as [q´ H_QCalMCS´ H_QCal´].
destruct (Q_CalMCSLock_completeness _ _ H_QCalMCS´) as [[old_tail´ la´] H_CalMCS´].
rewrite H_CalMCS´.
change ((o (CPU_ID labd)
(TEVENT (CPU_ID labd) (TTICKET GET_NEXT) :: ll´) ++
TEVENT (CPU_ID labd) (TTICKET GET_NEXT) :: ll´))
with (pass_lock_final1 ll´ (CPU_ID labd) o)
in Hpass_qlock.
destruct HCal´ as [[? ?] [? [? [? [? [? HCal´]]]]]] .
unfold curid in HCal´.
rewrite HCal´ in Hpass_qlock.
change (TEVENT (CPU_ID labd) (TTICKET SET_BUSY) :: pass_lock_final1 ll´ (CPU_ID labd) o)
with (pass_lock_final ll´ (CPU_ID labd) o)
in Hpass_qlock.
replace habd´
with (habd {multi_log: ZMap.set abid
(MultiDef (pass_lock_final ll´ (CPU_ID labd) o))
(multi_log labd)})
{lock : ZMap.set abid LockFalse (lock habd)}
by congruence.
eexists; split; [reflexivity|].
apply update_abd_log_rel;
assumption.
Qed.
Lemma mcs_pass_lock_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem pass_qslock_spec)
(id ↦ gensem mcs_pass_lock_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData); intros.
exploit mcs_pass_lock_exist; eauto 1.
intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
Lemma mcs_wait_lock_exist:
∀ habd habd´ labd bound n ofs f
(HhighQ: MQMCSLockOp.high_level_invariant habd),
wait_qslock_spec bound n ofs habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_wait_lock_spec bound n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold mcs_wait_lock_spec, wait_qslock_spec.
intros until f.
intros HhighQ.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
subrewrite´.
destruct (ikern labd); [|intros; congruence].
destruct (ihost labd); [|intros; congruence].
destruct (index2Z n ofs) as [abid|] eqn: H_abid; [|intros; congruence].
inversion HhighQ.
inv relate_qs_mcs_log_inv.
specialize (Hrelate_qs_mcs_log_type _ _ _ H_abid).
inv relate_mcs_qs_oracle_inv.
specialize (Hrelate_qs_mcs_oracle _ _ _ H_abid).
specialize (valid_qs_oracle_pool_inv _ _ _ H_abid).
destruct valid_qs_oracle_pool_inv as [Hvalid_oracle Hvalid_oracle_queue].
rewrite multi_oracle_re0 in ×.
rewrite multi_log_re0 in ×.
destruct (ZMap.get abid (multi_log labd)) as [|ll] eqn:H_l;
intros Hwait_qlock; try congruence.
specialize (get_free_qslock_pool_inv _ _ _ _ H_abid H_l).
specialize (get_free_qslock_oracle_pool_inv _ _ _ H_abid).
inversion Hrelate_qs_mcs_log_type; subst.
remember (ZMap.get abid (multi_oracle labd)) as o.
clear Heqo.
unfold correct_qslock_pool_status in valid_qslock_pool_status_inv.
specialize (valid_qslock_pool_status_inv _ _ _ _ H_abid H_l).
pose (curid := CPU_ID labd).
destruct (ZMap.get abid (lock habd)) eqn: H_lock; [|congruence].
inversion Hrelate_qs_mcs_oracle; subst.
pose (ll1 := o curid ll ++ ll).
assert (relate_qs_mcs_log ll1) as Hrelate_log1.
{ unfold ll1.
apply Hrelate_mcs_qs_oracle_res; assumption.
}
change (o (CPU_ID labd) ll ++ ll) with ll1.
change (o (CPU_ID labd) ll ++ ll) with ll1 in Hwait_qlock.
destruct (Hrelate_qs_mcs_log) as [queue H_CalMCS HCalLock].
assert (¬ In curid (map qthread_tid queue)) as H_not_In_queue.
{
unfold correct_qslock_status in valid_qslock_pool_status_inv.
inversion HCalLock as [self_c1 rel_c1 b1 q1 slow1 tq1 Hb1 Hq1 Htq1 Hslow1 HCalLock_inv].
symmetry in HCalLock_inv.
specialize (valid_qslock_pool_status_inv _ _ _ _ _ _ HCalLock_inv).
destruct valid_qslock_pool_status_inv as [valid_qslock_pool_status_inv _].
specialize (valid_qslock_pool_status_inv eq_refl).
rewrite CPU_ID_re0 in valid_qslock_pool_status_inv.
subst.
exact valid_qslock_pool_status_inv.
}
destruct Hrelate_log1 as [queue1 H_CalMCS1 H_CalLock1].
assert (¬ In curid (map qthread_tid queue1)) as H_not_In_queue1.
{
apply other_threads_preserve_Not_In with (l:=ll) (l´:=o curid ll)(q:=queue).
- exact H_CalMCS1.
- assumption.
- assumption.
- intros k e. apply Hvalid_oracle.
}
assert (get_free_qslock ll1) as Hfree1 by (apply get_free_qslock_oracle_pool_inv; assumption).
clearbody ll1.
clear ll H_l valid_qslock_pool_status_inv Hrelate_qs_mcs_log_type get_free_qslock_pool_inv queue H_CalMCS HCalLock
H_not_In_queue.
destruct (Q_CalMCSLock_completeness _ _ H_CalMCS1) as [[old_tail la] H_CalMCS].
rewrite H_CalMCS; simpl.
inversion H_CalLock1 as [self_c1 rel_c1 b1 q1 slow1 tq1 Hb1 Hq1 Hslow1 Htq1 HCalLock1_inv].
symmetry in HCalLock1_inv.
rewrite HCalLock1_inv in Hwait_qlock.
destruct (zeq old_tail CalMCSLock.NULL).
+ assert (queue1 = nil) as Hq1_nil.
{ assert (tailsound := tail_soundness ll1 queue1 H_CalMCS1 _ _ _ H_CalMCS).
rewrite (Q_CalMCSLock_tail_id_nil ll1 queue1).
reflexivity.
auto.
congruence.
}
rewrite Hq1_nil in ×.
clear Hq1_nil.
rewrite Hq1 in ×.
simpl in Hwait_qlock.
pose (ll2 := (TEVENT curid (TTICKET (SWAP_TAIL (nat_of_Z bound) true))) :: ll1).
eexists; split; [reflexivity|].
inversion Hwait_qlock.
change (TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) true)) :: ll1) with ll2.
apply update_abd_log_rel.
assumption.
assumption.
+ assert (old_tail = tail_id queue1) as Htail_id by (eapply tail_soundness; eauto).
destruct (Q_CalMCSLock_tail_id_nonnil queue1) as [q0 [s [bi Hq0]]].
congruence.
pose (ll2 := (TEVENT curid (TTICKET (SWAP_TAIL (nat_of_Z bound) false))) :: ll1).
assert (Q_CalMCSLock ll2 ((queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil))).
{
unfold ll2.
apply Q_CalMCSLock_SWAP_not_nil.
auto.
rewrite Hq0; destruct q0; simpl; discriminate.
rewrite CPU_ID_re0 in CPU_ID_range; apply (cpu_not_NULL _ CPU_ID_range).
assumption.
}
assert (queue1 ≠ nil) by (rewrite Hq0; destruct q0; discriminate).
assert (QState_of_QMCSLockState (queue1 ++ QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound) :: nil) (QS_CalLock ll2)).
{
Local Transparent QS_CalLock.
unfold ll2.
simpl.
rewrite HCalLock1_inv.
assert (¬ In curid q1) as H_not_In_q1 by (rewrite Hq1; assumption).
destruct (in_dec zeq curid q1); [tauto |].
destruct queue1 as [|[s0 i0 b0] q12]; [congruence|].
rewrite Hq1.
simpl.
assert (curid ≠ i0)
by (simpl in H_not_In_queue1; intros ?; apply H_not_In_queue1; left; congruence; tauto).
destruct (zeq curid i0) eqn:Heq_curid; [congruence|].
rewrite Htq1.
simpl.
apply QSTATE_OF_QMCSLOCKSTATE.
× rewrite Hb1; reflexivity.
× simpl; rewrite map_app; reflexivity.
× simpl.
rewrite Hslow1.
destruct s0;
rewrite <- slowset_BEFORE_SET_NEXT; try rewrite ZSet_add_commute; reflexivity.
× simpl. rewrite map_app. reflexivity.
}
assert (relate_qs_mcs_log ll2).
{
apply RELATE_QS_MCS_LOG with (q:= (queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil)).
× apply Q_CalMCSLock_SWAP_not_nil; auto.
rewrite CPU_ID_re0 in CPU_ID_range; apply (cpu_not_NULL _ CPU_ID_range).
× assumption.
}
assert (get_free_qslock ll2) as Hfree2 by (apply SWAP_TAIL_false_preserves_get_free_qslock; assumption).
pose (ll3 := o curid ll2 ++ ll2).
assert (relate_qs_mcs_log ll3) as Hrelate_log3
by (apply Hrelate_mcs_qs_oracle_res; assumption).
assert (old_tail = (last q1 NULL)) as Hold_tail.
{
rewrite Htail_id.
rewrite Hq1.
apply tail_id_last.
}
rewrite <- Hold_tail in Hwait_qlock.
destruct Hrelate_log3 as [queue3 H_QCalMCS3 H_QCal3].
assert (thread_before_set_next old_tail curid queue3) as Hbefore_set_next.
{
apply other_threads_preserve_BEFORE_SET_NEXT
with (l:=ll2) (l´ := o curid ll2)
(q := (queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil)).
assumption.
assumption.
rewrite Hq0.
rewrite <- app_assoc; simpl.
unfold thread_before_set_next.
(replace (tail_id queue1) with old_tail by assumption); eauto 6.
intros k e; apply Hvalid_oracle.
}
assert (get_free_qslock ll3) as Hfree3
by (apply get_free_qslock_oracle_pool_inv; assumption).
pose (ll4 := (TEVENT curid (TTICKET (SET_NEXT old_tail))) :: ll3).
change ((TEVENT (CPU_ID labd) (TTICKET (SET_NEXT old_tail))
:: o (CPU_ID labd) (TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1) ++
TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1)) with ll4.
change ((TEVENT (CPU_ID labd) (TTICKET (SET_NEXT old_tail))
:: o (CPU_ID labd) (TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1) ++
TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1))
with ll4 in Hwait_qlock.
assert (get_free_qslock ll4) as Hfree4 by (apply SET_NEXT_preserves_get_free_qslock; assumption).
destruct queue1 as [| [s0 i0 bi0]] eqn:?; [congruence|].
rewrite Hq1 in Hwait_qlock.
simpl in Hwait_qlock.
change ( match map qthread_tid q with
| nil ⇒ i0
| _ :: _ ⇒ last (map qthread_tid q) NULL
end)
with (last (map qthread_tid ((QT s0 i0 bi0):: q)) NULL) in Hwait_qlock.
clear q0 s Hq0.
destruct Hbefore_set_next as [q0 [s [b_old_tail [b_curid [qpost Hqueue3]]]]].
pose (queue4 := q0 ++ (QT s old_tail b_old_tail) :: (QT MCS_WAITING_BUSY curid b_curid) :: qpost).
assert (Q_CalMCSLock ll4 queue4).
{
unfold queue4.
apply Q_CalMCSLock_SET_NEXT with (q := queue3).
assumption.
congruence.
}
assert (QState_of_QMCSLockState queue4 (QS_CalLock ll4)).
{
unfold queue4. unfold ll4.
simpl.
inversion H_QCal3 as [self_c3 rel_c3 b3 q3 slow3 tq3 Hb3 Hq3 Hslow3 Htq3 H_QCal3_inv].
symmetry in H_QCal3_inv.
rewrite Hq3.
rewrite Htq3.
rewrite Hslow3.
replace (ZSet.mem curid (slowset_of_QMCSLockState queue3)) with true
by (rewrite Hqueue3; rewrite BEFORE_SET_NEXT_is_slow;
[ reflexivity |
rewrite <- Hqueue3; eapply Q_CalMCSLock_NoDup; eauto]).
assert (QState_of_QMCSLockState (q0 ++ QT s old_tail b_old_tail :: QT MCS_WAITING_BUSY curid b_curid :: qpost)
(Some (self_c3, rel_c3, b3, map qthread_tid queue3,
ZSet.remove curid (slowset_of_QMCSLockState queue3),
map qthread_bound queue3))).
{
apply QSTATE_OF_QMCSLOCKSTATE.
+ rewrite Hb3, Hqueue3.
rewrite QState_of_QMCSLockState_SET_NEXT_head_status.
reflexivity.
+ rewrite Hqueue3.
rewrite QState_of_QMCSLockState_SET_NEXT_queue.
reflexivity.
+ rewrite Hqueue3.
rewrite QState_of_QMCSLockState_SET_NEXT_slowset with (l := ll3).
reflexivity.
rewrite <- Hqueue3; auto.
+ rewrite Hqueue3.
rewrite QState_of_QMCSLockState_SET_NEXT_bounds.
reflexivity.
}
rewrite Hqueue3.
destruct q0.
+ simpl.
destruct (zeq curid old_tail).
-
assert (NoDup (map qthread_tid queue4)) as Hnodup4
by (eauto using Q_CalMCSLock_NoDup).
unfold queue4 in Hnodup4.
simpl in Hnodup4.
replace old_tail with curid in Hnodup4 by auto.
inversion Hnodup4.
simpl in ×.
tauto.
- simpl in H4.
rewrite Hqueue3 in H4.
exact H4.
+ simpl.
destruct (zeq curid (qthread_tid q0)).
-
assert (NoDup (map qthread_tid queue4)) as Hnodup4
by (eauto using Q_CalMCSLock_NoDup).
unfold queue4 in Hnodup4.
simpl in Hnodup4.
rewrite map_app in Hnodup4.
simpl in Hnodup4.
replace (qthread_tid q0) with curid in Hnodup4 by auto.
inversion Hnodup4 as [| ? ? Hnodup4´].
rewrite in_app in Hnodup4´.
simpl in Hnodup4´.
tauto.
- simpl in H4.
rewrite Hqueue3 in H4.
exact H4.
}
assert (relate_qs_mcs_log ll4) by (apply (RELATE_QS_MCS_LOG ll4 queue4); assumption).
assert (ZSet.mem curid (slowset_of_QMCSLockState queue4) = false).
{
unfold queue4.
apply slowset_of_QMCSLockState_SET_NEXT_false.
fold queue4.
eauto using Q_CalMCSLock_NoDup.
}
destruct (QS_CalWaitGet (CalWaitLockTime tq1) (CPU_ID labd) ll4 o) as [hl´|] eqn:H_CalWaitGet;
[|congruence].
destruct (wait_lock_CalMCS_AcqWait o Hrelate_qs_mcs_oracle Hvalid_oracle get_free_qslock_oracle_pool_inv
(CalWaitLockTime tq1) ll4 hl´ queue4 curid b_curid)
as [H_CalWait_returns Hrelate_log´].
{ assumption. }
{ unfold queue4.
rewrite in_app.
right.
simpl.
auto.
}
{ assumption. }
{assumption. }
{ exact Hfree4. }
{ exact H_CalWaitGet. }
replace bounds with tq1 by (symmetry; apply (CalMCS_QSCal_bound _ _ _ _ _ _ _ _ _ _ H_CalMCS HCalLock1_inv)).
eexists.
fold curid.
rewrite H_CalWait_returns.
split; [reflexivity|].
replace habd´ with
(habd {multi_log: ZMap.set abid (MultiDef hl´) (multi_log labd)}
{lock: ZMap.set abid (LockOwn false) (lock habd)}) by congruence.
apply update_abd_log_rel;
assumption.
Qed.
Lemma mcs_wait_lock_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem wait_qslock_spec)
(id ↦ gensem mcs_wait_lock_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData); intros.
exploit mcs_wait_lock_exist; eauto 1.
intros [labd´ [HP HM]].
match_external_states_simpl.
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_init_spec n labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold ticket_lock_init_spec; unfold ticket_lock_init0_spec; intros until f; exist_simpl.
Qed.
Lemma ticket_lock_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ticket_lock_init0_spec)
(id ↦ gensem ticket_lock_init_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) mqmcslockop mmcslockop.
Proof.
unfold mqmcslockop.
unfold mqmcslockop_fresh.
rewrite id_left.
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 mcs_pass_lock_sim.
- apply mcs_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 update_abd_log_rel : ∀ abid f habd labd l LOCK,
relate_RData f habd labd →
(multi_log habd) = (multi_log labd) →
relate_RData f
(habd {multi_log : ZMap.set abid (MultiDef l) (multi_log labd)})
{lock : ZMap.set abid LOCK (lock habd)}
(labd {multi_log : ZMap.set abid (MultiDef l) (multi_log labd)}).
Proof.
inversion 1.
constructor; auto.
Qed.
Lemma acquire_shared_exist:
∀ habd habd´ labd n ofs i l f,
acquire_shared1_mcs_spec0 n ofs habd = Some (habd´, i, l)
→ relate_RData f habd labd
→ ∃ labd´, acquire_shared0_spec0 n ofs labd = Some (labd´, i, l) ∧ relate_RData f habd´ labd´
∧ Shared2ID0 n = Some i.
Proof.
unfold acquire_shared0_spec, acquire_shared1_mcs_spec. intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct;
inv HQ; refine_split; eauto.
destruct (GetSharedMemEvent l0); trivial.
inv HR´; constructor; eauto.
Qed.
Lemma acquire_shared_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_shared_compatsem acquire_shared1_mcs_spec0)
(id ↦ primcall_acquire_shared_compatsem acquire_shared0_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 page_copy_exist:
∀ s habd habd´ labd index i from f,
mcs_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 mcs_page_copy´´_spec, page_copy´´´_spec.
intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct;
inv HQ; refine_split; eauto.
- exploit page_copy_aux_exists; eauto.
intros HCopy´.
rewrite HCopy´. trivial.
- inv HR´; constructor; eauto.
Qed.
Lemma page_copy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem mcs_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 release_shared_exist:
∀ habd habd´ labd n ofs e f,
release_shared1_mcs_spec0 n ofs e habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, release_shared0_spec0 n ofs e labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold release_shared0_spec, release_shared1_mcs_spec. intros until f.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
subdestruct. inv HQ.
refine_split; eauto.
inv HR´; constructor; eauto.
Qed.
Lemma release_shared_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_release_lock_compatsem id release_shared1_mcs_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_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 mcs_pass_lock_exist:
∀ habd habd´ labd n ofs f
(HhighQ: MQMCSLockOp.high_level_invariant habd),
pass_qslock_spec n ofs habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_pass_lock_spec n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold mcs_pass_lock_spec, pass_qslock_spec.
intros until f.
intros HhighQ.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
subrewrite´.
destruct (ikern labd); [|intros; congruence].
destruct (ihost labd); [|intros; congruence].
destruct (index2Z n ofs) as [abid|] eqn: H_abid; [|intros; congruence].
inversion HhighQ.
inv relate_qs_mcs_log_inv.
specialize (Hrelate_qs_mcs_log_type _ _ _ H_abid).
inv relate_mcs_qs_oracle_inv.
specialize (Hrelate_qs_mcs_oracle _ _ _ H_abid).
rewrite multi_oracle_re0 in ×.
rewrite multi_log_re0 in ×.
specialize (valid_qs_oracle_pool_inv _ _ _ H_abid).
destruct valid_qs_oracle_pool_inv as [Hvalid_oracle _].
destruct (ZMap.get abid (multi_log labd)) as [|ll] eqn: H_l ;
intros Hpass_qlock; try congruence.
specialize (get_free_qslock_pool_inv _ _ _ _ H_abid H_l).
specialize (get_free_qslock_oracle_pool_inv _ _ _ H_abid).
specialize (cal_qslock_pool_status_inv _ _ _ _ H_abid H_l).
inversion Hrelate_qs_mcs_log_type; subst.
remember (ZMap.get abid (multi_oracle labd)) as o.
clear Heqo.
unfold correct_qslock_pool_status in valid_qslock_pool_status_inv.
specialize (valid_qslock_pool_status_inv _ _ _ _ H_abid H_l).
assert (CalValidBit ll = Some FreeToPull) as Hvalid.
{
unfold cal_qslock_status in cal_qslock_pool_status_inv.
destruct (ZMap.get abid (lock habd)); [congruence|].
destruct b; [congruence|].
destruct Hrelate_qs_mcs_log as [? ? H0].
inversion H0 as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq HCal_inv].
symmetry in HCal_inv.
destruct (cal_qslock_pool_status_inv _ _ _ _ _ _ HCal_inv) as [cal_qslock_pool_status_inv0 _].
auto.
}
pose (curid := CPU_ID labd).
inversion Hrelate_qs_mcs_oracle; subst.
pose (ll1 := o curid ll ++ ll).
change (o (CPU_ID labd) ll ++ ll) with ll1.
change (o (CPU_ID labd) ll ++ ll) with ll1 in Hpass_qlock.
assert (Hrelate_log1 : relate_qs_mcs_log ll1 ).
{ unfold ll1. apply Hrelate_mcs_qs_oracle_res; auto. }
destruct Hrelate_qs_mcs_log as [queue H_QCalMCS H_QCal].
assert (thread_has_lock curid queue) as Hhas_lock.
{
assert (Foo := CalLock_thread_has_lock queue).
inversion H_QCal
as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq H_QCal_inv].
symmetry in H_QCal_inv.
destruct (ZMap.get abid (lock habd)); [congruence|].
replace (CPU_ID habd) with (CPU_ID labd) in valid_qslock_pool_status_inv by congruence. unfold correct_qslock_status in valid_qslock_pool_status_inv.
specialize (valid_qslock_pool_status_inv self_c rel_c b qs tq slow H_QCal_inv).
destruct valid_qslock_pool_status_inv as [_ valid_qslock_pool_status_inv].
destruct b0; [inversion Hpass_qlock|].
assert (eq_refl: LockOwn false = LockOwn false) by reflexivity.
destruct (valid_qslock_pool_status_inv _ eq_refl) as [queue0 [Hvalid1 [Hvalid2 _]]] .
apply Foo with (queue0 := queue0); unfold curid; congruence.
}
destruct (ZMap.get abid (lock habd)); [congruence|].
destruct Hrelate_log1 as [queue1 H_QCalMCS1 H_QCal1].
assert (thread_has_lock curid queue1) as Hhas_lock1.
{
unfold ll1 in H_QCalMCS1.
apply other_threads_preserve_thread_has_lock with (l:=ll) (l´:=o curid ll) (q:=queue); auto.
intros k e.
apply Hvalid_oracle.
}
assert (CalValidBit ll1 = Some FreeToPull) as Hvalid1.
{
destruct b; [congruence|].
inversion H_QCal as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq HQCal_inv].
symmetry in HQCal_inv.
inversion Hhas_lock.
subst.
simpl in HQCal_inv.
inversion H_QCal1 as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 HQCal_inv1].
symmetry in HQCal_inv1.
inversion Hhas_lock1.
subst.
simpl in HQCal_inv1.
unfold ll1.
apply (other_threads_preserve_FreeToPull _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HQCal_inv HQCal_inv1); assumption.
}
clearbody ll1.
clear ll H_l valid_qslock_pool_status_inv get_free_qslock_pool_inv cal_qslock_pool_status_inv Hrelate_qs_mcs_log_type queue H_QCalMCS H_QCal Hhas_lock Hvalid.
inversion H_QCal1
as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 H_QCal_inv1].
symmetry in H_QCal_inv1.
destruct Hhas_lock1.
rewrite H_QCal_inv1 in Hpass_qlock.
rewrite Hqs1 in Hpass_qlock.
simpl in Hpass_qlock.
destruct (Q_CalMCSLock_completeness _ _ H_QCalMCS1) as [[old_tail1 la1] H_CalMCS1].
rewrite H_CalMCS1.
destruct (zeq old_tail1 (CPU_ID labd)) as [H_old_tail1 | H_old_tail1].
+ rewrite (Q_CalMCSLock_tail_AT_HEAD ll1 MCS_INSIDE (CPU_ID labd) bi q0 H_QCalMCS1 old_tail1 la1 bounds H_CalMCS1) in H_old_tail1.
subst.
simpl in ×.
destruct b; [inversion Hpass_qlock|].
destruct rel_c1 as [|rel_c1´]; [congruence|].
replace habd´
with (habd {multi_log: ZMap.set abid
(MultiDef (TEVENT (CPU_ID labd) (TTICKET (CAS_TAIL true)) :: ll1))
(multi_log habd)}
{lock: ZMap.set abid LockFalse (lock habd)})
by congruence.
eexists; split; [reflexivity|].
rewrite multi_log_re0.
apply update_abd_log_rel.
assumption.
assumption.
+ assert (q0 ≠ nil).
{
pose (Q_CalMCSLock_tail_AT_HEAD ll1 MCS_INSIDE curid bi q0 H_QCalMCS1 old_tail1 la1 bounds H_CalMCS1).
tauto.
}
destruct q0 as [|[s j bj] q00]; [congruence|].
simpl in Hpass_qlock.
pose (ll2 := (TEVENT curid (TTICKET (CAS_TAIL false)) :: ll1)).
assert (Q_CalMCSLock ll2 ((QT MCS_INSIDE curid bi) :: (QT s j bj) :: q00)) as H_QCalMCS2
by (unfold ll2; apply Q_CalMCSLock_CAS_TAIL_false; auto).
assert (relate_qs_mcs_log ll2) as Hrelate_log2.
{
apply RELATE_QS_MCS_LOG with (q := (QT MCS_INSIDE curid bi) :: (QT s j bj) :: q00).
auto.
unfold ll2.
Transparent QS_CalLock.
simpl.
Opaque QS_CalLock.
rewrite H_QCal_inv1.
rewrite Hqs1, Hb1, Htq1.
simpl.
rewrite zeq_true.
destruct b; [inversion Hpass_qlock|].
destruct rel_c1 as [|rel_c´]; [congruence|].
apply QSTATE_OF_QMCSLOCKSTATE.
reflexivity.
reflexivity.
rewrite Hslow1; reflexivity.
reflexivity.
}
assert (CalValidBit ll2 = Some FreeToPull) as Hvalid2 by (simpl; rewrite Hvalid1; reflexivity).
change (TEVENT (CPU_ID labd) (TTICKET (CAS_TAIL false)) :: ll1) with ll2.
change (TEVENT (CPU_ID labd) (TTICKET (CAS_TAIL false)) :: ll1) with ll2 in Hpass_qlock.
clearbody ll2.
destruct b; [inversion Hpass_qlock|].
destruct rel_c1 as [|rel_c´]; [congruence|].
destruct (QS_CalWaitRel CalPassLockLoopTime (CPU_ID labd) j ll2 o) as [ll´|] eqn:H_CalWaitRel;
[|congruence].
destruct (pass_lock_CalWaitRel curid j o Hvalid_oracle Hrelate_qs_mcs_oracle CalPassLockLoopTime ll2 ll´ _
H_QCalMCS2 H_CalWaitRel Hrelate_log2) as [H1_ll´ [H2_ll´ [HCal´ _]]].
{ apply THREAD_HAS_LOCK_NEXT. }
{ assumption. }
fold curid. rewrite H1_ll´.
inversion H2_ll´ as [q´ H_QCalMCS´ H_QCal´].
destruct (Q_CalMCSLock_completeness _ _ H_QCalMCS´) as [[old_tail´ la´] H_CalMCS´].
rewrite H_CalMCS´.
change ((o (CPU_ID labd)
(TEVENT (CPU_ID labd) (TTICKET GET_NEXT) :: ll´) ++
TEVENT (CPU_ID labd) (TTICKET GET_NEXT) :: ll´))
with (pass_lock_final1 ll´ (CPU_ID labd) o)
in Hpass_qlock.
destruct HCal´ as [[? ?] [? [? [? [? [? HCal´]]]]]] .
unfold curid in HCal´.
rewrite HCal´ in Hpass_qlock.
change (TEVENT (CPU_ID labd) (TTICKET SET_BUSY) :: pass_lock_final1 ll´ (CPU_ID labd) o)
with (pass_lock_final ll´ (CPU_ID labd) o)
in Hpass_qlock.
replace habd´
with (habd {multi_log: ZMap.set abid
(MultiDef (pass_lock_final ll´ (CPU_ID labd) o))
(multi_log labd)})
{lock : ZMap.set abid LockFalse (lock habd)}
by congruence.
eexists; split; [reflexivity|].
apply update_abd_log_rel;
assumption.
Qed.
Lemma mcs_pass_lock_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem pass_qslock_spec)
(id ↦ gensem mcs_pass_lock_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData); intros.
exploit mcs_pass_lock_exist; eauto 1.
intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
Lemma mcs_wait_lock_exist:
∀ habd habd´ labd bound n ofs f
(HhighQ: MQMCSLockOp.high_level_invariant habd),
wait_qslock_spec bound n ofs habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_wait_lock_spec bound n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold mcs_wait_lock_spec, wait_qslock_spec.
intros until f.
intros HhighQ.
intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
subrewrite´.
destruct (ikern labd); [|intros; congruence].
destruct (ihost labd); [|intros; congruence].
destruct (index2Z n ofs) as [abid|] eqn: H_abid; [|intros; congruence].
inversion HhighQ.
inv relate_qs_mcs_log_inv.
specialize (Hrelate_qs_mcs_log_type _ _ _ H_abid).
inv relate_mcs_qs_oracle_inv.
specialize (Hrelate_qs_mcs_oracle _ _ _ H_abid).
specialize (valid_qs_oracle_pool_inv _ _ _ H_abid).
destruct valid_qs_oracle_pool_inv as [Hvalid_oracle Hvalid_oracle_queue].
rewrite multi_oracle_re0 in ×.
rewrite multi_log_re0 in ×.
destruct (ZMap.get abid (multi_log labd)) as [|ll] eqn:H_l;
intros Hwait_qlock; try congruence.
specialize (get_free_qslock_pool_inv _ _ _ _ H_abid H_l).
specialize (get_free_qslock_oracle_pool_inv _ _ _ H_abid).
inversion Hrelate_qs_mcs_log_type; subst.
remember (ZMap.get abid (multi_oracle labd)) as o.
clear Heqo.
unfold correct_qslock_pool_status in valid_qslock_pool_status_inv.
specialize (valid_qslock_pool_status_inv _ _ _ _ H_abid H_l).
pose (curid := CPU_ID labd).
destruct (ZMap.get abid (lock habd)) eqn: H_lock; [|congruence].
inversion Hrelate_qs_mcs_oracle; subst.
pose (ll1 := o curid ll ++ ll).
assert (relate_qs_mcs_log ll1) as Hrelate_log1.
{ unfold ll1.
apply Hrelate_mcs_qs_oracle_res; assumption.
}
change (o (CPU_ID labd) ll ++ ll) with ll1.
change (o (CPU_ID labd) ll ++ ll) with ll1 in Hwait_qlock.
destruct (Hrelate_qs_mcs_log) as [queue H_CalMCS HCalLock].
assert (¬ In curid (map qthread_tid queue)) as H_not_In_queue.
{
unfold correct_qslock_status in valid_qslock_pool_status_inv.
inversion HCalLock as [self_c1 rel_c1 b1 q1 slow1 tq1 Hb1 Hq1 Htq1 Hslow1 HCalLock_inv].
symmetry in HCalLock_inv.
specialize (valid_qslock_pool_status_inv _ _ _ _ _ _ HCalLock_inv).
destruct valid_qslock_pool_status_inv as [valid_qslock_pool_status_inv _].
specialize (valid_qslock_pool_status_inv eq_refl).
rewrite CPU_ID_re0 in valid_qslock_pool_status_inv.
subst.
exact valid_qslock_pool_status_inv.
}
destruct Hrelate_log1 as [queue1 H_CalMCS1 H_CalLock1].
assert (¬ In curid (map qthread_tid queue1)) as H_not_In_queue1.
{
apply other_threads_preserve_Not_In with (l:=ll) (l´:=o curid ll)(q:=queue).
- exact H_CalMCS1.
- assumption.
- assumption.
- intros k e. apply Hvalid_oracle.
}
assert (get_free_qslock ll1) as Hfree1 by (apply get_free_qslock_oracle_pool_inv; assumption).
clearbody ll1.
clear ll H_l valid_qslock_pool_status_inv Hrelate_qs_mcs_log_type get_free_qslock_pool_inv queue H_CalMCS HCalLock
H_not_In_queue.
destruct (Q_CalMCSLock_completeness _ _ H_CalMCS1) as [[old_tail la] H_CalMCS].
rewrite H_CalMCS; simpl.
inversion H_CalLock1 as [self_c1 rel_c1 b1 q1 slow1 tq1 Hb1 Hq1 Hslow1 Htq1 HCalLock1_inv].
symmetry in HCalLock1_inv.
rewrite HCalLock1_inv in Hwait_qlock.
destruct (zeq old_tail CalMCSLock.NULL).
+ assert (queue1 = nil) as Hq1_nil.
{ assert (tailsound := tail_soundness ll1 queue1 H_CalMCS1 _ _ _ H_CalMCS).
rewrite (Q_CalMCSLock_tail_id_nil ll1 queue1).
reflexivity.
auto.
congruence.
}
rewrite Hq1_nil in ×.
clear Hq1_nil.
rewrite Hq1 in ×.
simpl in Hwait_qlock.
pose (ll2 := (TEVENT curid (TTICKET (SWAP_TAIL (nat_of_Z bound) true))) :: ll1).
eexists; split; [reflexivity|].
inversion Hwait_qlock.
change (TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) true)) :: ll1) with ll2.
apply update_abd_log_rel.
assumption.
assumption.
+ assert (old_tail = tail_id queue1) as Htail_id by (eapply tail_soundness; eauto).
destruct (Q_CalMCSLock_tail_id_nonnil queue1) as [q0 [s [bi Hq0]]].
congruence.
pose (ll2 := (TEVENT curid (TTICKET (SWAP_TAIL (nat_of_Z bound) false))) :: ll1).
assert (Q_CalMCSLock ll2 ((queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil))).
{
unfold ll2.
apply Q_CalMCSLock_SWAP_not_nil.
auto.
rewrite Hq0; destruct q0; simpl; discriminate.
rewrite CPU_ID_re0 in CPU_ID_range; apply (cpu_not_NULL _ CPU_ID_range).
assumption.
}
assert (queue1 ≠ nil) by (rewrite Hq0; destruct q0; discriminate).
assert (QState_of_QMCSLockState (queue1 ++ QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound) :: nil) (QS_CalLock ll2)).
{
Local Transparent QS_CalLock.
unfold ll2.
simpl.
rewrite HCalLock1_inv.
assert (¬ In curid q1) as H_not_In_q1 by (rewrite Hq1; assumption).
destruct (in_dec zeq curid q1); [tauto |].
destruct queue1 as [|[s0 i0 b0] q12]; [congruence|].
rewrite Hq1.
simpl.
assert (curid ≠ i0)
by (simpl in H_not_In_queue1; intros ?; apply H_not_In_queue1; left; congruence; tauto).
destruct (zeq curid i0) eqn:Heq_curid; [congruence|].
rewrite Htq1.
simpl.
apply QSTATE_OF_QMCSLOCKSTATE.
× rewrite Hb1; reflexivity.
× simpl; rewrite map_app; reflexivity.
× simpl.
rewrite Hslow1.
destruct s0;
rewrite <- slowset_BEFORE_SET_NEXT; try rewrite ZSet_add_commute; reflexivity.
× simpl. rewrite map_app. reflexivity.
}
assert (relate_qs_mcs_log ll2).
{
apply RELATE_QS_MCS_LOG with (q:= (queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil)).
× apply Q_CalMCSLock_SWAP_not_nil; auto.
rewrite CPU_ID_re0 in CPU_ID_range; apply (cpu_not_NULL _ CPU_ID_range).
× assumption.
}
assert (get_free_qslock ll2) as Hfree2 by (apply SWAP_TAIL_false_preserves_get_free_qslock; assumption).
pose (ll3 := o curid ll2 ++ ll2).
assert (relate_qs_mcs_log ll3) as Hrelate_log3
by (apply Hrelate_mcs_qs_oracle_res; assumption).
assert (old_tail = (last q1 NULL)) as Hold_tail.
{
rewrite Htail_id.
rewrite Hq1.
apply tail_id_last.
}
rewrite <- Hold_tail in Hwait_qlock.
destruct Hrelate_log3 as [queue3 H_QCalMCS3 H_QCal3].
assert (thread_before_set_next old_tail curid queue3) as Hbefore_set_next.
{
apply other_threads_preserve_BEFORE_SET_NEXT
with (l:=ll2) (l´ := o curid ll2)
(q := (queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil)).
assumption.
assumption.
rewrite Hq0.
rewrite <- app_assoc; simpl.
unfold thread_before_set_next.
(replace (tail_id queue1) with old_tail by assumption); eauto 6.
intros k e; apply Hvalid_oracle.
}
assert (get_free_qslock ll3) as Hfree3
by (apply get_free_qslock_oracle_pool_inv; assumption).
pose (ll4 := (TEVENT curid (TTICKET (SET_NEXT old_tail))) :: ll3).
change ((TEVENT (CPU_ID labd) (TTICKET (SET_NEXT old_tail))
:: o (CPU_ID labd) (TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1) ++
TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1)) with ll4.
change ((TEVENT (CPU_ID labd) (TTICKET (SET_NEXT old_tail))
:: o (CPU_ID labd) (TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1) ++
TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1))
with ll4 in Hwait_qlock.
assert (get_free_qslock ll4) as Hfree4 by (apply SET_NEXT_preserves_get_free_qslock; assumption).
destruct queue1 as [| [s0 i0 bi0]] eqn:?; [congruence|].
rewrite Hq1 in Hwait_qlock.
simpl in Hwait_qlock.
change ( match map qthread_tid q with
| nil ⇒ i0
| _ :: _ ⇒ last (map qthread_tid q) NULL
end)
with (last (map qthread_tid ((QT s0 i0 bi0):: q)) NULL) in Hwait_qlock.
clear q0 s Hq0.
destruct Hbefore_set_next as [q0 [s [b_old_tail [b_curid [qpost Hqueue3]]]]].
pose (queue4 := q0 ++ (QT s old_tail b_old_tail) :: (QT MCS_WAITING_BUSY curid b_curid) :: qpost).
assert (Q_CalMCSLock ll4 queue4).
{
unfold queue4.
apply Q_CalMCSLock_SET_NEXT with (q := queue3).
assumption.
congruence.
}
assert (QState_of_QMCSLockState queue4 (QS_CalLock ll4)).
{
unfold queue4. unfold ll4.
simpl.
inversion H_QCal3 as [self_c3 rel_c3 b3 q3 slow3 tq3 Hb3 Hq3 Hslow3 Htq3 H_QCal3_inv].
symmetry in H_QCal3_inv.
rewrite Hq3.
rewrite Htq3.
rewrite Hslow3.
replace (ZSet.mem curid (slowset_of_QMCSLockState queue3)) with true
by (rewrite Hqueue3; rewrite BEFORE_SET_NEXT_is_slow;
[ reflexivity |
rewrite <- Hqueue3; eapply Q_CalMCSLock_NoDup; eauto]).
assert (QState_of_QMCSLockState (q0 ++ QT s old_tail b_old_tail :: QT MCS_WAITING_BUSY curid b_curid :: qpost)
(Some (self_c3, rel_c3, b3, map qthread_tid queue3,
ZSet.remove curid (slowset_of_QMCSLockState queue3),
map qthread_bound queue3))).
{
apply QSTATE_OF_QMCSLOCKSTATE.
+ rewrite Hb3, Hqueue3.
rewrite QState_of_QMCSLockState_SET_NEXT_head_status.
reflexivity.
+ rewrite Hqueue3.
rewrite QState_of_QMCSLockState_SET_NEXT_queue.
reflexivity.
+ rewrite Hqueue3.
rewrite QState_of_QMCSLockState_SET_NEXT_slowset with (l := ll3).
reflexivity.
rewrite <- Hqueue3; auto.
+ rewrite Hqueue3.
rewrite QState_of_QMCSLockState_SET_NEXT_bounds.
reflexivity.
}
rewrite Hqueue3.
destruct q0.
+ simpl.
destruct (zeq curid old_tail).
-
assert (NoDup (map qthread_tid queue4)) as Hnodup4
by (eauto using Q_CalMCSLock_NoDup).
unfold queue4 in Hnodup4.
simpl in Hnodup4.
replace old_tail with curid in Hnodup4 by auto.
inversion Hnodup4.
simpl in ×.
tauto.
- simpl in H4.
rewrite Hqueue3 in H4.
exact H4.
+ simpl.
destruct (zeq curid (qthread_tid q0)).
-
assert (NoDup (map qthread_tid queue4)) as Hnodup4
by (eauto using Q_CalMCSLock_NoDup).
unfold queue4 in Hnodup4.
simpl in Hnodup4.
rewrite map_app in Hnodup4.
simpl in Hnodup4.
replace (qthread_tid q0) with curid in Hnodup4 by auto.
inversion Hnodup4 as [| ? ? Hnodup4´].
rewrite in_app in Hnodup4´.
simpl in Hnodup4´.
tauto.
- simpl in H4.
rewrite Hqueue3 in H4.
exact H4.
}
assert (relate_qs_mcs_log ll4) by (apply (RELATE_QS_MCS_LOG ll4 queue4); assumption).
assert (ZSet.mem curid (slowset_of_QMCSLockState queue4) = false).
{
unfold queue4.
apply slowset_of_QMCSLockState_SET_NEXT_false.
fold queue4.
eauto using Q_CalMCSLock_NoDup.
}
destruct (QS_CalWaitGet (CalWaitLockTime tq1) (CPU_ID labd) ll4 o) as [hl´|] eqn:H_CalWaitGet;
[|congruence].
destruct (wait_lock_CalMCS_AcqWait o Hrelate_qs_mcs_oracle Hvalid_oracle get_free_qslock_oracle_pool_inv
(CalWaitLockTime tq1) ll4 hl´ queue4 curid b_curid)
as [H_CalWait_returns Hrelate_log´].
{ assumption. }
{ unfold queue4.
rewrite in_app.
right.
simpl.
auto.
}
{ assumption. }
{assumption. }
{ exact Hfree4. }
{ exact H_CalWaitGet. }
replace bounds with tq1 by (symmetry; apply (CalMCS_QSCal_bound _ _ _ _ _ _ _ _ _ _ H_CalMCS HCalLock1_inv)).
eexists.
fold curid.
rewrite H_CalWait_returns.
split; [reflexivity|].
replace habd´ with
(habd {multi_log: ZMap.set abid (MultiDef hl´) (multi_log labd)}
{lock: ZMap.set abid (LockOwn false) (lock habd)}) by congruence.
apply update_abd_log_rel;
assumption.
Qed.
Lemma mcs_wait_lock_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem wait_qslock_spec)
(id ↦ gensem mcs_wait_lock_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData); intros.
exploit mcs_wait_lock_exist; eauto 1.
intros [labd´ [HP HM]].
match_external_states_simpl.
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_init_spec n labd = Some labd´ ∧ relate_RData f habd´ labd´.
Proof.
unfold ticket_lock_init_spec; unfold ticket_lock_init0_spec; intros until f; exist_simpl.
Qed.
Lemma ticket_lock_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ticket_lock_init0_spec)
(id ↦ gensem ticket_lock_init_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) mqmcslockop mmcslockop.
Proof.
unfold mqmcslockop.
unfold mqmcslockop_fresh.
rewrite id_left.
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 mcs_pass_lock_sim.
- apply mcs_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.