Library mcertikos.mcslock.MCSLockIntroGenFresh3
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Require Import MCSLockIntroGenDef.
Require Import MCSLockIntroGenSpec.
Require Import Conventions.
Require Import XOmega.
Require Import LAsmModuleSemAux.
Require Import AuxLemma.
Section Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section mcs_CAS_TAIL_ref.
Lemma mcs_CAS_TAIL_spec_ref:
compatsim (crel HDATA LDATA) (gensem mcs_CAS_TAIL_spec) mcs_CAS_TAIL_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros Hargs0 Hasm_inv Hesp HRA Hle.
inv Hlog.
assert (HFB: ι b0 = Some (b0, 0)).
{ eapply stencil_find_symbol_inject´; eauto. }
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
assert (Hcpuid_range: 0 ≤ (CPU_ID d1) ≤ Int.max_unsigned).
{ generalize max_unsigned_val; intros.
rewrite H; inv Hhigh´; omega. }
assert (Hcpuid_eq: Int.unsigned (Int.repr ((CPU_ID d1))) = (CPU_ID d1)).
{ rewrite Int.unsigned_repr; trivial. }
revert Hcpuid_eq.
unfold mcs_CAS_TAIL_spec.
subrewrite´.
intros ? HQ.
set (rs2´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))).
∃ ι, (rs2´#PC <- (rs2#RA) #EAX <- (Vint z)).
subdestruct; inv HQ.
{
pose proof HMCSLock as HMCSLock´.
specialize (HMCSLock _ a).
rewrite multi_log_re in HMCSLock.
destruct HMCSLock as (la_v & bs0_v & ne0_v & bs1_v & ne1_v & bs2_v & ne2_v & bs3_v & ne3_v &
bs4_v & ne4_v & bs5_v & ne5_v & bs6_v & ne6_v & bs7_v & ne7_v &
HL__la & HL__bs0 & HL__ne0 & HL__bs1 & HL__ne1 & HL__bs2 & HL__ne2 & HL__bs3 & HL__ne3 &
HL__bs4 & HL__ne4 & HL__bs5 & HL__ne5 & HL__bs6 & HL__ne6 & HL__bs7 & HL__ne7 &
HV__la & HV__bs0 & HV__ne0 & HV__bs1 & HV__ne1 & HV__bs2 & HV__ne2 & HV__bs3 & HV__ne3 &
HV__bs4 & HV__ne4 & HV__bs5 & HV__ne5 & HV__bs6 & HV__ne6 & HV__bs7 & HV__ne7 & Hm).
assert (HST: ∃ m´, Mem.store Mint32 m2 b0 (tail_pos (Int.unsigned i)) (Vint (Int.repr NULL)) = Some m´).
{ eapply Mem.valid_access_store; eauto. }
destruct HST as (m´ & HST).
refine_split´; repeat val_inject_inv; eauto.
- econstructor; eauto; simpl; lift_trivial.
× unfold atomic_mcs_CAS_spec.
simpl; subrewrite´.
× eapply (extcall_args_without_data (D:= HDATAOps) d2).
inv Hargs.
inv H2.
inv Hargs0.
inv H3.
inv H7.
inv H6.
inv H8.
inv H1.
constructor; eauto.
econstructor; eauto.
econstructor; eauto.
- split; eauto; pattern2_refinement_simpl;
econstructor; eauto.
simpl.
econstructor; eauto; intros.
destruct (zeq (Int.unsigned i) lock_index); subst.
{ ∃ (Vint (Int.repr TOTAL_CPU)).
∃ bs0_v, ne0_v.
∃ bs1_v, ne1_v.
∃ bs2_v, ne2_v.
∃ bs3_v, ne3_v.
∃ bs4_v, ne4_v.
∃ bs5_v, ne5_v.
∃ bs6_v, ne6_v.
∃ bs7_v, ne7_v.
refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
- erewrite Mem.load_store_same; eauto; trivial.
- inv Hm.
+ rewrite Hdestruct3 in H0.
inv H0.
+ rewrite ZMap.gss.
rewrite Hdestruct3 in H0.
inv H0.
rewrite Hcal in Hdestruct4; inv Hdestruct4.
assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (CAS_TAIL true)) :: l)
= Some (MCSLOCK TOTAL_CPU lock_array nil)).
{ Transparent CalMCSLock.
simpl; rewrite Hcal; unfold CalMCSLock.NULL.
rewrite zeq_true; try reflexivity. }
eapply MATCH_MCSLOCK_VALID with (2:= Hnc0) (3:= Hnc1) (4:= Hnc2) (5:= Hnc3) (6:= Hnc4)
(7:= Hnc5) (8:= Hnc6) (9:= Hnc7) in Hcal´; assumption. }
{ specialize (HMCSLock´ _ Hvalid).
clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
∃ la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
[ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
rewrite ZMap.gso; auto.
rewrite <- multi_log_re; trivial. }
- repeat simpl_Pregmap; eauto.
- intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H; eauto 20). }
{
pose proof HMCSLock as HMCSLock´.
specialize (HMCSLock _ a).
rewrite multi_log_re in HMCSLock.
destruct HMCSLock as (la_v & bs0_v & ne0_v & bs1_v & ne1_v & bs2_v & ne2_v & bs3_v & ne3_v &
bs4_v & ne4_v & bs5_v & ne5_v & bs6_v & ne6_v & bs7_v & ne7_v &
HL__la & HL__bs0 & HL__ne0 & HL__bs1 & HL__ne1 & HL__bs2 & HL__ne2 & HL__bs3 & HL__ne3 &
HL__bs4 & HL__ne4 & HL__bs5 & HL__ne5 & HL__bs6 & HL__ne6 & HL__bs7 & HL__ne7 &
HV__la & HV__bs0 & HV__ne0 & HV__bs1 & HV__ne1 & HV__bs2 & HV__ne2 & HV__bs3 & HV__ne3 &
HV__bs4 & HV__ne4 & HV__bs5 & HV__ne5 & HV__bs6 & HV__ne6 & HV__bs7 & HV__ne7 & Hm).
assert (HLoad: Mem.load Mint32 m2 b0 (tail_pos (Int.unsigned i)) = Some (Vint (Int.repr tail))).
{ inv Hm.
- rewrite Hdestruct3 in H0; inversion H0.
- rewrite Hdestruct3 in H0; inv H0.
rewrite Hdestruct4 in Hcal; inv Hcal.
eassumption. }
assert (tail_val_eq : Vint (Int.repr tail) = la_v).
{ unfold tail_pos in HLoad.
unfold tail_pos in HL__la.
rewrite HL__la in HLoad.
inv HLoad; reflexivity. }
assert (HST: ∃ m´, Mem.store Mint32 m2 b0 (tail_pos (Int.unsigned i)) (Vint (Int.repr tail)) = Some m´).
{ eapply Mem.valid_access_store; eauto. }
destruct HST as (m´ & HST).
refine_split´; repeat val_inject_inv; eauto.
- econstructor; eauto; simpl; lift_trivial.
× unfold atomic_mcs_CAS_spec.
simpl; subrewrite´.
× eapply (extcall_args_without_data (D:= HDATAOps) d2).
inv Hargs.
inv H2.
inv Hargs0.
inv H3.
inv H7.
inv H6.
inv H8.
inv H1.
constructor; eauto.
econstructor; eauto.
econstructor; eauto.
- split; eauto; pattern2_refinement_simpl;
econstructor; eauto.
simpl.
econstructor; eauto; intros.
destruct (zeq (Int.unsigned i) lock_index); subst.
{ ∃ (Vint (Int.repr tail)).
∃ bs0_v, ne0_v.
∃ bs1_v, ne1_v.
∃ bs2_v, ne2_v.
∃ bs3_v, ne3_v.
∃ bs4_v, ne4_v.
∃ bs5_v, ne5_v.
∃ bs6_v, ne6_v.
∃ bs7_v, ne7_v.
refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
- erewrite Mem.load_store_same; eauto; trivial.
- inv Hm.
+ rewrite Hdestruct3 in H0.
inv H0.
+ rewrite ZMap.gss.
rewrite Hdestruct3 in H0.
inv H0.
rewrite Hcal in Hdestruct4; inv Hdestruct4.
assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (CAS_TAIL false)) :: l)
= Some (MCSLOCK tail lock_array bounds)).
{ Transparent CalMCSLock.
simpl.
rewrite Hcal; reflexivity. }
eapply MATCH_MCSLOCK_VALID with (2:= Hnc0) (3:= Hnc1) (4:= Hnc2) (5:= Hnc3) (6:= Hnc4)
(7:= Hnc5) (8:= Hnc6) (9:= Hnc7) in Hcal´; assumption. }
{ specialize (HMCSLock´ _ Hvalid).
clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
∃ la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
[ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
rewrite ZMap.gso; auto.
rewrite <- multi_log_re; trivial. }
- repeat simpl_Pregmap; eauto.
- intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H; eauto 20). }
Qed.
End mcs_CAS_TAIL_ref.
End WITHMEM.
End Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section mcs_CAS_TAIL_ref.
Lemma mcs_CAS_TAIL_spec_ref:
compatsim (crel HDATA LDATA) (gensem mcs_CAS_TAIL_spec) mcs_CAS_TAIL_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros Hargs0 Hasm_inv Hesp HRA Hle.
inv Hlog.
assert (HFB: ι b0 = Some (b0, 0)).
{ eapply stencil_find_symbol_inject´; eauto. }
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
assert (Hcpuid_range: 0 ≤ (CPU_ID d1) ≤ Int.max_unsigned).
{ generalize max_unsigned_val; intros.
rewrite H; inv Hhigh´; omega. }
assert (Hcpuid_eq: Int.unsigned (Int.repr ((CPU_ID d1))) = (CPU_ID d1)).
{ rewrite Int.unsigned_repr; trivial. }
revert Hcpuid_eq.
unfold mcs_CAS_TAIL_spec.
subrewrite´.
intros ? HQ.
set (rs2´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))).
∃ ι, (rs2´#PC <- (rs2#RA) #EAX <- (Vint z)).
subdestruct; inv HQ.
{
pose proof HMCSLock as HMCSLock´.
specialize (HMCSLock _ a).
rewrite multi_log_re in HMCSLock.
destruct HMCSLock as (la_v & bs0_v & ne0_v & bs1_v & ne1_v & bs2_v & ne2_v & bs3_v & ne3_v &
bs4_v & ne4_v & bs5_v & ne5_v & bs6_v & ne6_v & bs7_v & ne7_v &
HL__la & HL__bs0 & HL__ne0 & HL__bs1 & HL__ne1 & HL__bs2 & HL__ne2 & HL__bs3 & HL__ne3 &
HL__bs4 & HL__ne4 & HL__bs5 & HL__ne5 & HL__bs6 & HL__ne6 & HL__bs7 & HL__ne7 &
HV__la & HV__bs0 & HV__ne0 & HV__bs1 & HV__ne1 & HV__bs2 & HV__ne2 & HV__bs3 & HV__ne3 &
HV__bs4 & HV__ne4 & HV__bs5 & HV__ne5 & HV__bs6 & HV__ne6 & HV__bs7 & HV__ne7 & Hm).
assert (HST: ∃ m´, Mem.store Mint32 m2 b0 (tail_pos (Int.unsigned i)) (Vint (Int.repr NULL)) = Some m´).
{ eapply Mem.valid_access_store; eauto. }
destruct HST as (m´ & HST).
refine_split´; repeat val_inject_inv; eauto.
- econstructor; eauto; simpl; lift_trivial.
× unfold atomic_mcs_CAS_spec.
simpl; subrewrite´.
× eapply (extcall_args_without_data (D:= HDATAOps) d2).
inv Hargs.
inv H2.
inv Hargs0.
inv H3.
inv H7.
inv H6.
inv H8.
inv H1.
constructor; eauto.
econstructor; eauto.
econstructor; eauto.
- split; eauto; pattern2_refinement_simpl;
econstructor; eauto.
simpl.
econstructor; eauto; intros.
destruct (zeq (Int.unsigned i) lock_index); subst.
{ ∃ (Vint (Int.repr TOTAL_CPU)).
∃ bs0_v, ne0_v.
∃ bs1_v, ne1_v.
∃ bs2_v, ne2_v.
∃ bs3_v, ne3_v.
∃ bs4_v, ne4_v.
∃ bs5_v, ne5_v.
∃ bs6_v, ne6_v.
∃ bs7_v, ne7_v.
refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
- erewrite Mem.load_store_same; eauto; trivial.
- inv Hm.
+ rewrite Hdestruct3 in H0.
inv H0.
+ rewrite ZMap.gss.
rewrite Hdestruct3 in H0.
inv H0.
rewrite Hcal in Hdestruct4; inv Hdestruct4.
assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (CAS_TAIL true)) :: l)
= Some (MCSLOCK TOTAL_CPU lock_array nil)).
{ Transparent CalMCSLock.
simpl; rewrite Hcal; unfold CalMCSLock.NULL.
rewrite zeq_true; try reflexivity. }
eapply MATCH_MCSLOCK_VALID with (2:= Hnc0) (3:= Hnc1) (4:= Hnc2) (5:= Hnc3) (6:= Hnc4)
(7:= Hnc5) (8:= Hnc6) (9:= Hnc7) in Hcal´; assumption. }
{ specialize (HMCSLock´ _ Hvalid).
clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
∃ la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
[ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
rewrite ZMap.gso; auto.
rewrite <- multi_log_re; trivial. }
- repeat simpl_Pregmap; eauto.
- intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H; eauto 20). }
{
pose proof HMCSLock as HMCSLock´.
specialize (HMCSLock _ a).
rewrite multi_log_re in HMCSLock.
destruct HMCSLock as (la_v & bs0_v & ne0_v & bs1_v & ne1_v & bs2_v & ne2_v & bs3_v & ne3_v &
bs4_v & ne4_v & bs5_v & ne5_v & bs6_v & ne6_v & bs7_v & ne7_v &
HL__la & HL__bs0 & HL__ne0 & HL__bs1 & HL__ne1 & HL__bs2 & HL__ne2 & HL__bs3 & HL__ne3 &
HL__bs4 & HL__ne4 & HL__bs5 & HL__ne5 & HL__bs6 & HL__ne6 & HL__bs7 & HL__ne7 &
HV__la & HV__bs0 & HV__ne0 & HV__bs1 & HV__ne1 & HV__bs2 & HV__ne2 & HV__bs3 & HV__ne3 &
HV__bs4 & HV__ne4 & HV__bs5 & HV__ne5 & HV__bs6 & HV__ne6 & HV__bs7 & HV__ne7 & Hm).
assert (HLoad: Mem.load Mint32 m2 b0 (tail_pos (Int.unsigned i)) = Some (Vint (Int.repr tail))).
{ inv Hm.
- rewrite Hdestruct3 in H0; inversion H0.
- rewrite Hdestruct3 in H0; inv H0.
rewrite Hdestruct4 in Hcal; inv Hcal.
eassumption. }
assert (tail_val_eq : Vint (Int.repr tail) = la_v).
{ unfold tail_pos in HLoad.
unfold tail_pos in HL__la.
rewrite HL__la in HLoad.
inv HLoad; reflexivity. }
assert (HST: ∃ m´, Mem.store Mint32 m2 b0 (tail_pos (Int.unsigned i)) (Vint (Int.repr tail)) = Some m´).
{ eapply Mem.valid_access_store; eauto. }
destruct HST as (m´ & HST).
refine_split´; repeat val_inject_inv; eauto.
- econstructor; eauto; simpl; lift_trivial.
× unfold atomic_mcs_CAS_spec.
simpl; subrewrite´.
× eapply (extcall_args_without_data (D:= HDATAOps) d2).
inv Hargs.
inv H2.
inv Hargs0.
inv H3.
inv H7.
inv H6.
inv H8.
inv H1.
constructor; eauto.
econstructor; eauto.
econstructor; eauto.
- split; eauto; pattern2_refinement_simpl;
econstructor; eauto.
simpl.
econstructor; eauto; intros.
destruct (zeq (Int.unsigned i) lock_index); subst.
{ ∃ (Vint (Int.repr tail)).
∃ bs0_v, ne0_v.
∃ bs1_v, ne1_v.
∃ bs2_v, ne2_v.
∃ bs3_v, ne3_v.
∃ bs4_v, ne4_v.
∃ bs5_v, ne5_v.
∃ bs6_v, ne6_v.
∃ bs7_v, ne7_v.
refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
- erewrite Mem.load_store_same; eauto; trivial.
- inv Hm.
+ rewrite Hdestruct3 in H0.
inv H0.
+ rewrite ZMap.gss.
rewrite Hdestruct3 in H0.
inv H0.
rewrite Hcal in Hdestruct4; inv Hdestruct4.
assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (CAS_TAIL false)) :: l)
= Some (MCSLOCK tail lock_array bounds)).
{ Transparent CalMCSLock.
simpl.
rewrite Hcal; reflexivity. }
eapply MATCH_MCSLOCK_VALID with (2:= Hnc0) (3:= Hnc1) (4:= Hnc2) (5:= Hnc3) (6:= Hnc4)
(7:= Hnc5) (8:= Hnc6) (9:= Hnc7) in Hcal´; assumption. }
{ specialize (HMCSLock´ _ Hvalid).
clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
∃ la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
[ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
rewrite ZMap.gso; auto.
rewrite <- multi_log_re; trivial. }
- repeat simpl_Pregmap; eauto.
- intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H; eauto 20). }
Qed.
End mcs_CAS_TAIL_ref.
End WITHMEM.
End Refinement.