Library mcertikos.ticketlog.QTicketLockGenAsm
This file provide the contextual refinement proof between MPTInit layer and MPTBit layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import MQTicketLock.
Require Import QTicketLockGenSpec.
Require Import QTicketLockGenAsmSource.
Require Import QTicketLockGenAsmData.
Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.
Section ASM_VERIFICATION.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Ltac accessors_simpl:=
match goal with
| |- exec_storeex _ _ _ _ _ _ _ = _ ⇒
unfold exec_storeex, LoadStoreSem1.exec_storeex1;
simpl; Lregset_simpl_tac;
match goal with
| |- context [Asm.exec_store _ _ _ _ _ _ _] ⇒
unfold Asm.exec_store; simpl;
Lregset_simpl_tac; lift_trivial
end
| |- exec_loadex _ _ _ _ _ _ = _ ⇒
unfold exec_loadex, LoadStoreSem1.exec_loadex1;
simpl; Lregset_simpl_tac;
match goal with
| |- context[Asm.exec_load _ _ _ _ _ _] ⇒
unfold Asm.exec_load; simpl;
Lregset_simpl_tac; lift_trivial
end
end.
Ltac clearAll := repeat match goal with
| [H: _ |- _] ⇒ clear H
end.
Lemma H_CalLock_pull:
∀ c l e
(Hcal: H_CalLock (TEVENT c (TSHARED OPULL):: l) = Some e),
∃ e´, H_CalLock l = Some e´.
Proof.
Transparent H_CalLock.
simpl; intros.
subdestruct. inv Hcal. eauto.
Opaque H_CalLock.
Qed.
Lemma acquire_lock_spec:
∀ ge (s: stencil) (rs rs´ : regset) b b0 (m m´: mem) (labd labd´ : RData) sig bound i ofs ls id
(Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m, labd))
(Hlow: low_level_invariant (Mem.nextblock m) labd)
(Hhinv: high_level_invariant labd),
find_symbol s acquire_lock = Some b →
make_globalenv s (acquire_lock ↦ acquire_lock_function) mhticketlockop = ret ge →
rs PC = Vptr b Int.zero →
acquire_lock_spec0 (Int.unsigned bound) (Int.unsigned i) (Int.unsigned ofs) labd = Some (labd´, id, ls) →
find_symbol s id = Some b0 →
(match ls with
| Some l´ ⇒ Mem.storebytes m b0 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end) →
sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint bound ::Vint i ::Vint ofs :: nil) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m´´ r_,
lasm_step (acquire_lock ↦ acquire_lock_function) (mhticketlockop (Hmwd:= Hmwd) (Hmem:= Hmem))
acquire_lock s rs
(m, labd) r_ (m´´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock m´)) f´
∧ Memtype.Mem.inject f´ m´ m´´
∧ (Mem.nextblock m´ ≤ Mem.nextblock m´´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#RA <- Vundef #PC <- (rs#RA)))
(Pregmap.get l r_)).
Proof.
intros.
inv Hasm.
inv H6.
inv H9.
inv H11.
inv H8.
inv H12.
inv H8.
simpl in H10.
simpl in H11.
simpl in H12.
caseEq(Mem.alloc m 0 20).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
exploit Hacquire_shared; eauto.
intros [[b_acquire_shared [Hacquire_shared_symbol Hacquire_shared_fun] prim_acquire_shared]].
exploit Hwait_lock; eauto.
intros [[b_wait_lock [Hwait_lock_symbol Hwait_lock_fun] prim_wait_lock]].
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b1 12 Freeable).
{
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 3; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 16 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 4; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.valid_access m3 Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint bound) HV3) as [m4 HST3].
assert(Hnextblock4: Mem.nextblock m4 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
}
assert (HV4: Mem.valid_access m4 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 1.
omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV4; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint i) HV4) as [m5 HST4].
assert (HVofs: Mem.valid_access m5 Mint32 b1 8 Freeable).
{
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.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 2; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVofs; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint ofs) HVofs) as [mofs HSTofs].
assert(Hnextblockofs: Mem.nextblock mofs = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTofs); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
}
assert (HV5: Mem.valid_access mofs Mint32 b1 0 Freeable).
{
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.
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV5; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint i) HV5) as [m6 HST5].
assert(Hnextblock6: Mem.nextblock m6 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
}
assert (HVofs´: Mem.valid_access m6 Mint32 b1 4 Freeable).
{
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.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVofs´; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint ofs) HVofs´) as [mofs´ HSTofs´].
assert(Hnextblockofs´: Mem.nextblock mofs´ = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTofs´); trivial.
}
assert (HV6: Mem.range_perm mofs´ b1 0 20 Cur Freeable).
{
unfold Mem.range_perm.
intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
assert (HFB: ∀ b2 delta, Mem.flat_inj (Mem.nextblock m) b2 ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b2 (Mem.nextblock m)). inv H6.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H6.
}
assert (Hinject: Mem.inject (Mem.flat_inj (Mem.nextblock m)) m mofs´).
{
repeat (eapply Mem.storebytes_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
}
assert (HF: ∃ m7,
match ls with
| Some l´ ⇒ Mem.storebytes mofs´ b0 0 (ByteList l´) = Some m7
| None ⇒ m7 = mofs´
end
∧ Mem.inject (Mem.flat_inj (Mem.nextblock m)) m´ m7
∧ Mem.nextblock m7 = Mem.nextblock m1
∧ Mem.range_perm m7 b1 0 20 Cur Freeable).
{
destruct ls; subst.
- exploit Mem.storebytes_mapped_inject; eauto.
{
exploit stencil_find_symbol_inject´; eauto.
intros HF.
inv inv_inject_neutral.
eapply flat_inj_inject_incr; eauto.
}
{
eapply list_forall2_bytelist_inject.
}
simpl.
intros (m7 & HSTB & Hinject´).
∃ m7.
refine_split´; trivial.
+ erewrite (Mem.nextblock_storebytes _ _ _ _ _ HSTB); eauto.
+ unfold Mem.range_perm. intros.
eapply Mem.perm_storebytes_1; eauto.
- refine_split´; trivial.
}
destruct HF as (m7 & HSTB & Hinject´ & Hnextblock7 & HV7).
destruct (Mem.range_perm_free _ _ _ _ HV7) as [m8 Free].
assert(HFreeInj: Mem.inject (Mem.flat_inj (Mem.nextblock m)) m´ m8).
{
eapply Mem.free_right_inject; eauto 1.
intros.
exploit HFB; eauto.
}
clear Hinject´.
unfold acquire_lock_spec in H2.
assert (ikern_val : ikern labd = true).
{ destruct (ikern labd); try inv H2; auto. }
rewrite ikern_val in H2.
assert (ihost_val : ihost labd = true).
{ destruct (ihost labd); try inv H2; auto. }
rewrite ihost_val in H2.
Opaque index2Z Shared2ID0.
assert (tmp_ev: ∃ abid, index2Z (Int.unsigned i) (Int.unsigned ofs) = Some abid).
{ destruct (index2Z (Int.unsigned i) (Int.unsigned ofs)); try inv H2.
∃ z; auto. }
destruct tmp_ev as (abid, index2Z_val).
rewrite index2Z_val in H2.
assert (tmp_ev: ∃ v, Shared2ID0 (Int.unsigned i) = Some v).
{ destruct (Shared2ID0 (Int.unsigned i)); try inv H2.
∃ p; auto. }
destruct tmp_ev as (pv, Shared2ID0_val).
rewrite Shared2ID0_val in H2.
assert (tmp_ev: ∃ l, ZMap.get abid (multi_log labd) = MultiDef l).
{ destruct (ZMap.get abid (multi_log labd)); try inv H2.
∃ l; auto. }
destruct tmp_ev as (l_val, multi_log_val).
rewrite multi_log_val in H2.
assert (lock_st: ZMap.get abid (lock labd) = LockFalse).
{ destruct (ZMap.get abid (lock labd)); try inv H2.
reflexivity. }
rewrite lock_st in H2.
assert (tmp_ev: ∃ h_lock_st, H_CalLock (TEVENT (CPU_ID labd) (TSHARED OPULL):: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat (Int.unsigned bound))))
:: ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)
= Some h_lock_st).
{ destruct (H_CalLock (TEVENT (CPU_ID labd) (TSHARED OPULL):: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat (Int.unsigned bound))))
:: ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)); try (inv H2; fail).
∃ p; auto. }
destruct tmp_ev as (h_lock_st, H_CalLock_val).
rewrite H_CalLock_val in H2.
inv H2.
assert (tmp_ev: ∃ h_lock_st´,
H_CalLock (TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat (Int.unsigned bound))))
:: ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)
= Some h_lock_st´).
{
eapply H_CalLock_pull; eauto.
}
destruct tmp_ev as (h_lock_st´, H_CalLock_val´).
exploit Hacquire_lock; eauto 2.
intros Hfunct.
rewrite (Lregset_rewrite rs).
∃ (Mem.flat_inj (Mem.nextblock m´)).
refine_split´; try eassumption.
rewrite H1.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1.
simpl.
rewrite HST2.
reflexivity.
Lregset_simpl_tac´ 1.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H10.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
case_eq (Val.add (rs ESP) (Vint (Int.repr 0))); intros;
try rewrite H2 in H10; try discriminate H10.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m)).
{
eapply Mem.load_valid_access in H10.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H10; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HST3.
reflexivity.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H11.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
try rewrite H2 in H11; try discriminate H11.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m)).
{
eapply Mem.load_valid_access in H11.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H11; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HST4.
reflexivity.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H12.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 8)) with (Int.repr 8).
case_eq (Val.add (rs ESP) (Vint (Int.repr 8))); intros;
try rewrite H2 in H12; try discriminate H12.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m)).
{
eapply Mem.load_valid_access in H12.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H12; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
assert ( Mem.load Mint32 m1 b2 (Int.unsigned i0) = Some (Vint ofs)).
{
erewrite Mem.load_alloc_other; eauto.
}
rewrite H8; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 8)))) with 8.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HSTofs.
reflexivity.
one_step_forward´.
unfold symbol_offset.
unfold fundef.
rewrite Hwait_lock_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_external _ b_wait_lock); eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
right. left. simpl. omega.
right. left. simpl. omega.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change ((Int.unsigned (Int.add Int.zero (Int.repr 4)))) with 4.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
right. left. simpl. omega.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change ((Int.unsigned (Int.add Int.zero (Int.repr 8)))) with 8.
erewrite Mem.load_store_same; eauto.
econstructor; eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
refine_split´. eassumption.
simpl. econstructor; eauto 1.
inversion Hstencil_matches.
constructor_gen_sem_intro.
simpl. econstructor. repeat econstructor.
unfold wait_hlock_spec.
Opaque H_CalLock. simpl.
rewrite ikern_val, ihost_val, index2Z_val.
rewrite multi_log_val, lock_st.
rewrite H_CalLock_val´.
reflexivity.
simpl. lift_trivial.
intros.
assert (Hb2_mofs: Ple (Genv.genv_next ge) b2 ∧ Plt b2 (Mem.nextblock mofs)).
{
unfold Lregset_fold in H2; simpl in H2.
rewrite Pregmap.gso in H2; [|congruence].
rewrite Pregmap.gso in H2; [|congruence].
rewrite Pregmap.gss in H2.
inv H2. rewrite Hnextblockofs.
eauto.
}
eauto.
intros F. inv F.
intros F. inv F.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
rewrite ikern_val, ihost_val.
unfold Mem.loadv in H11.
Lregset_simpl_tac.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
try rewrite H2 in H11; try discriminate H11.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
right. left. simpl. omega.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HST5.
reflexivity.
one_step_forward´.
accessors_simpl.
rewrite ikern_val, ihost_val.
unfold Mem.loadv in H12.
Lregset_simpl_tac.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 8)))) with 8.
case_eq (Val.add (rs ESP) (Vint (Int.repr 8))); intros;
try rewrite H2 in H12; try discriminate H12.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
right. right. simpl. omega.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HSTofs´.
reflexivity.
one_step_forward´.
unfold symbol_offset.
unfold fundef.
rewrite Hacquire_shared_symbol.
Lregset_simpl_tac.
eapply star_step; eauto.
eapply (LAsm.exec_step_prim_call _ b_acquire_shared); eauto 1; trivial.
econstructor.
refine_split´; eauto 1.
econstructor; eauto 1.
simpl.
econstructor.
instantiate (4:= ofs).
instantiate (4:= i).
unfold acquire_shared_spec.
simpl.
rewrite ikern_val, ihost_val, index2Z_val, Shared2ID0_val.
Locate acquire_lock_spec0.
repeat rewrite ZMap.gss.
rewrite H_CalLock_val.
reflexivity.
eassumption.
simpl.
eassumption.
reflexivity.
econstructor; eauto.
econstructor; eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto; simpl; eauto.
right. left. simpl. omega.
simpl.
econstructor.
econstructor.
eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
erewrite Mem.load_store_same; eauto; simpl; eauto.
simpl.
econstructor.
instantiate (1 := b_acquire_shared).
assert (Hsymbol: ∀ x, Genv.find_symbol ge x = find_symbol s x).
{
intros.
generalize (stencil_matches_symbols _ _ Hstencil_matches x).
auto.
}
erewrite Hsymbol in Hacquire_shared_symbol. auto.
Lregset_simpl_tac.
auto.
Lregset_simpl_tac.
one_step_forward´.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
unfold set; simpl.
assert (Hneq: b1 ≠ b0).
{
red; intros; subst.
specialize (genv_symb_range _ _ _ H3).
intro HB.
inv inv_inject_neutral.
exploit Mem.alloc_result; eauto.
intros; subst.
revert HB inv_mem_valid.
clear. intros. lift_unfold.
xomega.
}
assert (HLD1: Mem.load Mint32 m7 b1 16 = Some (rs RA)).
{
assert (HLD1: Mem.load Mint32 mofs´ b1 16 = Some (rs RA)).
{
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result. trivial.
apply inv_reg_wt.
}
destruct (GetSharedMemEvent
(ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)); subst; trivial.
erewrite Mem.load_storebytes_other; eauto; simpl.
}
rewrite HLD1.
assert (HLD2: Mem.load Mint32 m7 b1 12 = Some (rs ESP)).
{
assert (HLD2: Mem.load Mint32 mofs´ b1 12 = Some (rs ESP)).
{
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; left; omega].
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result. trivial.
apply inv_reg_wt.
}
destruct (GetSharedMemEvent
(ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)); subst; trivial.
erewrite Mem.load_storebytes_other; eauto; simpl.
}
rewrite HLD2.
rewrite Free. reflexivity.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
repeat rewrite ZMap.set2.
eapply star_refl.
reflexivity.
eapply inject_incr_refl.
assert(nbeq: Mem.nextblock m = Mem.nextblock m´).
{
destruct (GetSharedMemEvent
(ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)).
eapply Mem.nextblock_storebytes in H4; eauto.
subst. eauto.
}
rewrite nbeq in HFB.
rewrite <- nbeq; assumption.
generalize (Mem.nextblock_free _ _ _ _ _ Free); intro Hnextblock5.
generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro Hnextblock1.
assert(nbeq: Mem.nextblock m = Mem.nextblock m´).
{
destruct (GetSharedMemEvent
(ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)).
eapply Mem.nextblock_storebytes in H4; eauto.
subst. eauto.
}
rewrite Hnextblock5, Hnextblock7, Hnextblock1, nbeq.
xomega.
Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
unfold nextinstr; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
destruct reg; try congruence.
destruct i0; try congruence.
destruct f; try congruence.
destruct c; try congruence.
Qed.
Lemma acquire_lock_code_correct:
asm_spec_le (acquire_lock ↦ acquire_lock_spec_low)
(〚 acquire_lock ↦ acquire_lock_function 〛 mhticketlockop).
Proof.
eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b =
Some (Internal acquire_lock_function)).
{
assert (Hmodule:
get_module_function acquire_lock (acquire_lock ↦ acquire_lock_function)
= OK (Some acquire_lock_function)) by reflexivity.
assert (HInternal:
make_internal acquire_lock_function
= OK (AST.Internal acquire_lock_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol´ ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol´.
rewrite Hsymbol_PC in Hsymbol´. inv Hsymbol´.
assumption.
}
lift_trivial.
unfold lift; simpl.
set (Hstorebytes´ := match l with
| Some l´ ⇒
Mem.storebytes m´0 b0 0 (ByteList l´) = Some m0
| None ⇒ m0 = m´0
end).
subdestruct.
- assert(Hnextblock: Mem.nextblock m0 = Mem.nextblock m´0).
{ erewrite (Mem.nextblock_storebytes m´0 b0 0 (ByteList l0) m0 Hstorebytes); trivial. }
rewrite <- Hnextblock.
generalize Hspec; intro tmp.
unfold ObjQLock.acquire_lock_spec in tmp.
exploit acquire_lock_spec; eauto 2; simpl.
+ exact Hstorebytes.
+ subdestruct.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
split; [ reflexivity |].
∃ f´, (m0´, adt´), r_.
repeat split; try assumption.
try assumption.
inv tmp; subst.
exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
- generalize Hspec; intro tmp.
unfold ObjQLock.acquire_lock_spec in tmp.
exploit acquire_lock_spec; eauto 2; simpl.
+ reflexivity.
+ subst.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
split; [ reflexivity |].
∃ f´, (m0´, adt´), r_.
repeat split; try assumption; subst.
exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
Qed.
Lemma release_lock_spec:
∀ ge (s: stencil) (rs rs´ : regset) b b0 (m0: mem) (labd labd´ : RData) sig i ofs ls size id
(Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m0, labd))
(Hlow: low_level_invariant (Mem.nextblock m0) labd)
(Hhinv: high_level_invariant labd),
find_symbol s release_lock = Some b →
make_globalenv s (release_lock ↦ release_lock_function) mhticketlockop = ret ge →
rs PC = Vptr b Int.zero →
release_lock_spec0 (Int.unsigned i) (Int.unsigned ofs) ls labd = Some labd´ →
id2size (Int.unsigned i) = Some (size, id) →
find_symbol s id = Some b0 →
Mem.loadbytes m0 b0 0 size = Some (ByteList ls) →
asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
low_level_invariant (Mem.nextblock m0) labd →
high_level_invariant labd →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m0 sig (Vint i ::Vint ofs :: nil) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (release_lock ↦ release_lock_function) (mhticketlockop (Hmwd:= Hmwd) (Hmem:= Hmem))
release_lock s rs
(m0, labd) r_ (m0´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock m0)) f´
∧ Memtype.Mem.inject f´ m0 m0´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#RA <- Vundef #PC <- (rs#RA))) (Pregmap.get l r_)).
Proof.
intros.
inv Hasm.
inv H10.
inv H13.
inv H15.
inv H12.
simpl in H14.
simpl in H15.
caseEq(Mem.alloc m0 0 16).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
exploit Hrelease_shared; eauto.
intros [[b_release_shared [Hrelease_shared_symbol Hrelease_shared_fun] prim_release_shared]].
exploit Hpass_lock; eauto.
intros [[b_pass_lock [Hpass_lock_symbol Hpass_lock_fun] prim_pass_lock]].
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b1 8 Freeable).
{
eapply H9; auto; simpl; try omega.
unfold Z.divide.
∃ 2; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 12 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply H9; auto; simpl; try omega.
unfold Z.divide.
∃ 3; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.valid_access m3 Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H9; auto; simpl; try omega.
apply Zdivide_0.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint i) HV3) as [m4 HST3].
assert(Hnextblock4: Mem.nextblock m4 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
}
assert (HVofs: Mem.valid_access m4 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H9; auto; simpl; try omega.
∃ 1.
omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVofs; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint ofs) HVofs) as [mofs HSTofs].
assert(Hnextblockofs: Mem.nextblock mofs = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTofs); trivial.
}
assert (HV4: Mem.range_perm mofs b1 0 16 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV4) as [m5 Free].
unfold release_lock_spec in H2.
assert (ikern_val : ikern labd = true).
{ destruct (ikern labd); try inv H2; auto. }
rewrite ikern_val in H2.
assert (ihost_val : ihost labd = true).
{ destruct (ihost labd); try inv H2; auto. }
rewrite ihost_val in H2.
Opaque index2Z Shared2ID0.
assert (tmp_ev: ∃ abid, index2Z (Int.unsigned i) (Int.unsigned ofs) = Some abid).
{ destruct (index2Z (Int.unsigned i) (Int.unsigned ofs)); try inv H2.
∃ z; auto. }
destruct tmp_ev as (abid, index2Z_val).
rewrite index2Z_val in H2.
assert (tmp_ev: ∃ v, Shared2ID0 (Int.unsigned i) = Some v).
{ destruct (Shared2ID0 (Int.unsigned i)); try inv H2.
∃ p; auto. }
destruct tmp_ev as (pv, Shared2ID0_val).
rewrite Shared2ID0_val in H2.
assert (tmp_ev: ∃ l, ZMap.get abid (multi_log labd) = MultiDef l).
{ destruct (ZMap.get abid (multi_log labd)); try inv H2.
∃ l; auto. }
destruct tmp_ev as (l_val, multi_log_val).
rewrite multi_log_val in H2.
assert (lock_st: ZMap.get abid (lock labd) = LockOwn true).
{ destruct (ZMap.get abid (lock labd)); try inv H2.
destruct b2; inv H11.
reflexivity. }
rewrite lock_st in H2.
assert (tmp_ev: ∃ h_lock_st, H_CalLock
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OMEME ls)) :: l_val)
= Some h_lock_st).
{ destruct (H_CalLock
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OMEME ls)) :: l_val)); try inv H2.
∃ p; auto. }
destruct tmp_ev as (h_lock_st, H_CalLock_val).
rewrite H_CalLock_val in H2.
inv H2.
exploit Hrelease_lock; eauto 2.
intros Hfunct.
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption.
rewrite H1.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1.
simpl.
rewrite HST2.
reflexivity.
Lregset_simpl_tac´ 1.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H14.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
case_eq (Val.add (rs ESP) (Vint (Int.repr 0))); intros;
try rewrite H2 in H14; try discriminate H14.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m0)).
{
eapply Mem.load_valid_access in H14.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H14; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HST3.
reflexivity.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H15.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
try rewrite H2 in H15; try discriminate H15.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m0)).
{
eapply Mem.load_valid_access in H15.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H15; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HSTofs.
reflexivity.
one_step_forward´.
unfold symbol_offset.
unfold fundef.
rewrite Hrelease_shared_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_release_shared); eauto 1; trivial.
econstructor.
refine_split´; eauto 1.
econstructor; eauto 1.
simpl.
econstructor.
instantiate (2:= ls).
instantiate (2:= ofs).
instantiate (2:= i).
unfold release_shared_spec.
rewrite ikern_val, ihost_val, index2Z_val, Shared2ID0_val.
rewrite lock_st, multi_log_val.
Transparent H_CalLock.
assert (tmp_ev: ∃ h_lock_st´, H_CalLock (TEVENT (CPU_ID labd) (TSHARED (OMEME ls)) :: l_val) = Some h_lock_st´).
{
simpl.
simpl in H_CalLock_val.
destruct (H_CalLock l_val); try (inv H_CalLock_val; fail).
destruct p.
destruct p.
destruct h; try (inv H_CalLock_val; fail).
destruct o; try (inv H_CalLock_val; fail).
destruct o; try (inv H_CalLock_val; fail).
destruct (zeq (CPU_ID labd)); try (inv H_CalLock_val; fail).
destruct n; try (inv H_CalLock_val; fail); subst.
rewrite zeq_true in H_CalLock_val; try ring.
inv H_CalLock_val.
eexists; auto.
}
destruct tmp_ev as (? & tmp_ev).
rewrite tmp_ev.
reflexivity.
eassumption.
eassumption.
assert (Hb0b1: Plt b0 b1).
{
exploit (genv_symb_range). eapply H4.
inv Hstencil_matches. rewrite <- stencil_matches_genv_next.
destruct Hblock as [Hbge Hbm]. generalize Hbge. clearAll.
assert (Homega: ∀ a b c, Plt a b → Ple b c → Plt a c).
{
intros. xomega.
}
intros.
eapply Homega. eapply H. eapply Hbge.
}
assert (Homega_neq: ∀ a b, Plt a b → a ≠ b).
{
intros. xomega.
}
assert (b0 ≠ b1).
{
eapply Homega_neq. auto.
}
eapply Mem.loadbytes_store_other in HSTofs; eauto.
rewrite HSTofs.
eapply Mem.loadbytes_store_other in HST3; eauto.
rewrite HST3.
eapply Mem.loadbytes_store_other in HST2; eauto.
rewrite HST2.
eapply Mem.loadbytes_store_other in HST1; eauto.
rewrite HST1.
assert (Mem.loadbytes m1 b0 0 size = Mem.loadbytes m0 b0 0 size).
{
exploit Mem.loadbytes_alloc_unchanged. eapply HALC. unfold Mem.valid_block.
exploit Mem.alloc_result. eapply HALC. generalize Hb0b1. clearAll. intros.
assert (Homega: ∀ a b c, Plt a b → b = c → Plt a c).
{
intros. xomega.
}
eapply Homega; eauto.
intros Heq. apply Heq.
}
rewrite H10.
eassumption.
eauto.
change (Int.add (Int.add (Int.add (Int.add (Int.add (Int.repr 1) Int.one) Int.one)
Int.one) Int.one) Int.one) with (Int.repr 6).
simpl.
econstructor.
econstructor.
econstructor.
eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto; simpl; eauto.
right. left. simpl. omega.
simpl.
econstructor.
econstructor.
eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
erewrite Mem.load_store_same; eauto; simpl; eauto.
simpl.
econstructor.
instantiate (1 := b_release_shared).
eauto; try eassumption.
eauto.
assert (Hsymbol: ∀ x, Genv.find_symbol ge x = find_symbol s x).
{
intros.
generalize (stencil_matches_symbols _ _ Hstencil_matches x).
auto.
}
erewrite Hsymbol in Hrelease_shared_symbol. auto.
Lregset_simpl_tac.
auto.
Lregset_simpl_tac.
change (Int.add
(Int.add
(Int.add (Int.add (Int.add (Int.repr 1) Int.one) Int.one)
Int.one) Int.one) Int.one) with (Int.repr 6).
one_step_forward´.
unfold symbol_offset.
unfold fundef.
rewrite Hpass_lock_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_external _ b_pass_lock); eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
exploit (Mem.load_store_same). eapply HST3. simpl. intros Hb1_0.
exploit (Mem.load_store_other). eapply HSTofs. right. left.
instantiate (1:=Mint32).
instantiate (1:=0). simpl. omega.
intros Hloadb1_0. erewrite Hloadb1_0; eauto.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change ((Int.unsigned (Int.add Int.zero (Int.repr 4)))) with 4.
exploit (Mem.load_store_same). eapply HSTofs. simpl. intros Hb1_4.
eapply Hb1_4.
econstructor; eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
refine_split´. eassumption.
simpl. econstructor; eauto 1.
inversion Hstencil_matches.
constructor_gen_sem_intro.
simpl. econstructor. repeat econstructor.
unfold pass_hlock_spec.
Opaque H_CalLock. simpl.
rewrite ikern_val, ihost_val, index2Z_val.
repeat rewrite ZMap.gss.
rewrite H_CalLock_val.
reflexivity.
simpl. lift_trivial.
intros.
assert (Hb2_mofs: Ple (Genv.genv_next ge) b2 ∧ Plt b2 (Mem.nextblock mofs)).
{
unfold Lregset_fold in H2; simpl in H2.
rewrite Pregmap.gso in H2; [|congruence].
rewrite Pregmap.gso in H2; [|congruence].
rewrite Pregmap.gss in H2.
inv H2. rewrite Hnextblockofs.
eauto.
}
eauto.
intros F. inv F.
intros F. inv F.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
unfold set; simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
Ltac or_3_way_omega :=
try (left; omega);
try (right; left; omega);
try (right; right; try omega).
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_same; [| eauto].
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_same; [| eauto].
erewrite register_type_load_result.
rewrite Free. reflexivity.
apply inv_reg_wt.
Lregset_simpl_tac.
rewrite register_type_load_result by (apply inv_reg_wt; eauto).
one_step_forward´.
Lregset_simpl_tac.
repeat rewrite ZMap.set2.
eapply star_refl.
reflexivity.
eapply inject_incr_refl.
assert (HFB: ∀ bx delta, Mem.flat_inj (Mem.nextblock m0) bx ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt bx (Mem.nextblock m0)). inv H2.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H2.
}
eapply Mem.free_right_inject;[| eassumption |].
eapply Mem.store_outside_inject; [ | | eassumption].
eapply Mem.store_outside_inject; [ | | eassumption].
eapply Mem.store_outside_inject; [ | | eassumption].
eapply Mem.store_outside_inject; [ | | eassumption].
eapply Mem.alloc_right_inject; eauto.
inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
generalize (Mem.nextblock_free _ _ _ _ _ Free); intro Hnextblock5.
generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro Hnextblock1.
rewrite Hnextblock5, Hnextblockofs, Hnextblock1. xomega.
Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
unfold nextinstr; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
destruct reg; try congruence.
destruct i0; try congruence.
destruct f; try congruence.
destruct c; try congruence.
Qed.
Lemma release_lock_code_correct:
asm_spec_le (release_lock ↦ release_lock_spec_low)
(〚 release_lock ↦ release_lock_function 〛 mhticketlockop).
Proof.
eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
intros.
inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b =
Some (Internal release_lock_function)).
{
assert (Hmodule:
get_module_function release_lock (release_lock ↦ release_lock_function)
= OK (Some release_lock_function)) by reflexivity.
assert (HInternal:
make_internal release_lock_function
= OK (AST.Internal release_lock_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol´ ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol´.
rewrite Hsymbol_PC in Hsymbol´.
inv Hsymbol´.
assumption.
}
lift_trivial.
unfold lift; simpl.
generalize Hspec; intro tmp.
functional inversion tmp.
exploit release_lock_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
split; [ reflexivity |].
∃ f´, (m0´, adt´), r_.
repeat split; try assumption; subst.
exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
Qed.
End WITHMEM.
End ASM_VERIFICATION.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import MQTicketLock.
Require Import QTicketLockGenSpec.
Require Import QTicketLockGenAsmSource.
Require Import QTicketLockGenAsmData.
Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.
Section ASM_VERIFICATION.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Ltac accessors_simpl:=
match goal with
| |- exec_storeex _ _ _ _ _ _ _ = _ ⇒
unfold exec_storeex, LoadStoreSem1.exec_storeex1;
simpl; Lregset_simpl_tac;
match goal with
| |- context [Asm.exec_store _ _ _ _ _ _ _] ⇒
unfold Asm.exec_store; simpl;
Lregset_simpl_tac; lift_trivial
end
| |- exec_loadex _ _ _ _ _ _ = _ ⇒
unfold exec_loadex, LoadStoreSem1.exec_loadex1;
simpl; Lregset_simpl_tac;
match goal with
| |- context[Asm.exec_load _ _ _ _ _ _] ⇒
unfold Asm.exec_load; simpl;
Lregset_simpl_tac; lift_trivial
end
end.
Ltac clearAll := repeat match goal with
| [H: _ |- _] ⇒ clear H
end.
Lemma H_CalLock_pull:
∀ c l e
(Hcal: H_CalLock (TEVENT c (TSHARED OPULL):: l) = Some e),
∃ e´, H_CalLock l = Some e´.
Proof.
Transparent H_CalLock.
simpl; intros.
subdestruct. inv Hcal. eauto.
Opaque H_CalLock.
Qed.
Lemma acquire_lock_spec:
∀ ge (s: stencil) (rs rs´ : regset) b b0 (m m´: mem) (labd labd´ : RData) sig bound i ofs ls id
(Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m, labd))
(Hlow: low_level_invariant (Mem.nextblock m) labd)
(Hhinv: high_level_invariant labd),
find_symbol s acquire_lock = Some b →
make_globalenv s (acquire_lock ↦ acquire_lock_function) mhticketlockop = ret ge →
rs PC = Vptr b Int.zero →
acquire_lock_spec0 (Int.unsigned bound) (Int.unsigned i) (Int.unsigned ofs) labd = Some (labd´, id, ls) →
find_symbol s id = Some b0 →
(match ls with
| Some l´ ⇒ Mem.storebytes m b0 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end) →
sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint bound ::Vint i ::Vint ofs :: nil) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m´´ r_,
lasm_step (acquire_lock ↦ acquire_lock_function) (mhticketlockop (Hmwd:= Hmwd) (Hmem:= Hmem))
acquire_lock s rs
(m, labd) r_ (m´´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock m´)) f´
∧ Memtype.Mem.inject f´ m´ m´´
∧ (Mem.nextblock m´ ≤ Mem.nextblock m´´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#RA <- Vundef #PC <- (rs#RA)))
(Pregmap.get l r_)).
Proof.
intros.
inv Hasm.
inv H6.
inv H9.
inv H11.
inv H8.
inv H12.
inv H8.
simpl in H10.
simpl in H11.
simpl in H12.
caseEq(Mem.alloc m 0 20).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
exploit Hacquire_shared; eauto.
intros [[b_acquire_shared [Hacquire_shared_symbol Hacquire_shared_fun] prim_acquire_shared]].
exploit Hwait_lock; eauto.
intros [[b_wait_lock [Hwait_lock_symbol Hwait_lock_fun] prim_wait_lock]].
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b1 12 Freeable).
{
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 3; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 16 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 4; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.valid_access m3 Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint bound) HV3) as [m4 HST3].
assert(Hnextblock4: Mem.nextblock m4 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
}
assert (HV4: Mem.valid_access m4 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 1.
omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV4; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint i) HV4) as [m5 HST4].
assert (HVofs: Mem.valid_access m5 Mint32 b1 8 Freeable).
{
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.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 2; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVofs; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint ofs) HVofs) as [mofs HSTofs].
assert(Hnextblockofs: Mem.nextblock mofs = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTofs); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
}
assert (HV5: Mem.valid_access mofs Mint32 b1 0 Freeable).
{
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.
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV5; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint i) HV5) as [m6 HST5].
assert(Hnextblock6: Mem.nextblock m6 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
}
assert (HVofs´: Mem.valid_access m6 Mint32 b1 4 Freeable).
{
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.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H5; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVofs´; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint ofs) HVofs´) as [mofs´ HSTofs´].
assert(Hnextblockofs´: Mem.nextblock mofs´ = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTofs´); trivial.
}
assert (HV6: Mem.range_perm mofs´ b1 0 20 Cur Freeable).
{
unfold Mem.range_perm.
intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
assert (HFB: ∀ b2 delta, Mem.flat_inj (Mem.nextblock m) b2 ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b2 (Mem.nextblock m)). inv H6.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H6.
}
assert (Hinject: Mem.inject (Mem.flat_inj (Mem.nextblock m)) m mofs´).
{
repeat (eapply Mem.storebytes_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
}
assert (HF: ∃ m7,
match ls with
| Some l´ ⇒ Mem.storebytes mofs´ b0 0 (ByteList l´) = Some m7
| None ⇒ m7 = mofs´
end
∧ Mem.inject (Mem.flat_inj (Mem.nextblock m)) m´ m7
∧ Mem.nextblock m7 = Mem.nextblock m1
∧ Mem.range_perm m7 b1 0 20 Cur Freeable).
{
destruct ls; subst.
- exploit Mem.storebytes_mapped_inject; eauto.
{
exploit stencil_find_symbol_inject´; eauto.
intros HF.
inv inv_inject_neutral.
eapply flat_inj_inject_incr; eauto.
}
{
eapply list_forall2_bytelist_inject.
}
simpl.
intros (m7 & HSTB & Hinject´).
∃ m7.
refine_split´; trivial.
+ erewrite (Mem.nextblock_storebytes _ _ _ _ _ HSTB); eauto.
+ unfold Mem.range_perm. intros.
eapply Mem.perm_storebytes_1; eauto.
- refine_split´; trivial.
}
destruct HF as (m7 & HSTB & Hinject´ & Hnextblock7 & HV7).
destruct (Mem.range_perm_free _ _ _ _ HV7) as [m8 Free].
assert(HFreeInj: Mem.inject (Mem.flat_inj (Mem.nextblock m)) m´ m8).
{
eapply Mem.free_right_inject; eauto 1.
intros.
exploit HFB; eauto.
}
clear Hinject´.
unfold acquire_lock_spec in H2.
assert (ikern_val : ikern labd = true).
{ destruct (ikern labd); try inv H2; auto. }
rewrite ikern_val in H2.
assert (ihost_val : ihost labd = true).
{ destruct (ihost labd); try inv H2; auto. }
rewrite ihost_val in H2.
Opaque index2Z Shared2ID0.
assert (tmp_ev: ∃ abid, index2Z (Int.unsigned i) (Int.unsigned ofs) = Some abid).
{ destruct (index2Z (Int.unsigned i) (Int.unsigned ofs)); try inv H2.
∃ z; auto. }
destruct tmp_ev as (abid, index2Z_val).
rewrite index2Z_val in H2.
assert (tmp_ev: ∃ v, Shared2ID0 (Int.unsigned i) = Some v).
{ destruct (Shared2ID0 (Int.unsigned i)); try inv H2.
∃ p; auto. }
destruct tmp_ev as (pv, Shared2ID0_val).
rewrite Shared2ID0_val in H2.
assert (tmp_ev: ∃ l, ZMap.get abid (multi_log labd) = MultiDef l).
{ destruct (ZMap.get abid (multi_log labd)); try inv H2.
∃ l; auto. }
destruct tmp_ev as (l_val, multi_log_val).
rewrite multi_log_val in H2.
assert (lock_st: ZMap.get abid (lock labd) = LockFalse).
{ destruct (ZMap.get abid (lock labd)); try inv H2.
reflexivity. }
rewrite lock_st in H2.
assert (tmp_ev: ∃ h_lock_st, H_CalLock (TEVENT (CPU_ID labd) (TSHARED OPULL):: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat (Int.unsigned bound))))
:: ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)
= Some h_lock_st).
{ destruct (H_CalLock (TEVENT (CPU_ID labd) (TSHARED OPULL):: TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat (Int.unsigned bound))))
:: ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)); try (inv H2; fail).
∃ p; auto. }
destruct tmp_ev as (h_lock_st, H_CalLock_val).
rewrite H_CalLock_val in H2.
inv H2.
assert (tmp_ev: ∃ h_lock_st´,
H_CalLock (TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat (Int.unsigned bound))))
:: ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)
= Some h_lock_st´).
{
eapply H_CalLock_pull; eauto.
}
destruct tmp_ev as (h_lock_st´, H_CalLock_val´).
exploit Hacquire_lock; eauto 2.
intros Hfunct.
rewrite (Lregset_rewrite rs).
∃ (Mem.flat_inj (Mem.nextblock m´)).
refine_split´; try eassumption.
rewrite H1.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1.
simpl.
rewrite HST2.
reflexivity.
Lregset_simpl_tac´ 1.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H10.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
case_eq (Val.add (rs ESP) (Vint (Int.repr 0))); intros;
try rewrite H2 in H10; try discriminate H10.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m)).
{
eapply Mem.load_valid_access in H10.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H10; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HST3.
reflexivity.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H11.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
try rewrite H2 in H11; try discriminate H11.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m)).
{
eapply Mem.load_valid_access in H11.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H11; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HST4.
reflexivity.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H12.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 8)) with (Int.repr 8).
case_eq (Val.add (rs ESP) (Vint (Int.repr 8))); intros;
try rewrite H2 in H12; try discriminate H12.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m)).
{
eapply Mem.load_valid_access in H12.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H12; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
assert ( Mem.load Mint32 m1 b2 (Int.unsigned i0) = Some (Vint ofs)).
{
erewrite Mem.load_alloc_other; eauto.
}
rewrite H8; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 8)))) with 8.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HSTofs.
reflexivity.
one_step_forward´.
unfold symbol_offset.
unfold fundef.
rewrite Hwait_lock_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_external _ b_wait_lock); eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
right. left. simpl. omega.
right. left. simpl. omega.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change ((Int.unsigned (Int.add Int.zero (Int.repr 4)))) with 4.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
right. left. simpl. omega.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change ((Int.unsigned (Int.add Int.zero (Int.repr 8)))) with 8.
erewrite Mem.load_store_same; eauto.
econstructor; eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
refine_split´. eassumption.
simpl. econstructor; eauto 1.
inversion Hstencil_matches.
constructor_gen_sem_intro.
simpl. econstructor. repeat econstructor.
unfold wait_hlock_spec.
Opaque H_CalLock. simpl.
rewrite ikern_val, ihost_val, index2Z_val.
rewrite multi_log_val, lock_st.
rewrite H_CalLock_val´.
reflexivity.
simpl. lift_trivial.
intros.
assert (Hb2_mofs: Ple (Genv.genv_next ge) b2 ∧ Plt b2 (Mem.nextblock mofs)).
{
unfold Lregset_fold in H2; simpl in H2.
rewrite Pregmap.gso in H2; [|congruence].
rewrite Pregmap.gso in H2; [|congruence].
rewrite Pregmap.gss in H2.
inv H2. rewrite Hnextblockofs.
eauto.
}
eauto.
intros F. inv F.
intros F. inv F.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
rewrite ikern_val, ihost_val.
unfold Mem.loadv in H11.
Lregset_simpl_tac.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
try rewrite H2 in H11; try discriminate H11.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
right. left. simpl. omega.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HST5.
reflexivity.
one_step_forward´.
accessors_simpl.
rewrite ikern_val, ihost_val.
unfold Mem.loadv in H12.
Lregset_simpl_tac.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 8)))) with 8.
case_eq (Val.add (rs ESP) (Vint (Int.repr 8))); intros;
try rewrite H2 in H12; try discriminate H12.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
right. right. simpl. omega.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HSTofs´.
reflexivity.
one_step_forward´.
unfold symbol_offset.
unfold fundef.
rewrite Hacquire_shared_symbol.
Lregset_simpl_tac.
eapply star_step; eauto.
eapply (LAsm.exec_step_prim_call _ b_acquire_shared); eauto 1; trivial.
econstructor.
refine_split´; eauto 1.
econstructor; eauto 1.
simpl.
econstructor.
instantiate (4:= ofs).
instantiate (4:= i).
unfold acquire_shared_spec.
simpl.
rewrite ikern_val, ihost_val, index2Z_val, Shared2ID0_val.
Locate acquire_lock_spec0.
repeat rewrite ZMap.gss.
rewrite H_CalLock_val.
reflexivity.
eassumption.
simpl.
eassumption.
reflexivity.
econstructor; eauto.
econstructor; eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto; simpl; eauto.
right. left. simpl. omega.
simpl.
econstructor.
econstructor.
eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
erewrite Mem.load_store_same; eauto; simpl; eauto.
simpl.
econstructor.
instantiate (1 := b_acquire_shared).
assert (Hsymbol: ∀ x, Genv.find_symbol ge x = find_symbol s x).
{
intros.
generalize (stencil_matches_symbols _ _ Hstencil_matches x).
auto.
}
erewrite Hsymbol in Hacquire_shared_symbol. auto.
Lregset_simpl_tac.
auto.
Lregset_simpl_tac.
one_step_forward´.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
unfold set; simpl.
assert (Hneq: b1 ≠ b0).
{
red; intros; subst.
specialize (genv_symb_range _ _ _ H3).
intro HB.
inv inv_inject_neutral.
exploit Mem.alloc_result; eauto.
intros; subst.
revert HB inv_mem_valid.
clear. intros. lift_unfold.
xomega.
}
assert (HLD1: Mem.load Mint32 m7 b1 16 = Some (rs RA)).
{
assert (HLD1: Mem.load Mint32 mofs´ b1 16 = Some (rs RA)).
{
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result. trivial.
apply inv_reg_wt.
}
destruct (GetSharedMemEvent
(ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)); subst; trivial.
erewrite Mem.load_storebytes_other; eauto; simpl.
}
rewrite HLD1.
assert (HLD2: Mem.load Mint32 m7 b1 12 = Some (rs ESP)).
{
assert (HLD2: Mem.load Mint32 mofs´ b1 12 = Some (rs ESP)).
{
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; right; omega].
erewrite Mem.load_store_other; eauto; simpl; [| right; left; omega].
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result. trivial.
apply inv_reg_wt.
}
destruct (GetSharedMemEvent
(ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)); subst; trivial.
erewrite Mem.load_storebytes_other; eauto; simpl.
}
rewrite HLD2.
rewrite Free. reflexivity.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
repeat rewrite ZMap.set2.
eapply star_refl.
reflexivity.
eapply inject_incr_refl.
assert(nbeq: Mem.nextblock m = Mem.nextblock m´).
{
destruct (GetSharedMemEvent
(ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)).
eapply Mem.nextblock_storebytes in H4; eauto.
subst. eauto.
}
rewrite nbeq in HFB.
rewrite <- nbeq; assumption.
generalize (Mem.nextblock_free _ _ _ _ _ Free); intro Hnextblock5.
generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro Hnextblock1.
assert(nbeq: Mem.nextblock m = Mem.nextblock m´).
{
destruct (GetSharedMemEvent
(ZMap.get abid (multi_oracle labd) (CPU_ID labd) l_val ++ l_val)).
eapply Mem.nextblock_storebytes in H4; eauto.
subst. eauto.
}
rewrite Hnextblock5, Hnextblock7, Hnextblock1, nbeq.
xomega.
Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
unfold nextinstr; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
destruct reg; try congruence.
destruct i0; try congruence.
destruct f; try congruence.
destruct c; try congruence.
Qed.
Lemma acquire_lock_code_correct:
asm_spec_le (acquire_lock ↦ acquire_lock_spec_low)
(〚 acquire_lock ↦ acquire_lock_function 〛 mhticketlockop).
Proof.
eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b =
Some (Internal acquire_lock_function)).
{
assert (Hmodule:
get_module_function acquire_lock (acquire_lock ↦ acquire_lock_function)
= OK (Some acquire_lock_function)) by reflexivity.
assert (HInternal:
make_internal acquire_lock_function
= OK (AST.Internal acquire_lock_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol´ ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol´.
rewrite Hsymbol_PC in Hsymbol´. inv Hsymbol´.
assumption.
}
lift_trivial.
unfold lift; simpl.
set (Hstorebytes´ := match l with
| Some l´ ⇒
Mem.storebytes m´0 b0 0 (ByteList l´) = Some m0
| None ⇒ m0 = m´0
end).
subdestruct.
- assert(Hnextblock: Mem.nextblock m0 = Mem.nextblock m´0).
{ erewrite (Mem.nextblock_storebytes m´0 b0 0 (ByteList l0) m0 Hstorebytes); trivial. }
rewrite <- Hnextblock.
generalize Hspec; intro tmp.
unfold ObjQLock.acquire_lock_spec in tmp.
exploit acquire_lock_spec; eauto 2; simpl.
+ exact Hstorebytes.
+ subdestruct.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
split; [ reflexivity |].
∃ f´, (m0´, adt´), r_.
repeat split; try assumption.
try assumption.
inv tmp; subst.
exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
- generalize Hspec; intro tmp.
unfold ObjQLock.acquire_lock_spec in tmp.
exploit acquire_lock_spec; eauto 2; simpl.
+ reflexivity.
+ subst.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
split; [ reflexivity |].
∃ f´, (m0´, adt´), r_.
repeat split; try assumption; subst.
exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
Qed.
Lemma release_lock_spec:
∀ ge (s: stencil) (rs rs´ : regset) b b0 (m0: mem) (labd labd´ : RData) sig i ofs ls size id
(Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m0, labd))
(Hlow: low_level_invariant (Mem.nextblock m0) labd)
(Hhinv: high_level_invariant labd),
find_symbol s release_lock = Some b →
make_globalenv s (release_lock ↦ release_lock_function) mhticketlockop = ret ge →
rs PC = Vptr b Int.zero →
release_lock_spec0 (Int.unsigned i) (Int.unsigned ofs) ls labd = Some labd´ →
id2size (Int.unsigned i) = Some (size, id) →
find_symbol s id = Some b0 →
Mem.loadbytes m0 b0 0 size = Some (ByteList ls) →
asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
low_level_invariant (Mem.nextblock m0) labd →
high_level_invariant labd →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m0 sig (Vint i ::Vint ofs :: nil) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (release_lock ↦ release_lock_function) (mhticketlockop (Hmwd:= Hmwd) (Hmem:= Hmem))
release_lock s rs
(m0, labd) r_ (m0´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock m0)) f´
∧ Memtype.Mem.inject f´ m0 m0´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#RA <- Vundef #PC <- (rs#RA))) (Pregmap.get l r_)).
Proof.
intros.
inv Hasm.
inv H10.
inv H13.
inv H15.
inv H12.
simpl in H14.
simpl in H15.
caseEq(Mem.alloc m0 0 16).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
exploit Hrelease_shared; eauto.
intros [[b_release_shared [Hrelease_shared_symbol Hrelease_shared_fun] prim_release_shared]].
exploit Hpass_lock; eauto.
intros [[b_pass_lock [Hpass_lock_symbol Hpass_lock_fun] prim_pass_lock]].
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b1 8 Freeable).
{
eapply H9; auto; simpl; try omega.
unfold Z.divide.
∃ 2; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 12 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply H9; auto; simpl; try omega.
unfold Z.divide.
∃ 3; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.valid_access m3 Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H9; auto; simpl; try omega.
apply Zdivide_0.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint i) HV3) as [m4 HST3].
assert(Hnextblock4: Mem.nextblock m4 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
}
assert (HVofs: Mem.valid_access m4 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H9; auto; simpl; try omega.
∃ 1.
omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVofs; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint ofs) HVofs) as [mofs HSTofs].
assert(Hnextblockofs: Mem.nextblock mofs = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTofs); trivial.
}
assert (HV4: Mem.range_perm mofs b1 0 16 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV4) as [m5 Free].
unfold release_lock_spec in H2.
assert (ikern_val : ikern labd = true).
{ destruct (ikern labd); try inv H2; auto. }
rewrite ikern_val in H2.
assert (ihost_val : ihost labd = true).
{ destruct (ihost labd); try inv H2; auto. }
rewrite ihost_val in H2.
Opaque index2Z Shared2ID0.
assert (tmp_ev: ∃ abid, index2Z (Int.unsigned i) (Int.unsigned ofs) = Some abid).
{ destruct (index2Z (Int.unsigned i) (Int.unsigned ofs)); try inv H2.
∃ z; auto. }
destruct tmp_ev as (abid, index2Z_val).
rewrite index2Z_val in H2.
assert (tmp_ev: ∃ v, Shared2ID0 (Int.unsigned i) = Some v).
{ destruct (Shared2ID0 (Int.unsigned i)); try inv H2.
∃ p; auto. }
destruct tmp_ev as (pv, Shared2ID0_val).
rewrite Shared2ID0_val in H2.
assert (tmp_ev: ∃ l, ZMap.get abid (multi_log labd) = MultiDef l).
{ destruct (ZMap.get abid (multi_log labd)); try inv H2.
∃ l; auto. }
destruct tmp_ev as (l_val, multi_log_val).
rewrite multi_log_val in H2.
assert (lock_st: ZMap.get abid (lock labd) = LockOwn true).
{ destruct (ZMap.get abid (lock labd)); try inv H2.
destruct b2; inv H11.
reflexivity. }
rewrite lock_st in H2.
assert (tmp_ev: ∃ h_lock_st, H_CalLock
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OMEME ls)) :: l_val)
= Some h_lock_st).
{ destruct (H_CalLock
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OMEME ls)) :: l_val)); try inv H2.
∃ p; auto. }
destruct tmp_ev as (h_lock_st, H_CalLock_val).
rewrite H_CalLock_val in H2.
inv H2.
exploit Hrelease_lock; eauto 2.
intros Hfunct.
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption.
rewrite H1.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1.
simpl.
rewrite HST2.
reflexivity.
Lregset_simpl_tac´ 1.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H14.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
case_eq (Val.add (rs ESP) (Vint (Int.repr 0))); intros;
try rewrite H2 in H14; try discriminate H14.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m0)).
{
eapply Mem.load_valid_access in H14.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H14; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HST3.
reflexivity.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H15.
Lregset_simpl_tac.
change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
try rewrite H2 in H15; try discriminate H15.
rewrite ikern_val, ihost_val.
unfold Asm.exec_load.
unfold Mem.loadv.
unfold eval_addrmode; simpl.
Lregset_simpl_tac.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m0)).
{
eapply Mem.load_valid_access in H15.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H15; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b2 ≠ b1).
{
intro.
subst.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
unfold set; simpl.
rewrite ikern_val, ihost_val.
rewrite HSTofs.
reflexivity.
one_step_forward´.
unfold symbol_offset.
unfold fundef.
rewrite Hrelease_shared_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_release_shared); eauto 1; trivial.
econstructor.
refine_split´; eauto 1.
econstructor; eauto 1.
simpl.
econstructor.
instantiate (2:= ls).
instantiate (2:= ofs).
instantiate (2:= i).
unfold release_shared_spec.
rewrite ikern_val, ihost_val, index2Z_val, Shared2ID0_val.
rewrite lock_st, multi_log_val.
Transparent H_CalLock.
assert (tmp_ev: ∃ h_lock_st´, H_CalLock (TEVENT (CPU_ID labd) (TSHARED (OMEME ls)) :: l_val) = Some h_lock_st´).
{
simpl.
simpl in H_CalLock_val.
destruct (H_CalLock l_val); try (inv H_CalLock_val; fail).
destruct p.
destruct p.
destruct h; try (inv H_CalLock_val; fail).
destruct o; try (inv H_CalLock_val; fail).
destruct o; try (inv H_CalLock_val; fail).
destruct (zeq (CPU_ID labd)); try (inv H_CalLock_val; fail).
destruct n; try (inv H_CalLock_val; fail); subst.
rewrite zeq_true in H_CalLock_val; try ring.
inv H_CalLock_val.
eexists; auto.
}
destruct tmp_ev as (? & tmp_ev).
rewrite tmp_ev.
reflexivity.
eassumption.
eassumption.
assert (Hb0b1: Plt b0 b1).
{
exploit (genv_symb_range). eapply H4.
inv Hstencil_matches. rewrite <- stencil_matches_genv_next.
destruct Hblock as [Hbge Hbm]. generalize Hbge. clearAll.
assert (Homega: ∀ a b c, Plt a b → Ple b c → Plt a c).
{
intros. xomega.
}
intros.
eapply Homega. eapply H. eapply Hbge.
}
assert (Homega_neq: ∀ a b, Plt a b → a ≠ b).
{
intros. xomega.
}
assert (b0 ≠ b1).
{
eapply Homega_neq. auto.
}
eapply Mem.loadbytes_store_other in HSTofs; eauto.
rewrite HSTofs.
eapply Mem.loadbytes_store_other in HST3; eauto.
rewrite HST3.
eapply Mem.loadbytes_store_other in HST2; eauto.
rewrite HST2.
eapply Mem.loadbytes_store_other in HST1; eauto.
rewrite HST1.
assert (Mem.loadbytes m1 b0 0 size = Mem.loadbytes m0 b0 0 size).
{
exploit Mem.loadbytes_alloc_unchanged. eapply HALC. unfold Mem.valid_block.
exploit Mem.alloc_result. eapply HALC. generalize Hb0b1. clearAll. intros.
assert (Homega: ∀ a b c, Plt a b → b = c → Plt a c).
{
intros. xomega.
}
eapply Homega; eauto.
intros Heq. apply Heq.
}
rewrite H10.
eassumption.
eauto.
change (Int.add (Int.add (Int.add (Int.add (Int.add (Int.repr 1) Int.one) Int.one)
Int.one) Int.one) Int.one) with (Int.repr 6).
simpl.
econstructor.
econstructor.
econstructor.
eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto; simpl; eauto.
right. left. simpl. omega.
simpl.
econstructor.
econstructor.
eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
erewrite Mem.load_store_same; eauto; simpl; eauto.
simpl.
econstructor.
instantiate (1 := b_release_shared).
eauto; try eassumption.
eauto.
assert (Hsymbol: ∀ x, Genv.find_symbol ge x = find_symbol s x).
{
intros.
generalize (stencil_matches_symbols _ _ Hstencil_matches x).
auto.
}
erewrite Hsymbol in Hrelease_shared_symbol. auto.
Lregset_simpl_tac.
auto.
Lregset_simpl_tac.
change (Int.add
(Int.add
(Int.add (Int.add (Int.add (Int.repr 1) Int.one) Int.one)
Int.one) Int.one) Int.one) with (Int.repr 6).
one_step_forward´.
unfold symbol_offset.
unfold fundef.
rewrite Hpass_lock_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_external _ b_pass_lock); eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
exploit (Mem.load_store_same). eapply HST3. simpl. intros Hb1_0.
exploit (Mem.load_store_other). eapply HSTofs. right. left.
instantiate (1:=Mint32).
instantiate (1:=0). simpl. omega.
intros Hloadb1_0. erewrite Hloadb1_0; eauto.
econstructor; eauto 1.
econstructor; eauto 1.
simpl. lift_trivial.
change ((Int.unsigned (Int.add Int.zero (Int.repr 4)))) with 4.
exploit (Mem.load_store_same). eapply HSTofs. simpl. intros Hb1_4.
eapply Hb1_4.
econstructor; eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
refine_split´. eassumption.
simpl. econstructor; eauto 1.
inversion Hstencil_matches.
constructor_gen_sem_intro.
simpl. econstructor. repeat econstructor.
unfold pass_hlock_spec.
Opaque H_CalLock. simpl.
rewrite ikern_val, ihost_val, index2Z_val.
repeat rewrite ZMap.gss.
rewrite H_CalLock_val.
reflexivity.
simpl. lift_trivial.
intros.
assert (Hb2_mofs: Ple (Genv.genv_next ge) b2 ∧ Plt b2 (Mem.nextblock mofs)).
{
unfold Lregset_fold in H2; simpl in H2.
rewrite Pregmap.gso in H2; [|congruence].
rewrite Pregmap.gso in H2; [|congruence].
rewrite Pregmap.gss in H2.
inv H2. rewrite Hnextblockofs.
eauto.
}
eauto.
intros F. inv F.
intros F. inv F.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
unfold set; simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
Ltac or_3_way_omega :=
try (left; omega);
try (right; left; omega);
try (right; right; try omega).
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_same; [| eauto].
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_other; eauto; [| simpl; or_3_way_omega].
erewrite Mem.load_store_same; [| eauto].
erewrite register_type_load_result.
rewrite Free. reflexivity.
apply inv_reg_wt.
Lregset_simpl_tac.
rewrite register_type_load_result by (apply inv_reg_wt; eauto).
one_step_forward´.
Lregset_simpl_tac.
repeat rewrite ZMap.set2.
eapply star_refl.
reflexivity.
eapply inject_incr_refl.
assert (HFB: ∀ bx delta, Mem.flat_inj (Mem.nextblock m0) bx ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt bx (Mem.nextblock m0)). inv H2.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H2.
}
eapply Mem.free_right_inject;[| eassumption |].
eapply Mem.store_outside_inject; [ | | eassumption].
eapply Mem.store_outside_inject; [ | | eassumption].
eapply Mem.store_outside_inject; [ | | eassumption].
eapply Mem.store_outside_inject; [ | | eassumption].
eapply Mem.alloc_right_inject; eauto.
inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
intros bx delta; intros; specialize (HFB bx delta); apply HFB; trivial.
generalize (Mem.nextblock_free _ _ _ _ _ Free); intro Hnextblock5.
generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro Hnextblock1.
rewrite Hnextblock5, Hnextblockofs, Hnextblock1. xomega.
Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
unfold nextinstr; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
destruct reg; try congruence.
destruct i0; try congruence.
destruct f; try congruence.
destruct c; try congruence.
Qed.
Lemma release_lock_code_correct:
asm_spec_le (release_lock ↦ release_lock_spec_low)
(〚 release_lock ↦ release_lock_function 〛 mhticketlockop).
Proof.
eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
intros.
inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b =
Some (Internal release_lock_function)).
{
assert (Hmodule:
get_module_function release_lock (release_lock ↦ release_lock_function)
= OK (Some release_lock_function)) by reflexivity.
assert (HInternal:
make_internal release_lock_function
= OK (AST.Internal release_lock_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol´ ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol´.
rewrite Hsymbol_PC in Hsymbol´.
inv Hsymbol´.
assumption.
}
lift_trivial.
unfold lift; simpl.
generalize Hspec; intro tmp.
functional inversion tmp.
exploit release_lock_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
split; [ reflexivity |].
∃ f´, (m0´, adt´), r_.
repeat split; try assumption; subst.
exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
Qed.
End WITHMEM.
End ASM_VERIFICATION.