Library mcertikos.proc.QueueIntroGenFresh
This file provide the contextual refinement proof between PThreadInit layer and PQueueIntro layer
Require Import QueueIntroGenDef.
Require Import QueueIntroGenSpec.
Require Import XOmega.
Require Import Conventions.
Require Import QueueIntroGenLemma.
Require Import QueueIntroGenSpec.
Require Import XOmega.
Require Import Conventions.
Require Import QueueIntroGenLemma.
Section Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{real_params: RealParams}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section acquire_lock_TCB_ref.
Lemma acquire_lock_TCB_spec_ref:
compatsim (crel HDATA LDATA) (gensem acquire_lock_TCB_spec) acquire_lock_TCB_spec_low.
Proof.
compatsim_simpl (@match_AbData).
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 acquire_lock_TCB_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 H0 as Hre´.
specialize (H0 _ a).
rewrite Hdestruct4 in H0. inv H0.
exploit (relate_TCB_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_TCB_Log_GetSharedTCB_Some; eauto.
intros (a´ & Hget & Hrel_e).
inv Hrel_e.
rewrite Hsymbol in H6. inv H6.
assert (HST: ∃ m2´, Mem.storebytes m2 b1 0 (ByteList a´) = Some m2´).
{
eapply Mem.range_perm_storebytes; eauto. rewrite H8. simpl.
intros ofs Hofs.
destruct (zlt ofs (num_proc × 16)).
{
inv HTCBP.
assert (Hrange: 0 ≤ ofs / 16 < num_proc).
{
xomega.
}
specialize (Hmatch_TCB _ Hrange).
destruct Hmatch_TCB 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.
}
}
{
inv HTDQP.
assert (Hieq: ∃ j, ofs = (ofs / 8) × 8 + j ∧ 0 ≤ j < 8).
{
specialize (Z_div_mod_eq ofs 8). intros Hieq.
∃ (ofs mod 8).
split.
- replace (ofs / 8 × 8) with (8 × (ofs / 8)) by omega.
eapply Hieq. omega.
- eapply Z_mod_lt. omega.
}
destruct Hieq as (j & Heq & Hj).
rewrite Heq.
assert (Hrange: 0 ≤ ofs / 8 - num_proc × 2 < num_chan).
{
xomega.
}
specialize (Hmatch_TDQ _ Hrange).
assert (Heq´: (ofs / 8 - num_proc × 2) × 8 = ofs / 8 × 8 - num_proc × 16).
{
xomega.
}
rewrite Heq´ in Hmatch_TDQ.
destruct Hmatch_TDQ as (_ & _ & _ & Hv1 & _ & Hv2 & _).
destruct (zlt j 4).
{
destruct Hv1 as (Hv1 & _).
eapply Hv1. simpl. omega.
}
{
destruct Hv2 as (Hv2 & _).
eapply Hv2. simpl. omega.
}
}
}
destruct HST as (m2´ & HST).
specialize (H7 _ _ HST).
destruct H7 as (HTCB & HTDQ).
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec. simpl; subrewrite´.
erewrite index2Z_eq; eauto.
rewrite <- H3. rewrite Hdestruct3.
erewrite (H_CalLock_relate_TCB_log _ _ s); eauto.
eapply relate_TCB_Log_pull; eauto.
eapply relate_TCB_Log_ticket; eauto.
× rewrite Hget; eauto.
× inv Hargs. inv H2.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 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_TCB_Log_pull; eauto.
eapply relate_TCB_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 H0; eauto 20).
- inv HQ.
inv multi_log_re. pose proof H0 as Hre´.
specialize (H0 _ a).
rewrite Hdestruct4 in H0. inv H0.
exploit (relate_TCB_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_TCB_Log_GetSharedTCB_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 <- H3. rewrite Hdestruct3.
erewrite (H_CalLock_relate_TCB_log _ _ s); eauto.
eapply relate_TCB_Log_pull; eauto.
eapply relate_TCB_Log_ticket; eauto.
× rewrite Hget; eauto.
× inv Hargs. inv H2.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 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_TCB_Log_pull; eauto.
eapply relate_TCB_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 H0; eauto 20).
Qed.
End acquire_lock_TCB_ref.
Section release_lock_TCB_ref.
Lemma match_TCB_Vint:
∀ tb v1 v2 v3 v4,
match_TCB 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_tcb:
∀ 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_TCB (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_TCB (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_TCB_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_tcb:
∀ 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_TCB (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_TCB (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_tcb; 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_tcb:
∀ tb m b
(Htb: match_TCBPool b tb m),
∃ l, Mem.loadbytes m b 0 (num_proc × 16) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_TCBPool b tb m´).
Proof.
intros.
specialize (loadbytes_rel_ind_tcb (Z.to_nat num_proc) tb m b).
rewrite Z2Nat.id; [| omega].
intros HM. inv Htb. specialize (HM Hmatch_TCB).
destruct HM as (l & HLD & HST).
∃ l. split; trivial.
intros. econstructor. eauto.
Qed.
Lemma match_TDQ_Vint:
∀ tb v1 v2,
match_TDQ tb v1 v2 →
∃ v1´ v2´,
v1 = Vint v1´ ∧ v2 = Vint v2´.
Proof.
intros. inv H; unfold Vzero; eauto 10.
Qed.
Lemma loadbytes_rel_tdq:
∀ iend tq m b
(Hpre: ∀ ofs,
0 ≤ ofs < iend →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8 + num_proc × 16) = Some v1 ∧
Mem.valid_access m Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
Mem.load Mint32 m b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
match_TDQ (ZMap.get ofs tq) v1 v2),
∀ ofs
(Hrange: 0 ≤ ofs < iend),
∃ l, Mem.loadbytes m b (ofs × 8 + num_proc × 16) 8 = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (ofs × 8 + num_proc × 16) (ByteList l) = Some m´ →
∃ v1 v2,
Mem.load Mint32 m´ b (ofs × 8 + num_proc × 16) = Some v1 ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
Mem.load Mint32 m´ b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
match_TDQ (ZMap.get ofs tq) v1 v2).
Proof.
intros. specialize (Hpre _ Hrange).
destruct Hpre as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
exploit match_TDQ_Vint; eauto.
intros (v1´ & v2´ & ? & ?); 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.
}
∃ (l1´ ++ l2´).
replace 16384 with (num_proc × 16) in *; try omega.
split.
- repeat rewrite ByteList_cons.
change 8 with (4 + 4) at 2.
eapply Mem.loadbytes_concat; eauto; try omega.
replace (ofs × 8 + num_proc × 16 + 4) with (ofs × 8 + 4 + num_proc × 16) 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.
replace (ofs × 8 + num_proc × 16 + 4) with (ofs × 8 + 4 + num_proc × 16) in HST2 by omega.
∃ (Vint v1´), (Vint v2´).
refine_split´; eauto.
+ 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 × 2 + num_proc × 4).
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 HST1.
unfold Mem.valid_access.
simpl. rewrite Hlen1 in HST1.
split; trivial. ∃ (ofs × 2 + num_proc × 4).
omega.
+ eapply Mem.loadbytes_storebytes_same in HST2.
rewrite Hlen2 in HST2.
rewrite Hd2. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 2 + 1 + num_proc × 4).
xomega.
+ 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 × 2 + 1 + num_proc × 4).
omega.
Qed.
Lemma loadbytes_rel_ind_tdq:
∀ iend tq m b
(Hpre: ∀ ofs,
0 ≤ ofs < Z.of_nat (iend) →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8 + num_proc × 16) = Some v1 ∧
Mem.valid_access m Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
Mem.load Mint32 m b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
match_TDQ (ZMap.get ofs tq) v1 v2),
∃ l, Mem.loadbytes m b (num_proc × 16) (Z.of_nat iend × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (num_proc × 16) (ByteList l) = Some m´ →
(∀ ofs,
0 ≤ ofs < Z.of_nat iend →
∃ v1 v2,
Mem.load Mint32 m´ b (ofs × 8 + num_proc × 16) = Some v1 ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
Mem.load Mint32 m´ b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
match_TDQ (ZMap.get ofs tq) v1 v2)).
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_tdq; eauto.
intros (l & HLD & HST).
exploit (IHiend tq m b); eauto.
{
intros. eapply Hpre. omega.
}
intros (l´ & HLD´ & HST´).
∃ (l´ ++ l).
split.
+ replace (Z.of_nat (S iend) × 8)
with ((Z.of_nat (iend) × 8) + 8) by xomega.
rewrite ByteList_cons.
eapply Mem.loadbytes_concat; eauto; try xomega.
replace (num_proc × 16 + Z.of_nat iend × 8)
with (Z.of_nat iend × 8 + num_proc × 16) by omega.
trivial.
+ 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 × 8) 0)
with (Z.of_nat iend × 8) in HST2 by xomega.
destruct (zlt ofs (Z.of_nat (iend))).
{
specialize (HST´ _ _ HST1).
exploit (HST´ ofs). omega.
intros (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
refine_split´; eauto.
- erewrite Mem.load_storebytes_other; eauto.
right. left.
Local Opaque Z.add.
simpl. 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.
}
{
replace (num_proc × 16 + Z.of_nat iend × 8)
with (Z.of_nat iend × 8 + num_proc × 16)
in HST2 by omega.
specialize (HST _ _ HST2).
destruct HST as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & 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_tdq:
∀ tq m b
(Htq: match_TDQPool b tq m),
∃ l, Mem.loadbytes m b (num_proc × 16) (num_chan × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (num_proc × 16) (ByteList l) = Some m´ →
match_TDQPool b tq m´).
Proof.
intros.
specialize (loadbytes_rel_ind_tdq (Z.to_nat num_chan) tq m b).
rewrite Z2Nat.id; [| omega].
intros HM. inv Htq. specialize (HM Hmatch_TDQ).
destruct HM as (l & HLD & HST).
∃ l. split; trivial.
intros. econstructor. eauto.
Qed.
Lemma match_TCBPool_gso:
∀ b t m m´ ofs v
(Hmatch: match_TCBPool b t m)
(HST: Mem.store Mint32 m b ofs v = Some m´)
(Hge: ofs ≥ num_proc × 16),
match_TCBPool b t m´.
Proof.
intros. inv Hmatch. constructor; eauto.
intros. specialize (Hmatch_TCB _ Hofs).
destruct Hmatch_TCB 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 match_TCBPool_gso´:
∀ b t m m´ l
(Hmatch: match_TCBPool b t m)
(HST: Mem.storebytes m b (num_proc × 16) l = Some m´),
match_TCBPool b t m´.
Proof.
intros. inv Hmatch. constructor; eauto.
intros. specialize (Hmatch_TCB _ Hofs).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
repeat (rewrite (Mem.load_storebytes_other _ _ _ _ _ HST); auto; [|simpl; right; left; omega]).
refine_split´; eauto;
eapply Mem.storebytes_valid_access_1; eauto.
Qed.
Lemma loadbytes_rel_storebytes:
∀ tb tq m b
(Htq: match_TDQPool b tq m)
(Htb: match_TCBPool b tb m),
∃ l, Mem.loadbytes m b 0 (num_proc × 16 + num_chan × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_TCBPool b tb m´
∧ match_TDQPool b tq m´).
Proof.
intros.
exploit loadbytes_rel_storebytes_tcb; eauto.
intros (l1 & HLD1 & HST1).
exploit loadbytes_rel_storebytes_tdq; eauto.
intros (l2 & HLD2 & HST2).
∃ (l1 ++ l2).
repeat rewrite ByteList_cons.
split.
- eapply Mem.loadbytes_concat; eauto; omega.
- intros.
eapply Mem.storebytes_split in H.
destruct H as (m1 & HSTB1 & HSTB2).
eapply HST1 in HSTB1.
eapply Mem.loadbytes_length in HLD1. rewrite HLD1 in HSTB2.
rewrite nat_of_Z_max in HSTB2.
replace (Z.max (num_proc × 16) 0) with 16384
in HSTB2 by xomega.
pose proof HSTB2 as ST.
eapply HST2 in HSTB2. split; trivial.
eapply match_TCBPool_gso´; eauto.
Qed.
Lemma release_lock_TCB_spec_ref:
compatsim (crel HDATA LDATA) (gensem release_lock_TCB_spec) release_lock_TCB_spec_low.
Proof.
compatsim_simpl (@match_AbData).
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_TCB_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 H0 as Hre´.
specialize (H0 _ a).
rewrite Hdestruct3 in H0. inv H0.
exploit loadbytes_rel_storebytes; eauto.
intros (l1 & HLD & HST).
assert (Hrel_e: relate_TCB_MultiEvent s (TSHARED (OTCBE (tcb d1) (tdq 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 <- H3. rewrite Hdestruct5.
erewrite (H_CalLock_relate_TCB_log _ _ s); eauto.
eapply relate_TCB_Log_ticket; eauto.
econstructor; eauto.
× trivial.
× inv Hargs. inv H2.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 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_TCB_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 H0; eauto 20).
Qed.
End release_lock_TCB_ref.
Lemma get_state_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_state_spec) get_state_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (HP: v1 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
apply ZtoThreadState_correct in Hzs; inv Hzs.
rewrite <- Int.repr_unsigned with z; rewrite <- H.
rewrite H8. rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma tcb_get_CPU_ID_spec_ref:
compatsim (crel HDATA LDATA) (gensem tcb_get_CPU_ID_spec) tcb_get_CPU_ID_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (HP: v2 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H8.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma get_prev_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_prev_spec) get_prev_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (HP: v3 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H9.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma get_next_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_next_spec) get_next_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (HP: v4 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H10.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma match_TDQPool_gso:
∀ b t m m´ ofs v
(Hmatch: match_TDQPool b t m)
(HST: Mem.store Mint32 m b ofs v = Some m´)
(Hge: ofs ≤ num_proc × 16 - 4),
match_TDQPool b t m´.
Proof.
intros. inv Hmatch. constructor; eauto.
intros. specialize (Hmatch_TDQ _ Hofs).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
repeat (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto).
refine_split´; eauto;
eapply Mem.store_valid_access_1; eauto.
simpl; right. right; omega.
simpl; right. right; omega.
Qed.
Lemma set_state_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_state_spec) set_state_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H7 in HM. inv HM.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2; eauto.
simpl; right; right. reflexivity.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3; eauto.
simpl; right; right. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4; eauto.
simpl; right; right. omega.
rewrite ZMap.gss. simpl.
constructor. assumption.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma tcb_set_CPU_ID_spec_ref:
compatsim (crel HDATA LDATA) (gensem tcb_set_CPU_ID_spec) tcb_set_CPU_ID_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV2); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H7 in HM. inv HM.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; eauto.
simpl; right; left. reflexivity.
eapply Mem.load_store_same; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3; eauto.
simpl; right; right. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4; eauto.
simpl; right; right. omega.
rewrite ZMap.gss. simpl.
constructor. assumption.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma set_prev_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_prev_spec) set_prev_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV3); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H7 in HM. inv HM.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; eauto.
simpl; right; left. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2; eauto.
simpl; right; left. omega.
eapply Mem.load_store_same; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4; eauto.
simpl; right; right. omega.
rewrite ZMap.gss. simpl.
constructor. assumption.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma set_next_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_next_spec) set_next_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV4); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H7 in HM. inv HM.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; eauto.
simpl; right; left. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2; eauto.
simpl; right; left. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3; eauto.
simpl; right; left. omega.
eapply Mem.load_store_same; eauto.
rewrite ZMap.gss. simpl.
constructor. assumption.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma tcb_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem tcb_init_spec) tcb_init_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr 3)) HV1); intros [m´1 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV2.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr 0)) HV2); intros [m´2 HST2].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST2) in HV3.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_proc)) HV3); intros [m´3 HST3].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST2) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST3) in HV4.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_proc)) HV4); intros [m´4 HST4].
refine_split.
- econstructor; eauto.
instantiate (1:= (m´1, d2)).
simpl; lift_trivial. subrewrite´.
instantiate (1:= (m´2, d2)).
simpl; lift_trivial. subrewrite´.
instantiate (1:= (m´3, d2)).
simpl; lift_trivial. subrewrite´.
instantiate (1:= d2).
instantiate (1:= m´4).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; try eapply HST4; [| omega].
eapply match_TDQPool_gso; try eapply HST3; [| omega].
eapply match_TDQPool_gso; try eapply HST2; [| omega].
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
erewrite (Mem.load_store_other _ _ _ _ _ _ HST4); eauto; [|right; left; simpl; omega].
erewrite (Mem.load_store_other _ _ _ _ _ _ HST3); eauto; [|right; left; simpl; omega].
erewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto; [|right; left; simpl; omega].
eapply Mem.load_store_same; eauto.
erewrite (Mem.load_store_other _ _ _ _ _ _ HST4); eauto; [|right; left; simpl; omega].
erewrite (Mem.load_store_other _ _ _ _ _ _ HST3); eauto; [|right; left; simpl; omega].
eapply Mem.load_store_same; eauto.
erewrite (Mem.load_store_other _ _ _ _ _ _ HST4); eauto; [|right; left; simpl; omega].
eapply Mem.load_store_same; eauto.
eapply Mem.load_store_same; eauto.
rewrite ZMap.gss.
replace num_proc with (Int.unsigned (Int.repr num_proc)).
replace 0 with (Int.unsigned (Int.repr 0)).
econstructor; trivial.
apply Int.unsigned_repr. rewrite_omega.
apply Int.unsigned_repr. rewrite_omega.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST4); [|load_other_simpl ofs i]).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST3); [|load_other_simpl ofs i]).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST2); [|load_other_simpl ofs i]).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST1); [|load_other_simpl ofs i]).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite ZMap.gso; auto.
}
- apply inject_incr_refl.
Qed.
Lemma tdq_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem tdq_init_spec) tdq_init_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_chan).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_proc)) HV1); intros [m´1 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV2.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_proc)) HV2); intros [m´2 HST2].
refine_split.
- econstructor; eauto.
instantiate (1:= (m´1, d2)).
simpl. lift_trivial. simpl in HST1. rewrite HST1.
reflexivity.
simpl. lift_trivial. simpl in HST2. rewrite HST2.
reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
erewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto; [|right; left; simpl; omega].
eapply Mem.load_store_same; eauto.
eapply Mem.load_store_same; eauto.
simpl.
rewrite ZMap.gss.
replace num_proc
with (Int.unsigned (Int.repr num_proc)).
econstructor; eauto.
apply Int.unsigned_repr. rewrite_omega.
+
specialize (HMem _ Hofs).
destruct HMem as [v1´[v2´[HL1´[HV1´[HL2´[HV2´ HM´]]]]]].
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST2); [|load_other_simpl ofs i]).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST1); [|load_other_simpl ofs i]).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite ZMap.gso; auto.
}
{
eapply match_TCBPool_gso; try eapply HST2;[|omega].
eapply match_TCBPool_gso; eauto. omega.
}
- apply inject_incr_refl.
Qed.
Lemma get_head_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_head_spec) get_head_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_chan).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
assert (HP: v1 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H7.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma get_tail_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_tail_spec) get_tail_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_chan).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
assert (HP: v2 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H8.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma set_head_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_head_spec) set_head_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_chan).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m´ HST].
refine_split.
- econstructor; eauto.
simpl; lift_trivial. simpl in HST.
rewrite HST. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H6 in HM. inv HM.
econstructor; simpl; eauto.
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2; eauto.
simpl; right; right. omega.
rewrite ZMap.gss. simpl.
constructor.
+
specialize (HMem _ Hofs).
destruct HMem as [v1´[v2´[HL1´[HV1´[HL2´[HV2´ HM´]]]]]].
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
{
eapply match_TCBPool_gso; eauto. omega.
}
- apply inject_incr_refl.
Qed.
Lemma set_tail_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_tail_spec) set_tail_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_chan).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV2); intros [m´ HST].
refine_split.
- econstructor; eauto.
simpl; lift_trivial. simpl in HST.
rewrite HST. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H6 in HM. inv HM.
econstructor; simpl; eauto.
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; eauto.
simpl; right; left. omega.
eapply Mem.load_store_same; eauto.
rewrite ZMap.gss. simpl.
constructor.
+
specialize (HMem _ Hofs).
destruct HMem as [v1´[v2´[HL1´[HV1´[HL2´[HV2´ HM´]]]]]].
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
{
eapply match_TCBPool_gso; eauto. omega.
}
- apply inject_incr_refl.
Qed.
End WITHMEM.
End Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{real_params: RealParams}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section acquire_lock_TCB_ref.
Lemma acquire_lock_TCB_spec_ref:
compatsim (crel HDATA LDATA) (gensem acquire_lock_TCB_spec) acquire_lock_TCB_spec_low.
Proof.
compatsim_simpl (@match_AbData).
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 acquire_lock_TCB_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 H0 as Hre´.
specialize (H0 _ a).
rewrite Hdestruct4 in H0. inv H0.
exploit (relate_TCB_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_TCB_Log_GetSharedTCB_Some; eauto.
intros (a´ & Hget & Hrel_e).
inv Hrel_e.
rewrite Hsymbol in H6. inv H6.
assert (HST: ∃ m2´, Mem.storebytes m2 b1 0 (ByteList a´) = Some m2´).
{
eapply Mem.range_perm_storebytes; eauto. rewrite H8. simpl.
intros ofs Hofs.
destruct (zlt ofs (num_proc × 16)).
{
inv HTCBP.
assert (Hrange: 0 ≤ ofs / 16 < num_proc).
{
xomega.
}
specialize (Hmatch_TCB _ Hrange).
destruct Hmatch_TCB 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.
}
}
{
inv HTDQP.
assert (Hieq: ∃ j, ofs = (ofs / 8) × 8 + j ∧ 0 ≤ j < 8).
{
specialize (Z_div_mod_eq ofs 8). intros Hieq.
∃ (ofs mod 8).
split.
- replace (ofs / 8 × 8) with (8 × (ofs / 8)) by omega.
eapply Hieq. omega.
- eapply Z_mod_lt. omega.
}
destruct Hieq as (j & Heq & Hj).
rewrite Heq.
assert (Hrange: 0 ≤ ofs / 8 - num_proc × 2 < num_chan).
{
xomega.
}
specialize (Hmatch_TDQ _ Hrange).
assert (Heq´: (ofs / 8 - num_proc × 2) × 8 = ofs / 8 × 8 - num_proc × 16).
{
xomega.
}
rewrite Heq´ in Hmatch_TDQ.
destruct Hmatch_TDQ as (_ & _ & _ & Hv1 & _ & Hv2 & _).
destruct (zlt j 4).
{
destruct Hv1 as (Hv1 & _).
eapply Hv1. simpl. omega.
}
{
destruct Hv2 as (Hv2 & _).
eapply Hv2. simpl. omega.
}
}
}
destruct HST as (m2´ & HST).
specialize (H7 _ _ HST).
destruct H7 as (HTCB & HTDQ).
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec. simpl; subrewrite´.
erewrite index2Z_eq; eauto.
rewrite <- H3. rewrite Hdestruct3.
erewrite (H_CalLock_relate_TCB_log _ _ s); eauto.
eapply relate_TCB_Log_pull; eauto.
eapply relate_TCB_Log_ticket; eauto.
× rewrite Hget; eauto.
× inv Hargs. inv H2.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 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_TCB_Log_pull; eauto.
eapply relate_TCB_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 H0; eauto 20).
- inv HQ.
inv multi_log_re. pose proof H0 as Hre´.
specialize (H0 _ a).
rewrite Hdestruct4 in H0. inv H0.
exploit (relate_TCB_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_TCB_Log_GetSharedTCB_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 <- H3. rewrite Hdestruct3.
erewrite (H_CalLock_relate_TCB_log _ _ s); eauto.
eapply relate_TCB_Log_pull; eauto.
eapply relate_TCB_Log_ticket; eauto.
× rewrite Hget; eauto.
× inv Hargs. inv H2.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 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_TCB_Log_pull; eauto.
eapply relate_TCB_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 H0; eauto 20).
Qed.
End acquire_lock_TCB_ref.
Section release_lock_TCB_ref.
Lemma match_TCB_Vint:
∀ tb v1 v2 v3 v4,
match_TCB 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_tcb:
∀ 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_TCB (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_TCB (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_TCB_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_tcb:
∀ 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_TCB (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_TCB (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_tcb; 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_tcb:
∀ tb m b
(Htb: match_TCBPool b tb m),
∃ l, Mem.loadbytes m b 0 (num_proc × 16) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_TCBPool b tb m´).
Proof.
intros.
specialize (loadbytes_rel_ind_tcb (Z.to_nat num_proc) tb m b).
rewrite Z2Nat.id; [| omega].
intros HM. inv Htb. specialize (HM Hmatch_TCB).
destruct HM as (l & HLD & HST).
∃ l. split; trivial.
intros. econstructor. eauto.
Qed.
Lemma match_TDQ_Vint:
∀ tb v1 v2,
match_TDQ tb v1 v2 →
∃ v1´ v2´,
v1 = Vint v1´ ∧ v2 = Vint v2´.
Proof.
intros. inv H; unfold Vzero; eauto 10.
Qed.
Lemma loadbytes_rel_tdq:
∀ iend tq m b
(Hpre: ∀ ofs,
0 ≤ ofs < iend →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8 + num_proc × 16) = Some v1 ∧
Mem.valid_access m Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
Mem.load Mint32 m b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
match_TDQ (ZMap.get ofs tq) v1 v2),
∀ ofs
(Hrange: 0 ≤ ofs < iend),
∃ l, Mem.loadbytes m b (ofs × 8 + num_proc × 16) 8 = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (ofs × 8 + num_proc × 16) (ByteList l) = Some m´ →
∃ v1 v2,
Mem.load Mint32 m´ b (ofs × 8 + num_proc × 16) = Some v1 ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
Mem.load Mint32 m´ b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
match_TDQ (ZMap.get ofs tq) v1 v2).
Proof.
intros. specialize (Hpre _ Hrange).
destruct Hpre as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
exploit match_TDQ_Vint; eauto.
intros (v1´ & v2´ & ? & ?); 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.
}
∃ (l1´ ++ l2´).
replace 16384 with (num_proc × 16) in *; try omega.
split.
- repeat rewrite ByteList_cons.
change 8 with (4 + 4) at 2.
eapply Mem.loadbytes_concat; eauto; try omega.
replace (ofs × 8 + num_proc × 16 + 4) with (ofs × 8 + 4 + num_proc × 16) 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.
replace (ofs × 8 + num_proc × 16 + 4) with (ofs × 8 + 4 + num_proc × 16) in HST2 by omega.
∃ (Vint v1´), (Vint v2´).
refine_split´; eauto.
+ 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 × 2 + num_proc × 4).
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 HST1.
unfold Mem.valid_access.
simpl. rewrite Hlen1 in HST1.
split; trivial. ∃ (ofs × 2 + num_proc × 4).
omega.
+ eapply Mem.loadbytes_storebytes_same in HST2.
rewrite Hlen2 in HST2.
rewrite Hd2. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 2 + 1 + num_proc × 4).
xomega.
+ 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 × 2 + 1 + num_proc × 4).
omega.
Qed.
Lemma loadbytes_rel_ind_tdq:
∀ iend tq m b
(Hpre: ∀ ofs,
0 ≤ ofs < Z.of_nat (iend) →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8 + num_proc × 16) = Some v1 ∧
Mem.valid_access m Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
Mem.load Mint32 m b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
match_TDQ (ZMap.get ofs tq) v1 v2),
∃ l, Mem.loadbytes m b (num_proc × 16) (Z.of_nat iend × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (num_proc × 16) (ByteList l) = Some m´ →
(∀ ofs,
0 ≤ ofs < Z.of_nat iend →
∃ v1 v2,
Mem.load Mint32 m´ b (ofs × 8 + num_proc × 16) = Some v1 ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
Mem.load Mint32 m´ b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
match_TDQ (ZMap.get ofs tq) v1 v2)).
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_tdq; eauto.
intros (l & HLD & HST).
exploit (IHiend tq m b); eauto.
{
intros. eapply Hpre. omega.
}
intros (l´ & HLD´ & HST´).
∃ (l´ ++ l).
split.
+ replace (Z.of_nat (S iend) × 8)
with ((Z.of_nat (iend) × 8) + 8) by xomega.
rewrite ByteList_cons.
eapply Mem.loadbytes_concat; eauto; try xomega.
replace (num_proc × 16 + Z.of_nat iend × 8)
with (Z.of_nat iend × 8 + num_proc × 16) by omega.
trivial.
+ 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 × 8) 0)
with (Z.of_nat iend × 8) in HST2 by xomega.
destruct (zlt ofs (Z.of_nat (iend))).
{
specialize (HST´ _ _ HST1).
exploit (HST´ ofs). omega.
intros (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
refine_split´; eauto.
- erewrite Mem.load_storebytes_other; eauto.
right. left.
Local Opaque Z.add.
simpl. 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.
}
{
replace (num_proc × 16 + Z.of_nat iend × 8)
with (Z.of_nat iend × 8 + num_proc × 16)
in HST2 by omega.
specialize (HST _ _ HST2).
destruct HST as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & 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_tdq:
∀ tq m b
(Htq: match_TDQPool b tq m),
∃ l, Mem.loadbytes m b (num_proc × 16) (num_chan × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (num_proc × 16) (ByteList l) = Some m´ →
match_TDQPool b tq m´).
Proof.
intros.
specialize (loadbytes_rel_ind_tdq (Z.to_nat num_chan) tq m b).
rewrite Z2Nat.id; [| omega].
intros HM. inv Htq. specialize (HM Hmatch_TDQ).
destruct HM as (l & HLD & HST).
∃ l. split; trivial.
intros. econstructor. eauto.
Qed.
Lemma match_TCBPool_gso:
∀ b t m m´ ofs v
(Hmatch: match_TCBPool b t m)
(HST: Mem.store Mint32 m b ofs v = Some m´)
(Hge: ofs ≥ num_proc × 16),
match_TCBPool b t m´.
Proof.
intros. inv Hmatch. constructor; eauto.
intros. specialize (Hmatch_TCB _ Hofs).
destruct Hmatch_TCB 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 match_TCBPool_gso´:
∀ b t m m´ l
(Hmatch: match_TCBPool b t m)
(HST: Mem.storebytes m b (num_proc × 16) l = Some m´),
match_TCBPool b t m´.
Proof.
intros. inv Hmatch. constructor; eauto.
intros. specialize (Hmatch_TCB _ Hofs).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
repeat (rewrite (Mem.load_storebytes_other _ _ _ _ _ HST); auto; [|simpl; right; left; omega]).
refine_split´; eauto;
eapply Mem.storebytes_valid_access_1; eauto.
Qed.
Lemma loadbytes_rel_storebytes:
∀ tb tq m b
(Htq: match_TDQPool b tq m)
(Htb: match_TCBPool b tb m),
∃ l, Mem.loadbytes m b 0 (num_proc × 16 + num_chan × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_TCBPool b tb m´
∧ match_TDQPool b tq m´).
Proof.
intros.
exploit loadbytes_rel_storebytes_tcb; eauto.
intros (l1 & HLD1 & HST1).
exploit loadbytes_rel_storebytes_tdq; eauto.
intros (l2 & HLD2 & HST2).
∃ (l1 ++ l2).
repeat rewrite ByteList_cons.
split.
- eapply Mem.loadbytes_concat; eauto; omega.
- intros.
eapply Mem.storebytes_split in H.
destruct H as (m1 & HSTB1 & HSTB2).
eapply HST1 in HSTB1.
eapply Mem.loadbytes_length in HLD1. rewrite HLD1 in HSTB2.
rewrite nat_of_Z_max in HSTB2.
replace (Z.max (num_proc × 16) 0) with 16384
in HSTB2 by xomega.
pose proof HSTB2 as ST.
eapply HST2 in HSTB2. split; trivial.
eapply match_TCBPool_gso´; eauto.
Qed.
Lemma release_lock_TCB_spec_ref:
compatsim (crel HDATA LDATA) (gensem release_lock_TCB_spec) release_lock_TCB_spec_low.
Proof.
compatsim_simpl (@match_AbData).
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_TCB_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 H0 as Hre´.
specialize (H0 _ a).
rewrite Hdestruct3 in H0. inv H0.
exploit loadbytes_rel_storebytes; eauto.
intros (l1 & HLD & HST).
assert (Hrel_e: relate_TCB_MultiEvent s (TSHARED (OTCBE (tcb d1) (tdq 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 <- H3. rewrite Hdestruct5.
erewrite (H_CalLock_relate_TCB_log _ _ s); eauto.
eapply relate_TCB_Log_ticket; eauto.
econstructor; eauto.
× trivial.
× inv Hargs. inv H2.
args_list_inv.
repeat econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 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_TCB_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 H0; eauto 20).
Qed.
End release_lock_TCB_ref.
Lemma get_state_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_state_spec) get_state_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (HP: v1 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
apply ZtoThreadState_correct in Hzs; inv Hzs.
rewrite <- Int.repr_unsigned with z; rewrite <- H.
rewrite H8. rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma tcb_get_CPU_ID_spec_ref:
compatsim (crel HDATA LDATA) (gensem tcb_get_CPU_ID_spec) tcb_get_CPU_ID_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (HP: v2 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H8.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma get_prev_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_prev_spec) get_prev_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (HP: v3 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H9.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma get_next_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_next_spec) get_next_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
assert (HP: v4 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H10.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma match_TDQPool_gso:
∀ b t m m´ ofs v
(Hmatch: match_TDQPool b t m)
(HST: Mem.store Mint32 m b ofs v = Some m´)
(Hge: ofs ≤ num_proc × 16 - 4),
match_TDQPool b t m´.
Proof.
intros. inv Hmatch. constructor; eauto.
intros. specialize (Hmatch_TDQ _ Hofs).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
repeat (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto).
refine_split´; eauto;
eapply Mem.store_valid_access_1; eauto.
simpl; right. right; omega.
simpl; right. right; omega.
Qed.
Lemma set_state_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_state_spec) set_state_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H7 in HM. inv HM.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2; eauto.
simpl; right; right. reflexivity.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3; eauto.
simpl; right; right. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4; eauto.
simpl; right; right. omega.
rewrite ZMap.gss. simpl.
constructor. assumption.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma tcb_set_CPU_ID_spec_ref:
compatsim (crel HDATA LDATA) (gensem tcb_set_CPU_ID_spec) tcb_set_CPU_ID_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV2); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H7 in HM. inv HM.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; eauto.
simpl; right; left. reflexivity.
eapply Mem.load_store_same; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3; eauto.
simpl; right; right. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4; eauto.
simpl; right; right. omega.
rewrite ZMap.gss. simpl.
constructor. assumption.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma set_prev_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_prev_spec) set_prev_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV3); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H7 in HM. inv HM.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; eauto.
simpl; right; left. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2; eauto.
simpl; right; left. omega.
eapply Mem.load_store_same; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4; eauto.
simpl; right; right. omega.
rewrite ZMap.gss. simpl.
constructor. assumption.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma set_next_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_next_spec) set_next_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV4); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H7 in HM. inv HM.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; eauto.
simpl; right; left. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2; eauto.
simpl; right; left. omega.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3; eauto.
simpl; right; left. omega.
eapply Mem.load_store_same; eauto.
rewrite ZMap.gss. simpl.
constructor. assumption.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL3´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL4´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma tcb_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem tcb_init_spec) tcb_init_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_proc).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTCBP.
pose proof Hmatch_TCB as HMem.
specialize (Hmatch_TCB _ HOS).
destruct Hmatch_TCB as (v1 & v2 & v3 & v4 & HL1 & HV1 & HL2 & HV2 & HL3 & HV3 & HL4 & HV4 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr 3)) HV1); intros [m´1 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV2.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr 0)) HV2); intros [m´2 HST2].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST2) in HV3.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_proc)) HV3); intros [m´3 HST3].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST2) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST3) in HV4.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_proc)) HV4); intros [m´4 HST4].
refine_split.
- econstructor; eauto.
instantiate (1:= (m´1, d2)).
simpl; lift_trivial. subrewrite´.
instantiate (1:= (m´2, d2)).
simpl; lift_trivial. subrewrite´.
instantiate (1:= (m´3, d2)).
simpl; lift_trivial. subrewrite´.
instantiate (1:= d2).
instantiate (1:= m´4).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
{
eapply match_TDQPool_gso; try eapply HST4; [| omega].
eapply match_TDQPool_gso; try eapply HST3; [| omega].
eapply match_TDQPool_gso; try eapply HST2; [| omega].
eapply match_TDQPool_gso; eauto. omega.
}
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
erewrite (Mem.load_store_other _ _ _ _ _ _ HST4); eauto; [|right; left; simpl; omega].
erewrite (Mem.load_store_other _ _ _ _ _ _ HST3); eauto; [|right; left; simpl; omega].
erewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto; [|right; left; simpl; omega].
eapply Mem.load_store_same; eauto.
erewrite (Mem.load_store_other _ _ _ _ _ _ HST4); eauto; [|right; left; simpl; omega].
erewrite (Mem.load_store_other _ _ _ _ _ _ HST3); eauto; [|right; left; simpl; omega].
eapply Mem.load_store_same; eauto.
erewrite (Mem.load_store_other _ _ _ _ _ _ HST4); eauto; [|right; left; simpl; omega].
eapply Mem.load_store_same; eauto.
eapply Mem.load_store_same; eauto.
rewrite ZMap.gss.
replace num_proc with (Int.unsigned (Int.repr num_proc)).
replace 0 with (Int.unsigned (Int.repr 0)).
econstructor; trivial.
apply Int.unsigned_repr. rewrite_omega.
apply Int.unsigned_repr. rewrite_omega.
+
specialize (HMem _ Hofs).
destruct HMem as (v1´ & v2´ & v3´ & v4´ & HL1´ & HV1´ & HL2´ & HV2´ & HL3´ & HV3´ & HL4´ & HV4´ & HM´).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST4); [|load_other_simpl ofs i]).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST3); [|load_other_simpl ofs i]).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST2); [|load_other_simpl ofs i]).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST1); [|load_other_simpl ofs i]).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite ZMap.gso; auto.
}
- apply inject_incr_refl.
Qed.
Lemma tdq_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem tdq_init_spec) tdq_init_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_chan).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_proc)) HV1); intros [m´1 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV2.
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr num_proc)) HV2); intros [m´2 HST2].
refine_split.
- econstructor; eauto.
instantiate (1:= (m´1, d2)).
simpl. lift_trivial. simpl in HST1. rewrite HST1.
reflexivity.
simpl. lift_trivial. simpl in HST2. rewrite HST2.
reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
erewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto; [|right; left; simpl; omega].
eapply Mem.load_store_same; eauto.
eapply Mem.load_store_same; eauto.
simpl.
rewrite ZMap.gss.
replace num_proc
with (Int.unsigned (Int.repr num_proc)).
econstructor; eauto.
apply Int.unsigned_repr. rewrite_omega.
+
specialize (HMem _ Hofs).
destruct HMem as [v1´[v2´[HL1´[HV1´[HL2´[HV2´ HM´]]]]]].
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST2); [|load_other_simpl ofs i]).
repeat (erewrite (Mem.load_store_other _ _ _ _ _ _ HST1); [|load_other_simpl ofs i]).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite ZMap.gso; auto.
}
{
eapply match_TCBPool_gso; try eapply HST2;[|omega].
eapply match_TCBPool_gso; eauto. omega.
}
- apply inject_incr_refl.
Qed.
Lemma get_head_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_head_spec) get_head_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_chan).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
assert (HP: v1 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H7.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma get_tail_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_tail_spec) get_tail_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_chan).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
assert (HP: v2 = Vint z).
{
functional inversion H2; subst. rewrite H6 in HM; inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H8.
rewrite Int.repr_unsigned. trivial.
}
refine_split; eauto; econstructor; eauto.
Qed.
Lemma set_head_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_head_spec) set_head_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_chan).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m´ HST].
refine_split.
- econstructor; eauto.
simpl; lift_trivial. simpl in HST.
rewrite HST. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H6 in HM. inv HM.
econstructor; simpl; eauto.
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2; eauto.
simpl; right; right. omega.
rewrite ZMap.gss. simpl.
constructor.
+
specialize (HMem _ Hofs).
destruct HMem as [v1´[v2´[HL1´[HV1´[HL2´[HV2´ HM´]]]]]].
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
{
eapply match_TCBPool_gso; eauto. omega.
}
- apply inject_incr_refl.
Qed.
Lemma set_tail_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_tail_spec) set_tail_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < num_chan).
{
inv match_related. functional inversion H1; subst.
repeat (split; trivial); try congruence; eauto.
}
destruct Hkern as [Hkern HOS].
inv HTDQP.
pose proof Hmatch_TDQ as HMem.
specialize (Hmatch_TDQ _ HOS).
destruct Hmatch_TDQ as (v1 & v2 & HL1 & HV1 & HL2 & HV2 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV2); intros [m´ HST].
refine_split.
- econstructor; eauto.
simpl; lift_trivial. simpl in HST.
rewrite HST. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
rewrite H6 in HM. inv HM.
econstructor; simpl; eauto.
{
econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; eauto.
simpl; right; left. omega.
eapply Mem.load_store_same; eauto.
rewrite ZMap.gss. simpl.
constructor.
+
specialize (HMem _ Hofs).
destruct HMem as [v1´[v2´[HL1´[HV1´[HL2´[HV2´ HM´]]]]]].
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
simpl; right. destruct (zlt ofs (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
}
{
eapply match_TCBPool_gso; eauto. omega.
}
- apply inject_incr_refl.
Qed.
End WITHMEM.
End Refinement.