Library mcertikos.ticketlog.TicketLockIntroGenFresh
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Require Import TicketLockIntroGenDef.
Require Import TicketLockIntroGenSpec.
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 `{multi_oracle_prop: MultiOracleProp}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section get_now_ref.
Lemma IntUnsignedRange: ∀ i,
0 ≤ Int.unsigned i ≤ Int.max_unsigned.
Proof.
intros.
generalize (Int.unsigned_range i).
generalize max_unsigned_val; intro muval.
unfold Int.modulus, two_power_nat, shift_nat; simpl.
intro.
omega.
Qed.
Lemma CalTicketLockWraparoundRange: ∀ l l´ t n,
CalTicketLockWraparound l = Some (t, n, l´) →
(0 ≤ t ≤ Int.max_unsigned ∧
0 ≤ n ≤ Int.max_unsigned).
Proof.
generalize max_unsigned_val; intro muval.
intros.
destruct l.
simpl in H.
inv H.
split; omega.
simpl in H;
subdestruct; inv H; simpl in *;
split; eapply IntUnsignedRange.
Qed.
Lemma get_now_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_now_spec) get_now_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 (Hcurid_range: 0 ≤ ZMap.get (CPU_ID d1) (cid d1) ≤ Int.max_unsigned).
{
generalize max_unsigned_val; intros.
rewrite H; inv Hhigh´; omega.
}
assert (Hcurid_eq: Int.unsigned (Int.repr (ZMap.get (CPU_ID d1) (cid d1))) = ZMap.get (CPU_ID d1) (cid d1)).
{
rewrite Int.unsigned_repr; trivial.
}
revert Hcurid_eq.
unfold get_now_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 Hticket as Hticket´.
specialize (Hticket _ _ _ Hdestruct1).
rewrite multi_log_re, Hdestruct2 in Hticket.
destruct Hticket as (? & ? & _ & _ & HV1 & HV2 & _).
assert (HST1: ∃ m3, Mem.store Mint32 m2 b0 (z0 × 8)
(Vint (Int.repr z1)) = Some m3).
{
eapply Mem.valid_access_store; eauto.
}
destruct HST1 as (m3 & HST1).
assert (HST2: ∃ m4, Mem.store Mint32 m3 b0 (z0 × 8 + 4)
(Vint (Int.repr (Int.unsigned z))) = Some m4).
{
eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1); trivial.
}
destruct HST2 as (m4 & HST2).
refine_split´; repeat val_inject_inv; eauto.
+ rewrite <- (Int.repr_unsigned z).
econstructor; eauto; simpl; lift_trivial.
× unfold log_get_spec.
simpl; subrewrite´.
eapply CalTicketLockWraparoundRange in Hdestruct3.
destruct Hdestruct3.
rewrite Int.unsigned_repr by omega.
reflexivity.
× eapply (extcall_args_without_data (D:= HDATAOps) d2).
inv Hargs. inv H3. inv H2. inv Hargs0. inv H5. inv H8.
constructor; eauto.
constructor; eauto. constructor.
+ split; eauto; pattern2_refinement_simpl;
econstructor; eauto. simpl.
econstructor; eauto.
intros. destruct (zeq z3 z0); subst.
{
∃ (Vint (Int.repr z1)), (Vint (Int.repr (Int.unsigned z))).
refine_split´; trivial.
- erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
simpl. trivial.
right. simpl. left. reflexivity.
- erewrite Mem.load_store_same; eauto.
simpl. trivial.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST2); trivial.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
-
rewrite ZMap.gss. econstructor.
simpl.
rewrite Hdestruct3.
rewrite H1.
eapply CalTicketLockWraparoundRange in Hdestruct3.
destruct Hdestruct3.
rewrite Int.unsigned_repr by omega.
reflexivity.
}
{
specialize (Hticket´ _ _ _ Hvalid).
clear HV1 HV2.
destruct Hticket´ as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
∃ v1, v2.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1, HLD2;
try (simpl; right; destruct (zle z3 z0); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HLD1, HLD2;
try (simpl; right; destruct (zle z3 z0); [left; omega|right; omega]).
refine_split´; trivial.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
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 get_now_ref.
Section incr_ticket_ref.
Lemma incr_ticket_spec_ref:
compatsim (crel HDATA LDATA) (gensem incr_ticket_spec) incr_ticket_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 (Hcurid_range: 0 ≤ ZMap.get (CPU_ID d1) (cid d1) ≤ Int.max_unsigned).
{
generalize max_unsigned_val; intros.
rewrite H; inv Hhigh´; omega.
}
assert (Hcurid_eq: Int.unsigned (Int.repr (ZMap.get (CPU_ID d1) (cid d1))) = ZMap.get (CPU_ID d1) (cid d1)).
{
rewrite Int.unsigned_repr; trivial.
}
revert Hcurid_eq.
unfold incr_ticket_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 Hticket as Hticket´.
specialize (Hticket _ _ _ Hdestruct1).
rewrite multi_log_re, Hdestruct2 in Hticket.
destruct Hticket as (? & ? & _ & _ & HV1 & HV2 & _).
assert (HST1: ∃ m3, Mem.store Mint32 m2 b0 (z0 × 8)
(Vint (Int.repr (Int.unsigned (Int.repr (Int.unsigned z + 1))))) = Some m3).
{
eapply Mem.valid_access_store; eauto.
}
destruct HST1 as (m3 & HST1).
assert (HST2: ∃ m4, Mem.store Mint32 m3 b0 (z0 × 8 + 4)
(Vint (Int.repr z2)) = Some m4).
{
eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1); trivial.
}
destruct HST2 as (m4 & HST2).
refine_split´; repeat val_inject_inv; eauto.
+ rewrite <- (Int.repr_unsigned z).
econstructor; eauto; simpl; lift_trivial.
× unfold atomic_FAI_spec. simpl; subrewrite´.
× eapply (extcall_args_without_data (D:= HDATAOps) d2).
inv Hargs. inv H2. inv Hargs0. inv H3. inv H7. inv H8. inv H1.
constructor; eauto. econstructor; eauto. econstructor; eauto. constructor.
+ split; eauto; pattern2_refinement_simpl;
econstructor; eauto. simpl.
econstructor; eauto.
intros. destruct (zeq z1 z0); subst.
{
∃ (Vint (Int.repr (Int.unsigned (Int.repr (Int.unsigned z + 1))))), (Vint (Int.repr z2)).
refine_split´; trivial.
- erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
simpl. trivial.
right. simpl. left. reflexivity.
- erewrite Mem.load_store_same; eauto.
simpl. trivial.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST2); trivial.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
-
rewrite ZMap.gss. econstructor.
Local Transparent CalTicketLockWraparound.
simpl. rewrite Hdestruct3.
f_equal.
f_equal.
f_equal.
rewrite Int.unsigned_repr.
reflexivity.
eapply CalTicketLockWraparoundRange; eauto.
}
{
specialize (Hticket´ _ _ _ Hvalid).
clear HV1 HV2.
destruct Hticket´ as (v1´ & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
∃ v1´, v2.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1, HLD2;
try (simpl; right; destruct (zle z1 z0); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HLD1, HLD2;
try (simpl; right; destruct (zle z1 z0); [left; omega|right; omega]).
refine_split´; trivial.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
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 incr_ticket_ref.
Section incr_now_ref.
Lemma incr_now_spec_ref:
compatsim (crel HDATA LDATA) (gensem incr_now_spec) incr_now_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related.
unfold incr_now_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
inv Hlog.
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
assert (Hcurid_range: 0 ≤ ZMap.get (CPU_ID d1) (cid d1) ≤ Int.max_unsigned).
{
generalize max_unsigned_val; intros.
rewrite H; inv Hhigh´; omega.
}
assert (Hcurid_eq: Int.unsigned (Int.repr (ZMap.get (CPU_ID d1) (cid d1))) = ZMap.get (CPU_ID d1) (cid d1)).
{
rewrite Int.unsigned_repr; trivial.
}
revert Hcurid_eq.
unfold incr_now_spec. subrewrite´. intros ? HQ.
subdestruct. inv HQ.
pose proof Hticket as Hticket´.
specialize (Hticket _ _ _ Hdestruct1).
rewrite multi_log_re, Hdestruct2 in Hticket.
destruct Hticket as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
inv HM.
assert (HST1: ∃ m3, Mem.store Mint32 m2 b (z × 8 + 4)
(Vint (Int.add (Int.repr n) Int.one)) = Some m3).
{
eapply Mem.valid_access_store; eauto.
}
destruct HST1 as (m3 & HST1).
refine_split.
- econstructor; eauto.
unfold log_incr_spec. subrewrite´.
- constructor.
- split; eauto; pattern2_refinement_simpl; trivial.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq z0 z); subst.
{
∃ (Vint (Int.repr t)), (Vint (Int.add (Int.repr n) Int.one)).
refine_split´; try eapply Mem.store_valid_access_1; eauto.
- rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1; auto.
right; left; simpl; omega.
- apply Mem.load_store_same in HST1; trivial.
-
rewrite ZMap.gss.
unfold Int.one. rewrite Int_add_aux.
Local Transparent CalTicketLockWraparound.
rewrite <- Int.repr_unsigned with (Int.repr (n + 1)).
destruct tq.
+ econstructor.
simpl. rewrite HCal.
repeat f_equal.
rewrite Int.unsigned_repr.
reflexivity.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
auto.
+ econstructor.
simpl. rewrite HCal.
repeat f_equal.
rewrite Int.unsigned_repr.
reflexivity.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
auto.
}
{
specialize (Hticket´ _ _ _ Hvalid).
clear HV1 HV2.
destruct Hticket´ as (v1´ & v2´ & HLD1´ & HLD2´ & HV1´ & HV2´ & HM´).
∃ v1´, v2´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1´, HLD2´;
try (simpl; right; destruct (zle z0 z); [left; omega|right; omega]).
refine_split´; trivial.
- eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gso; auto. rewrite <- multi_log_re. trivial.
}
- apply inject_incr_refl.
Qed.
End incr_now_ref.
Section init_ticket_ref.
Lemma init_ticket_spec_ref:
compatsim (crel HDATA LDATA) (gensem init_ticket_spec) init_ticket_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related.
unfold init_ticket_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
inv Hlog.
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold init_ticket_spec; subrewrite.
subdestruct. inv HQ.
pose proof Hticket as Hticket´.
specialize (Hticket _ _ _ Hdestruct1).
destruct Hticket as (_ & _ & _ & _ & HV1 & HV2 & _).
assert (HST1: ∃ m3, Mem.store Mint32 m2 b (z × 8)
Vzero = Some m3).
{
eapply Mem.valid_access_store; eauto.
}
destruct HST1 as (m3 & HST1).
assert (HST2: ∃ m4, Mem.store Mint32 m3 b (z × 8 + 4)
Vzero = Some m4).
{
eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1); trivial.
}
destruct HST2 as (m4 & HST2).
refine_split.
- econstructor; eauto.
unfold log_init_spec. subrewrite´.
- constructor.
- split; eauto; pattern2_refinement_simpl; trivial.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq z0 z); subst.
{
∃ Vzero, Vzero.
refine_split´; eauto.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); auto.
erewrite Mem.load_store_same; eauto.
trivial.
right; left; simpl; omega.
- erewrite Mem.load_store_same; eauto.
trivial.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
-
rewrite ZMap.gss.
econstructor.
Local Transparent CalTicketLock.
simpl. trivial.
}
{
specialize (Hticket´ _ _ _ Hvalid).
clear HV1 HV2.
destruct Hticket´ as (v1´ & v2´ & HLD1´ & HLD2´ & HV1´ & HV2´ & HM´).
∃ v1´, v2´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1´, HLD2´;
try (simpl; right; destruct (zle z0 z); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HLD1´, HLD2´;
try (simpl; right; destruct (zle z0 z); [left; omega|right; omega]).
refine_split´; trivial.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gso; auto. rewrite <- multi_log_re. trivial.
}
- apply inject_incr_refl.
Qed.
End init_ticket_ref.
End WITHMEM.
End Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section get_now_ref.
Lemma IntUnsignedRange: ∀ i,
0 ≤ Int.unsigned i ≤ Int.max_unsigned.
Proof.
intros.
generalize (Int.unsigned_range i).
generalize max_unsigned_val; intro muval.
unfold Int.modulus, two_power_nat, shift_nat; simpl.
intro.
omega.
Qed.
Lemma CalTicketLockWraparoundRange: ∀ l l´ t n,
CalTicketLockWraparound l = Some (t, n, l´) →
(0 ≤ t ≤ Int.max_unsigned ∧
0 ≤ n ≤ Int.max_unsigned).
Proof.
generalize max_unsigned_val; intro muval.
intros.
destruct l.
simpl in H.
inv H.
split; omega.
simpl in H;
subdestruct; inv H; simpl in *;
split; eapply IntUnsignedRange.
Qed.
Lemma get_now_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_now_spec) get_now_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 (Hcurid_range: 0 ≤ ZMap.get (CPU_ID d1) (cid d1) ≤ Int.max_unsigned).
{
generalize max_unsigned_val; intros.
rewrite H; inv Hhigh´; omega.
}
assert (Hcurid_eq: Int.unsigned (Int.repr (ZMap.get (CPU_ID d1) (cid d1))) = ZMap.get (CPU_ID d1) (cid d1)).
{
rewrite Int.unsigned_repr; trivial.
}
revert Hcurid_eq.
unfold get_now_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 Hticket as Hticket´.
specialize (Hticket _ _ _ Hdestruct1).
rewrite multi_log_re, Hdestruct2 in Hticket.
destruct Hticket as (? & ? & _ & _ & HV1 & HV2 & _).
assert (HST1: ∃ m3, Mem.store Mint32 m2 b0 (z0 × 8)
(Vint (Int.repr z1)) = Some m3).
{
eapply Mem.valid_access_store; eauto.
}
destruct HST1 as (m3 & HST1).
assert (HST2: ∃ m4, Mem.store Mint32 m3 b0 (z0 × 8 + 4)
(Vint (Int.repr (Int.unsigned z))) = Some m4).
{
eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1); trivial.
}
destruct HST2 as (m4 & HST2).
refine_split´; repeat val_inject_inv; eauto.
+ rewrite <- (Int.repr_unsigned z).
econstructor; eauto; simpl; lift_trivial.
× unfold log_get_spec.
simpl; subrewrite´.
eapply CalTicketLockWraparoundRange in Hdestruct3.
destruct Hdestruct3.
rewrite Int.unsigned_repr by omega.
reflexivity.
× eapply (extcall_args_without_data (D:= HDATAOps) d2).
inv Hargs. inv H3. inv H2. inv Hargs0. inv H5. inv H8.
constructor; eauto.
constructor; eauto. constructor.
+ split; eauto; pattern2_refinement_simpl;
econstructor; eauto. simpl.
econstructor; eauto.
intros. destruct (zeq z3 z0); subst.
{
∃ (Vint (Int.repr z1)), (Vint (Int.repr (Int.unsigned z))).
refine_split´; trivial.
- erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
simpl. trivial.
right. simpl. left. reflexivity.
- erewrite Mem.load_store_same; eauto.
simpl. trivial.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST2); trivial.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
-
rewrite ZMap.gss. econstructor.
simpl.
rewrite Hdestruct3.
rewrite H1.
eapply CalTicketLockWraparoundRange in Hdestruct3.
destruct Hdestruct3.
rewrite Int.unsigned_repr by omega.
reflexivity.
}
{
specialize (Hticket´ _ _ _ Hvalid).
clear HV1 HV2.
destruct Hticket´ as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
∃ v1, v2.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1, HLD2;
try (simpl; right; destruct (zle z3 z0); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HLD1, HLD2;
try (simpl; right; destruct (zle z3 z0); [left; omega|right; omega]).
refine_split´; trivial.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
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 get_now_ref.
Section incr_ticket_ref.
Lemma incr_ticket_spec_ref:
compatsim (crel HDATA LDATA) (gensem incr_ticket_spec) incr_ticket_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 (Hcurid_range: 0 ≤ ZMap.get (CPU_ID d1) (cid d1) ≤ Int.max_unsigned).
{
generalize max_unsigned_val; intros.
rewrite H; inv Hhigh´; omega.
}
assert (Hcurid_eq: Int.unsigned (Int.repr (ZMap.get (CPU_ID d1) (cid d1))) = ZMap.get (CPU_ID d1) (cid d1)).
{
rewrite Int.unsigned_repr; trivial.
}
revert Hcurid_eq.
unfold incr_ticket_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 Hticket as Hticket´.
specialize (Hticket _ _ _ Hdestruct1).
rewrite multi_log_re, Hdestruct2 in Hticket.
destruct Hticket as (? & ? & _ & _ & HV1 & HV2 & _).
assert (HST1: ∃ m3, Mem.store Mint32 m2 b0 (z0 × 8)
(Vint (Int.repr (Int.unsigned (Int.repr (Int.unsigned z + 1))))) = Some m3).
{
eapply Mem.valid_access_store; eauto.
}
destruct HST1 as (m3 & HST1).
assert (HST2: ∃ m4, Mem.store Mint32 m3 b0 (z0 × 8 + 4)
(Vint (Int.repr z2)) = Some m4).
{
eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1); trivial.
}
destruct HST2 as (m4 & HST2).
refine_split´; repeat val_inject_inv; eauto.
+ rewrite <- (Int.repr_unsigned z).
econstructor; eauto; simpl; lift_trivial.
× unfold atomic_FAI_spec. simpl; subrewrite´.
× eapply (extcall_args_without_data (D:= HDATAOps) d2).
inv Hargs. inv H2. inv Hargs0. inv H3. inv H7. inv H8. inv H1.
constructor; eauto. econstructor; eauto. econstructor; eauto. constructor.
+ split; eauto; pattern2_refinement_simpl;
econstructor; eauto. simpl.
econstructor; eauto.
intros. destruct (zeq z1 z0); subst.
{
∃ (Vint (Int.repr (Int.unsigned (Int.repr (Int.unsigned z + 1))))), (Vint (Int.repr z2)).
refine_split´; trivial.
- erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
simpl. trivial.
right. simpl. left. reflexivity.
- erewrite Mem.load_store_same; eauto.
simpl. trivial.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST2); trivial.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
-
rewrite ZMap.gss. econstructor.
Local Transparent CalTicketLockWraparound.
simpl. rewrite Hdestruct3.
f_equal.
f_equal.
f_equal.
rewrite Int.unsigned_repr.
reflexivity.
eapply CalTicketLockWraparoundRange; eauto.
}
{
specialize (Hticket´ _ _ _ Hvalid).
clear HV1 HV2.
destruct Hticket´ as (v1´ & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
∃ v1´, v2.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1, HLD2;
try (simpl; right; destruct (zle z1 z0); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HLD1, HLD2;
try (simpl; right; destruct (zle z1 z0); [left; omega|right; omega]).
refine_split´; trivial.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
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 incr_ticket_ref.
Section incr_now_ref.
Lemma incr_now_spec_ref:
compatsim (crel HDATA LDATA) (gensem incr_now_spec) incr_now_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related.
unfold incr_now_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
inv Hlog.
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
assert (Hcurid_range: 0 ≤ ZMap.get (CPU_ID d1) (cid d1) ≤ Int.max_unsigned).
{
generalize max_unsigned_val; intros.
rewrite H; inv Hhigh´; omega.
}
assert (Hcurid_eq: Int.unsigned (Int.repr (ZMap.get (CPU_ID d1) (cid d1))) = ZMap.get (CPU_ID d1) (cid d1)).
{
rewrite Int.unsigned_repr; trivial.
}
revert Hcurid_eq.
unfold incr_now_spec. subrewrite´. intros ? HQ.
subdestruct. inv HQ.
pose proof Hticket as Hticket´.
specialize (Hticket _ _ _ Hdestruct1).
rewrite multi_log_re, Hdestruct2 in Hticket.
destruct Hticket as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
inv HM.
assert (HST1: ∃ m3, Mem.store Mint32 m2 b (z × 8 + 4)
(Vint (Int.add (Int.repr n) Int.one)) = Some m3).
{
eapply Mem.valid_access_store; eauto.
}
destruct HST1 as (m3 & HST1).
refine_split.
- econstructor; eauto.
unfold log_incr_spec. subrewrite´.
- constructor.
- split; eauto; pattern2_refinement_simpl; trivial.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq z0 z); subst.
{
∃ (Vint (Int.repr t)), (Vint (Int.add (Int.repr n) Int.one)).
refine_split´; try eapply Mem.store_valid_access_1; eauto.
- rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1; auto.
right; left; simpl; omega.
- apply Mem.load_store_same in HST1; trivial.
-
rewrite ZMap.gss.
unfold Int.one. rewrite Int_add_aux.
Local Transparent CalTicketLockWraparound.
rewrite <- Int.repr_unsigned with (Int.repr (n + 1)).
destruct tq.
+ econstructor.
simpl. rewrite HCal.
repeat f_equal.
rewrite Int.unsigned_repr.
reflexivity.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
auto.
+ econstructor.
simpl. rewrite HCal.
repeat f_equal.
rewrite Int.unsigned_repr.
reflexivity.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
auto.
}
{
specialize (Hticket´ _ _ _ Hvalid).
clear HV1 HV2.
destruct Hticket´ as (v1´ & v2´ & HLD1´ & HLD2´ & HV1´ & HV2´ & HM´).
∃ v1´, v2´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1´, HLD2´;
try (simpl; right; destruct (zle z0 z); [left; omega|right; omega]).
refine_split´; trivial.
- eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gso; auto. rewrite <- multi_log_re. trivial.
}
- apply inject_incr_refl.
Qed.
End incr_now_ref.
Section init_ticket_ref.
Lemma init_ticket_spec_ref:
compatsim (crel HDATA LDATA) (gensem init_ticket_spec) init_ticket_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related.
unfold init_ticket_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
inv Hlog.
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold init_ticket_spec; subrewrite.
subdestruct. inv HQ.
pose proof Hticket as Hticket´.
specialize (Hticket _ _ _ Hdestruct1).
destruct Hticket as (_ & _ & _ & _ & HV1 & HV2 & _).
assert (HST1: ∃ m3, Mem.store Mint32 m2 b (z × 8)
Vzero = Some m3).
{
eapply Mem.valid_access_store; eauto.
}
destruct HST1 as (m3 & HST1).
assert (HST2: ∃ m4, Mem.store Mint32 m3 b (z × 8 + 4)
Vzero = Some m4).
{
eapply Mem.valid_access_store; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1); trivial.
}
destruct HST2 as (m4 & HST2).
refine_split.
- econstructor; eauto.
unfold log_init_spec. subrewrite´.
- constructor.
- split; eauto; pattern2_refinement_simpl; trivial.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq z0 z); subst.
{
∃ Vzero, Vzero.
refine_split´; eauto.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); auto.
erewrite Mem.load_store_same; eauto.
trivial.
right; left; simpl; omega.
- erewrite Mem.load_store_same; eauto.
trivial.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
-
rewrite ZMap.gss.
econstructor.
Local Transparent CalTicketLock.
simpl. trivial.
}
{
specialize (Hticket´ _ _ _ Hvalid).
clear HV1 HV2.
destruct Hticket´ as (v1´ & v2´ & HLD1´ & HLD2´ & HV1´ & HV2´ & HM´).
∃ v1´, v2´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HLD1´, HLD2´;
try (simpl; right; destruct (zle z0 z); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HLD1´, HLD2´;
try (simpl; right; destruct (zle z0 z); [left; omega|right; omega]).
refine_split´; trivial.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gso; auto. rewrite <- multi_log_re. trivial.
}
- apply inject_incr_refl.
Qed.
End init_ticket_ref.
End WITHMEM.
End Refinement.