Library mcertikos.proc.AbQueueGen
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem2.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import PQueueInit.
Require Import PAbQueue.
Require Import LayerCalculusLemma.
Require Import CalRealProcModule.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem2.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import PQueueInit.
Require Import PAbQueue.
Require Import LayerCalculusLemma.
Require Import CalRealProcModule.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := pabqueue_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := pqueueinit_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := pabqueue_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := pqueueinit_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Relation between raw data at two layers
Record relate_RData (f: meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
AC_re: AC hadt = AC ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
LAT_re: LAT hadt = LAT ladt;
nps_re: nps hadt = nps ladt;
init_re: init hadt = init ladt;
pperm_re: pperm hadt = pperm ladt;
PT_re: PT hadt = PT ladt;
ptp_re: ptpool hadt = ptpool ladt;
idpde_re: idpde hadt = idpde ladt;
ipt_re: ipt hadt = ipt ladt;
smspool_re: smspool hadt = smspool ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
lock_re: lock hadt = lock ladt;
com1_re: com1 hadt = com1 ladt;
console_re: console hadt = console ladt;
console_concrete_re: console_concrete hadt = console_concrete ladt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr ladt = in_intr hadt;
drv_serial_re: drv_serial hadt = drv_serial ladt;
kctxt_re: kctxt_inj f num_proc (kctxt hadt) (kctxt ladt);
abq_re: AbQ_RealQ (abtcb hadt) (abq hadt) (tcb ladt) (tdq ladt);
sleeper_re: sleeper hadt = sleeper ladt;
multi_oracle_re: relate_ABTCB_Oracle_Pool (multi_oracle hadt) (multi_oracle ladt);
multi_log_re: relate_ABTCB_Log_Pool (multi_log hadt) (multi_log ladt)
}.
Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
| MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := nil
}.
End REFINEMENT_REL.
Local Hint Resolve MATCH_RDATA.
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
AC_re: AC hadt = AC ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
LAT_re: LAT hadt = LAT ladt;
nps_re: nps hadt = nps ladt;
init_re: init hadt = init ladt;
pperm_re: pperm hadt = pperm ladt;
PT_re: PT hadt = PT ladt;
ptp_re: ptpool hadt = ptpool ladt;
idpde_re: idpde hadt = idpde ladt;
ipt_re: ipt hadt = ipt ladt;
smspool_re: smspool hadt = smspool ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
lock_re: lock hadt = lock ladt;
com1_re: com1 hadt = com1 ladt;
console_re: console hadt = console ladt;
console_concrete_re: console_concrete hadt = console_concrete ladt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr ladt = in_intr hadt;
drv_serial_re: drv_serial hadt = drv_serial ladt;
kctxt_re: kctxt_inj f num_proc (kctxt hadt) (kctxt ladt);
abq_re: AbQ_RealQ (abtcb hadt) (abq hadt) (tcb ladt) (tdq ladt);
sleeper_re: sleeper hadt = sleeper ladt;
multi_oracle_re: relate_ABTCB_Oracle_Pool (multi_oracle hadt) (multi_oracle ladt);
multi_log_re: relate_ABTCB_Log_Pool (multi_log hadt) (multi_log ladt)
}.
Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
| MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := nil
}.
End REFINEMENT_REL.
Local Hint Resolve MATCH_RDATA.
Prove that after taking one step, the refinement relation still holds
Lemma relate_incr:
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
- eapply kctxt_inj_incr; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
eapply relate_incr; eauto.
Qed.
End Rel_Property.
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
- eapply kctxt_inj_incr; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
eapply relate_incr; eauto.
Qed.
End Rel_Property.
Section Init_Relation.
Lemma AbQ_RealQ_init:
AbQ_RealQ (ZMap.init AbTCBUndef) (ZMap.init AbQUndef) (ZMap.init TCBUndef) (ZMap.init TDQUndef).
Proof.
constructor.
× intros qi l Hqi Hl.
rewrite ZMap.gi in Hl.
discriminate Hl.
× intros i tds parent inq Hi H.
rewrite ZMap.gi in H.
discriminate H.
Qed.
End Init_Relation.
Lemma AbQ_RealQ_init:
AbQ_RealQ (ZMap.init AbTCBUndef) (ZMap.init AbQUndef) (ZMap.init TCBUndef) (ZMap.init TDQUndef).
Proof.
constructor.
× intros qi l Hqi Hl.
rewrite ZMap.gi in Hl.
discriminate Hl.
× intros i tds parent inq Hi H.
rewrite ZMap.gi in H.
discriminate H.
Qed.
End Init_Relation.
Section Exists.
Lemma real_data : ∀ abtcb abq tcb tdq,
AbQ_RealQ (real_abtcb abtcb) (real_abq abq)
(real_tcb tcb) (real_tdq tdq).
Proof.
constructor.
- unfold abqueue_match_dllist, real_abq, real_tcb, real_tdq.
intros qi l Hqi.
rewrite !init_zmap_inside by omega.
intro H; inv H.
∃ num_proc, num_proc; split; auto; constructor.
- unfold abtcbpool_tcbpool, real_abtcb, real_tcb.
intros i tds inq parent Hi.
rewrite !init_zmap_inside by assumption.
intro H; inv H; eauto.
Qed.
Lemma real_relate_ABTCB_Log_Pool:
∀ habd labd,
relate_ABTCB_Log_Pool (multi_log habd) (multi_log labd) →
relate_ABTCB_Log_Pool (CalTicketLock.real_multi_log (multi_log habd)) (CalTicketLock.real_multi_log (multi_log labd)).
Proof.
assert (Hcases: ∀ a b, 0 ≤ a < b ∨ (a < 0 ∨ b ≤ a)) by (intros; omega).
assert (HZ2Nat: ∀ a b, 0 ≤ a < b → (0 ≤ Z.to_nat a < Z.to_nat b)%nat).
{
split.
rewrite <- Z2Nat.inj_0; rewrite <- Z2Nat.inj_le; omega.
rewrite <- Z2Nat.inj_lt; omega.
}
unfold CalTicketLock.real_multi_log; intros d1 d2 Hrel; inv Hrel; constructor.
- intros i ofs r Hneq Hind.
destruct (Hcases r lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id r); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
- intros i Hi.
destruct (Hcases (i + ID_AT_range) lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id (i + ID_AT_range)); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto; constructor; constructor.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
Qed.
Lemma tdqueue_init_exists :
∀ mbi_adr adt adt´ ladt f,
tdqueue_init0_spec (Int.unsigned mbi_adr) adt = Some adt´
→ relate_RData f adt ladt
→ ∃ ladt´,
tdqueue_init_spec (Int.unsigned mbi_adr) ladt = Some ladt´
∧ relate_RData f adt´ ladt´.
Proof.
unfold tdqueue_init_spec, tdqueue_init0_spec.
intros until f. exist_simpl.
- apply real_data.
- apply real_relate_ABTCB_Log_Pool; eauto.
Qed.
Lemma get_state_exists :
∀ n i adt ladt f,
get_state0_spec (Int.unsigned n) adt = Some i
→ relate_RData f adt ladt
→ get_state_spec (Int.unsigned n) ladt = Some i.
Proof.
unfold get_state_spec, get_state0_spec;
intros. inv H0. revert H. subrewrite. subdestruct.
destruct (ZMap.get (Int.unsigned n) (abtcb adt)) eqn: Hget; contra_inv.
inv Hdestruct4. inv HQ.
inv abq_re0.
unfold abtcbpool_tcbpool in Ht_match.
apply Ht_match in Hget; try omega.
destruct Hget as [pv [nx HT]].
rewrite HT. trivial.
Qed.
Lemma match_next_prev_presv_set_state:
∀ l start ending hd tl itcbp,
abqueue_match_next_prev_rec l hd tl start ending itcbp
→ ∀ i tds pv nx parent,
ZMap.get i itcbp = TCBValid tds parent pv nx
→ ∀ tds´ parent´, abqueue_match_next_prev_rec l hd tl start ending (ZMap.set i (TCBValid tds´ parent´ pv nx) itcbp).
Proof.
clear.
induction l; intros; inv H; econstructor; eauto.
destruct Hvalid as (st & parent0 & Hvalid).
destruct (zeq hd i); subst.
- rewrite ZMap.gss. rewrite H0 in Hvalid. inv Hvalid. eauto.
- rewrite ZMap.gso; eauto.
Qed.
Lemma set_state_exists:
∀ f n ts adt adt´ ladt,
set_state0_spec (Int.unsigned n) ts adt = Some adt´
→ relate_RData f adt ladt
→ ∃ ladt´,
set_state_spec (Int.unsigned n) ts ladt = Some ladt´
∧ relate_RData f adt´ ladt´.
Proof.
intros f n ts adt adt´ ladt HQ H.
inversion_clear H.
revert HQ.
unfold set_state0_spec, set_state_spec.
subrewrite.
subdestruct.
destruct (ZMap.get (Int.unsigned n) (abtcb adt)) eqn:Hgetn; contra_inv.
assert (Hget´ : ∃ pv nx,
ZMap.get (Int.unsigned n) (tcb ladt)
= TCBValid tds cpuid pv nx).
{
inv abq_re0.
unfold abtcbpool_tcbpool in Ht_match. inv Hdestruct4.
exploit Ht_match; eauto.
}
destruct Hget´ as [pv [nx Hget´]].
rewrite Hget´.
destruct (ZtoThreadState ts); contra_inv.
eexists.
split; eauto.
inv HQ. constructor; eauto; simpl.
inv abq_re0.
constructor; trivial.
- simpl in × .
intros qi l´ Hqi Hgetl´.
destruct (Hq_match _ _ Hqi Hgetl´) as [hd [tl [HgetQ Hx]]].
∃ hd; ∃ tl.
split; trivial.
apply match_next_prev_presv_set_state with tds cpuid; trivial.
- unfold abtcbpool_tcbpool in × .
simpl in × .
intros i tds´ inq parent Hi HT.
destruct (zeq i (Int.unsigned n)); subst.
+ rewrite ZMap.gss in ×. inv HT.
refine_split´; eauto.
+ rewrite ZMap.gso in *; eauto.
Qed.
Lemma match_next_prev_presv_gso:
∀ l start ending hd tl itcbp tcb i
(Hmatch: abqueue_match_next_prev_rec l hd tl start ending itcbp)
(HnotIn: ¬ In i l),
abqueue_match_next_prev_rec l hd tl start ending (ZMap.set i tcb itcbp).
Proof.
clear.
induction l; intros; inv Hmatch; try constructor.
destruct Hvalid as (st & parent & Hvalid).
econstructor; eauto.
- destruct (zeq hd i); subst.
+ elim HnotIn. left; trivial.
+ rewrite ZMap.gso; eauto.
- eapply IHl; eauto. intro HF. elim HnotIn.
right; trivial.
Qed.
Lemma dequeue_exists:
∀ f n i adt adt´ ladt,
dequeue0_spec (Int.unsigned n) adt = Some (adt´, i)
→ relate_RData f adt ladt
→ high_level_invariant adt
→ ∃ ladt´,
dequeue_spec (Int.unsigned n) ladt = Some (ladt´, i)
∧ relate_RData f adt´ ladt´.
Proof.
intros f n i adt adt´ ladt HQ H INV.
pose proof H as Hrel.
inversion_clear H.
revert HQ.
unfold dequeue_spec, dequeue0_spec.
subrewrite.
destruct (ikern ladt) eqn: HIK; contra_inv.
destruct (pg ladt) eqn: HIP; contra_inv.
destruct (ihost ladt) eqn: HIH; contra_inv.
destruct (ipt ladt) eqn: HIT; contra_inv.
destruct (zle_lt 0 (Int.unsigned n) num_chan); contra_inv.
destruct (ZMap.get (Int.unsigned n) (abq adt)) eqn: Hgetl; contra_inv.
pose proof abq_re0 as Habq.
inv Habq. exploit Hq_match; eauto.
intros (hd & tl & → & Hq_match´).
destruct l.
- inv Hq_match´. rewrite zeq_true. inv HQ.
refine_split´; eauto.
- assert (Hvalid_q : AbQCorrect (ZMap.get (Int.unsigned n) (abq adt))).
{
inversion INV.
eapply valid_TDQ; eauto.
}
assert (Hz_range: 0 ≤ z < num_proc).
{
unfold AbQCorrect in ×.
rewrite Hgetl in Hvalid_q.
destruct Hvalid_q as (l0 & Heq & Hrange).
inv Heq. eapply Hrange. left; trivial.
}
inv Hq_match´. rewrite zeq_false; [| omega].
destruct (ZMap.get hd (abtcb adt)) eqn: Hgett; contra_inv. inv HQ.
exploit Ht_match; eauto.
intros (pv & nx & Hvalid´).
destruct Hvalid as (st & parent & Heq).
rewrite Hvalid´ in Heq. inv Heq. rewrite Hvalid´.
destruct l.
+ inv Hmatch_ind.
rewrite zeq_true.
refine_split´; eauto.
econstructor; eauto; simpl.
constructor.
× intros qi l´ Hqi Hgetl´.
destruct (zeq qi (Int.unsigned n)); subst.
{
rewrite ZMap.gss in ×. inv Hgetl´.
refine_split´; eauto.
econstructor.
}
{
rewrite ZMap.gso in *; auto.
}
× intros i0 tds´ inq parent0 Hi0 HT.
destruct (zeq i0 i); subst.
{
rewrite ZMap.gss in ×. inv HT. eauto.
}
{
rewrite ZMap.gso in *; eauto.
}
+ inv Hmatch_ind.
assert (Hnext_range: 0 ≤ next < num_proc).
{
unfold AbQCorrect in ×.
rewrite Hgetl in Hvalid_q.
destruct Hvalid_q as (l0 & Heq & Hrange).
inv Heq. eapply Hrange. right. left; trivial.
}
rewrite zeq_false; [| omega].
destruct Hvalid as (st0 & parent0 & Hvalid).
rewrite Hvalid.
refine_split´; eauto.
econstructor; eauto; simpl.
assert (Hnext: ZMap.get next (abtcb adt) = AbTCBValid st0 parent0 (Int.unsigned n)).
{
inversion INV.
exploit valid_inQ; try eapply Hgetl; eauto.
right; left. trivial.
intros (s & c & Hnext).
exploit Ht_match; eauto.
rewrite Hvalid. intros (? & ? & Heq).
inv Heq. trivial.
}
assert (Hcount: count_occ zeq (i :: next :: l) next = 1%nat).
{
exploit valid_count; eauto.
rewrite Hgetl.
intros (l0 & Heq & Hcount). inv Heq.
trivial.
}
assert (Hneq: i ≠ next).
{
destruct (zeq i next); subst; trivial.
rewrite count_occ_cons_eq in Hcount; trivial.
rewrite count_occ_cons_eq in Hcount; trivial.
inv Hcount.
}
constructor.
× intros qi l´ Hqi Hgetl´.
destruct (zeq qi (Int.unsigned n)); subst.
{
rewrite ZMap.gss in ×. inv Hgetl´.
refine_split´; eauto.
econstructor.
- rewrite ZMap.gss. eauto.
- assert (HnotIn: ¬ In next l).
{
rewrite count_occ_cons_neq in Hcount; trivial.
rewrite count_occ_cons_eq in Hcount; trivial.
intro HF.
eapply (count_occ_In zeq) in HF. omega.
}
eapply match_next_prev_presv_gso; eauto.
}
{
rewrite ZMap.gso in *; eauto.
exploit Hq_match; eauto.
intros (hd & tl0 & Heq & Hmatch).
refine_split´; eauto.
eapply match_next_prev_presv_gso; eauto.
intro HF. elim n0.
exploit valid_inQ; eauto.
rewrite Hnext. intros (s0 & c0 & Heq´).
inv Heq´. trivial.
}
× intros i0 tds´ inq parent1 Hi0 HT.
destruct (zeq i0 i); subst.
{
rewrite ZMap.gss in ×. inv HT.
rewrite ZMap.gso; eauto.
}
{
rewrite ZMap.gso in HT; auto.
destruct (zeq i0 next); subst.
- rewrite ZMap.gss. rewrite Hnext in HT. inv HT. eauto.
- rewrite ZMap.gso; eauto.
}
Qed.
Lemma abqueue_match_next_prev_rec_tail:
∀ l hd tl start ending tcb
(Hrange: ∀ x, In x l → 0 ≤ x < num_proc)
(Hmatch: abqueue_match_next_prev_rec l hd tl start ending tcb),
l = nil ∨ ((∃ z l´, l = z :: l´) ∧ 0 ≤ tl < num_proc ∧ In tl l).
Proof.
induction l; intros; inv Hmatch; eauto.
destruct l.
- inv Hmatch_ind. right.
split; eauto.
split.
+ exploit (Hrange hd). left; trivial.
intros; trivial.
+ left; trivial.
- exploit IHl; eauto.
intros. eapply Hrange. right; trivial.
intros HF. inv HF; contra_inv.
right. destruct H as ((z0 & l´ &Hl) & Hneq & Hin). inv Hl.
split; eauto.
split; eauto.
right; trivial.
Qed.
Lemma abqueue_match_next_prev_rec_tail´:
∀ l x y hd tl start ending tcb
(Hmatch: abqueue_match_next_prev_rec (x :: y :: l) hd tl start ending tcb),
In tl (y :: l).
Proof.
induction l; intros; inv Hmatch; eauto.
- inv Hmatch_ind.
inv Hmatch_ind0.
left. trivial.
- exploit IHl; eauto.
intros. right; trivial.
Qed.
Lemma abqueue_match_next_prev_rec_enqueue:
∀ l z hd tl tcb i tds cpuid st´ c´ prev´ next´ starting ending prev0 next0
(Hmatch: abqueue_match_next_prev_rec (z :: l) hd tl starting ending tcb)
(Hi: ZMap.get i tcb = TCBValid tds cpuid prev0 next0)
(Htl: ZMap.get tl tcb = TCBValid st´ c´ prev´ next´)
(Hcount: ∀ x, In x (z :: l) → count_occ zeq (z :: l) x = 1%nat)
(Hneq: ∀ x, In x (z:: l) → x ≠ i),
abqueue_match_next_prev_rec (z :: l ++ i :: nil) hd i starting ending
(ZMap.set i (TCBValid tds cpuid tl ending)
(ZMap.set tl (TCBValid st´ c´ prev´ i) tcb)).
Proof.
induction l; intros.
- inv Hmatch. inv Hmatch_ind.
rewrite Htl in Hvalid.
destruct Hvalid as (st & parent & Heq). inv Heq.
econstructor.
+ rewrite ZMap.gso; eauto.
rewrite ZMap.gss; eauto.
eapply Hneq. left; trivial.
+ econstructor; eauto.
× rewrite ZMap.gss; eauto.
× econstructor.
- assert (Hneq0: hd ≠ tl).
{
intro HF. subst.
exploit abqueue_match_next_prev_rec_tail´; eauto. intros HIn.
inv Hmatch. exploit (Hcount tl).
left; trivial.
intros.
rewrite count_occ_cons_eq in H; trivial.
eapply (count_occ_In zeq) in HIn. omega.
}
inv Hmatch.
destruct Hvalid as (st & parent & Hvalid).
rewrite <- app_comm_cons.
econstructor; eauto.
+ rewrite ZMap.gso; eauto.
rewrite ZMap.gso; eauto.
eapply Hneq. left; trivial.
+ eapply IHl; eauto.
× intros. destruct (zeq x hd); subst.
{
exploit (Hcount hd); eauto.
left; trivial.
intros HIn.
rewrite count_occ_cons_eq in HIn; trivial.
eapply (count_occ_In zeq) in H. omega.
}
{
exploit (Hcount x); eauto.
right; trivial.
intros Hin.
rewrite count_occ_cons_neq in Hin; auto.
}
× intros. eapply Hneq. right; trivial.
Qed.
Lemma enqueue_exists:
∀ f n i adt adt´ ladt
(HQ: enqueue0_spec (Int.unsigned n) i adt = Some adt´)
(Hr: relate_RData f adt ladt)
(INV: high_level_invariant adt)
(INV´: PQueueInit.high_level_invariant ladt),
∃ ladt´,
enqueue_spec (Int.unsigned n) i ladt = Some ladt´
∧ relate_RData f adt´ ladt´.
Proof.
intros.
inversion_clear Hr.
revert HQ.
unfold enqueue_spec, enqueue0_spec.
subrewrite. subdestruct; subst. functional inversion Hdestruct3.
assert (Hvalid_q : AbQCorrect (ZMap.get (Int.unsigned n) (abq adt))).
{
inversion INV.
eapply valid_TDQ; eauto.
}
inv HQ.
pose proof abq_re0 as Habq.
inv Habq. exploit Hq_match; eauto.
intros (hd & tl & Hvalidq & Hq_match´). rewrite Hvalidq.
exploit Ht_match; eauto.
intros (pv & nx & Hvalid´). rewrite Hvalid´.
unfold AbQCorrect in ×.
rewrite Hdestruct5 in Hvalid_q.
destruct Hvalid_q as (l0 & Heq & Hvalid_q). inv Heq.
pose proof Hvalid_q as Hvalid_q´.
eapply abqueue_match_next_prev_rec_tail in Hvalid_q´; eauto.
destruct Hvalid_q´ as [HFF | HFF]; subst.
+ inv Hq_match´.
rewrite zeq_true.
refine_split´; eauto.
econstructor; eauto; simpl.
constructor.
× intros qi l´ Hqi Hgetl´.
destruct (zeq qi (Int.unsigned n)); subst.
{
rewrite ZMap.gss in ×. inv Hgetl´.
refine_split´; eauto.
econstructor.
- rewrite ZMap.gss. eauto.
- constructor.
}
{
rewrite ZMap.gso in *; auto.
exploit Hq_match; eauto.
intros (hd & tl & Hvalidq´ & Hmatch).
refine_split´; eauto.
eapply match_next_prev_presv_gso; eauto.
intro HF.
inv INV.
exploit valid_inQ; eauto. rewrite Hdestruct6.
intros (s & c & Heq). inv Heq. omega.
}
× intros i0 tds´ inq parent0 Hi0 HT.
destruct (zeq i0 i); subst.
{
rewrite ZMap.gss in ×. inv HT. eauto.
}
{
rewrite ZMap.gso in *; eauto.
}
+ destruct HFF as ((z & l´ & Hl) & Hneq & Hin´). subst.
rewrite zeq_false; [| omega].
assert (Htcb: ∃ st´ c´ prev´ next´,
ZMap.get tl (tcb ladt) = TCBValid st´ c´ prev´ next´).
{
inv INV´. exploit valid_TCB; eauto.
unfold TCBCorrect.
intros (s & c & p & next & Htcb & _ & _).
eauto.
}
destruct Htcb as (st´ & c´ & prev´ & next´ & Htcb).
rewrite Htcb.
refine_split´; eauto.
constructor; eauto; simpl.
constructor.
× intros qi l Hqi Hgetl.
destruct (zeq qi (Int.unsigned n)); subst.
{
rewrite ZMap.gss in ×. inv Hgetl.
refine_split´; eauto.
eapply abqueue_match_next_prev_rec_enqueue; eauto.
- intros. exploit Hvalid_q; eauto. intros Hrange_x.
inv INV.
exploit valid_inQ; eauto.
intros (s & c & Habtcb).
exploit valid_count; eauto.
rewrite Hdestruct5.
intros (l & Heq & Hcount). inv Heq. trivial.
- intros. exploit Hvalid_q; eauto. intros Hrange_x.
inv INV.
exploit valid_inQ; eauto.
intros (s & c & Habtcb).
intro HF; subst.
rewrite Hdestruct6 in Habtcb. inv Habtcb. omega.
}
{
rewrite ZMap.gso in *; eauto.
exploit Hq_match; eauto.
intros (hd0 & tl0 & Heq & Hmatch).
assert (Hin: InQ (abtcb adt) (abq adt)).
{
inv INV. eauto.
}
refine_split´; eauto.
eapply match_next_prev_presv_gso; eauto.
eapply match_next_prev_presv_gso; eauto.
- intros HF. exploit Hin; eauto.
intros (s & c & Habtcb).
clear Hqi.
exploit Hin; eauto.
rewrite Habtcb.
intros (s0 & c0 & Habtcb´). inv Habtcb´.
congruence.
- intros HF. clear Hneq. exploit Hin; eauto.
intros (s & c & Habtcb).
rewrite Hdestruct6 in Habtcb. inv Habtcb.
omega.
}
× intros i0 tds´ inq parent1 Hi0 HT.
destruct (zeq i0 i); subst.
{
rewrite ZMap.gss in ×. inv HT. eauto.
}
{
rewrite ZMap.gso in HT; auto.
rewrite ZMap.gso; auto.
destruct (zeq i0 tl); subst.
- rewrite ZMap.gss.
exploit Ht_match; eauto.
rewrite Htcb.
intros (pv0 & nx0 & Heq).
inv Heq. eauto.
- rewrite ZMap.gso; eauto.
}
Qed.
Lemma relate_ABTCB_Log_Pool_gss:
∀ hl ll l0,
relate_ABTCB_Log_Pool hl ll →
relate_ABTCB_Log_Pool
(ZMap.set 0 l0 hl) (ZMap.set 0 l0 ll).
Proof.
intros. inv H. constructor; eauto.
- intros. destruct (zeq r 0); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- intros.
assert (Hneq: i + ID_AT_range ≠ 0).
{
unfold ID_AT_range. omega.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma palloc_exist:
∀ habd habd´ labd n i f,
palloc_spec n habd = Some (habd´, i)
→ relate_RData f habd labd
→ ∃ labd´, palloc_spec n labd = Some (labd´, i) ∧ relate_RData f habd´ labd´.
Proof.
unfold palloc_spec; intros.
revert H. pose proof H0 as HR. inv H0.
assert (Hlog: ZMap.get 0 (multi_log habd) = ZMap.get 0 (multi_log labd)).
{
inv multi_log_re0. eapply (H 0 0); auto. omega.
}
assert (Horacle: ZMap.get 0 (multi_oracle habd) = ZMap.get 0 (multi_oracle labd)).
{
inv multi_oracle_re0. eapply (H 0 0); auto. omega.
}
rewrite Horacle.
subrewrite. subdestruct; inv HQ.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_ABTCB_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_ABTCB_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_ABTCB_Log_Pool_gss. eauto.
Qed.
Lemma ptAllocPDE0_exist:
∀ habd habd´ labd i n v f,
ptAllocPDE0_spec n v habd = Some (habd´, i)
→ relate_RData f habd labd
→ ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
∧ relate_RData f habd´ labd´.
Proof.
unfold ptAllocPDE0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; destruct p; inv HQ.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
rewrite H. rewrite Hdestruct8.
refine_split´; trivial.
inv H0.
constructor; simpl; try eassumption.
+ apply FlatMem.free_page_inj´. trivial.
+ subrewrite´.
+ subrewrite´.
Qed.
Lemma ptInsert0_exist:
∀ s habd habd´ labd i n v pa pe f,
ptInsert0_spec n v pa pe habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptInsert0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- exploit (ptInsertPTE0_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
exploit (ptInsertPTE0_exist s); eauto.
intros (labd´0 & HptInsert0´´ & Hre´).
subrewrite´.
refine_split´; trivial.
Qed.
Lemma ptResv_exist:
∀ s habd habd´ labd i n v p f,
ptResv_spec n v p habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv_spec; intros.
subdestruct. destruct p0.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
Qed.
Lemma ptResv2_exist:
∀ s habd habd´ labd i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv2_spec; intros.
subdestruct; destruct p0; inv H.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?). revert H2.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?). intros.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
Qed.
Lemma offer_shared_mem_exists:
∀ s habd habd´ labd i1 i2 v z f,
offer_shared_mem_spec i1 i2 v habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, offer_shared_mem_spec i1 i2 v labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold offer_shared_mem_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- refine_split´; trivial.
constructor; eauto.
Qed.
Lemma tcb_get_CPU_ID_exist:
∀ habd labd i z f,
get_abtcb_CPU_ID_spec i habd = Some z
→ relate_RData f habd labd
→ tcb_get_CPU_ID_spec i labd = Some z.
Proof.
unfold tcb_get_CPU_ID_spec, get_abtcb_CPU_ID_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
inv abq_re0.
exploit Ht_match; eauto.
intros (pv & nx & ->). trivial.
Qed.
Lemma tcb_set_CPU_ID_exist:
∀ habd habd´ labd i z f,
set_abtcb_CPU_ID_spec i z habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, tcb_set_CPU_ID_spec i z labd = Some labd´
∧ relate_RData f habd´ labd´.
Proof.
unfold tcb_set_CPU_ID_spec, set_abtcb_CPU_ID_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
inv abq_re0.
exploit Ht_match; eauto.
intros (pv & nx & Htcb). rewrite Htcb.
refine_split´; trivial.
constructor; eauto.
constructor; simpl.
- simpl in × .
intros qi l´ Hqi Hgetl´.
destruct (Hq_match _ _ Hqi Hgetl´) as [hd [tl [HgetQ Hx]]].
∃ hd; ∃ tl.
split; trivial.
apply match_next_prev_presv_set_state with tds cpuid; trivial.
- unfold abtcbpool_tcbpool in × .
simpl in × .
intros i0 tds´ inq parent Hi HT.
destruct (zeq i0 i); subst.
+ rewrite ZMap.gss in ×. inv HT.
refine_split´; eauto.
+ rewrite ZMap.gso in *; eauto.
Qed.
Lemma H_CalLock_rel:
∀ l l´ p
(Hcal: H_CalLock l = Some p)
(Hrel: relate_ABTCB_Log l l´),
H_CalLock l´ = Some p.
Proof.
induction l; intros; inv Hrel; trivial.
Local Transparent H_CalLock.
simpl in ×.
subdestruct_one.
exploit IHl; eauto.
destruct p0. destruct p0.
intros Hcal´. rewrite Hcal´.
subdestruct; inv Hrelate_event; inv Hcal; trivial.
Local Opaque H_CalLock.
Qed.
Lemma index2Z_neq_TCB:
∀ i i0 ofs r
(Hi: 0 ≤ i < num_chan)
(Hi0: i0 ≠ ID_TCB)
(Hindex: index2Z i0 ofs = Some r),
r ≠ i + ID_AT_range.
Proof.
intros. functional inversion Hindex.
clear Hindex. functional inversion H1; subst.
- inv H0. unfold ID_AT_range in ×. omega.
- elim Hi0; trivial.
- inv H0. unfold ID_SC_range, lock_TCB_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma add_false:
∀ i i0 n,
i0 ≠ i →
i0 + n ≠ i + n.
Proof.
intros. omega.
Qed.
Lemma relate_ABTCB_Log_gss_ticket:
∀ e c l l´
(Hrel: relate_ABTCB_Log l l´),
relate_ABTCB_Log (TEVENT c (TTICKET e) :: l) (TEVENT c (TTICKET e) :: l´).
Proof.
intros. constructor; trivial.
constructor.
Qed.
Lemma relate_ABTCB_Log_gss_pull:
∀ c l l´
(Hrel: relate_ABTCB_Log l l´),
relate_ABTCB_Log (TEVENT c (TSHARED OPULL) :: l) (TEVENT c (TSHARED OPULL) :: l´).
Proof.
intros. constructor; trivial.
constructor.
Qed.
Lemma relate_ABTCB_Log_gss_TCB:
∀ ta qa t q c l l´
(Hrel: relate_ABTCB_Log l l´)
(Hrel_e: AbQ_RealQ ta qa t q),
relate_ABTCB_Log (TEVENT c (TSHARED (OABTCBE ta qa)) :: l) (TEVENT c (TSHARED (OTCBE t q)) :: l´).
Proof.
intros. constructor; trivial.
constructor. constructor. trivial.
Qed.
Lemma release_lock_TCB_exist:
∀ habd habd´ labd i f,
release_lock_ABTCB_spec i habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, release_lock_TCB_spec i labd = Some labd´ ∧
relate_RData f habd´ labd´.
Proof.
unfold release_lock_ABTCB_spec, release_lock_TCB_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
inv multi_log_re0.
exploit H0; eauto. intros Htcb.
rewrite Hdestruct3 in Htcb. inv Htcb.
assert (Hrel: relate_ABTCB_Log
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OABTCBE (abtcb habd) (abq habd)))
:: l)
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OTCBE (tcb labd) (tdq labd))) :: l2)).
{
eapply relate_ABTCB_Log_gss_ticket.
eapply relate_ABTCB_Log_gss_TCB; eauto.
}
erewrite (H_CalLock_rel _ _ _ Hdestruct4); eauto.
refine_split´; trivial.
constructor; eauto.
constructor; simpl.
- intros.
assert (Hneq: r ≠ (i + ID_AT_range)).
{
eapply index2Z_neq_TCB; eauto.
}
repeat rewrite ZMap.gso; eauto.
- intros. destruct (zeq i0 i); subst.
+ repeat rewrite ZMap.gss; eauto. constructor; trivial.
+ repeat rewrite ZMap.gso; eauto.
eapply add_false; eauto.
eapply add_false; eauto.
Qed.
Lemma relate_ABTCB_Log_getshared:
∀ l l´
(Hrel: relate_ABTCB_Log l l´),
∀ p
(Hget: GetSharedABTCB l = p),
match p with
| Some (ta, qa) ⇒
∃ t q,
GetSharedTCB l´ = Some (t, q)
∧ AbQ_RealQ ta qa t q
| None ⇒ GetSharedTCB l´ = None
end.
Proof.
induction l; simpl; intros.
- inv Hget. inv Hrel. trivial.
- destruct a. destruct e; inv Hget.
+ inv Hrel. inv Hrelate_event; simpl.
exploit IHl; eauto.
+ destruct e; inv Hrel; inv Hrelate_event; simpl.
× exploit IHl; eauto.
× inv Hrelate_e. refine_split´; eauto.
Qed.
Lemma acquire_lock_TCB_exist:
∀ n habd habd´ labd f,
acquire_lock_ABTCB_spec n habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, acquire_lock_TCB_spec n labd = Some labd´ ∧
relate_RData f habd´ labd´.
Proof.
unfold acquire_lock_ABTCB_spec, acquire_lock_TCB_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
subdestruct_one.
destruct (ZMap.get (n + ID_AT_range) (multi_log habd)) eqn: Hlog; contra_inv.
inv multi_log_re0.
exploit H0; eauto. intros Htcb.
rewrite Hlog in Htcb. inv Htcb.
subdestruct_one.
subdestruct_one.
assert (Hrel: relate_ABTCB_Log
(ZMap.get (n + ID_AT_range) (multi_oracle habd) (CPU_ID labd) l ++ l)
(ZMap.get (n + ID_AT_range) (multi_oracle labd) (CPU_ID labd) l2 ++ l2)).
{
inv multi_oracle_re0. specialize (H4 _ a). inv H4.
eapply H5; eauto.
}
assert (Hrel´: relate_ABTCB_Log
(TEVENT (CPU_ID labd) (TSHARED OPULL) ::
TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get (n + ID_AT_range) (multi_oracle habd) (CPU_ID labd) l ++ l)
(TEVENT (CPU_ID labd) (TSHARED OPULL) ::
TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get (n + ID_AT_range) (multi_oracle labd) (CPU_ID labd) l2 ++ l2)).
{
eapply relate_ABTCB_Log_gss_pull; eauto.
eapply relate_ABTCB_Log_gss_ticket; eauto.
}
erewrite (H_CalLock_rel _ _ _ Hdestruct4); eauto.
pose proof (relate_ABTCB_Log_getshared _ _ Hrel) as Htcb.
subdestruct_one; contra_inv.
- destruct p0. exploit Htcb; eauto. simpl.
intros (t & q & → & Hreal).
refine_split´; trivial. inv HQ.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
assert (Hneq: r ≠ (n + ID_AT_range)).
{
eapply index2Z_neq_TCB; eauto.
}
repeat rewrite ZMap.gso; eauto.
+ intros. destruct (zeq i n); subst.
× repeat rewrite ZMap.gss; eauto. constructor; trivial.
× repeat rewrite ZMap.gso; eauto.
eapply add_false; eauto.
eapply add_false; eauto.
- exploit Htcb; eauto. simpl.
intros Hreal. rewrite Hreal.
refine_split´; trivial. inv HQ.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
assert (Hneq: r ≠ (n + ID_AT_range)).
{
eapply index2Z_neq_TCB; eauto.
}
repeat rewrite ZMap.gso; eauto.
+ intros. destruct (zeq i n); subst.
× repeat rewrite ZMap.gss; eauto. constructor; trivial.
× repeat rewrite ZMap.gso; eauto.
eapply add_false; eauto.
eapply add_false; eauto.
Qed.
Lemma Shared2ID2_neq:
∀ i p,
Shared2ID2 i = Some p →
i ≠ ID_TCB.
Proof.
intros. functional inversion H; subst. omega.
Qed.
Lemma index2Z_neq_TCB´:
∀ i ofs p z i0,
Shared2ID2 i = Some p →
index2Z i ofs = Some z →
0 ≤ i0 < num_chan →
z ≠ i0 + ID_AT_range.
Proof.
intros. functional inversion H; subst.
functional inversion H0.
inv H4. inv H3.
unfold ID_SC_range, lock_TCB_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma release_lock_exist:
∀ i ofs e habd habd´ labd f,
release_lock_spec2 i ofs e habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, release_lock_spec2 i ofs e labd = Some labd´ ∧
relate_RData f habd´ labd´.
Proof.
unfold release_lock_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct. inv HQ.
inv multi_log_re0.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
subrewrite´.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq_TCB´; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Require Import LAsmModuleSemAux.
Lemma release_lock_sim2 :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id release_lock_spec2)
(id ↦ primcall_release_lock_compatsem id release_lock_spec2).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_lock_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- repeat (econstructor; eauto).
subst rs´. val_inject_simpl.
Qed.
Lemma acquire_lock_exist:
∀ bound i ofs habd habd´ labd f p l,
acquire_lock_spec2 bound i ofs habd = Some (habd´, p, l)
→ relate_RData f habd labd
→ (∃ labd´, acquire_lock_spec2 bound i ofs labd = Some (labd´, p, l) ∧
relate_RData f habd´ labd´)
∧ Shared2ID2 i = Some p.
Proof.
unfold acquire_lock_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct. inv HQ.
inv multi_log_re0.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
pose proof multi_oracle_re0 as Horacle.
inv multi_oracle_re0.
exploit H1; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
subrewrite´.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq_TCB´; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma acquire_lock_sim2:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec2)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec2).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_lock_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
match_external_states_simpl.
- simpl; trivial.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. inv H.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
match_external_states_simpl.
subst rs´. val_inject_simpl.
}
Qed.
Section PAGE_COPY_SIM.
Lemma page_copy_exist:
∀ s habd habd´ labd index i from f,
page_copy_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_spec; intros.
inv H0.
revert H. subrewrite.
subdestruct. inv HQ.
inv multi_log_re0.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
reflexivity.
}
intros.
rewrite <- H1.
rewrite Hdestruct7.
exploit page_copy_aux_exists; eauto.
intros Hcopy; rewrite Hcopy.
rewrite Hdestruct11.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq_TCB´; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy_match:
∀ s d d´ m index i from f,
page_copy_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_spec; intros. subdestruct.
inv H. inv H0; econstructor; eauto.
Qed.
Lemma page_copy_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_spec)
(id ↦ gensem page_copy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_exist; eauto 1.
exploit page_copy_match; eauto 1.
intros Hmatch.
intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Lemma page_copy_back_exist:
∀ s habd habd´ labd index i to f,
page_copy_back_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back_spec; intros.
inv H0.
revert H. subrewrite.
subdestruct. inv HQ.
inv multi_log_re0.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
reflexivity.
}
intros.
rewrite <- H1.
rewrite Hdestruct7.
rewrite Hdestruct10.
exploit page_copy_back_aux_exists; eauto.
intros [lh´ [Hcopy HPrel]].
rewrite Hcopy.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq_TCB´; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy_back_match:
∀ s d d´ m index i to f,
page_copy_back_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back_spec; intros. subdestruct.
inv H. inv H0; econstructor; eauto.
Qed.
Lemma page_copy_back_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back_spec)
(id ↦ gensem page_copy_back_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_back_match; eauto. intros Hmatch.
exploit page_copy_back_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End PAGE_COPY_BACK_SIM.
End Exists.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) pabqueue pqueueinit.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply page_copy_sim.
- apply page_copy_back_sim.
- apply vmxinfo_get_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply setPT_sim.
- apply ptRead_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply kctxt_new_sim.
- apply shared_mem_status_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit offer_shared_mem_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
match_external_states_simpl.
erewrite get_state_exists; simpl; eauto 1; reflexivity.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit set_state_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite tcb_get_CPU_ID_exist; eauto. reflexivity.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit tcb_set_CPU_ID_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit acquire_lock_TCB_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit release_lock_TCB_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl.
constructor.
split; simpl in *;
match goal with
| |- res_le _ _ _ ⇒ repeat constructor
| _ ⇒ try reflexivity
end.
intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2
HWB _ Hlow Hhigh Hhigh´ H Hι Hmd.
compatsim_simpl_inv_match H Hmd (@match_AbData).
exploit tdqueue_init_exists; eauto 1. intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit enqueue_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit dequeue_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply ptin_sim.
- apply ptout_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply sleeper_inc_sim.
- apply sleeper_dec_sim.
- apply sleeper_zzz_sim.
- apply release_lock_sim2.
- eapply acquire_lock_sim2; eauto.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply trapin_sim.
- apply trapout_sim.
- apply hostin_sim.
- apply hostout_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply kctxt_switch_sim.
- layer_sim_simpl.
+ eapply load_correct2.
+ eapply store_correct2.
Qed.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.
Lemma real_data : ∀ abtcb abq tcb tdq,
AbQ_RealQ (real_abtcb abtcb) (real_abq abq)
(real_tcb tcb) (real_tdq tdq).
Proof.
constructor.
- unfold abqueue_match_dllist, real_abq, real_tcb, real_tdq.
intros qi l Hqi.
rewrite !init_zmap_inside by omega.
intro H; inv H.
∃ num_proc, num_proc; split; auto; constructor.
- unfold abtcbpool_tcbpool, real_abtcb, real_tcb.
intros i tds inq parent Hi.
rewrite !init_zmap_inside by assumption.
intro H; inv H; eauto.
Qed.
Lemma real_relate_ABTCB_Log_Pool:
∀ habd labd,
relate_ABTCB_Log_Pool (multi_log habd) (multi_log labd) →
relate_ABTCB_Log_Pool (CalTicketLock.real_multi_log (multi_log habd)) (CalTicketLock.real_multi_log (multi_log labd)).
Proof.
assert (Hcases: ∀ a b, 0 ≤ a < b ∨ (a < 0 ∨ b ≤ a)) by (intros; omega).
assert (HZ2Nat: ∀ a b, 0 ≤ a < b → (0 ≤ Z.to_nat a < Z.to_nat b)%nat).
{
split.
rewrite <- Z2Nat.inj_0; rewrite <- Z2Nat.inj_le; omega.
rewrite <- Z2Nat.inj_lt; omega.
}
unfold CalTicketLock.real_multi_log; intros d1 d2 Hrel; inv Hrel; constructor.
- intros i ofs r Hneq Hind.
destruct (Hcases r lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id r); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
- intros i Hi.
destruct (Hcases (i + ID_AT_range) lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id (i + ID_AT_range)); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto; constructor; constructor.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
Qed.
Lemma tdqueue_init_exists :
∀ mbi_adr adt adt´ ladt f,
tdqueue_init0_spec (Int.unsigned mbi_adr) adt = Some adt´
→ relate_RData f adt ladt
→ ∃ ladt´,
tdqueue_init_spec (Int.unsigned mbi_adr) ladt = Some ladt´
∧ relate_RData f adt´ ladt´.
Proof.
unfold tdqueue_init_spec, tdqueue_init0_spec.
intros until f. exist_simpl.
- apply real_data.
- apply real_relate_ABTCB_Log_Pool; eauto.
Qed.
Lemma get_state_exists :
∀ n i adt ladt f,
get_state0_spec (Int.unsigned n) adt = Some i
→ relate_RData f adt ladt
→ get_state_spec (Int.unsigned n) ladt = Some i.
Proof.
unfold get_state_spec, get_state0_spec;
intros. inv H0. revert H. subrewrite. subdestruct.
destruct (ZMap.get (Int.unsigned n) (abtcb adt)) eqn: Hget; contra_inv.
inv Hdestruct4. inv HQ.
inv abq_re0.
unfold abtcbpool_tcbpool in Ht_match.
apply Ht_match in Hget; try omega.
destruct Hget as [pv [nx HT]].
rewrite HT. trivial.
Qed.
Lemma match_next_prev_presv_set_state:
∀ l start ending hd tl itcbp,
abqueue_match_next_prev_rec l hd tl start ending itcbp
→ ∀ i tds pv nx parent,
ZMap.get i itcbp = TCBValid tds parent pv nx
→ ∀ tds´ parent´, abqueue_match_next_prev_rec l hd tl start ending (ZMap.set i (TCBValid tds´ parent´ pv nx) itcbp).
Proof.
clear.
induction l; intros; inv H; econstructor; eauto.
destruct Hvalid as (st & parent0 & Hvalid).
destruct (zeq hd i); subst.
- rewrite ZMap.gss. rewrite H0 in Hvalid. inv Hvalid. eauto.
- rewrite ZMap.gso; eauto.
Qed.
Lemma set_state_exists:
∀ f n ts adt adt´ ladt,
set_state0_spec (Int.unsigned n) ts adt = Some adt´
→ relate_RData f adt ladt
→ ∃ ladt´,
set_state_spec (Int.unsigned n) ts ladt = Some ladt´
∧ relate_RData f adt´ ladt´.
Proof.
intros f n ts adt adt´ ladt HQ H.
inversion_clear H.
revert HQ.
unfold set_state0_spec, set_state_spec.
subrewrite.
subdestruct.
destruct (ZMap.get (Int.unsigned n) (abtcb adt)) eqn:Hgetn; contra_inv.
assert (Hget´ : ∃ pv nx,
ZMap.get (Int.unsigned n) (tcb ladt)
= TCBValid tds cpuid pv nx).
{
inv abq_re0.
unfold abtcbpool_tcbpool in Ht_match. inv Hdestruct4.
exploit Ht_match; eauto.
}
destruct Hget´ as [pv [nx Hget´]].
rewrite Hget´.
destruct (ZtoThreadState ts); contra_inv.
eexists.
split; eauto.
inv HQ. constructor; eauto; simpl.
inv abq_re0.
constructor; trivial.
- simpl in × .
intros qi l´ Hqi Hgetl´.
destruct (Hq_match _ _ Hqi Hgetl´) as [hd [tl [HgetQ Hx]]].
∃ hd; ∃ tl.
split; trivial.
apply match_next_prev_presv_set_state with tds cpuid; trivial.
- unfold abtcbpool_tcbpool in × .
simpl in × .
intros i tds´ inq parent Hi HT.
destruct (zeq i (Int.unsigned n)); subst.
+ rewrite ZMap.gss in ×. inv HT.
refine_split´; eauto.
+ rewrite ZMap.gso in *; eauto.
Qed.
Lemma match_next_prev_presv_gso:
∀ l start ending hd tl itcbp tcb i
(Hmatch: abqueue_match_next_prev_rec l hd tl start ending itcbp)
(HnotIn: ¬ In i l),
abqueue_match_next_prev_rec l hd tl start ending (ZMap.set i tcb itcbp).
Proof.
clear.
induction l; intros; inv Hmatch; try constructor.
destruct Hvalid as (st & parent & Hvalid).
econstructor; eauto.
- destruct (zeq hd i); subst.
+ elim HnotIn. left; trivial.
+ rewrite ZMap.gso; eauto.
- eapply IHl; eauto. intro HF. elim HnotIn.
right; trivial.
Qed.
Lemma dequeue_exists:
∀ f n i adt adt´ ladt,
dequeue0_spec (Int.unsigned n) adt = Some (adt´, i)
→ relate_RData f adt ladt
→ high_level_invariant adt
→ ∃ ladt´,
dequeue_spec (Int.unsigned n) ladt = Some (ladt´, i)
∧ relate_RData f adt´ ladt´.
Proof.
intros f n i adt adt´ ladt HQ H INV.
pose proof H as Hrel.
inversion_clear H.
revert HQ.
unfold dequeue_spec, dequeue0_spec.
subrewrite.
destruct (ikern ladt) eqn: HIK; contra_inv.
destruct (pg ladt) eqn: HIP; contra_inv.
destruct (ihost ladt) eqn: HIH; contra_inv.
destruct (ipt ladt) eqn: HIT; contra_inv.
destruct (zle_lt 0 (Int.unsigned n) num_chan); contra_inv.
destruct (ZMap.get (Int.unsigned n) (abq adt)) eqn: Hgetl; contra_inv.
pose proof abq_re0 as Habq.
inv Habq. exploit Hq_match; eauto.
intros (hd & tl & → & Hq_match´).
destruct l.
- inv Hq_match´. rewrite zeq_true. inv HQ.
refine_split´; eauto.
- assert (Hvalid_q : AbQCorrect (ZMap.get (Int.unsigned n) (abq adt))).
{
inversion INV.
eapply valid_TDQ; eauto.
}
assert (Hz_range: 0 ≤ z < num_proc).
{
unfold AbQCorrect in ×.
rewrite Hgetl in Hvalid_q.
destruct Hvalid_q as (l0 & Heq & Hrange).
inv Heq. eapply Hrange. left; trivial.
}
inv Hq_match´. rewrite zeq_false; [| omega].
destruct (ZMap.get hd (abtcb adt)) eqn: Hgett; contra_inv. inv HQ.
exploit Ht_match; eauto.
intros (pv & nx & Hvalid´).
destruct Hvalid as (st & parent & Heq).
rewrite Hvalid´ in Heq. inv Heq. rewrite Hvalid´.
destruct l.
+ inv Hmatch_ind.
rewrite zeq_true.
refine_split´; eauto.
econstructor; eauto; simpl.
constructor.
× intros qi l´ Hqi Hgetl´.
destruct (zeq qi (Int.unsigned n)); subst.
{
rewrite ZMap.gss in ×. inv Hgetl´.
refine_split´; eauto.
econstructor.
}
{
rewrite ZMap.gso in *; auto.
}
× intros i0 tds´ inq parent0 Hi0 HT.
destruct (zeq i0 i); subst.
{
rewrite ZMap.gss in ×. inv HT. eauto.
}
{
rewrite ZMap.gso in *; eauto.
}
+ inv Hmatch_ind.
assert (Hnext_range: 0 ≤ next < num_proc).
{
unfold AbQCorrect in ×.
rewrite Hgetl in Hvalid_q.
destruct Hvalid_q as (l0 & Heq & Hrange).
inv Heq. eapply Hrange. right. left; trivial.
}
rewrite zeq_false; [| omega].
destruct Hvalid as (st0 & parent0 & Hvalid).
rewrite Hvalid.
refine_split´; eauto.
econstructor; eauto; simpl.
assert (Hnext: ZMap.get next (abtcb adt) = AbTCBValid st0 parent0 (Int.unsigned n)).
{
inversion INV.
exploit valid_inQ; try eapply Hgetl; eauto.
right; left. trivial.
intros (s & c & Hnext).
exploit Ht_match; eauto.
rewrite Hvalid. intros (? & ? & Heq).
inv Heq. trivial.
}
assert (Hcount: count_occ zeq (i :: next :: l) next = 1%nat).
{
exploit valid_count; eauto.
rewrite Hgetl.
intros (l0 & Heq & Hcount). inv Heq.
trivial.
}
assert (Hneq: i ≠ next).
{
destruct (zeq i next); subst; trivial.
rewrite count_occ_cons_eq in Hcount; trivial.
rewrite count_occ_cons_eq in Hcount; trivial.
inv Hcount.
}
constructor.
× intros qi l´ Hqi Hgetl´.
destruct (zeq qi (Int.unsigned n)); subst.
{
rewrite ZMap.gss in ×. inv Hgetl´.
refine_split´; eauto.
econstructor.
- rewrite ZMap.gss. eauto.
- assert (HnotIn: ¬ In next l).
{
rewrite count_occ_cons_neq in Hcount; trivial.
rewrite count_occ_cons_eq in Hcount; trivial.
intro HF.
eapply (count_occ_In zeq) in HF. omega.
}
eapply match_next_prev_presv_gso; eauto.
}
{
rewrite ZMap.gso in *; eauto.
exploit Hq_match; eauto.
intros (hd & tl0 & Heq & Hmatch).
refine_split´; eauto.
eapply match_next_prev_presv_gso; eauto.
intro HF. elim n0.
exploit valid_inQ; eauto.
rewrite Hnext. intros (s0 & c0 & Heq´).
inv Heq´. trivial.
}
× intros i0 tds´ inq parent1 Hi0 HT.
destruct (zeq i0 i); subst.
{
rewrite ZMap.gss in ×. inv HT.
rewrite ZMap.gso; eauto.
}
{
rewrite ZMap.gso in HT; auto.
destruct (zeq i0 next); subst.
- rewrite ZMap.gss. rewrite Hnext in HT. inv HT. eauto.
- rewrite ZMap.gso; eauto.
}
Qed.
Lemma abqueue_match_next_prev_rec_tail:
∀ l hd tl start ending tcb
(Hrange: ∀ x, In x l → 0 ≤ x < num_proc)
(Hmatch: abqueue_match_next_prev_rec l hd tl start ending tcb),
l = nil ∨ ((∃ z l´, l = z :: l´) ∧ 0 ≤ tl < num_proc ∧ In tl l).
Proof.
induction l; intros; inv Hmatch; eauto.
destruct l.
- inv Hmatch_ind. right.
split; eauto.
split.
+ exploit (Hrange hd). left; trivial.
intros; trivial.
+ left; trivial.
- exploit IHl; eauto.
intros. eapply Hrange. right; trivial.
intros HF. inv HF; contra_inv.
right. destruct H as ((z0 & l´ &Hl) & Hneq & Hin). inv Hl.
split; eauto.
split; eauto.
right; trivial.
Qed.
Lemma abqueue_match_next_prev_rec_tail´:
∀ l x y hd tl start ending tcb
(Hmatch: abqueue_match_next_prev_rec (x :: y :: l) hd tl start ending tcb),
In tl (y :: l).
Proof.
induction l; intros; inv Hmatch; eauto.
- inv Hmatch_ind.
inv Hmatch_ind0.
left. trivial.
- exploit IHl; eauto.
intros. right; trivial.
Qed.
Lemma abqueue_match_next_prev_rec_enqueue:
∀ l z hd tl tcb i tds cpuid st´ c´ prev´ next´ starting ending prev0 next0
(Hmatch: abqueue_match_next_prev_rec (z :: l) hd tl starting ending tcb)
(Hi: ZMap.get i tcb = TCBValid tds cpuid prev0 next0)
(Htl: ZMap.get tl tcb = TCBValid st´ c´ prev´ next´)
(Hcount: ∀ x, In x (z :: l) → count_occ zeq (z :: l) x = 1%nat)
(Hneq: ∀ x, In x (z:: l) → x ≠ i),
abqueue_match_next_prev_rec (z :: l ++ i :: nil) hd i starting ending
(ZMap.set i (TCBValid tds cpuid tl ending)
(ZMap.set tl (TCBValid st´ c´ prev´ i) tcb)).
Proof.
induction l; intros.
- inv Hmatch. inv Hmatch_ind.
rewrite Htl in Hvalid.
destruct Hvalid as (st & parent & Heq). inv Heq.
econstructor.
+ rewrite ZMap.gso; eauto.
rewrite ZMap.gss; eauto.
eapply Hneq. left; trivial.
+ econstructor; eauto.
× rewrite ZMap.gss; eauto.
× econstructor.
- assert (Hneq0: hd ≠ tl).
{
intro HF. subst.
exploit abqueue_match_next_prev_rec_tail´; eauto. intros HIn.
inv Hmatch. exploit (Hcount tl).
left; trivial.
intros.
rewrite count_occ_cons_eq in H; trivial.
eapply (count_occ_In zeq) in HIn. omega.
}
inv Hmatch.
destruct Hvalid as (st & parent & Hvalid).
rewrite <- app_comm_cons.
econstructor; eauto.
+ rewrite ZMap.gso; eauto.
rewrite ZMap.gso; eauto.
eapply Hneq. left; trivial.
+ eapply IHl; eauto.
× intros. destruct (zeq x hd); subst.
{
exploit (Hcount hd); eauto.
left; trivial.
intros HIn.
rewrite count_occ_cons_eq in HIn; trivial.
eapply (count_occ_In zeq) in H. omega.
}
{
exploit (Hcount x); eauto.
right; trivial.
intros Hin.
rewrite count_occ_cons_neq in Hin; auto.
}
× intros. eapply Hneq. right; trivial.
Qed.
Lemma enqueue_exists:
∀ f n i adt adt´ ladt
(HQ: enqueue0_spec (Int.unsigned n) i adt = Some adt´)
(Hr: relate_RData f adt ladt)
(INV: high_level_invariant adt)
(INV´: PQueueInit.high_level_invariant ladt),
∃ ladt´,
enqueue_spec (Int.unsigned n) i ladt = Some ladt´
∧ relate_RData f adt´ ladt´.
Proof.
intros.
inversion_clear Hr.
revert HQ.
unfold enqueue_spec, enqueue0_spec.
subrewrite. subdestruct; subst. functional inversion Hdestruct3.
assert (Hvalid_q : AbQCorrect (ZMap.get (Int.unsigned n) (abq adt))).
{
inversion INV.
eapply valid_TDQ; eauto.
}
inv HQ.
pose proof abq_re0 as Habq.
inv Habq. exploit Hq_match; eauto.
intros (hd & tl & Hvalidq & Hq_match´). rewrite Hvalidq.
exploit Ht_match; eauto.
intros (pv & nx & Hvalid´). rewrite Hvalid´.
unfold AbQCorrect in ×.
rewrite Hdestruct5 in Hvalid_q.
destruct Hvalid_q as (l0 & Heq & Hvalid_q). inv Heq.
pose proof Hvalid_q as Hvalid_q´.
eapply abqueue_match_next_prev_rec_tail in Hvalid_q´; eauto.
destruct Hvalid_q´ as [HFF | HFF]; subst.
+ inv Hq_match´.
rewrite zeq_true.
refine_split´; eauto.
econstructor; eauto; simpl.
constructor.
× intros qi l´ Hqi Hgetl´.
destruct (zeq qi (Int.unsigned n)); subst.
{
rewrite ZMap.gss in ×. inv Hgetl´.
refine_split´; eauto.
econstructor.
- rewrite ZMap.gss. eauto.
- constructor.
}
{
rewrite ZMap.gso in *; auto.
exploit Hq_match; eauto.
intros (hd & tl & Hvalidq´ & Hmatch).
refine_split´; eauto.
eapply match_next_prev_presv_gso; eauto.
intro HF.
inv INV.
exploit valid_inQ; eauto. rewrite Hdestruct6.
intros (s & c & Heq). inv Heq. omega.
}
× intros i0 tds´ inq parent0 Hi0 HT.
destruct (zeq i0 i); subst.
{
rewrite ZMap.gss in ×. inv HT. eauto.
}
{
rewrite ZMap.gso in *; eauto.
}
+ destruct HFF as ((z & l´ & Hl) & Hneq & Hin´). subst.
rewrite zeq_false; [| omega].
assert (Htcb: ∃ st´ c´ prev´ next´,
ZMap.get tl (tcb ladt) = TCBValid st´ c´ prev´ next´).
{
inv INV´. exploit valid_TCB; eauto.
unfold TCBCorrect.
intros (s & c & p & next & Htcb & _ & _).
eauto.
}
destruct Htcb as (st´ & c´ & prev´ & next´ & Htcb).
rewrite Htcb.
refine_split´; eauto.
constructor; eauto; simpl.
constructor.
× intros qi l Hqi Hgetl.
destruct (zeq qi (Int.unsigned n)); subst.
{
rewrite ZMap.gss in ×. inv Hgetl.
refine_split´; eauto.
eapply abqueue_match_next_prev_rec_enqueue; eauto.
- intros. exploit Hvalid_q; eauto. intros Hrange_x.
inv INV.
exploit valid_inQ; eauto.
intros (s & c & Habtcb).
exploit valid_count; eauto.
rewrite Hdestruct5.
intros (l & Heq & Hcount). inv Heq. trivial.
- intros. exploit Hvalid_q; eauto. intros Hrange_x.
inv INV.
exploit valid_inQ; eauto.
intros (s & c & Habtcb).
intro HF; subst.
rewrite Hdestruct6 in Habtcb. inv Habtcb. omega.
}
{
rewrite ZMap.gso in *; eauto.
exploit Hq_match; eauto.
intros (hd0 & tl0 & Heq & Hmatch).
assert (Hin: InQ (abtcb adt) (abq adt)).
{
inv INV. eauto.
}
refine_split´; eauto.
eapply match_next_prev_presv_gso; eauto.
eapply match_next_prev_presv_gso; eauto.
- intros HF. exploit Hin; eauto.
intros (s & c & Habtcb).
clear Hqi.
exploit Hin; eauto.
rewrite Habtcb.
intros (s0 & c0 & Habtcb´). inv Habtcb´.
congruence.
- intros HF. clear Hneq. exploit Hin; eauto.
intros (s & c & Habtcb).
rewrite Hdestruct6 in Habtcb. inv Habtcb.
omega.
}
× intros i0 tds´ inq parent1 Hi0 HT.
destruct (zeq i0 i); subst.
{
rewrite ZMap.gss in ×. inv HT. eauto.
}
{
rewrite ZMap.gso in HT; auto.
rewrite ZMap.gso; auto.
destruct (zeq i0 tl); subst.
- rewrite ZMap.gss.
exploit Ht_match; eauto.
rewrite Htcb.
intros (pv0 & nx0 & Heq).
inv Heq. eauto.
- rewrite ZMap.gso; eauto.
}
Qed.
Lemma relate_ABTCB_Log_Pool_gss:
∀ hl ll l0,
relate_ABTCB_Log_Pool hl ll →
relate_ABTCB_Log_Pool
(ZMap.set 0 l0 hl) (ZMap.set 0 l0 ll).
Proof.
intros. inv H. constructor; eauto.
- intros. destruct (zeq r 0); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- intros.
assert (Hneq: i + ID_AT_range ≠ 0).
{
unfold ID_AT_range. omega.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma palloc_exist:
∀ habd habd´ labd n i f,
palloc_spec n habd = Some (habd´, i)
→ relate_RData f habd labd
→ ∃ labd´, palloc_spec n labd = Some (labd´, i) ∧ relate_RData f habd´ labd´.
Proof.
unfold palloc_spec; intros.
revert H. pose proof H0 as HR. inv H0.
assert (Hlog: ZMap.get 0 (multi_log habd) = ZMap.get 0 (multi_log labd)).
{
inv multi_log_re0. eapply (H 0 0); auto. omega.
}
assert (Horacle: ZMap.get 0 (multi_oracle habd) = ZMap.get 0 (multi_oracle labd)).
{
inv multi_oracle_re0. eapply (H 0 0); auto. omega.
}
rewrite Horacle.
subrewrite. subdestruct; inv HQ.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_ABTCB_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_ABTCB_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_ABTCB_Log_Pool_gss. eauto.
Qed.
Lemma ptAllocPDE0_exist:
∀ habd habd´ labd i n v f,
ptAllocPDE0_spec n v habd = Some (habd´, i)
→ relate_RData f habd labd
→ ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
∧ relate_RData f habd´ labd´.
Proof.
unfold ptAllocPDE0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; destruct p; inv HQ.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
rewrite H. rewrite Hdestruct8.
refine_split´; trivial.
inv H0.
constructor; simpl; try eassumption.
+ apply FlatMem.free_page_inj´. trivial.
+ subrewrite´.
+ subrewrite´.
Qed.
Lemma ptInsert0_exist:
∀ s habd habd´ labd i n v pa pe f,
ptInsert0_spec n v pa pe habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptInsert0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- exploit (ptInsertPTE0_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
exploit (ptInsertPTE0_exist s); eauto.
intros (labd´0 & HptInsert0´´ & Hre´).
subrewrite´.
refine_split´; trivial.
Qed.
Lemma ptResv_exist:
∀ s habd habd´ labd i n v p f,
ptResv_spec n v p habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv_spec; intros.
subdestruct. destruct p0.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
Qed.
Lemma ptResv2_exist:
∀ s habd habd´ labd i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv2_spec; intros.
subdestruct; destruct p0; inv H.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?). revert H2.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?). intros.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
Qed.
Lemma offer_shared_mem_exists:
∀ s habd habd´ labd i1 i2 v z f,
offer_shared_mem_spec i1 i2 v habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, offer_shared_mem_spec i1 i2 v labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold offer_shared_mem_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- refine_split´; trivial.
constructor; eauto.
Qed.
Lemma tcb_get_CPU_ID_exist:
∀ habd labd i z f,
get_abtcb_CPU_ID_spec i habd = Some z
→ relate_RData f habd labd
→ tcb_get_CPU_ID_spec i labd = Some z.
Proof.
unfold tcb_get_CPU_ID_spec, get_abtcb_CPU_ID_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
inv abq_re0.
exploit Ht_match; eauto.
intros (pv & nx & ->). trivial.
Qed.
Lemma tcb_set_CPU_ID_exist:
∀ habd habd´ labd i z f,
set_abtcb_CPU_ID_spec i z habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, tcb_set_CPU_ID_spec i z labd = Some labd´
∧ relate_RData f habd´ labd´.
Proof.
unfold tcb_set_CPU_ID_spec, set_abtcb_CPU_ID_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
inv abq_re0.
exploit Ht_match; eauto.
intros (pv & nx & Htcb). rewrite Htcb.
refine_split´; trivial.
constructor; eauto.
constructor; simpl.
- simpl in × .
intros qi l´ Hqi Hgetl´.
destruct (Hq_match _ _ Hqi Hgetl´) as [hd [tl [HgetQ Hx]]].
∃ hd; ∃ tl.
split; trivial.
apply match_next_prev_presv_set_state with tds cpuid; trivial.
- unfold abtcbpool_tcbpool in × .
simpl in × .
intros i0 tds´ inq parent Hi HT.
destruct (zeq i0 i); subst.
+ rewrite ZMap.gss in ×. inv HT.
refine_split´; eauto.
+ rewrite ZMap.gso in *; eauto.
Qed.
Lemma H_CalLock_rel:
∀ l l´ p
(Hcal: H_CalLock l = Some p)
(Hrel: relate_ABTCB_Log l l´),
H_CalLock l´ = Some p.
Proof.
induction l; intros; inv Hrel; trivial.
Local Transparent H_CalLock.
simpl in ×.
subdestruct_one.
exploit IHl; eauto.
destruct p0. destruct p0.
intros Hcal´. rewrite Hcal´.
subdestruct; inv Hrelate_event; inv Hcal; trivial.
Local Opaque H_CalLock.
Qed.
Lemma index2Z_neq_TCB:
∀ i i0 ofs r
(Hi: 0 ≤ i < num_chan)
(Hi0: i0 ≠ ID_TCB)
(Hindex: index2Z i0 ofs = Some r),
r ≠ i + ID_AT_range.
Proof.
intros. functional inversion Hindex.
clear Hindex. functional inversion H1; subst.
- inv H0. unfold ID_AT_range in ×. omega.
- elim Hi0; trivial.
- inv H0. unfold ID_SC_range, lock_TCB_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma add_false:
∀ i i0 n,
i0 ≠ i →
i0 + n ≠ i + n.
Proof.
intros. omega.
Qed.
Lemma relate_ABTCB_Log_gss_ticket:
∀ e c l l´
(Hrel: relate_ABTCB_Log l l´),
relate_ABTCB_Log (TEVENT c (TTICKET e) :: l) (TEVENT c (TTICKET e) :: l´).
Proof.
intros. constructor; trivial.
constructor.
Qed.
Lemma relate_ABTCB_Log_gss_pull:
∀ c l l´
(Hrel: relate_ABTCB_Log l l´),
relate_ABTCB_Log (TEVENT c (TSHARED OPULL) :: l) (TEVENT c (TSHARED OPULL) :: l´).
Proof.
intros. constructor; trivial.
constructor.
Qed.
Lemma relate_ABTCB_Log_gss_TCB:
∀ ta qa t q c l l´
(Hrel: relate_ABTCB_Log l l´)
(Hrel_e: AbQ_RealQ ta qa t q),
relate_ABTCB_Log (TEVENT c (TSHARED (OABTCBE ta qa)) :: l) (TEVENT c (TSHARED (OTCBE t q)) :: l´).
Proof.
intros. constructor; trivial.
constructor. constructor. trivial.
Qed.
Lemma release_lock_TCB_exist:
∀ habd habd´ labd i f,
release_lock_ABTCB_spec i habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, release_lock_TCB_spec i labd = Some labd´ ∧
relate_RData f habd´ labd´.
Proof.
unfold release_lock_ABTCB_spec, release_lock_TCB_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
inv multi_log_re0.
exploit H0; eauto. intros Htcb.
rewrite Hdestruct3 in Htcb. inv Htcb.
assert (Hrel: relate_ABTCB_Log
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OABTCBE (abtcb habd) (abq habd)))
:: l)
(TEVENT (CPU_ID labd) (TTICKET REL_LOCK)
:: TEVENT (CPU_ID labd) (TSHARED (OTCBE (tcb labd) (tdq labd))) :: l2)).
{
eapply relate_ABTCB_Log_gss_ticket.
eapply relate_ABTCB_Log_gss_TCB; eauto.
}
erewrite (H_CalLock_rel _ _ _ Hdestruct4); eauto.
refine_split´; trivial.
constructor; eauto.
constructor; simpl.
- intros.
assert (Hneq: r ≠ (i + ID_AT_range)).
{
eapply index2Z_neq_TCB; eauto.
}
repeat rewrite ZMap.gso; eauto.
- intros. destruct (zeq i0 i); subst.
+ repeat rewrite ZMap.gss; eauto. constructor; trivial.
+ repeat rewrite ZMap.gso; eauto.
eapply add_false; eauto.
eapply add_false; eauto.
Qed.
Lemma relate_ABTCB_Log_getshared:
∀ l l´
(Hrel: relate_ABTCB_Log l l´),
∀ p
(Hget: GetSharedABTCB l = p),
match p with
| Some (ta, qa) ⇒
∃ t q,
GetSharedTCB l´ = Some (t, q)
∧ AbQ_RealQ ta qa t q
| None ⇒ GetSharedTCB l´ = None
end.
Proof.
induction l; simpl; intros.
- inv Hget. inv Hrel. trivial.
- destruct a. destruct e; inv Hget.
+ inv Hrel. inv Hrelate_event; simpl.
exploit IHl; eauto.
+ destruct e; inv Hrel; inv Hrelate_event; simpl.
× exploit IHl; eauto.
× inv Hrelate_e. refine_split´; eauto.
Qed.
Lemma acquire_lock_TCB_exist:
∀ n habd habd´ labd f,
acquire_lock_ABTCB_spec n habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, acquire_lock_TCB_spec n labd = Some labd´ ∧
relate_RData f habd´ labd´.
Proof.
unfold acquire_lock_ABTCB_spec, acquire_lock_TCB_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
subdestruct_one.
destruct (ZMap.get (n + ID_AT_range) (multi_log habd)) eqn: Hlog; contra_inv.
inv multi_log_re0.
exploit H0; eauto. intros Htcb.
rewrite Hlog in Htcb. inv Htcb.
subdestruct_one.
subdestruct_one.
assert (Hrel: relate_ABTCB_Log
(ZMap.get (n + ID_AT_range) (multi_oracle habd) (CPU_ID labd) l ++ l)
(ZMap.get (n + ID_AT_range) (multi_oracle labd) (CPU_ID labd) l2 ++ l2)).
{
inv multi_oracle_re0. specialize (H4 _ a). inv H4.
eapply H5; eauto.
}
assert (Hrel´: relate_ABTCB_Log
(TEVENT (CPU_ID labd) (TSHARED OPULL) ::
TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get (n + ID_AT_range) (multi_oracle habd) (CPU_ID labd) l ++ l)
(TEVENT (CPU_ID labd) (TSHARED OPULL) ::
TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get (n + ID_AT_range) (multi_oracle labd) (CPU_ID labd) l2 ++ l2)).
{
eapply relate_ABTCB_Log_gss_pull; eauto.
eapply relate_ABTCB_Log_gss_ticket; eauto.
}
erewrite (H_CalLock_rel _ _ _ Hdestruct4); eauto.
pose proof (relate_ABTCB_Log_getshared _ _ Hrel) as Htcb.
subdestruct_one; contra_inv.
- destruct p0. exploit Htcb; eauto. simpl.
intros (t & q & → & Hreal).
refine_split´; trivial. inv HQ.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
assert (Hneq: r ≠ (n + ID_AT_range)).
{
eapply index2Z_neq_TCB; eauto.
}
repeat rewrite ZMap.gso; eauto.
+ intros. destruct (zeq i n); subst.
× repeat rewrite ZMap.gss; eauto. constructor; trivial.
× repeat rewrite ZMap.gso; eauto.
eapply add_false; eauto.
eapply add_false; eauto.
- exploit Htcb; eauto. simpl.
intros Hreal. rewrite Hreal.
refine_split´; trivial. inv HQ.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
assert (Hneq: r ≠ (n + ID_AT_range)).
{
eapply index2Z_neq_TCB; eauto.
}
repeat rewrite ZMap.gso; eauto.
+ intros. destruct (zeq i n); subst.
× repeat rewrite ZMap.gss; eauto. constructor; trivial.
× repeat rewrite ZMap.gso; eauto.
eapply add_false; eauto.
eapply add_false; eauto.
Qed.
Lemma Shared2ID2_neq:
∀ i p,
Shared2ID2 i = Some p →
i ≠ ID_TCB.
Proof.
intros. functional inversion H; subst. omega.
Qed.
Lemma index2Z_neq_TCB´:
∀ i ofs p z i0,
Shared2ID2 i = Some p →
index2Z i ofs = Some z →
0 ≤ i0 < num_chan →
z ≠ i0 + ID_AT_range.
Proof.
intros. functional inversion H; subst.
functional inversion H0.
inv H4. inv H3.
unfold ID_SC_range, lock_TCB_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma release_lock_exist:
∀ i ofs e habd habd´ labd f,
release_lock_spec2 i ofs e habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, release_lock_spec2 i ofs e labd = Some labd´ ∧
relate_RData f habd´ labd´.
Proof.
unfold release_lock_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct. inv HQ.
inv multi_log_re0.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
subrewrite´.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq_TCB´; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Require Import LAsmModuleSemAux.
Lemma release_lock_sim2 :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id release_lock_spec2)
(id ↦ primcall_release_lock_compatsem id release_lock_spec2).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_lock_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- repeat (econstructor; eauto).
subst rs´. val_inject_simpl.
Qed.
Lemma acquire_lock_exist:
∀ bound i ofs habd habd´ labd f p l,
acquire_lock_spec2 bound i ofs habd = Some (habd´, p, l)
→ relate_RData f habd labd
→ (∃ labd´, acquire_lock_spec2 bound i ofs labd = Some (labd´, p, l) ∧
relate_RData f habd´ labd´)
∧ Shared2ID2 i = Some p.
Proof.
unfold acquire_lock_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct. inv HQ.
inv multi_log_re0.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
pose proof multi_oracle_re0 as Horacle.
inv multi_oracle_re0.
exploit H1; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
subrewrite´.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq_TCB´; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma acquire_lock_sim2:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec2)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec2).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_lock_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
match_external_states_simpl.
- simpl; trivial.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. inv H.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
match_external_states_simpl.
subst rs´. val_inject_simpl.
}
Qed.
Section PAGE_COPY_SIM.
Lemma page_copy_exist:
∀ s habd habd´ labd index i from f,
page_copy_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_spec; intros.
inv H0.
revert H. subrewrite.
subdestruct. inv HQ.
inv multi_log_re0.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
reflexivity.
}
intros.
rewrite <- H1.
rewrite Hdestruct7.
exploit page_copy_aux_exists; eauto.
intros Hcopy; rewrite Hcopy.
rewrite Hdestruct11.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq_TCB´; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy_match:
∀ s d d´ m index i from f,
page_copy_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_spec; intros. subdestruct.
inv H. inv H0; econstructor; eauto.
Qed.
Lemma page_copy_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_spec)
(id ↦ gensem page_copy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_exist; eauto 1.
exploit page_copy_match; eauto 1.
intros Hmatch.
intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Lemma page_copy_back_exist:
∀ s habd habd´ labd index i to f,
page_copy_back_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back_spec; intros.
inv H0.
revert H. subrewrite.
subdestruct. inv HQ.
inv multi_log_re0.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
reflexivity.
}
intros.
rewrite <- H1.
rewrite Hdestruct7.
rewrite Hdestruct10.
exploit page_copy_back_aux_exists; eauto.
intros [lh´ [Hcopy HPrel]].
rewrite Hcopy.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq_TCB´; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy_back_match:
∀ s d d´ m index i to f,
page_copy_back_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back_spec; intros. subdestruct.
inv H. inv H0; econstructor; eauto.
Qed.
Lemma page_copy_back_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back_spec)
(id ↦ gensem page_copy_back_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_back_match; eauto. intros Hmatch.
exploit page_copy_back_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End PAGE_COPY_BACK_SIM.
End Exists.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) pabqueue pqueueinit.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply page_copy_sim.
- apply page_copy_back_sim.
- apply vmxinfo_get_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply setPT_sim.
- apply ptRead_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply kctxt_new_sim.
- apply shared_mem_status_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit offer_shared_mem_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
match_external_states_simpl.
erewrite get_state_exists; simpl; eauto 1; reflexivity.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit set_state_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite tcb_get_CPU_ID_exist; eauto. reflexivity.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit tcb_set_CPU_ID_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit acquire_lock_TCB_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit release_lock_TCB_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl.
constructor.
split; simpl in *;
match goal with
| |- res_le _ _ _ ⇒ repeat constructor
| _ ⇒ try reflexivity
end.
intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2
HWB _ Hlow Hhigh Hhigh´ H Hι Hmd.
compatsim_simpl_inv_match H Hmd (@match_AbData).
exploit tdqueue_init_exists; eauto 1. intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit enqueue_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit dequeue_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply ptin_sim.
- apply ptout_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply sleeper_inc_sim.
- apply sleeper_dec_sim.
- apply sleeper_zzz_sim.
- apply release_lock_sim2.
- eapply acquire_lock_sim2; eauto.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply trapin_sim.
- apply trapout_sim.
- apply hostin_sim.
- apply hostout_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply kctxt_switch_sim.
- layer_sim_simpl.
+ eapply load_correct2.
+ eapply store_correct2.
Qed.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.