Library mcertikos.mcslock.MCSLockIntroGenFresh
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).
Ltac load_store_other_tac H :=
rewrite (Mem.load_store_other _ _ _ _ _ _ H); auto;
try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
Section mcs_init_node_ref.
Lemma mcs_init_node_spec_ref:
compatsim (crel HDATA LDATA) (gensem mcs_init_node_spec) mcs_init_node_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related.
unfold mcs_init_node_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
inv Hlog.
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold mcs_init_node_spec; subrewrite.
subdestruct.
inv HQ.
pose proof HMCSLock as HMCSLock´.
specialize (HMCSLock _ a).
destruct HMCSLock as (_ & _ & _ & _ & _ & _ & _ & _ & _ &
_ & _ & _ & _ & _ & _ & _ & _ &
_ & _ & _ & _ & _ & _ & _ & _ & _ &
_ & _ & _ & _ & _ & _ & _ & _ &
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 & _).
assert (HST__la: ∃ m_la, Mem.store Mint32 m2 b (tail_pos (Int.unsigned i))
(Vint (Int.repr TOTAL_CPU)) = Some m_la).
{ eapply Mem.valid_access_store; eauto. }
destruct HST__la as (m_la & HST__la).
assert (HST__bs0: ∃ m_bs0, Mem.store Mint32 m_la b (busy_pos (Int.unsigned i) 0)
Vzero = Some m_bs0).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs0 as (m_bs0 & HST__bs0).
assert (HST__ne0: ∃ m_ne0, Mem.store Mint32 m_bs0 b (next_pos (Int.unsigned i) 0)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne0).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne0 as (m_ne0 & HST__ne0).
assert (HST__bs1: ∃ m_bs1, Mem.store Mint32 m_ne0 b (busy_pos (Int.unsigned i) 1)
Vzero = Some m_bs1).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs1 as (m_bs1 & HST__bs1).
assert (HST__ne1: ∃ m_ne1, Mem.store Mint32 m_bs1 b (next_pos (Int.unsigned i) 1)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne1).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne1 as (m_ne1 & HST__ne1).
assert (HST__bs2: ∃ m_bs2, Mem.store Mint32 m_ne1 b (busy_pos (Int.unsigned i) 2)
Vzero = Some m_bs2).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs2 as (m_bs2 & HST__bs2).
assert (HST__ne2: ∃ m_ne2, Mem.store Mint32 m_bs2 b (next_pos (Int.unsigned i) 2)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne2).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne2 as (m_ne2 & HST__ne2).
assert (HST__bs3: ∃ m_bs3, Mem.store Mint32 m_ne2 b (busy_pos (Int.unsigned i) 3)
Vzero = Some m_bs3).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs3 as (m_bs3 & HST__bs3).
assert (HST__ne3: ∃ m_ne3, Mem.store Mint32 m_bs3 b (next_pos (Int.unsigned i) 3)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne3).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne3 as (m_ne3 & HST__ne3).
assert (HST__bs4: ∃ m_bs4, Mem.store Mint32 m_ne3 b (busy_pos (Int.unsigned i) 4)
Vzero = Some m_bs4).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs4 as (m_bs4 & HST__bs4).
assert (HST__ne4: ∃ m_ne4, Mem.store Mint32 m_bs4 b (next_pos (Int.unsigned i) 4)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne4).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne4 as (m_ne4 & HST__ne4).
assert (HST__bs5: ∃ m_bs5, Mem.store Mint32 m_ne4 b (busy_pos (Int.unsigned i) 5)
Vzero = Some m_bs5).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs5 as (m_bs5 & HST__bs5).
assert (HST__ne5: ∃ m_ne5, Mem.store Mint32 m_bs5 b (next_pos (Int.unsigned i) 5)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne5).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne5 as (m_ne5 & HST__ne5).
assert (HST__bs6: ∃ m_bs6, Mem.store Mint32 m_ne5 b (busy_pos (Int.unsigned i) 6)
Vzero = Some m_bs6).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs6 as (m_bs6 & HST__bs6).
assert (HST__ne6: ∃ m_ne6, Mem.store Mint32 m_bs6 b (next_pos (Int.unsigned i) 6)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne6).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne6 as (m_ne6 & HST__ne6).
assert (HST__bs7: ∃ m_bs7, Mem.store Mint32 m_ne6 b (busy_pos (Int.unsigned i) 7)
Vzero = Some m_bs7).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs7 as (m_bs7 & HST__bs7).
assert (HST__ne7: ∃ m_ne7, Mem.store Mint32 m_bs7 b (next_pos (Int.unsigned i) 7)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne7).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs7); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne7 as (m_ne7 & HST__ne7).
refine_split.
- econstructor; eauto.
unfold mcs_init_node_log_spec.
subrewrite´.
- constructor.
- split; eauto; pattern2_refinement_simpl; trivial.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq (Int.unsigned i) lock_index); subst.
{ ∃ (Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero,
(Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero,
(Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)).
refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto)).
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
load_store_other_tac HST__ne1; load_store_other_tac HST__bs1; load_store_other_tac HST__ne0; load_store_other_tac HST__bs0.
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
load_store_other_tac HST__ne1; load_store_other_tac HST__bs1.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne0); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
load_store_other_tac HST__ne1; load_store_other_tac HST__bs1.
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne1); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne2); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne3); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne4); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne5); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne6); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7;
erewrite Mem.load_store_same; eauto; trivial.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne7); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- erewrite Mem.load_store_same; eauto; trivial.
-
rewrite ZMap.gss.
assert (init_st: CalMCSLock nil = Some (MCSLOCK NULL (ZMap.init (false, NULL)) nil)).
{ econstructor. }
assert (∀ i, ZMap.get i (ZMap.init (false, NULL)) = (false, NULL)).
{ intros.
rewrite ZMap.gi.
reflexivity. }
assert (Hnval0: ZMap.get 0 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval1: ZMap.get 1 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval2: ZMap.get 2 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval3: ZMap.get 3 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval4: ZMap.get 4 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval5: ZMap.get 5 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval6: ZMap.get 6 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval7: ZMap.get 7 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (false_zero_eq: Vzero = (Vint (Int.repr (BooltoZ false)))).
{ unfold BooltoZ, Vzero.
unfold Int.zero; reflexivity. }
repeat rewrite false_zero_eq.
econstructor; eassumption. }
{ 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.
mcslock_destruct´ HMCSLock´.
∃ 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´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs0)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne0)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs1)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne1)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs2)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne2)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs3)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne3)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs4)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne4)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs5)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne5)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs6)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne6)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs7)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne7)
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. }
- apply inject_incr_refl.
Qed.
End mcs_init_node_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).
Ltac load_store_other_tac H :=
rewrite (Mem.load_store_other _ _ _ _ _ _ H); auto;
try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
Section mcs_init_node_ref.
Lemma mcs_init_node_spec_ref:
compatsim (crel HDATA LDATA) (gensem mcs_init_node_spec) mcs_init_node_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related.
unfold mcs_init_node_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
inv Hlog.
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold mcs_init_node_spec; subrewrite.
subdestruct.
inv HQ.
pose proof HMCSLock as HMCSLock´.
specialize (HMCSLock _ a).
destruct HMCSLock as (_ & _ & _ & _ & _ & _ & _ & _ & _ &
_ & _ & _ & _ & _ & _ & _ & _ &
_ & _ & _ & _ & _ & _ & _ & _ & _ &
_ & _ & _ & _ & _ & _ & _ & _ &
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 & _).
assert (HST__la: ∃ m_la, Mem.store Mint32 m2 b (tail_pos (Int.unsigned i))
(Vint (Int.repr TOTAL_CPU)) = Some m_la).
{ eapply Mem.valid_access_store; eauto. }
destruct HST__la as (m_la & HST__la).
assert (HST__bs0: ∃ m_bs0, Mem.store Mint32 m_la b (busy_pos (Int.unsigned i) 0)
Vzero = Some m_bs0).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs0 as (m_bs0 & HST__bs0).
assert (HST__ne0: ∃ m_ne0, Mem.store Mint32 m_bs0 b (next_pos (Int.unsigned i) 0)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne0).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne0 as (m_ne0 & HST__ne0).
assert (HST__bs1: ∃ m_bs1, Mem.store Mint32 m_ne0 b (busy_pos (Int.unsigned i) 1)
Vzero = Some m_bs1).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs1 as (m_bs1 & HST__bs1).
assert (HST__ne1: ∃ m_ne1, Mem.store Mint32 m_bs1 b (next_pos (Int.unsigned i) 1)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne1).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne1 as (m_ne1 & HST__ne1).
assert (HST__bs2: ∃ m_bs2, Mem.store Mint32 m_ne1 b (busy_pos (Int.unsigned i) 2)
Vzero = Some m_bs2).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs2 as (m_bs2 & HST__bs2).
assert (HST__ne2: ∃ m_ne2, Mem.store Mint32 m_bs2 b (next_pos (Int.unsigned i) 2)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne2).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne2 as (m_ne2 & HST__ne2).
assert (HST__bs3: ∃ m_bs3, Mem.store Mint32 m_ne2 b (busy_pos (Int.unsigned i) 3)
Vzero = Some m_bs3).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs3 as (m_bs3 & HST__bs3).
assert (HST__ne3: ∃ m_ne3, Mem.store Mint32 m_bs3 b (next_pos (Int.unsigned i) 3)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne3).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne3 as (m_ne3 & HST__ne3).
assert (HST__bs4: ∃ m_bs4, Mem.store Mint32 m_ne3 b (busy_pos (Int.unsigned i) 4)
Vzero = Some m_bs4).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs4 as (m_bs4 & HST__bs4).
assert (HST__ne4: ∃ m_ne4, Mem.store Mint32 m_bs4 b (next_pos (Int.unsigned i) 4)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne4).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne4 as (m_ne4 & HST__ne4).
assert (HST__bs5: ∃ m_bs5, Mem.store Mint32 m_ne4 b (busy_pos (Int.unsigned i) 5)
Vzero = Some m_bs5).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs5 as (m_bs5 & HST__bs5).
assert (HST__ne5: ∃ m_ne5, Mem.store Mint32 m_bs5 b (next_pos (Int.unsigned i) 5)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne5).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne5 as (m_ne5 & HST__ne5).
assert (HST__bs6: ∃ m_bs6, Mem.store Mint32 m_ne5 b (busy_pos (Int.unsigned i) 6)
Vzero = Some m_bs6).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs6 as (m_bs6 & HST__bs6).
assert (HST__ne6: ∃ m_ne6, Mem.store Mint32 m_bs6 b (next_pos (Int.unsigned i) 6)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne6).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne6 as (m_ne6 & HST__ne6).
assert (HST__bs7: ∃ m_bs7, Mem.store Mint32 m_ne6 b (busy_pos (Int.unsigned i) 7)
Vzero = Some m_bs7).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__bs7 as (m_bs7 & HST__bs7).
assert (HST__ne7: ∃ m_ne7, Mem.store Mint32 m_bs7 b (next_pos (Int.unsigned i) 7)
(Vint (Int.repr TOTAL_CPU)) = Some m_ne7).
{ eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs7); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
destruct HST__ne7 as (m_ne7 & HST__ne7).
refine_split.
- econstructor; eauto.
unfold mcs_init_node_log_spec.
subrewrite´.
- constructor.
- split; eauto; pattern2_refinement_simpl; trivial.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq (Int.unsigned i) lock_index); subst.
{ ∃ (Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero,
(Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero,
(Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)), Vzero, (Vint (Int.repr TOTAL_CPU)).
refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto)).
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
load_store_other_tac HST__ne1; load_store_other_tac HST__bs1; load_store_other_tac HST__ne0; load_store_other_tac HST__bs0.
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
load_store_other_tac HST__ne1; load_store_other_tac HST__bs1.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne0); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
load_store_other_tac HST__ne1; load_store_other_tac HST__bs1.
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne1); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne2); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
load_store_other_tac HST__ne3; load_store_other_tac HST__bs3;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne3); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne4); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
load_store_other_tac HST__ne5; load_store_other_tac HST__bs5;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne5); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne6); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- load_store_other_tac HST__ne7; load_store_other_tac HST__bs7;
erewrite Mem.load_store_same; eauto; trivial.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne7); auto;
try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
erewrite Mem.load_store_same; eauto; trivial.
- erewrite Mem.load_store_same; eauto; trivial.
-
rewrite ZMap.gss.
assert (init_st: CalMCSLock nil = Some (MCSLOCK NULL (ZMap.init (false, NULL)) nil)).
{ econstructor. }
assert (∀ i, ZMap.get i (ZMap.init (false, NULL)) = (false, NULL)).
{ intros.
rewrite ZMap.gi.
reflexivity. }
assert (Hnval0: ZMap.get 0 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval1: ZMap.get 1 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval2: ZMap.get 2 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval3: ZMap.get 3 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval4: ZMap.get 4 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval5: ZMap.get 5 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval6: ZMap.get 6 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (Hnval7: ZMap.get 7 (ZMap.init (false, TOTAL_CPU)) = (false, TOTAL_CPU)) by apply H; auto.
assert (false_zero_eq: Vzero = (Vint (Int.repr (BooltoZ false)))).
{ unfold BooltoZ, Vzero.
unfold Int.zero; reflexivity. }
repeat rewrite false_zero_eq.
econstructor; eassumption. }
{ 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.
mcslock_destruct´ HMCSLock´.
∃ 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´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs0)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne0)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs1)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne1)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs2)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne2)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs3)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne3)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs4)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne4)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs5)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne5)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs6)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne6)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs7)
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]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne7)
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. }
- apply inject_incr_refl.
Qed.
End mcs_init_node_ref.
End WITHMEM.
End Refinement.