Library mcertikos.proc.CVIntroGenFresh
This file provide the contextual refinement proof between PKContextNew layer and PThreadIntro layer
Require Import CVIntroGenDef.
Require Import CVIntroGenSpec.
Require Import XOmega.
Require Import CVIntroGenLemma.
Require Import CLemmas.
Require Import CVIntroGenSpec.
Require Import XOmega.
Require Import CVIntroGenLemma.
Require Import CLemmas.
Section Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section acquire_lock_SC_ref.
Lemma acquire_lock_Chan_spec_ref:
compatsim (crel HDATA LDATA) (gensem acquire_lock_SC_spec) acquire_lock_SC_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros Hargs0 Hasm_inv Hesp HRA Hle.
inv HSCP.
assert (HFB: ι b0 = Some (b0, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold acquire_lock_SC_spec; subrewrite.
set (rs2´ := (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) rs2))).
∃ ι, (rs2´#RA <- Vundef #PC <- (rs2#RA)).
subdestruct.
- inv HQ.
inv multi_log_re. pose proof H2 as Hre´.
specialize (H2 _ a).
rewrite Hdestruct3 in H2. inv H2.
exploit (relate_SC_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_SC_Log_GetSharedSC_Some; eauto.
intros (a´ & Hget & Hrel_e).
inv Hrel_e.
rewrite H0 in H4. inv H4.
assert (HST: ∃ m2´, Mem.storebytes m2 b1 0 (ByteList a´) = Some m2´).
{
eapply Mem.range_perm_storebytes; eauto. rewrite H9. simpl.
intros ofs Hofs.
rename H into Hmatch_SC.
assert (Hrange: 0 ≤ ofs / 16 < num_chan).
{
xomega.
}
specialize (Hmatch_SC _ Hrange).
destruct Hmatch_SC as (_ & _ & _ & _ & _ & Hv1 & _ & Hv2 & _ & Hv3 & _ & Hv4 & _).
assert (Hieq: ∃ j, ofs = (ofs / 16) × 16 + j ∧ 0 ≤ j < 16).
{
specialize (Z_div_mod_eq ofs 16). intros Hieq.
∃ (ofs mod 16).
split.
- replace (ofs / 16 × 16) with (16 × (ofs / 16)) by omega.
eapply Hieq. omega.
- eapply Z_mod_lt. omega.
}
destruct Hieq as (j & Heq & Hj).
rewrite Heq.
destruct (zlt j 4).
{
destruct Hv1 as (Hv1 & _).
eapply Hv1. simpl. omega.
}
destruct (zlt j 8).
{
destruct Hv2 as (Hv2 & _).
eapply Hv2. simpl. omega.
}
destruct (zlt j 12).
{
destruct Hv3 as (Hv3 & _).
eapply Hv3. simpl. omega.
}
{
destruct Hv4 as (Hv4 & _).
eapply Hv4. simpl. omega.
}
}
destruct HST as (m2´ & HST).
specialize (H8 _ _ HST).
rename H8 into HSC.
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec.
simpl; subrewrite´.
erewrite index2Z_eq; eauto.
rewrite <- H5. rewrite Hdestruct2.
erewrite (H_CalLock_relate_SC_log _ _ s); eauto.
eapply relate_SC_Log_pull; eauto.
eapply relate_SC_Log_ticket; eauto.
× rewrite Hget; eauto.
× inv Hargs. inv H4.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H3 as Hneq.
eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× intros.
destruct (zeq i0 (Int.unsigned i)); subst.
{
repeat rewrite ZMap.gss. constructor.
eapply relate_SC_Log_pull; eauto.
eapply relate_SC_Log_ticket; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
eapply neq_add; eauto.
eapply neq_add; eauto.
}
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H2; eauto 20).
- inv HQ.
inv multi_log_re. pose proof H2 as Hre´.
specialize (H2 _ a).
rewrite Hdestruct3 in H2. inv H2.
exploit (relate_SC_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_SC_Log_GetSharedSC_None; eauto.
intros Hget.
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec. simpl; subrewrite´.
erewrite index2Z_eq; eauto.
rewrite <- H5. rewrite Hdestruct2.
erewrite (H_CalLock_relate_SC_log _ _ s); eauto.
eapply relate_SC_Log_pull; eauto.
eapply relate_SC_Log_ticket; eauto.
× rewrite Hget; eauto.
× inv Hargs. inv H4.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H3 as Hneq.
eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× intros.
destruct (zeq i0 (Int.unsigned i)); subst.
{
repeat rewrite ZMap.gss. constructor.
eapply relate_SC_Log_pull; eauto.
eapply relate_SC_Log_ticket; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
eapply neq_add; eauto.
eapply neq_add; eauto.
}
× econstructor; eauto.
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H2; eauto 20).
Qed.
End acquire_lock_SC_ref.
Section release_lock_SC_ref.
Lemma match_SC_Vint:
∀ tb v1 v2 v3 v4,
match_Chan tb v1 v2 v3 v4 →
∃ v1´ v2´ v3´ v4´,
v1 = Vint v1´ ∧ v2 = Vint v2´ ∧ v3 = Vint v3´ ∧ v4 = Vint v4´.
Proof.
intros. inv H; unfold Vzero; eauto 10.
Qed.
Lemma loadbytes_rel_SC:
∀ iend tb m b
(Hpre: ∀ ofs,
0 ≤ ofs < iend →
∃ v1 v2 v3 v4,
Mem.load Mint32 m b (ofs × 16) = Some v1 ∧
Mem.valid_access m Mint32 b (ofs × 16) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 4) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 8) = Some v3 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 8) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 12) = Some v4 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 12) Writable ∧
match_Chan (ZMap.get ofs tb) v1 v2 v3 v4),
∀ ofs
(Hrange: 0 ≤ ofs < iend),
∃ l, Mem.loadbytes m b (ofs × 16) 16 = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (ofs × 16) (ByteList l) = Some m´ →
∃ v1 v2 v3 v4,
Mem.load Mint32 m´ b (ofs × 16) = Some v1 ∧
Mem.valid_access m´ Mint32 b (ofs × 16) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 4) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 4) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 8) = Some v3 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 8) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 12) = Some v4 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 12) Writable ∧
match_Chan (ZMap.get ofs tb) v1 v2 v3 v4).
Proof.
intros. specialize (Hpre _ Hrange).
destruct Hpre as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
exploit match_SC_Vint; eauto.
intros (v1´ & v2´ & v3´ & v4´ & ? & ? & ? & ?); subst.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l1 & HLD1 & Hd1).
exploit decode_val_bytelist; eauto.
intros (l1´ & ?); subst.
assert (Hof_nat: Z.of_nat (nat_of_Z 4) = 4).
{
rewrite nat_of_Z_max.
replace (Z.max 4 0) with 4 by xomega. trivial.
}
assert (Hlen1: Z.of_nat (length (ByteList l1´)) = 4).
{
exploit Mem.loadbytes_length; eauto.
intros Hlen1. rewrite Hlen1, Hof_nat. trivial.
}
revert HL2; intros.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l2 & HLD2 & Hd2).
exploit decode_val_bytelist; eauto.
intros (l2´ & ?); subst.
assert (Hlen2: Z.of_nat (length (ByteList l2´)) = 4).
{
exploit Mem.loadbytes_length; eauto.
intros Hlen2. rewrite Hlen2, Hof_nat. trivial.
}
revert HL3; intros.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l3 & HLD3 & Hd3).
exploit decode_val_bytelist; eauto.
intros (l3´ & ?); subst.
assert (Hlen3: Z.of_nat (length (ByteList l3´)) = 4).
{
exploit Mem.loadbytes_length; eauto.
intros Hlen3. rewrite Hlen3, Hof_nat. trivial.
}
revert HL4; intros.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l4 & HLD4 & Hd4).
exploit decode_val_bytelist; eauto.
intros (l4´ & ?); subst.
assert (Hlen4: Z.of_nat (length (ByteList l4´)) = 4).
{
exploit Mem.loadbytes_length; eauto.
intros Hlen4. rewrite Hlen4, Hof_nat. trivial.
}
∃ (l1´ ++ l2´ ++ l3´ ++ l4´).
split.
- repeat rewrite ByteList_cons.
change 16 with (4 + (4 + (4 + 4))) at 2.
eapply Mem.loadbytes_concat; eauto; try omega.
eapply Mem.loadbytes_concat; eauto; try omega.
eapply Mem.loadbytes_concat; eauto; try omega.
replace (ofs × 16 + 4 + 4) with (ofs × 16 + 8) by omega. trivial.
replace (ofs × 16 + 4 + 4 + 4) with (ofs × 16 + 12) by omega. trivial.
- intros ? ? HSTB.
repeat rewrite ByteList_cons in HSTB.
eapply Mem.storebytes_split in HSTB.
destruct HSTB as (m1 & HST1 & HST2).
rewrite Hlen1 in HST2.
eapply Mem.storebytes_split in HST2.
destruct HST2 as (m2 & HST2 & HST3).
rewrite Hlen2 in HST3.
replace (ofs × 16 + 4 + 4) with (ofs × 16 + 8) in HST3 by omega.
eapply Mem.storebytes_split in HST3.
destruct HST3 as (m3 & HST3 & HST4).
rewrite Hlen3 in HST4.
replace (ofs × 16 + 8 + 4) with (ofs × 16 + 12) in HST4 by omega.
∃ (Vint v1´), (Vint v2´), (Vint v3´), (Vint v4´).
refine_split´; eauto.
+ erewrite Mem.load_storebytes_other; try eapply HST4.
erewrite Mem.load_storebytes_other; try eapply HST3.
erewrite Mem.load_storebytes_other; try eapply HST2.
eapply Mem.loadbytes_storebytes_same in HST1.
rewrite Hlen1 in HST1.
rewrite Hd1. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 4). xomega.
right. simpl. left. reflexivity.
right. simpl. left. omega.
right. simpl. left. omega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST1.
unfold Mem.valid_access.
simpl. rewrite Hlen1 in HST1.
split; trivial. ∃ (ofs × 4). omega.
+ erewrite Mem.load_storebytes_other; try eapply HST4.
erewrite Mem.load_storebytes_other; try eapply HST3.
eapply Mem.loadbytes_storebytes_same in HST2.
rewrite Hlen2 in HST2.
rewrite Hd2. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 4 + 1). xomega.
right. simpl. left. omega.
right. simpl. left. omega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST2.
unfold Mem.valid_access.
simpl. rewrite Hlen2 in HST2.
split; trivial. ∃ (ofs × 4 + 1). omega.
+ erewrite Mem.load_storebytes_other; try eapply HST4.
eapply Mem.loadbytes_storebytes_same in HST3.
rewrite Hlen3 in HST3.
rewrite Hd3. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 4 + 2). xomega.
right. simpl. left. omega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST3.
unfold Mem.valid_access.
simpl. rewrite Hlen3 in HST3.
split; trivial. ∃ (ofs × 4 + 2). omega.
+ eapply Mem.loadbytes_storebytes_same in HST4.
rewrite Hlen4 in HST4.
rewrite Hd4. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 4 + 3). xomega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST4.
unfold Mem.valid_access.
simpl. rewrite Hlen4 in HST4.
split; trivial. ∃ (ofs × 4 + 3). omega.
Qed.
Lemma loadbytes_rel_ind_SC:
∀ iend tb m b
(Hpre: ∀ ofs,
0 ≤ ofs < Z.of_nat (iend) →
∃ v1 v2 v3 v4,
Mem.load Mint32 m b (ofs × 16) = Some v1 ∧
Mem.valid_access m Mint32 b (ofs × 16) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 4) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 8) = Some v3 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 8) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 12) = Some v4 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 12) Writable ∧
match_Chan (ZMap.get ofs tb) v1 v2 v3 v4),
∃ l, Mem.loadbytes m b 0 (Z.of_nat iend × 16) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
(∀ ofs,
0 ≤ ofs < Z.of_nat (iend) →
∃ v1 v2 v3 v4,
Mem.load Mint32 m´ b (ofs × 16) = Some v1 ∧
Mem.valid_access m´ Mint32 b (ofs × 16) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 4) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 4) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 8) = Some v3 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 8) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 12) = Some v4 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 12) Writable ∧
match_Chan (ZMap.get ofs tb) v1 v2 v3 v4)).
Proof.
induction iend.
- change (Z.of_nat 0) with 0.
intros. simpl.
erewrite Mem.loadbytes_empty; [|reflexivity].
∃ nil. split; trivial.
intros. omega.
- intros.
assert (Hrange: 0 ≤ Z.of_nat (iend) < Z.of_nat (S iend)) by xomega.
exploit loadbytes_rel_SC; eauto.
intros (l & HLD & HST).
exploit (IHiend tb m b); eauto.
{
intros. eapply Hpre. omega.
}
intros (l´ & HLD´ & HST´).
∃ (l´ ++ l).
split.
+ replace (Z.of_nat (S iend) × 16) with ((Z.of_nat (iend) × 16) + 16) by xomega.
rewrite ByteList_cons.
eapply Mem.loadbytes_concat; eauto; try xomega.
+ intros.
rewrite ByteList_cons in H.
eapply Mem.storebytes_split in H.
destruct H as (m1 & HST1 & HST2).
exploit Mem.loadbytes_length; eauto.
intros Heq. rewrite Heq in HST2.
rewrite nat_of_Z_max in HST2.
replace (Z.max (Z.of_nat iend × 16) 0) with (Z.of_nat iend × 16) in HST2 by xomega.
simpl in HST2.
destruct (zlt ofs (Z.of_nat (iend))).
{
specialize (HST´ _ _ HST1).
exploit (HST´ ofs). omega.
intros (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
refine_split´; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
}
{
specialize (HST _ _ HST2).
destruct HST as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (Heq1: ofs = Z.of_nat iend).
{
destruct (zeq ofs (Z.of_nat iend)); trivial.
xomega.
}
rewrite Heq1.
refine_split´; eauto.
}
Qed.
Lemma loadbytes_rel_storebytes_SC:
∀ s tb m b
(Htb: match_ChanPool s tb m)
(Hsymbol: find_symbol s SYNCCHPOOL_LOC = Some b),
∃ l, Mem.loadbytes m b 0 (num_chan × 16) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_ChanPool s tb m´).
Proof.
intros.
specialize (loadbytes_rel_ind_SC (Z.to_nat num_chan) tb m b).
rewrite Z2Nat.id; [| omega].
intros HM. inv Htb.
rewrite H0 in Hsymbol; inv Hsymbol.
specialize (HM H).
destruct HM as (l & HLD & HST).
∃ l. split; trivial.
intros. econstructor. eauto. assumption.
Qed.
Lemma match_ChanPool_gso:
∀ s b t m m´ ofs v
(Hmatch: match_ChanPool s t m)
(Hsymbol: find_symbol s SYNCCHPOOL_LOC = Some b)
(HST: Mem.store Mint32 m b ofs v = Some m´)
(Hge: ofs ≥ num_chan × 16),
match_ChanPool s t m´.
Proof.
intros. inv Hmatch. rewrite Hsymbol in H0; inv H0. econstructor; eauto.
intros. specialize (H _ H0).
destruct H as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
repeat (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto; [|simpl; right; left; omega]).
refine_split´; eauto;
eapply Mem.store_valid_access_1; eauto.
Qed.
Lemma loadbytes_rel_storebytes:
∀ s sc m b
(HSC: match_ChanPool s sc m)
(Hsymbol: find_symbol s SYNCCHPOOL_LOC = Some b),
∃ l, Mem.loadbytes m b 0 (num_chan × 16) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_ChanPool s sc m´).
Proof.
intros.
exploit loadbytes_rel_storebytes_SC; eauto.
Qed.
Lemma release_lock_SC_spec_ref:
compatsim (crel HDATA LDATA) (gensem release_lock_SC_spec) release_lock_SC_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
intros Hargs0 Hasm_inv Hesp HRA Hle.
assert (HFB: ι b0 = Some (b0, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold release_lock_SC_spec; subrewrite.
set (rs2´ := (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) rs2))).
∃ ι, (rs2´#RA <- Vundef #PC <- (rs2#RA)).
subdestruct.
- inv HQ.
inv multi_log_re. pose proof H2 as Hre´.
specialize (H2 _ a).
rewrite Hdestruct3 in H2. inv H2.
inv match_match.
exploit loadbytes_rel_storebytes; eauto.
intros (l1 & HLD & HST).
assert (Hrel_e: relate_SC_MultiEvent s (TSHARED (OSCE (syncchpool d1))) (TSHARED (OMEME l1))).
{
constructor; eauto.
econstructor; eauto.
eapply Mem.loadbytes_length in HLD. rewrite HLD.
rewrite nat_of_Z_max. reflexivity.
}
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold release_lock_spec. simpl; subrewrite´.
erewrite index2Z_eq; eauto.
rewrite <- H5. rewrite Hdestruct5.
erewrite (H_CalLock_relate_SC_log _ _ s); eauto.
eapply relate_SC_Log_ticket; eauto.
econstructor; eauto.
× trivial.
× inv Hargs. inv H4.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H3 as Hneq.
eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× intros.
destruct (zeq i0 (Int.unsigned i)); subst.
{
repeat rewrite ZMap.gss. constructor.
eapply relate_SC_Log_ticket; eauto.
constructor; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
eapply neq_add; eauto.
eapply neq_add; eauto.
}
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H2; eauto 20).
Qed.
End release_lock_SC_ref.
Lemma get_sync_chan_to_ref:
compatsim (crel HDATA LDATA) (gensem get_sync_chan_to_spec) get_sync_chan_to_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H2; subst; eauto.
}
refine_split; eauto.
econstructor; eauto.
specialize (H (Int.unsigned i) irange).
blast H; eauto.
lift_unfold.
rewrite Hex1.
{
functional inversion H2; subst.
inv Hex9;
rewrite <- H13 in H11; inv H11.
apply unsigned_inj in H. rewrite H. reflexivity.
}
Qed.
Lemma get_sync_chan_paddr_ref:
compatsim (crel HDATA LDATA) (gensem get_sync_chan_paddr_spec) get_sync_chan_paddr_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H2; subst; eauto.
}
refine_split; eauto.
econstructor; eauto.
specialize (H (Int.unsigned i) irange).
blast H; eauto.
lift_unfold.
rewrite Hex2.
{
functional inversion H2; subst.
inv Hex9;
rewrite <- H13 in H11; inv H11.
apply unsigned_inj in H. rewrite H. reflexivity.
}
Qed.
Lemma get_sync_chan_count_ref:
compatsim (crel HDATA LDATA) (gensem get_sync_chan_count_spec) get_sync_chan_count_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H2; subst; eauto.
}
refine_split; eauto.
econstructor; eauto.
specialize (H (Int.unsigned i) irange).
blast H; eauto.
lift_unfold.
rewrite Hex4.
{
functional inversion H2; subst.
inv Hex9;
rewrite <- H13 in H11; inv H11.
apply unsigned_inj in H. rewrite H. reflexivity.
}
Qed.
Lemma get_sync_chan_busy_ref:
compatsim (crel HDATA LDATA) (gensem get_sync_chan_busy_spec) get_sync_chan_busy_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H2; subst; eauto.
}
refine_split; eauto.
econstructor; eauto.
specialize (H (Int.unsigned i) irange).
blast H; eauto.
lift_unfold.
rewrite Hex6.
{
functional inversion H2; subst.
inv Hex9;
rewrite <- H13 in H11; inv H11.
apply unsigned_inj in H. rewrite H. reflexivity.
}
Qed.
Lemma set_sync_chan_to_ref:
compatsim (crel HDATA LDATA) (gensem set_sync_chan_to_spec) set_sync_chan_to_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) Hex0); intros [m´ HST].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. eapply HST. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ (Vint i0), e0, e1, e2. refine_split; eauto.
- exploit Mem.load_store_same. eapply HST. simpl. intros HL. eapply HL.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 4). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 8). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 12). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gss. rewrite Int.repr_unsigned.
inv Hex9;
rewrite <- H12 in H11; inv H11.
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma set_sync_chan_paddr_ref:
compatsim (crel HDATA LDATA) (gensem set_sync_chan_paddr_spec) set_sync_chan_paddr_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) Hex3); intros [m´ HST].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. eapply HST. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ e, (Vint i0), e1, e2. refine_split; eauto.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit Mem.load_store_same. eapply HST. simpl. intros HL. eapply HL.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 8). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 12). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gss. rewrite Int.repr_unsigned.
inv Hex9;
rewrite <- H12 in H11; inv H11.
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma set_sync_chan_count_ref:
compatsim (crel HDATA LDATA) (gensem set_sync_chan_count_spec) set_sync_chan_count_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) Hex5); intros [m´ HST].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. eapply HST. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ e, e0, (Vint i0), e2. refine_split; eauto.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16 + 4). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit Mem.load_store_same. eapply HST. simpl. intros HL. eapply HL.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 12). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gss. rewrite Int.repr_unsigned.
inv Hex9;
rewrite <- H12 in H11; inv H11.
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma set_sync_chan_busy_ref:
compatsim (crel HDATA LDATA) (gensem set_sync_chan_busy_spec) set_sync_chan_busy_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) Hex7); intros [m´ HST].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. eapply HST. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ e, e0, e1, (Vint i0). refine_split; eauto.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16 + 4). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16 + 8). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit Mem.load_store_same. eapply HST. simpl. intros HL. eapply HL.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gss. rewrite Int.repr_unsigned.
inv Hex9;
rewrite <- H12 in H11; inv H11.
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma init_sync_chan_ref:
compatsim (crel HDATA LDATA) (gensem init_sync_chan_spec) init_sync_chan_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_chan)) Hex0); intros [m´1 HST1].
assert (Hvalid1: Mem.valid_access m´1 Mint32 b (Int.unsigned i × 16 + 4) Writable).
{
eapply Mem.store_valid_access_1. eapply HST1. eassumption.
}
specialize (Mem.valid_access_store _ _ _ _ (Vint Int.zero) Hvalid1); intros [m´2 HST2].
assert (Hvalid2: Mem.valid_access m´2 Mint32 b (Int.unsigned i × 16 + 8) Writable).
{
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
}
specialize (Mem.valid_access_store _ _ _ _ (Vint Int.zero) Hvalid2); intros [m´3 HST3].
assert (Hvalid3: Mem.valid_access m´3 Mint32 b (Int.unsigned i × 16 + 12) Writable).
{
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
}
specialize (Mem.valid_access_store _ _ _ _ (Vint Int.zero) Hvalid3); intros [m´4 HST4].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. instantiate (1:= (m´1, d2)). eapply HST1. reflexivity.
lift_unfold. split. instantiate (1:= (m´2, d2)). eapply HST2. reflexivity.
lift_unfold. split. instantiate (1:= (m´3, d2)). eapply HST3. reflexivity.
lift_unfold. split. eapply HST4. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ (Vint (Int.repr num_chan)) ,(Vint (Int.zero)) ,(Vint (Int.zero)) ,(Vint (Int.zero)). refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_same; [| eapply HST1]; simpl; reflexivity.
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_same; [| eapply HST2]; simpl; reflexivity.
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_same; [| eapply HST3]; simpl; reflexivity.
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_same; [| eapply HST4]; simpl; reflexivity.
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- rewrite ZMap.gss. simpl.
inv Hex9;
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [eauto |eassumption| right; simpl; omega].
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [eauto |eassumption| right; simpl; omega].
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [eauto |eassumption| right; simpl; omega].
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [eauto |eassumption| right; simpl; omega].
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma get_kernel_pa_ref:
compatsim (crel HDATA LDATA) (gensem get_kernel_pa_spec)
get_kernel_pa_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
exploit get_kernel_pa_exist; eauto 1.
intros HP.
refine_split; try econstructor; eauto.
- functional inversion H2. functional inversion H4; functional inversion H7;
unfold PDE_Arg in *; subdestruct; try assumption.
- functional inversion HP. functional inversion H4; functional inversion H7; split; eauto.
Qed.
End WITHMEM.
End Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section acquire_lock_SC_ref.
Lemma acquire_lock_Chan_spec_ref:
compatsim (crel HDATA LDATA) (gensem acquire_lock_SC_spec) acquire_lock_SC_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros Hargs0 Hasm_inv Hesp HRA Hle.
inv HSCP.
assert (HFB: ι b0 = Some (b0, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold acquire_lock_SC_spec; subrewrite.
set (rs2´ := (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) rs2))).
∃ ι, (rs2´#RA <- Vundef #PC <- (rs2#RA)).
subdestruct.
- inv HQ.
inv multi_log_re. pose proof H2 as Hre´.
specialize (H2 _ a).
rewrite Hdestruct3 in H2. inv H2.
exploit (relate_SC_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_SC_Log_GetSharedSC_Some; eauto.
intros (a´ & Hget & Hrel_e).
inv Hrel_e.
rewrite H0 in H4. inv H4.
assert (HST: ∃ m2´, Mem.storebytes m2 b1 0 (ByteList a´) = Some m2´).
{
eapply Mem.range_perm_storebytes; eauto. rewrite H9. simpl.
intros ofs Hofs.
rename H into Hmatch_SC.
assert (Hrange: 0 ≤ ofs / 16 < num_chan).
{
xomega.
}
specialize (Hmatch_SC _ Hrange).
destruct Hmatch_SC as (_ & _ & _ & _ & _ & Hv1 & _ & Hv2 & _ & Hv3 & _ & Hv4 & _).
assert (Hieq: ∃ j, ofs = (ofs / 16) × 16 + j ∧ 0 ≤ j < 16).
{
specialize (Z_div_mod_eq ofs 16). intros Hieq.
∃ (ofs mod 16).
split.
- replace (ofs / 16 × 16) with (16 × (ofs / 16)) by omega.
eapply Hieq. omega.
- eapply Z_mod_lt. omega.
}
destruct Hieq as (j & Heq & Hj).
rewrite Heq.
destruct (zlt j 4).
{
destruct Hv1 as (Hv1 & _).
eapply Hv1. simpl. omega.
}
destruct (zlt j 8).
{
destruct Hv2 as (Hv2 & _).
eapply Hv2. simpl. omega.
}
destruct (zlt j 12).
{
destruct Hv3 as (Hv3 & _).
eapply Hv3. simpl. omega.
}
{
destruct Hv4 as (Hv4 & _).
eapply Hv4. simpl. omega.
}
}
destruct HST as (m2´ & HST).
specialize (H8 _ _ HST).
rename H8 into HSC.
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec.
simpl; subrewrite´.
erewrite index2Z_eq; eauto.
rewrite <- H5. rewrite Hdestruct2.
erewrite (H_CalLock_relate_SC_log _ _ s); eauto.
eapply relate_SC_Log_pull; eauto.
eapply relate_SC_Log_ticket; eauto.
× rewrite Hget; eauto.
× inv Hargs. inv H4.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H3 as Hneq.
eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× intros.
destruct (zeq i0 (Int.unsigned i)); subst.
{
repeat rewrite ZMap.gss. constructor.
eapply relate_SC_Log_pull; eauto.
eapply relate_SC_Log_ticket; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
eapply neq_add; eauto.
eapply neq_add; eauto.
}
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H2; eauto 20).
- inv HQ.
inv multi_log_re. pose proof H2 as Hre´.
specialize (H2 _ a).
rewrite Hdestruct3 in H2. inv H2.
exploit (relate_SC_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_SC_Log_GetSharedSC_None; eauto.
intros Hget.
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec. simpl; subrewrite´.
erewrite index2Z_eq; eauto.
rewrite <- H5. rewrite Hdestruct2.
erewrite (H_CalLock_relate_SC_log _ _ s); eauto.
eapply relate_SC_Log_pull; eauto.
eapply relate_SC_Log_ticket; eauto.
× rewrite Hget; eauto.
× inv Hargs. inv H4.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H3 as Hneq.
eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× intros.
destruct (zeq i0 (Int.unsigned i)); subst.
{
repeat rewrite ZMap.gss. constructor.
eapply relate_SC_Log_pull; eauto.
eapply relate_SC_Log_ticket; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
eapply neq_add; eauto.
eapply neq_add; eauto.
}
× econstructor; eauto.
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H2; eauto 20).
Qed.
End acquire_lock_SC_ref.
Section release_lock_SC_ref.
Lemma match_SC_Vint:
∀ tb v1 v2 v3 v4,
match_Chan tb v1 v2 v3 v4 →
∃ v1´ v2´ v3´ v4´,
v1 = Vint v1´ ∧ v2 = Vint v2´ ∧ v3 = Vint v3´ ∧ v4 = Vint v4´.
Proof.
intros. inv H; unfold Vzero; eauto 10.
Qed.
Lemma loadbytes_rel_SC:
∀ iend tb m b
(Hpre: ∀ ofs,
0 ≤ ofs < iend →
∃ v1 v2 v3 v4,
Mem.load Mint32 m b (ofs × 16) = Some v1 ∧
Mem.valid_access m Mint32 b (ofs × 16) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 4) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 8) = Some v3 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 8) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 12) = Some v4 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 12) Writable ∧
match_Chan (ZMap.get ofs tb) v1 v2 v3 v4),
∀ ofs
(Hrange: 0 ≤ ofs < iend),
∃ l, Mem.loadbytes m b (ofs × 16) 16 = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (ofs × 16) (ByteList l) = Some m´ →
∃ v1 v2 v3 v4,
Mem.load Mint32 m´ b (ofs × 16) = Some v1 ∧
Mem.valid_access m´ Mint32 b (ofs × 16) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 4) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 4) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 8) = Some v3 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 8) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 12) = Some v4 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 12) Writable ∧
match_Chan (ZMap.get ofs tb) v1 v2 v3 v4).
Proof.
intros. specialize (Hpre _ Hrange).
destruct Hpre as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
exploit match_SC_Vint; eauto.
intros (v1´ & v2´ & v3´ & v4´ & ? & ? & ? & ?); subst.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l1 & HLD1 & Hd1).
exploit decode_val_bytelist; eauto.
intros (l1´ & ?); subst.
assert (Hof_nat: Z.of_nat (nat_of_Z 4) = 4).
{
rewrite nat_of_Z_max.
replace (Z.max 4 0) with 4 by xomega. trivial.
}
assert (Hlen1: Z.of_nat (length (ByteList l1´)) = 4).
{
exploit Mem.loadbytes_length; eauto.
intros Hlen1. rewrite Hlen1, Hof_nat. trivial.
}
revert HL2; intros.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l2 & HLD2 & Hd2).
exploit decode_val_bytelist; eauto.
intros (l2´ & ?); subst.
assert (Hlen2: Z.of_nat (length (ByteList l2´)) = 4).
{
exploit Mem.loadbytes_length; eauto.
intros Hlen2. rewrite Hlen2, Hof_nat. trivial.
}
revert HL3; intros.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l3 & HLD3 & Hd3).
exploit decode_val_bytelist; eauto.
intros (l3´ & ?); subst.
assert (Hlen3: Z.of_nat (length (ByteList l3´)) = 4).
{
exploit Mem.loadbytes_length; eauto.
intros Hlen3. rewrite Hlen3, Hof_nat. trivial.
}
revert HL4; intros.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l4 & HLD4 & Hd4).
exploit decode_val_bytelist; eauto.
intros (l4´ & ?); subst.
assert (Hlen4: Z.of_nat (length (ByteList l4´)) = 4).
{
exploit Mem.loadbytes_length; eauto.
intros Hlen4. rewrite Hlen4, Hof_nat. trivial.
}
∃ (l1´ ++ l2´ ++ l3´ ++ l4´).
split.
- repeat rewrite ByteList_cons.
change 16 with (4 + (4 + (4 + 4))) at 2.
eapply Mem.loadbytes_concat; eauto; try omega.
eapply Mem.loadbytes_concat; eauto; try omega.
eapply Mem.loadbytes_concat; eauto; try omega.
replace (ofs × 16 + 4 + 4) with (ofs × 16 + 8) by omega. trivial.
replace (ofs × 16 + 4 + 4 + 4) with (ofs × 16 + 12) by omega. trivial.
- intros ? ? HSTB.
repeat rewrite ByteList_cons in HSTB.
eapply Mem.storebytes_split in HSTB.
destruct HSTB as (m1 & HST1 & HST2).
rewrite Hlen1 in HST2.
eapply Mem.storebytes_split in HST2.
destruct HST2 as (m2 & HST2 & HST3).
rewrite Hlen2 in HST3.
replace (ofs × 16 + 4 + 4) with (ofs × 16 + 8) in HST3 by omega.
eapply Mem.storebytes_split in HST3.
destruct HST3 as (m3 & HST3 & HST4).
rewrite Hlen3 in HST4.
replace (ofs × 16 + 8 + 4) with (ofs × 16 + 12) in HST4 by omega.
∃ (Vint v1´), (Vint v2´), (Vint v3´), (Vint v4´).
refine_split´; eauto.
+ erewrite Mem.load_storebytes_other; try eapply HST4.
erewrite Mem.load_storebytes_other; try eapply HST3.
erewrite Mem.load_storebytes_other; try eapply HST2.
eapply Mem.loadbytes_storebytes_same in HST1.
rewrite Hlen1 in HST1.
rewrite Hd1. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 4). xomega.
right. simpl. left. reflexivity.
right. simpl. left. omega.
right. simpl. left. omega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST1.
unfold Mem.valid_access.
simpl. rewrite Hlen1 in HST1.
split; trivial. ∃ (ofs × 4). omega.
+ erewrite Mem.load_storebytes_other; try eapply HST4.
erewrite Mem.load_storebytes_other; try eapply HST3.
eapply Mem.loadbytes_storebytes_same in HST2.
rewrite Hlen2 in HST2.
rewrite Hd2. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 4 + 1). xomega.
right. simpl. left. omega.
right. simpl. left. omega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST2.
unfold Mem.valid_access.
simpl. rewrite Hlen2 in HST2.
split; trivial. ∃ (ofs × 4 + 1). omega.
+ erewrite Mem.load_storebytes_other; try eapply HST4.
eapply Mem.loadbytes_storebytes_same in HST3.
rewrite Hlen3 in HST3.
rewrite Hd3. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 4 + 2). xomega.
right. simpl. left. omega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST3.
unfold Mem.valid_access.
simpl. rewrite Hlen3 in HST3.
split; trivial. ∃ (ofs × 4 + 2). omega.
+ eapply Mem.loadbytes_storebytes_same in HST4.
rewrite Hlen4 in HST4.
rewrite Hd4. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 4 + 3). xomega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST4.
unfold Mem.valid_access.
simpl. rewrite Hlen4 in HST4.
split; trivial. ∃ (ofs × 4 + 3). omega.
Qed.
Lemma loadbytes_rel_ind_SC:
∀ iend tb m b
(Hpre: ∀ ofs,
0 ≤ ofs < Z.of_nat (iend) →
∃ v1 v2 v3 v4,
Mem.load Mint32 m b (ofs × 16) = Some v1 ∧
Mem.valid_access m Mint32 b (ofs × 16) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 4) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 8) = Some v3 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 8) Writable ∧
Mem.load Mint32 m b (ofs × 16 + 12) = Some v4 ∧
Mem.valid_access m Mint32 b (ofs × 16 + 12) Writable ∧
match_Chan (ZMap.get ofs tb) v1 v2 v3 v4),
∃ l, Mem.loadbytes m b 0 (Z.of_nat iend × 16) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
(∀ ofs,
0 ≤ ofs < Z.of_nat (iend) →
∃ v1 v2 v3 v4,
Mem.load Mint32 m´ b (ofs × 16) = Some v1 ∧
Mem.valid_access m´ Mint32 b (ofs × 16) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 4) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 4) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 8) = Some v3 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 8) Writable ∧
Mem.load Mint32 m´ b (ofs × 16 + 12) = Some v4 ∧
Mem.valid_access m´ Mint32 b (ofs × 16 + 12) Writable ∧
match_Chan (ZMap.get ofs tb) v1 v2 v3 v4)).
Proof.
induction iend.
- change (Z.of_nat 0) with 0.
intros. simpl.
erewrite Mem.loadbytes_empty; [|reflexivity].
∃ nil. split; trivial.
intros. omega.
- intros.
assert (Hrange: 0 ≤ Z.of_nat (iend) < Z.of_nat (S iend)) by xomega.
exploit loadbytes_rel_SC; eauto.
intros (l & HLD & HST).
exploit (IHiend tb m b); eauto.
{
intros. eapply Hpre. omega.
}
intros (l´ & HLD´ & HST´).
∃ (l´ ++ l).
split.
+ replace (Z.of_nat (S iend) × 16) with ((Z.of_nat (iend) × 16) + 16) by xomega.
rewrite ByteList_cons.
eapply Mem.loadbytes_concat; eauto; try xomega.
+ intros.
rewrite ByteList_cons in H.
eapply Mem.storebytes_split in H.
destruct H as (m1 & HST1 & HST2).
exploit Mem.loadbytes_length; eauto.
intros Heq. rewrite Heq in HST2.
rewrite nat_of_Z_max in HST2.
replace (Z.max (Z.of_nat iend × 16) 0) with (Z.of_nat iend × 16) in HST2 by xomega.
simpl in HST2.
destruct (zlt ofs (Z.of_nat (iend))).
{
specialize (HST´ _ _ HST1).
exploit (HST´ ofs). omega.
intros (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
refine_split´; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
}
{
specialize (HST _ _ HST2).
destruct HST as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (Heq1: ofs = Z.of_nat iend).
{
destruct (zeq ofs (Z.of_nat iend)); trivial.
xomega.
}
rewrite Heq1.
refine_split´; eauto.
}
Qed.
Lemma loadbytes_rel_storebytes_SC:
∀ s tb m b
(Htb: match_ChanPool s tb m)
(Hsymbol: find_symbol s SYNCCHPOOL_LOC = Some b),
∃ l, Mem.loadbytes m b 0 (num_chan × 16) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_ChanPool s tb m´).
Proof.
intros.
specialize (loadbytes_rel_ind_SC (Z.to_nat num_chan) tb m b).
rewrite Z2Nat.id; [| omega].
intros HM. inv Htb.
rewrite H0 in Hsymbol; inv Hsymbol.
specialize (HM H).
destruct HM as (l & HLD & HST).
∃ l. split; trivial.
intros. econstructor. eauto. assumption.
Qed.
Lemma match_ChanPool_gso:
∀ s b t m m´ ofs v
(Hmatch: match_ChanPool s t m)
(Hsymbol: find_symbol s SYNCCHPOOL_LOC = Some b)
(HST: Mem.store Mint32 m b ofs v = Some m´)
(Hge: ofs ≥ num_chan × 16),
match_ChanPool s t m´.
Proof.
intros. inv Hmatch. rewrite Hsymbol in H0; inv H0. econstructor; eauto.
intros. specialize (H _ H0).
destruct H as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
repeat (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto; [|simpl; right; left; omega]).
refine_split´; eauto;
eapply Mem.store_valid_access_1; eauto.
Qed.
Lemma loadbytes_rel_storebytes:
∀ s sc m b
(HSC: match_ChanPool s sc m)
(Hsymbol: find_symbol s SYNCCHPOOL_LOC = Some b),
∃ l, Mem.loadbytes m b 0 (num_chan × 16) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_ChanPool s sc m´).
Proof.
intros.
exploit loadbytes_rel_storebytes_SC; eauto.
Qed.
Lemma release_lock_SC_spec_ref:
compatsim (crel HDATA LDATA) (gensem release_lock_SC_spec) release_lock_SC_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
intros Hargs0 Hasm_inv Hesp HRA Hle.
assert (HFB: ι b0 = Some (b0, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold release_lock_SC_spec; subrewrite.
set (rs2´ := (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) rs2))).
∃ ι, (rs2´#RA <- Vundef #PC <- (rs2#RA)).
subdestruct.
- inv HQ.
inv multi_log_re. pose proof H2 as Hre´.
specialize (H2 _ a).
rewrite Hdestruct3 in H2. inv H2.
inv match_match.
exploit loadbytes_rel_storebytes; eauto.
intros (l1 & HLD & HST).
assert (Hrel_e: relate_SC_MultiEvent s (TSHARED (OSCE (syncchpool d1))) (TSHARED (OMEME l1))).
{
constructor; eauto.
econstructor; eauto.
eapply Mem.loadbytes_length in HLD. rewrite HLD.
rewrite nat_of_Z_max. reflexivity.
}
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold release_lock_spec. simpl; subrewrite´.
erewrite index2Z_eq; eauto.
rewrite <- H5. rewrite Hdestruct5.
erewrite (H_CalLock_relate_SC_log _ _ s); eauto.
eapply relate_SC_Log_ticket; eauto.
econstructor; eauto.
× trivial.
× inv Hargs. inv H4.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H3 as Hneq.
eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× intros.
destruct (zeq i0 (Int.unsigned i)); subst.
{
repeat rewrite ZMap.gss. constructor.
eapply relate_SC_Log_ticket; eauto.
constructor; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
eapply neq_add; eauto.
eapply neq_add; eauto.
}
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H2; eauto 20).
Qed.
End release_lock_SC_ref.
Lemma get_sync_chan_to_ref:
compatsim (crel HDATA LDATA) (gensem get_sync_chan_to_spec) get_sync_chan_to_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H2; subst; eauto.
}
refine_split; eauto.
econstructor; eauto.
specialize (H (Int.unsigned i) irange).
blast H; eauto.
lift_unfold.
rewrite Hex1.
{
functional inversion H2; subst.
inv Hex9;
rewrite <- H13 in H11; inv H11.
apply unsigned_inj in H. rewrite H. reflexivity.
}
Qed.
Lemma get_sync_chan_paddr_ref:
compatsim (crel HDATA LDATA) (gensem get_sync_chan_paddr_spec) get_sync_chan_paddr_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H2; subst; eauto.
}
refine_split; eauto.
econstructor; eauto.
specialize (H (Int.unsigned i) irange).
blast H; eauto.
lift_unfold.
rewrite Hex2.
{
functional inversion H2; subst.
inv Hex9;
rewrite <- H13 in H11; inv H11.
apply unsigned_inj in H. rewrite H. reflexivity.
}
Qed.
Lemma get_sync_chan_count_ref:
compatsim (crel HDATA LDATA) (gensem get_sync_chan_count_spec) get_sync_chan_count_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H2; subst; eauto.
}
refine_split; eauto.
econstructor; eauto.
specialize (H (Int.unsigned i) irange).
blast H; eauto.
lift_unfold.
rewrite Hex4.
{
functional inversion H2; subst.
inv Hex9;
rewrite <- H13 in H11; inv H11.
apply unsigned_inj in H. rewrite H. reflexivity.
}
Qed.
Lemma get_sync_chan_busy_ref:
compatsim (crel HDATA LDATA) (gensem get_sync_chan_busy_spec) get_sync_chan_busy_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H2; subst; eauto.
}
refine_split; eauto.
econstructor; eauto.
specialize (H (Int.unsigned i) irange).
blast H; eauto.
lift_unfold.
rewrite Hex6.
{
functional inversion H2; subst.
inv Hex9;
rewrite <- H13 in H11; inv H11.
apply unsigned_inj in H. rewrite H. reflexivity.
}
Qed.
Lemma set_sync_chan_to_ref:
compatsim (crel HDATA LDATA) (gensem set_sync_chan_to_spec) set_sync_chan_to_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) Hex0); intros [m´ HST].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. eapply HST. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ (Vint i0), e0, e1, e2. refine_split; eauto.
- exploit Mem.load_store_same. eapply HST. simpl. intros HL. eapply HL.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 4). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 8). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 12). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gss. rewrite Int.repr_unsigned.
inv Hex9;
rewrite <- H12 in H11; inv H11.
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma set_sync_chan_paddr_ref:
compatsim (crel HDATA LDATA) (gensem set_sync_chan_paddr_spec) set_sync_chan_paddr_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) Hex3); intros [m´ HST].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. eapply HST. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ e, (Vint i0), e1, e2. refine_split; eauto.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit Mem.load_store_same. eapply HST. simpl. intros HL. eapply HL.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 8). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 12). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gss. rewrite Int.repr_unsigned.
inv Hex9;
rewrite <- H12 in H11; inv H11.
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma set_sync_chan_count_ref:
compatsim (crel HDATA LDATA) (gensem set_sync_chan_count_spec) set_sync_chan_count_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) Hex5); intros [m´ HST].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. eapply HST. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ e, e0, (Vint i0), e2. refine_split; eauto.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16 + 4). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit Mem.load_store_same. eapply HST. simpl. intros HL. eapply HL.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eapply HST. right. right. simpl.
instantiate (1 := Int.unsigned i × 16 + 12). omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gss. rewrite Int.repr_unsigned.
inv Hex9;
rewrite <- H12 in H11; inv H11.
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma set_sync_chan_busy_ref:
compatsim (crel HDATA LDATA) (gensem set_sync_chan_busy_spec) set_sync_chan_busy_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) Hex7); intros [m´ HST].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. eapply HST. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ e, e0, e1, (Vint i0). refine_split; eauto.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other); eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16 + 4). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit (Mem.load_store_other). eauto. right. left. simpl.
instantiate (1:= Mint32). instantiate (1 := Int.unsigned i × 16 + 8). simpl. omega.
intros HL. erewrite HL. assumption.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- exploit Mem.load_store_same. eapply HST. simpl. intros HL. eapply HL.
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gss. rewrite Int.repr_unsigned.
inv Hex9;
rewrite <- H12 in H11; inv H11.
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
- eapply Mem.store_valid_access_1. eapply HST. eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma init_sync_chan_ref:
compatsim (crel HDATA LDATA) (gensem init_sync_chan_spec) init_sync_chan_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1; repeat split; trivial; congruence.
}
assert(irange: 0 ≤ Int.unsigned i < num_chan).
{
functional inversion H1; subst; eauto.
}
generalize H; intro hmem.
specialize (H (Int.unsigned i) irange). blast H.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_chan)) Hex0); intros [m´1 HST1].
assert (Hvalid1: Mem.valid_access m´1 Mint32 b (Int.unsigned i × 16 + 4) Writable).
{
eapply Mem.store_valid_access_1. eapply HST1. eassumption.
}
specialize (Mem.valid_access_store _ _ _ _ (Vint Int.zero) Hvalid1); intros [m´2 HST2].
assert (Hvalid2: Mem.valid_access m´2 Mint32 b (Int.unsigned i × 16 + 8) Writable).
{
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
}
specialize (Mem.valid_access_store _ _ _ _ (Vint Int.zero) Hvalid2); intros [m´3 HST3].
assert (Hvalid3: Mem.valid_access m´3 Mint32 b (Int.unsigned i × 16 + 12) Writable).
{
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
}
specialize (Mem.valid_access_store _ _ _ _ (Vint Int.zero) Hvalid3); intros [m´4 HST4].
functional inversion H1; subst.
refine_split; eauto.
econstructor; eauto.
lift_unfold. split. instantiate (1:= (m´1, d2)). eapply HST1. reflexivity.
lift_unfold. split. instantiate (1:= (m´2, d2)). eapply HST2. reflexivity.
lift_unfold. split. instantiate (1:= (m´3, d2)). eapply HST3. reflexivity.
lift_unfold. split. eapply HST4. reflexivity.
{
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto.
intros id Hid.
assert (Hcase: id = Int.unsigned i ∨ id ≠ Int.unsigned i) by omega.
destruct Hcase as [Heq | Hneq].
{
rewrite Heq. ∃ (Vint (Int.repr num_chan)) ,(Vint (Int.zero)) ,(Vint (Int.zero)) ,(Vint (Int.zero)). refine_split; eauto.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_same; [| eapply HST1]; simpl; reflexivity.
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_same; [| eapply HST2]; simpl; reflexivity.
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; eauto; try (right; simpl; omega).
erewrite Mem.load_store_same; [| eapply HST3]; simpl; reflexivity.
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_same; [| eapply HST4]; simpl; reflexivity.
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- rewrite ZMap.gss. simpl.
inv Hex9;
econstructor; eauto.
}
{
specialize (hmem id Hid).
blast hmem.
refine_split; eauto.
- erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [eauto |eassumption| right; simpl; omega].
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [eauto |eassumption| right; simpl; omega].
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [eauto |eassumption| right; simpl; omega].
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [|eassumption| right; simpl; omega].
erewrite Mem.load_store_other; [eauto |eassumption| right; simpl; omega].
- eapply Mem.store_valid_access_1. eapply HST4.
eapply Mem.store_valid_access_1. eapply HST3.
eapply Mem.store_valid_access_1. eapply HST2.
eapply Mem.store_valid_access_1. eapply HST1.
eassumption.
- rewrite ZMap.gso by assumption; eauto.
}
}
Qed.
Lemma get_kernel_pa_ref:
compatsim (crel HDATA LDATA) (gensem get_kernel_pa_spec)
get_kernel_pa_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv HSCP.
exploit get_kernel_pa_exist; eauto 1.
intros HP.
refine_split; try econstructor; eauto.
- functional inversion H2. functional inversion H4; functional inversion H7;
unfold PDE_Arg in *; subdestruct; try assumption.
- functional inversion HP. functional inversion H4; functional inversion H7; split; eauto.
Qed.
End WITHMEM.
End Refinement.