Library mcertikos.proc.CVIntroGenAsm
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 PCVIntro.
Require Import PAbQueueAtomic.
Require Import CVIntroGenAsmSource.
Require Import CVIntroGenSpec.
Require Import LRegSet.
Require Import AbstractDataType.
Require Import LAsmModuleSemSpec.
Require Import LoadStoreSem2.
Section ASM_VERIFICATION.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation LDSCA := RData.
Notation LDSCAOps := (cdata (cdata_ops := pabqueue_data_ops) LDSCA).
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, LoadStoreSem2.exec_storeex2;
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, LoadStoreSem2.exec_loadex2;
simpl; Lregset_simpl_tac;
match goal with
| |- context[Asm.exec_load _ _ _ _ _ _ ] ⇒
unfold Asm.exec_load; simpl;
Lregset_simpl_tac; lift_trivial
end
end.
Section REL.
Lemma Hrel:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pabqueue_atomic = ret ge →
(∃ b, Genv.find_symbol ge release_lock = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external release_lock release_lock_sig)))
∧ get_layer_primitive release_lock pabqueue_atomic =
OK (Some (primcall_release_lock_compatsem release_lock release_lock_spec2)).
Proof.
intros.
assert (Hprim: get_layer_primitive release_lock pabqueue_atomic =
OK (Some (primcall_release_lock_compatsem release_lock release_lock_spec2)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hrel_SC:
∀ ge s b,
make_globalenv s (release_lock_CHAN ↦ release_lock_SC_function) pabqueue_atomic = ret ge →
find_symbol s release_lock_CHAN = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal release_lock_SC_function).
Proof.
intros.
assert (Hmodule: get_module_function release_lock_CHAN (release_lock_CHAN ↦ release_lock_SC_function)
= OK (Some release_lock_SC_function)) by
reflexivity.
assert (HInternal: make_internal release_lock_SC_function = OK (AST.Internal release_lock_SC_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma release_lock_SC_code_spec:
∀ ge (s: stencil) (rs: regset) m labd labd´ b b0 size id index sig
(Hsize: id2size ID_SC = Some (size, id))
(Hsig: sig = mksignature (AST.Tint::nil) None cc_default)
(Hargs: extcall_arguments rs m sig (Vint index :: nil))
l
,
make_globalenv s (release_lock_CHAN ↦ release_lock_SC_function) pabqueue_atomic = ret ge →
find_symbol s release_lock_CHAN = Some b →
rs PC = Vptr b Int.zero →
release_lock_spec2 ID_SC (Int.unsigned index) l labd = Some (labd´) →
find_symbol s SYNCCHPOOL_LOC = Some b0 →
Mem.loadbytes m b0 0 size = Some (ByteList l) →
asm_invariant (mem := mwd LDSCAOps) s rs (m, labd)→
low_level_invariant (Mem.nextblock m) labd →
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))# RA <- Vundef #PC <- (rs#RA)) in
∃ f´ m0´ r_,
lasm_step (release_lock_CHAN ↦ release_lock_SC_function) (pabqueue_atomic (Hmwd:= Hmwd) (Hmem:= Hmem))
release_lock_CHAN s rs
(m, labd) r_ (m0´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock m)) f´
∧ Memtype.Mem.inject f´ m m0´
∧ (Mem.nextblock m ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l rs´)
(Pregmap.get l r_)).
Proof.
intros until l.
intros Hge Hsymbol HPC Hspec Hsymbol0 Hloadbyte Hasm Hlow.
caseEq(Mem.alloc m 0 16).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDSCAOps)); eauto.
intros Hstencil_matches.
Local Opaque pabqueue_atomic.
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 Hasm. inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
exploit Hrel; eauto.
intros [[b_acq [Hacq_symbol Hacq_fun]] prim_acq].
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b1 8 Freeable).
{
eapply H; auto; simpl; try omega.
∃ 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 H; auto; simpl; try omega.
∃ 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 H; auto; simpl; try omega.
apply Zdivide_0.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ID_SC)) HV3) as [m4 HST3].
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 H; auto; simpl; try omega.
apply Zdivide_refl.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV4; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint index) HV4) as [m5 HST4].
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 H0.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H0.
}
assert (Hinject: Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m5).
{
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 Hasm. inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
}
assert (Hnextblock5: Mem.nextblock m5 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
}
assert (HV5: Mem.range_perm m5 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 _ _ _ _ HV5) as [m6 HFree].
assert (HUCTX: ikern labd = true
∧ ihost labd = true).
{
revert Hspec. clear.
unfold release_lock_spec. intros. subdestruct. auto.
}
destruct HUCTX as [ik ih].
exploit Hrel_SC; eauto 2. intros Hfunct.
assert (Hneq: b1 ≠ b0).
{
red; intros; subst.
specialize (genv_symb_range _ _ _ Hsymbol0).
intro HB.
inv Hasm. inv inv_inject_neutral.
exploit Mem.alloc_result; eauto.
intros; subst.
revert HB inv_mem_valid.
clear. intros. lift_unfold.
xomega.
}
inversion Hargs; subst.
inv H0.
inv H3.
simpl in H6.
rewrite (Lregset_rewrite rs).
refine_split´.
rewrite HPC.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
unfold set; simpl.
rewrite HALC. simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
Local Transparent pabqueue_atomic.
one_step_forward´.
unfold exec_storeex, LoadStoreSem2.exec_storeex2.
simpl; Lregset_simpl_tac. rewrite ik, ih.
unfold Asm.exec_store; simpl.
Lregset_simpl_tac. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
simpl in HST3.
rewrite HST3. reflexivity.
unfold set; simpl.
one_step_forward´.
accessors_simpl.
unfold Mem.loadv in H6.
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 H0 in H6; try discriminate H6.
rewrite ik, ih.
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 H6.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H6; [|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´.
unfold exec_storeex, LoadStoreSem2.exec_storeex2.
simpl; Lregset_simpl_tac. rewrite ik, ih.
unfold Asm.exec_store; simpl.
Lregset_simpl_tac. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
simpl in HST4.
rewrite HST4. reflexivity.
unfold set; simpl.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hacq_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_acq); eauto 1.
econstructor; eauto 1.
instantiate (4:= release_lock).
change positive with ident in ×.
rewrite prim_acq.
refine_split´; try reflexivity.
econstructor; eauto. simpl.
intros; subst. simpl in Hspec.
change 2 with (Int.unsigned (Int.repr 2)) in Hspec.
{
econstructor; eauto.
{
change (Int.unsigned (Int.repr 2)) with 2.
simpl. trivial.
}
{
erewrite Mem.loadbytes_store_other; try eapply HST4; [| left; auto].
erewrite Mem.loadbytes_store_other; try eapply HST3; [| left; auto].
erewrite Mem.loadbytes_store_other; try eapply HST2; [| left; auto].
erewrite Mem.loadbytes_store_other; try eapply HST1; [| left; auto].
inv Hsize.
erewrite Mem.loadbytes_alloc_unchanged; eauto.
eapply Mem.loadbytes_range_perm in Hloadbyte; eauto.
eapply (Mem.perm_valid_block _ _ 0); eauto.
}
constructor; eauto.
{
eapply extcall_arg_stack; eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto; [|simpl; right; left; omega].
erewrite Mem.load_store_same; eauto. trivial.
}
constructor; eauto.
{
eapply extcall_arg_stack; eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
erewrite Mem.load_store_same; eauto. trivial.
}
constructor; eauto.
{
inv Hstencil_matches.
erewrite <- stencil_matches_symbols; eauto.
}
{ reflexivity. }
}
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 8))) with 8.
unfold set; simpl.
assert (HLD1: Mem.load Mint32 m5 b1 12 = 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_same; eauto.
erewrite register_type_load_result. trivial.
inv Hasm.
apply inv_reg_wt.
}
rewrite HLD1.
assert (HLD2: Mem.load Mint32 m5 b1 8 = 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; left; omega].
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result. trivial.
inv Hasm.
apply inv_reg_wt.
}
rewrite HLD2.
rewrite HFree. reflexivity.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
constructor.
- reflexivity.
- reflexivity.
- eapply Mem.free_right_inject; eauto 1.
intros; specialize (HFB b2 delta); apply HFB; trivial.
- rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite Hnextblock5.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC); eauto.
clear. abstract xomega.
- subst rs´.
intros reg.
unfold Lregset_fold; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma release_lock_SC_code_correct:
asm_spec_le (release_lock_CHAN ↦ release_lock_SC_spec_low)
(〚release_lock_CHAN ↦ release_lock_SC_function 〛 pabqueue_atomic).
Proof.
eapply asm_sem_intro; try reflexivity; try (simpl; trivial; fail).
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDSCAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal release_lock_SC_function)).
{
assert (Hmodule: get_module_function release_lock_CHAN (release_lock_CHAN ↦ release_lock_SC_function)
= OK (Some release_lock_SC_function)) by
reflexivity.
assert (HInternal: make_internal release_lock_SC_function = OK (AST.Internal release_lock_SC_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.
}
simpl in Hsize. inv Hsize.
exploit release_lock_SC_code_spec; eauto 2.
reflexivity.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hv & Hnext & HV).
refine_split´; try eassumption.
- simpl. lift_trivial.
reflexivity.
- lift_unfold. split; trivial.
Qed.
End REL.
Section ACQ.
Lemma Hacq:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pabqueue_atomic = ret ge →
(∃ b, Genv.find_symbol ge acquire_lock = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external acquire_lock acquire_lock_sig)))
∧ get_layer_primitive acquire_lock pabqueue_atomic =
OK (Some (primcall_acquire_lock_compatsem acquire_lock_spec2)).
Proof.
intros.
assert (Hprim: get_layer_primitive acquire_lock pabqueue_atomic =
OK (Some (primcall_acquire_lock_compatsem acquire_lock_spec2)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hacq_SC:
∀ ge s b,
make_globalenv s (acquire_lock_CHAN ↦ acquire_lock_SC_function) pabqueue_atomic = ret ge →
find_symbol s acquire_lock_CHAN = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal acquire_lock_SC_function).
Proof.
intros.
assert (Hmodule: get_module_function acquire_lock_CHAN (acquire_lock_CHAN ↦ acquire_lock_SC_function)
= OK (Some acquire_lock_SC_function)) by
reflexivity.
assert (HInternal: make_internal acquire_lock_SC_function = OK (AST.Internal acquire_lock_SC_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma id_eq:
∀ labd labd´ id l index,
acquire_lock_spec2 (Z.of_nat local_lock_bound) ID_SC (Int.unsigned index) labd = Some (labd´, id, l) →
id = SYNCCHPOOL_LOC.
Proof.
intros. unfold acquire_lock_spec in ×.
subdestruct; inv H. trivial.
Qed.
Lemma acquire_lock_SC_code_spec:
∀ ge (s: stencil) (rs: regset) m m´ labd labd´ b b0 id sig index
(Hsig: sig = mksignature (AST.Tint::nil) None cc_default)
(Hargs: extcall_arguments rs m sig (Vint index :: nil))
l,
make_globalenv s (acquire_lock_CHAN ↦ acquire_lock_SC_function) pabqueue_atomic = ret ge →
find_symbol s acquire_lock_CHAN = Some b →
rs PC = Vptr b Int.zero →
acquire_lock_spec2 (Z.of_nat local_lock_bound) ID_SC (Int.unsigned index) labd = Some (labd´, id, l) →
find_symbol s SYNCCHPOOL_LOC = Some b0 →
match l with
| Some l´ ⇒ Mem.storebytes m b0 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end →
asm_invariant (mem := mwd LDSCAOps) s rs (m, labd)→
low_level_invariant (Mem.nextblock m) labd →
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))# RA <- Vundef #PC <- (rs#RA)) in
∃ f´ m0´ r_,
lasm_step (acquire_lock_CHAN ↦ acquire_lock_SC_function) (pabqueue_atomic (Hmwd:= Hmwd) (Hmem:= Hmem))
acquire_lock_CHAN s rs
(m, labd) r_ (m0´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock m)) f´
∧ Memtype.Mem.inject f´ m´ m0´
∧ (Mem.nextblock m´ ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l rs´)
(Pregmap.get l r_)).
Proof.
intros until l.
intros Hge Hsymbol HPC Hspec Hsymbol0 Hstorebyte Hasm Hlow.
caseEq(Mem.alloc m 0 20).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDSCAOps)); eauto.
intros Hstencil_matches.
Local Opaque pabqueue_atomic.
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 Hasm. inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
exploit Hacq; eauto.
intros [[b_acq [Hacq_symbol Hacq_fun]] prim_acq].
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b1 12 Freeable).
{
eapply H; auto; simpl; try omega.
∃ 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 H; auto; simpl; try omega.
∃ 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 H; auto; simpl; try omega.
apply Zdivide_0.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr (Z.of_nat local_lock_bound))) HV3) as [m4 HST3].
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 H; auto; simpl; try omega.
apply Zdivide_refl.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV4; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ID_SC)) HV4) as [m5 HST4].
assert (HV5: 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 H; auto; simpl; try omega.
∃ 2; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV5; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint index) HV5) as [m6 HST5].
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 H0.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H0.
}
assert (Hinject: Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m6).
{
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 Hasm. inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
}
assert (HF: ∃ m7,
match l with
| Some l´ ⇒ Mem.storebytes m6 b0 0 (ByteList l´) = Some m7
| None ⇒ m7 = m6
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 l; subst.
- exploit Mem.storebytes_mapped_inject; eauto.
{
exploit stencil_find_symbol_inject´; eauto.
intros HF.
inv Hasm. inv inv_inject_neutral.
lift_unfold.
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.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
+ unfold Mem.range_perm. intros.
eapply Mem.perm_storebytes_1; eauto.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
- refine_split´; trivial.
+ rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
+ unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct HF as (m7 & HSTB & Hinject´ & Hnextblock7 & HV7).
destruct (Mem.range_perm_free _ _ _ _ HV7) as [m8 HFree].
assert (HUCTX: ikern labd = true
∧ ihost labd = true).
{
revert Hspec. clear.
unfold acquire_lock_spec. intros. subdestruct. auto.
}
destruct HUCTX as [ik ih].
exploit Hacq_SC; eauto 2. intros Hfunct.
rewrite (Lregset_rewrite rs).
refine_split´.
rewrite HPC.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
unfold set; simpl.
rewrite HALC. simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
Local Transparent pabqueue_atomic.
one_step_forward´.
unfold exec_storeex, LoadStoreSem2.exec_storeex2.
simpl; Lregset_simpl_tac. rewrite ik, ih.
unfold Asm.exec_store; simpl.
Lregset_simpl_tac. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
simpl in HST3.
rewrite HST3. reflexivity.
unfold set; simpl.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
unfold exec_storeex, LoadStoreSem2.exec_storeex2.
simpl; Lregset_simpl_tac. rewrite ik, ih.
unfold Asm.exec_store; simpl.
Lregset_simpl_tac. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
simpl in HST4.
rewrite HST4. reflexivity.
unfold set; simpl.
one_step_forward´.
accessors_simpl.
inv Hargs.
inv H0.
inv H3.
simpl in H6.
unfold Mem.loadv in H6.
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 H0 in H6; try discriminate H6.
rewrite ik, ih.
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 H6.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H6; [|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.
erewrite Mem.load_alloc_other; eauto.
Lregset_simpl_tac.
one_step_forward´.
unfold exec_storeex, LoadStoreSem2.exec_storeex2.
simpl; Lregset_simpl_tac. rewrite ik, ih.
unfold Asm.exec_store; simpl.
Lregset_simpl_tac. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 8)))) with 8.
simpl in HST5.
rewrite HST5. reflexivity.
unfold set; simpl.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hacq_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_acq); eauto 1.
econstructor; eauto 1.
instantiate (4:= acquire_lock).
change positive with ident in ×.
rewrite prim_acq.
refine_split´; try reflexivity.
econstructor; eauto. simpl.
exploit id_eq; eauto.
intros; subst. simpl in Hspec.
change 2 with (Int.unsigned (Int.repr 2)) in Hspec.
change 10 with (Int.unsigned (Int.repr 10)) in Hspec.
{
econstructor; eauto.
constructor; eauto.
{
eapply extcall_arg_stack; eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto; [|simpl; right; left; omega].
erewrite Mem.load_store_other; eauto; [|simpl; right; left; omega].
erewrite Mem.load_store_same; eauto. trivial.
}
constructor; eauto.
{
eapply extcall_arg_stack; eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
erewrite Mem.load_store_other; eauto; [|simpl; right; left; omega].
erewrite Mem.load_store_same; eauto. trivial.
}
constructor; eauto.
{
eapply extcall_arg_stack; eauto.
simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
erewrite Mem.load_store_same; eauto. trivial.
}
constructor; eauto.
{
inv Hstencil_matches.
erewrite <- stencil_matches_symbols; eauto.
}
{ reflexivity. }
}
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 _ _ _ Hsymbol0).
intro HB.
inv Hasm. 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 m6 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_same; eauto.
erewrite register_type_load_result. trivial.
inv Hasm.
apply inv_reg_wt.
}
destruct l; 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 m6 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; left; omega].
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result. trivial.
inv Hasm.
apply inv_reg_wt.
}
destruct l; subst; trivial.
erewrite Mem.load_storebytes_other; eauto; simpl.
}
rewrite HLD2.
rewrite HFree. reflexivity.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
constructor.
- reflexivity.
- reflexivity.
- eapply Mem.free_right_inject; eauto 1.
intros; specialize (HFB b2 delta); apply HFB; trivial.
- rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite Hnextblock7.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC); eauto.
destruct l; subst.
+ erewrite (Mem.nextblock_storebytes _ _ _ _ _ Hstorebyte); eauto.
clear. abstract xomega.
+ clear. abstract xomega.
- subst rs´.
intros reg.
unfold Lregset_fold; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma acquire_lock_SC_code_correct:
asm_spec_le (acquire_lock_CHAN ↦ acquire_lock_SC_spec_low)
(〚acquire_lock_CHAN ↦ acquire_lock_SC_function 〛 pabqueue_atomic).
Proof.
eapply asm_sem_intro; try reflexivity; try (simpl; trivial; fail).
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDSCAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal acquire_lock_SC_function)).
{
assert (Hmodule: get_module_function acquire_lock_CHAN (acquire_lock_CHAN ↦ acquire_lock_SC_function)
= OK (Some acquire_lock_SC_function)) by
reflexivity.
assert (HInternal: make_internal acquire_lock_SC_function = OK (AST.Internal acquire_lock_SC_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.
}
exploit id_eq; eauto. intros; subst.
exploit acquire_lock_SC_code_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hv & Hnext & HV).
refine_split´; try eassumption.
- simpl; lift_trivial.
destruct l; subst.
+ exploit Mem.nextblock_storebytes; eauto.
intros He. rewrite He. reflexivity.
+ reflexivity.
- simpl; lift_trivial.
destruct l; subst.
+ exploit Mem.nextblock_storebytes; try eassumption.
intros He. rewrite He. eassumption.
+ eassumption.
- lift_unfold. split; trivial.
Qed.
End ACQ.
End WITHMEM.
End ASM_VERIFICATION.