Library mcertikos.driver.CertiKOSExtraction
Require Import CertiKOS.
Require Import Maps.
Require Import Coqlib.
Require Import GlobalOracleProp.
Require Import LogReplay.
Require Import ZArith.
Require Import Omega.
Instance waittime_instances: WaitTime.
econstructor. instantiate (1:= 1%nat). omega.
Defined.
Require Import AuxStateDataType.
Require Import Constant.
Definition fair_oracle (cid: Z) (l: MultiLog) :=
match Q_CalLock l with
| Some (self_c, O, b, c :: q, tq) ⇒
if zeq c cid then nil
else if zle_lt 0 c TOTAL_CPU then
match b with
| LEMPTY ⇒ (TEVENT c (TTICKET (GET_NOW))) :: nil
| LGET ⇒ (TEVENT c (TTICKET HOLD_LOCK)) :: nil
| LHOLD ⇒ (TEVENT c (TTICKET INC_NOW)) :: nil
end
else nil
| _ ⇒ nil
end.
Instance oracle_ops0_instances: MultiOracleOps0 :=
{
multi_oracle_init0:= ZMap.init fair_oracle
}.
Instance oracle_ops1_instances: GlobalOracleProp.MultiOracleOps1 :=
{
multi_oracle_init1:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops2_instances: GlobalOracleProp.MultiOracleOps2 :=
{
multi_oracle_init2:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops3_instances: GlobalOracleProp.MultiOracleOps3 :=
{
multi_oracle_init3:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops4_instances: GlobalOracleProp.MultiOracleOps4 :=
{
multi_oracle_init4:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops5_instances: GlobalOracleProp.MultiOracleOps5 :=
{
multi_oracle_init5:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops6_instances: GlobalOracleProp.MultiOracleOps6 :=
{
multi_oracle_init6:= ZMap.init (fun _ _ ⇒ nil);
multi_oracle_init7:= ZMap.init (fun _ _ ⇒ nil);
multi_oracle_init8:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops_instances: GlobalOracle.MultiOracleOps.
econstructor.
instantiate (1 := 1%Z). omega.
instantiate (1 := 2%Z). omega.
constructor.
Defined.
Instance big_ops_instances: BigStepGlobalOracle.BigOracleOps.
repeat constructor.
Defined.
Require Import CommonTactic.
Transparent Q_CalLock.
Lemma nil_other:
∀ l self_c other_c b tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, nil, tq)),
other_c ≠ O.
Proof.
induction l; simpl; intros.
- inv Hcal. omega.
- destruct a. subdestruct; contra_inv; inv Hcal; try omega.
Qed.
Lemma head_other:
∀ l c self_c other_c b q tq
(Hlast : match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end)
(Hcal : Q_CalLock l = Some (self_c, other_c, b, c :: q, tq)),
other_c ≠ O.
Proof.
intros. destruct l; simpl in Hcal.
- inv Hcal.
- destruct m; subst. subdestruct; contra_inv; inversion Hcal; try omega.
subst.
eapply nil_other; eauto.
Qed.
Lemma cpu_range:
∀ l self_c other_c b q tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hin´: ∀ i1 e1, In (TEVENT i1 e1) l → 0 ≤ i1 < 8),
(∀ c, In c q → 0 ≤ c < 8).
Proof.
induction l; simpl; intros.
- inv Hcal. inv H.
- destruct a. subdestruct; contra_inv; inv Hcal; try omega.
+ inv H. eapply Hin´. left. trivial. inv H0.
+ inv H; [eapply Hin´; eauto | eapply IHl; eauto; right; trivial].
+ eapply IHl; eauto; right; trivial.
+ eapply IHl; eauto; right; trivial.
+ eapply IHl; eauto; right; trivial.
+ eapply IHl; eauto; right; trivial.
+ rewrite app_comm_cons in H.
eapply in_app_or in H.
inv H.
× eapply IHl; eauto; right; trivial.
× inv H0. eapply Hin´; eauto. inv H.
+ eapply IHl; eauto; right; trivial.
Qed.
Lemma other_zero_head:
∀ l self_c h q tq
(Hcal: Q_CalLock l = Some (self_c, 0%nat, h, q, tq)),
∃ z q´ t tq´, q = z :: q´ ∧ tq = t :: tq´.
Proof.
destruct l; simpl; intros. inv Hcal.
subdestruct; inv Hcal; eauto 20.
Qed.
Lemma valid_fair:
∀ l c r
(Hin : valid_qlock l)
(Hin´: ∀ (i1 : Z) (e1 : MultiOracleEventUnit),
In (TEVENT i1 e1) l → 0 ≤ i1 < 8)
(Hlast : match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end),
∃
(self_c other_c : nat) (b : head_status) (q : list Z)
(tq : list nat),
Q_CalLock (ZMap.get r (ZMap.init fair_oracle) c l ++ l) =
Some (self_c, other_c, b, q, tq) ∧ other_c ≠ 0%nat.
Proof.
intros. unfold LogReplay.valid_qlock in Hin. destruct Hin as (self_c & other_c & b & q & tq & Hcal).
rewrite ZMap.gi. unfold fair_oracle. rewrite Hcal.
destruct other_c.
× exploit other_zero_head; eauto.
intros (z & q´ & t & tq´ & ? & ? ); subst.
destruct (zeq z c).
{
subst. simpl; intros.
eapply head_other in Hcal; eauto. elim Hcal. trivial.
}
exploit cpu_range; eauto.
{ left. eauto. }
intros Hz.
rewrite zle_lt_true; trivial. destruct b; simpl; rewrite Hcal.
{
simpl. rewrite zeq_true.
repeat esplit; eauto.
}
{
simpl. rewrite zeq_true.
repeat esplit; eauto.
}
{
simpl. rewrite zeq_true.
repeat esplit; eauto.
}
× repeat esplit; eauto.
Qed.
Lemma get_free_weak:
∀ e l
(Hfree : get_free_qlock (e:: l)),
get_free_qlock l.
Proof.
unfold get_free_qlock. intros.
destruct Hincr as (prefix & Hprefix).
destruct prefix.
- simpl in Hprefix. inv Hprefix. eapply Hfree; eauto. ∃ (e::nil).
simpl; trivial.
- inv Hprefix. eapply Hfree; eauto. ∃ (e::m::prefix). trivial.
Qed.
Lemma fair_case:
∀ i l,
let l´ := fair_oracle i l in
∀ c e, ¬ In (TEVENT c (TSHARED e)) l´.
Proof.
unfold fair_oracle. intros. intro HF.
destruct (Q_CalLock l) eqn:Hcal; contra_inv.
- destruct p as ((((self_c & other_c) & h) & q) & tq).
destruct other_c; [| inv HF].
destruct q. inv HF.
destruct (zeq z i). inv HF.
destruct (zle_lt 0 z 8); [|inv HF].
destruct h; inv HF; try inv H.
- inv HF.
Qed.
Lemma fair_free:
∀ l self_c other_c h q tq i
(Hfrom: ∀ i1 e1,
In (TEVENT i1 e1) l →
i1 ≠ i →
∃ l0, In (TEVENT i1 e1) (fair_oracle i l0))
(Hcal: Q_CalLock l = Some (self_c, other_c, h, q, tq))
(Hfree: get_free_qlock l),
CalValidBit l = Some FreeToPull ∨ (h = LHOLD ∧ ∃ q´, q = i :: q´).
Proof.
induction l; simpl; intros; auto.
destruct a.
destruct (Q_CalLock l) eqn:Hcal´; contra_inv.
destruct p as ((((self_c´ & other_c´) & h´) & q´) & tq´).
subdestruct; inv Hcal.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv H.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv H.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq. unfold get_free_qlock in Hfree.
specialize (Hfree LEMPTY O (S O) q´ tq (TEVENT i (TTICKET INC_NOW) :: l)).
exploit Hfree; eauto.
{
∃ nil. trivial.
}
simpl. rewrite Hcal´. rewrite zeq_true. trivial.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
destruct (zeq z i); subst.
{
right. split; eauto.
}
{
left. exploit Hfrom; eauto.
intros (l2 & HIn).
exploit fair_case; eauto. intros HF; inv HF.
}
× inv Heq. right. split; eauto.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq. right. split; eauto.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq. right. split; eauto.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq. right. split; eauto.
Qed.
Lemma fair_free´:
∀ i l,
let l´ := fair_oracle i l in
l´ = nil ∨ ∃ c, c ≠ i ∧
(l´ = ((TEVENT c (TTICKET (GET_NOW))) :: nil)
∨ l´ = ((TEVENT c (TTICKET HOLD_LOCK)) :: nil)
∨ (l´ = ((TEVENT c (TTICKET INC_NOW)) :: nil))).
Proof.
unfold fair_oracle. intros.
destruct (Q_CalLock l) eqn:Hcal; [|left;trivial].
destruct p as ((((self_c & other_c) & h) & q) & tq).
destruct other_c; [|left; trivial].
destruct q. left; trivial.
destruct (zeq z i). left; trivial.
destruct (zle_lt 0 z 8); [|left; trivial].
right. ∃ z. split; trivial.
destruct h.
+ left; trivial.
+ right; left. trivial.
+ right. right. trivial.
Qed.
Require Import MQTicketLockOp.
Instance multi_oracle_prop_instances: GlobalOracleProp.MultiOracleProp.
constructor.
- unfold LogReplay.valid_multi_oracle_pool.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_queue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. unfold fair_oracle in Hin.
subdestruct; inv Hin; inv H; eauto.
+ eapply valid_fair; eauto.
- unfold LogReplay.get_free_qlock_oracle_pool.
unfold LogReplay.get_free_qlock_oracle; simpl.
intros. rewrite ZMap.gi.
specialize (fair_free´ i0 l); eauto. intros Hfree.
destruct Hfree.
+ rewrite H. trivial.
+ destruct H as (c & Hc & HV). destruct HV as [HV´ | [HV´ | HV´]]; rewrite HV´.
× eapply get_free_GET_NOW; eauto.
× eapply get_free_HOLD_LOCK; eauto.
× simpl.
rewrite ZMap.gi in Hfrom.
pose proof Hget as Hget´. unfold get_free_qlock in Hget´.
unfold get_free_qlock. intros.
destruct Hincr as (prefix & Hprefix).
destruct prefix.
{
simpl in ×. inv Hprefix. simpl in ×.
subdestruct; inv Hcal.
- eapply fair_free in Hdestruct; eauto.
destruct Hdestruct; subst.
+ rewrite H. trivial.
+ destruct H as (_ & (q´ & Heq)); subst. inv Heq. elim Hc; trivial.
- eapply fair_free in Hdestruct; eauto.
destruct Hdestruct; subst.
+ rewrite H. trivial.
+ destruct H as (_ & (q´ & Heq)); subst. inv Heq. elim Hc; trivial.
}
{
simpl in Hprefix. inv Hprefix. unfold get_free_qlock in ×.
exploit Hget; eauto.
}
- unfold LogReplay.valid_multi_oracle_pool_H.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H1.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H1.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H1.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H1.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold GlobalOracleProp.valid_AT_oracle_pool.
unfold GlobalOracleProp.valid_AT_oracle, GlobalOracleProp.valid_AT_log; simpl.
intros. rewrite ZMap.gi in H0. simpl in H0. eauto.
- unfold LogReplay.valid_AT_oracle_pool_H.
unfold LogReplay.valid_AT_oracle_H, LogReplay.valid_AT_log_H; simpl.
intros. rewrite ZMap.gi. simpl. eauto.
- unfold LogReplay.valid_AT_oracle_pool_H.
unfold LogReplay.valid_AT_oracle_H, LogReplay.valid_AT_log_H; simpl.
intros. rewrite ZMap.gi. simpl. eauto.
- unfold GlobalOracleProp.valid_TCB_oracle_pool.
unfold GlobalOracleProp.valid_TCB_oracle, GlobalOracleProp.valid_TCB_log; simpl.
intros. rewrite ZMap.gi in Hshared. simpl in Hshared. eauto.
- unfold LogReplay.valid_AT_oracle_pool_H.
unfold LogReplay.valid_AT_oracle_H, LogReplay.valid_AT_log_H; simpl.
intros. rewrite ZMap.gi. simpl. eauto.
- unfold GlobalOracleProp.valid_ABTCB_oracle_pool.
unfold GlobalOracleProp.valid_ABTCB_oracle, GlobalOracleProp.valid_ABTCB_log; simpl.
intros. rewrite ZMap.gi. simpl.
unfold GlobalOracleProp.valid_SABTCB_log.
split; intros; eauto.
- unfold LogReplay.valid_AT_oracle_pool_H.
unfold LogReplay.valid_AT_oracle_H, LogReplay.valid_AT_log_H; simpl.
intros. rewrite ZMap.gi. simpl. eauto.
- unfold GlobalOracleProp.valid_ABTCB_oracle_pool.
unfold GlobalOracleProp.valid_ABTCB_oracle, GlobalOracleProp.valid_ABTCB_log; simpl.
intros. rewrite ZMap.gi. simpl.
unfold GlobalOracleProp.valid_SABTCB_log.
split; intros; eauto.
- unfold BigStepLogReplay.valid_big_oracle.
unfold BigStepLogReplay.valid_big_oracle_domain, BigStepLogReplay.valid_TCB_oracle_B, BigStepLogReplay.valid_AT_oracle_B, BigStepLogReplay.valid_lock_oracle_B; simpl.
repeat split; intros; trivial. inversion Hin.
- unfold GlobalOracleProp.valid_big_oracle_cpu_id. simpl; intros.
rewrite ZMap.gi in H. inversion H.
Defined.
Instance thread_conf_instances: SingleOracle.ThreadsConfigurationOps.
constructor.
exact 1%Z.
exact 2%Z.
exact 2%Z.
exact 2%Z.
exact (cons 17%Z (cons 18%Z (cons 19%Z (cons 20%Z (cons 21%Z nil))))).
exact 2%Z.
exact (100%nat).
Defined.
Instance single_oracle_ops_instances: SingleOracle.SingleOracleOps.
constructor.
exact nil.
repeat constructor.
exact 1000%positive.
exact 1%positive.
Defined.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Existing Instance AuxSingleAbstractDataType.single_data.
Existing Instance SingleOracleImpl.s_oracle_prf.
Require Import CommonTactic.
Instance thread_configuration_instances: SingleOracle.ThreadsConfiguration.
constructor.
-
intros; induction l.
+ simpl; auto.
+ simpl.
case_eq (ObjPHBThreadReplayFunction.apply_event a (ObjPHBThreadReplayFunction.update init_shared_adt l));
intros; simpl; auto.
unfold ObjPHBThreadReplayFunction.apply_event in H.
destruct a.
destruct l0; try auto.
× subdestruct.
inversion H; simpl; auto.
× destruct (syncch); [ | inversion H].
Opaque BigStepLogReplay.B_CalLock.
Opaque BigStepLogReplay.B_CalTCB_log_real.
subdestruct.
inversion H; auto.
× destruct (ObjPHBThreadReplayFunction.prim_id_num id); try congruence.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H.
subdestruct.
inversion H; auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in H.
Opaque BigLogThreadConfigFunction.B_GetContainerUsed.
Opaque List.in_dec.
Opaque BigStepLogReplay.B_CalTCB_log_real.
subdestruct.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in H.
subdestruct.
destruct p; simpl in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in Hdestruct7.
simpl in ×.
subdestruct.
inversion Hdestruct7.
subst.
inversion H; simpl.
auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; auto.
inversion H; auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct choice; simpl; try (inversion H; fail).
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; auto.
destruct p; simpl; auto.
inversion H.
inversion H.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; auto.
destruct p; simpl; auto.
inversion H; auto.
inversion H; auto.
inversion H; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
inversion H; simpl; auto.
inversion H; simpl; auto.
× inversion H.
simpl in *; auto.
-
simpl; auto.
-
simpl.
unfold init_real_cidpool.
replace ((8 - 1)%Z) with 7%Z; try omega.
simpl.
rewrite ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gss; auto.
-
simpl; auto.
-
simpl.
omega.
-
simpl.
auto.
-
simpl.
unfold init_real_cidpool.
replace ((8 - 1)%Z) with 7%Z; try omega.
simpl.
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gss; auto.
-
intros.
simpl.
simpl in H.
destruct H; [right; simpl; auto | ].
left.
try omega.
-
intros; induction l.
+ simpl; auto.
+ Opaque SingleOracle.full_thread_list.
simpl.
case_eq (ObjPHBThreadReplayFunction.apply_event a (ObjPHBThreadReplayFunction.update init_shared_adt l));
intros; simpl; auto.
unfold ObjPHBThreadReplayFunction.apply_event in H.
destruct a.
destruct l0; try auto.
× subdestruct.
inversion H.
simpl.
rewrite Maps.ZMap.gss.
unfold ObjPHBThreadReplayFunction.z_check in Hdestruct10.
revert Hdestruct10.
clear.
simpl in *; intros.
unfold Coqlib.proj_sumbool in Hdestruct10.
subdestruct.
auto.
× destruct (syncch); [ | inversion H].
Opaque BigStepLogReplay.B_CalLock.
Opaque BigStepLogReplay.B_CalTCB_log_real.
subdestruct.
inversion H.
simpl.
rewrite Maps.ZMap.gss.
unfold ObjPHBThreadReplayFunction.z_check in Hdestruct13.
revert Hdestruct13.
clear.
simpl in *; intros.
unfold Coqlib.proj_sumbool in Hdestruct13.
subdestruct.
auto.
× destruct (ObjPHBThreadReplayFunction.prim_id_num id); try congruence.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H.
subdestruct.
inversion H; auto.
simpl.
rewrite Maps.ZMap.gss.
Transparent SingleOracle.full_thread_list.
simpl; auto.
Opaque SingleOracle.full_thread_list.
unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in H.
Opaque BigLogThreadConfigFunction.B_GetContainerUsed.
Opaque List.in_dec.
Opaque BigStepLogReplay.B_CalTCB_log_real.
subdestruct.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in H.
subdestruct.
destruct p; simpl in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in Hdestruct7.
simpl in ×.
subdestruct.
inversion Hdestruct7.
subst.
inversion H; simpl.
auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; auto.
inversion H; auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct choice; simpl; try (inversion H; fail).
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; auto.
destruct p; simpl; auto.
inversion H.
inversion H.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; auto.
destruct p; simpl; auto.
inversion H; auto.
inversion H; auto.
inversion H; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
inversion H; simpl; auto.
inversion H; simpl; auto.
× inversion H.
simpl in *; auto.
-
Transparent SingleOracle.full_thread_list.
unfold SingleOracle.full_thread_list.
simpl.
constructor.
intro contra.
simpl in contra.
destruct contra; try omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
Defined.
Instance single_oracle_basic_prop_instances: SingleOracleImpl.SingleOracleBasicProp.
constructor.
-
simpl; auto.
-
simpl; auto.
-
simpl; intros; auto.
-
simpl; intros.
elim H.
auto.
Defined.
Existing Instance SingleOracleImpl.s_config.
Definition certikos_instance : Errors.res LAsm.module
:= (@certikos waittime_instances
oracle_ops0_instances
oracle_ops1_instances
oracle_ops2_instances
oracle_ops3_instances
oracle_ops4_instances
oracle_ops5_instances
oracle_ops6_instances
oracle_ops_instances
big_ops_instances
multi_oracle_prop_instances
single_oracle_ops_instances
thread_conf_instances
thread_configuration_instances
single_oracle_basic_prop_instances).
Require Import Maps.
Require Import Coqlib.
Require Import GlobalOracleProp.
Require Import LogReplay.
Require Import ZArith.
Require Import Omega.
Instance waittime_instances: WaitTime.
econstructor. instantiate (1:= 1%nat). omega.
Defined.
Require Import AuxStateDataType.
Require Import Constant.
Definition fair_oracle (cid: Z) (l: MultiLog) :=
match Q_CalLock l with
| Some (self_c, O, b, c :: q, tq) ⇒
if zeq c cid then nil
else if zle_lt 0 c TOTAL_CPU then
match b with
| LEMPTY ⇒ (TEVENT c (TTICKET (GET_NOW))) :: nil
| LGET ⇒ (TEVENT c (TTICKET HOLD_LOCK)) :: nil
| LHOLD ⇒ (TEVENT c (TTICKET INC_NOW)) :: nil
end
else nil
| _ ⇒ nil
end.
Instance oracle_ops0_instances: MultiOracleOps0 :=
{
multi_oracle_init0:= ZMap.init fair_oracle
}.
Instance oracle_ops1_instances: GlobalOracleProp.MultiOracleOps1 :=
{
multi_oracle_init1:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops2_instances: GlobalOracleProp.MultiOracleOps2 :=
{
multi_oracle_init2:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops3_instances: GlobalOracleProp.MultiOracleOps3 :=
{
multi_oracle_init3:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops4_instances: GlobalOracleProp.MultiOracleOps4 :=
{
multi_oracle_init4:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops5_instances: GlobalOracleProp.MultiOracleOps5 :=
{
multi_oracle_init5:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops6_instances: GlobalOracleProp.MultiOracleOps6 :=
{
multi_oracle_init6:= ZMap.init (fun _ _ ⇒ nil);
multi_oracle_init7:= ZMap.init (fun _ _ ⇒ nil);
multi_oracle_init8:= ZMap.init (fun _ _ ⇒ nil)
}.
Instance oracle_ops_instances: GlobalOracle.MultiOracleOps.
econstructor.
instantiate (1 := 1%Z). omega.
instantiate (1 := 2%Z). omega.
constructor.
Defined.
Instance big_ops_instances: BigStepGlobalOracle.BigOracleOps.
repeat constructor.
Defined.
Require Import CommonTactic.
Transparent Q_CalLock.
Lemma nil_other:
∀ l self_c other_c b tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, nil, tq)),
other_c ≠ O.
Proof.
induction l; simpl; intros.
- inv Hcal. omega.
- destruct a. subdestruct; contra_inv; inv Hcal; try omega.
Qed.
Lemma head_other:
∀ l c self_c other_c b q tq
(Hlast : match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end)
(Hcal : Q_CalLock l = Some (self_c, other_c, b, c :: q, tq)),
other_c ≠ O.
Proof.
intros. destruct l; simpl in Hcal.
- inv Hcal.
- destruct m; subst. subdestruct; contra_inv; inversion Hcal; try omega.
subst.
eapply nil_other; eauto.
Qed.
Lemma cpu_range:
∀ l self_c other_c b q tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hin´: ∀ i1 e1, In (TEVENT i1 e1) l → 0 ≤ i1 < 8),
(∀ c, In c q → 0 ≤ c < 8).
Proof.
induction l; simpl; intros.
- inv Hcal. inv H.
- destruct a. subdestruct; contra_inv; inv Hcal; try omega.
+ inv H. eapply Hin´. left. trivial. inv H0.
+ inv H; [eapply Hin´; eauto | eapply IHl; eauto; right; trivial].
+ eapply IHl; eauto; right; trivial.
+ eapply IHl; eauto; right; trivial.
+ eapply IHl; eauto; right; trivial.
+ eapply IHl; eauto; right; trivial.
+ rewrite app_comm_cons in H.
eapply in_app_or in H.
inv H.
× eapply IHl; eauto; right; trivial.
× inv H0. eapply Hin´; eauto. inv H.
+ eapply IHl; eauto; right; trivial.
Qed.
Lemma other_zero_head:
∀ l self_c h q tq
(Hcal: Q_CalLock l = Some (self_c, 0%nat, h, q, tq)),
∃ z q´ t tq´, q = z :: q´ ∧ tq = t :: tq´.
Proof.
destruct l; simpl; intros. inv Hcal.
subdestruct; inv Hcal; eauto 20.
Qed.
Lemma valid_fair:
∀ l c r
(Hin : valid_qlock l)
(Hin´: ∀ (i1 : Z) (e1 : MultiOracleEventUnit),
In (TEVENT i1 e1) l → 0 ≤ i1 < 8)
(Hlast : match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end),
∃
(self_c other_c : nat) (b : head_status) (q : list Z)
(tq : list nat),
Q_CalLock (ZMap.get r (ZMap.init fair_oracle) c l ++ l) =
Some (self_c, other_c, b, q, tq) ∧ other_c ≠ 0%nat.
Proof.
intros. unfold LogReplay.valid_qlock in Hin. destruct Hin as (self_c & other_c & b & q & tq & Hcal).
rewrite ZMap.gi. unfold fair_oracle. rewrite Hcal.
destruct other_c.
× exploit other_zero_head; eauto.
intros (z & q´ & t & tq´ & ? & ? ); subst.
destruct (zeq z c).
{
subst. simpl; intros.
eapply head_other in Hcal; eauto. elim Hcal. trivial.
}
exploit cpu_range; eauto.
{ left. eauto. }
intros Hz.
rewrite zle_lt_true; trivial. destruct b; simpl; rewrite Hcal.
{
simpl. rewrite zeq_true.
repeat esplit; eauto.
}
{
simpl. rewrite zeq_true.
repeat esplit; eauto.
}
{
simpl. rewrite zeq_true.
repeat esplit; eauto.
}
× repeat esplit; eauto.
Qed.
Lemma get_free_weak:
∀ e l
(Hfree : get_free_qlock (e:: l)),
get_free_qlock l.
Proof.
unfold get_free_qlock. intros.
destruct Hincr as (prefix & Hprefix).
destruct prefix.
- simpl in Hprefix. inv Hprefix. eapply Hfree; eauto. ∃ (e::nil).
simpl; trivial.
- inv Hprefix. eapply Hfree; eauto. ∃ (e::m::prefix). trivial.
Qed.
Lemma fair_case:
∀ i l,
let l´ := fair_oracle i l in
∀ c e, ¬ In (TEVENT c (TSHARED e)) l´.
Proof.
unfold fair_oracle. intros. intro HF.
destruct (Q_CalLock l) eqn:Hcal; contra_inv.
- destruct p as ((((self_c & other_c) & h) & q) & tq).
destruct other_c; [| inv HF].
destruct q. inv HF.
destruct (zeq z i). inv HF.
destruct (zle_lt 0 z 8); [|inv HF].
destruct h; inv HF; try inv H.
- inv HF.
Qed.
Lemma fair_free:
∀ l self_c other_c h q tq i
(Hfrom: ∀ i1 e1,
In (TEVENT i1 e1) l →
i1 ≠ i →
∃ l0, In (TEVENT i1 e1) (fair_oracle i l0))
(Hcal: Q_CalLock l = Some (self_c, other_c, h, q, tq))
(Hfree: get_free_qlock l),
CalValidBit l = Some FreeToPull ∨ (h = LHOLD ∧ ∃ q´, q = i :: q´).
Proof.
induction l; simpl; intros; auto.
destruct a.
destruct (Q_CalLock l) eqn:Hcal´; contra_inv.
destruct p as ((((self_c´ & other_c´) & h´) & q´) & tq´).
subdestruct; inv Hcal.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv H.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv H.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq. unfold get_free_qlock in Hfree.
specialize (Hfree LEMPTY O (S O) q´ tq (TEVENT i (TTICKET INC_NOW) :: l)).
exploit Hfree; eauto.
{
∃ nil. trivial.
}
simpl. rewrite Hcal´. rewrite zeq_true. trivial.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
destruct (zeq z i); subst.
{
right. split; eauto.
}
{
left. exploit Hfrom; eauto.
intros (l2 & HIn).
exploit fair_case; eauto. intros HF; inv HF.
}
× inv Heq. right. split; eauto.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq. right. split; eauto.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq. right. split; eauto.
+ exploit IHl; eauto. eapply get_free_weak; eauto.
intros HV. destruct HV as [HV | (? & (q´ & Heq))]; subst.
× rewrite HV; auto.
× inv Heq. right. split; eauto.
Qed.
Lemma fair_free´:
∀ i l,
let l´ := fair_oracle i l in
l´ = nil ∨ ∃ c, c ≠ i ∧
(l´ = ((TEVENT c (TTICKET (GET_NOW))) :: nil)
∨ l´ = ((TEVENT c (TTICKET HOLD_LOCK)) :: nil)
∨ (l´ = ((TEVENT c (TTICKET INC_NOW)) :: nil))).
Proof.
unfold fair_oracle. intros.
destruct (Q_CalLock l) eqn:Hcal; [|left;trivial].
destruct p as ((((self_c & other_c) & h) & q) & tq).
destruct other_c; [|left; trivial].
destruct q. left; trivial.
destruct (zeq z i). left; trivial.
destruct (zle_lt 0 z 8); [|left; trivial].
right. ∃ z. split; trivial.
destruct h.
+ left; trivial.
+ right; left. trivial.
+ right. right. trivial.
Qed.
Require Import MQTicketLockOp.
Instance multi_oracle_prop_instances: GlobalOracleProp.MultiOracleProp.
constructor.
- unfold LogReplay.valid_multi_oracle_pool.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_queue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. unfold fair_oracle in Hin.
subdestruct; inv Hin; inv H; eauto.
+ eapply valid_fair; eauto.
- unfold LogReplay.get_free_qlock_oracle_pool.
unfold LogReplay.get_free_qlock_oracle; simpl.
intros. rewrite ZMap.gi.
specialize (fair_free´ i0 l); eauto. intros Hfree.
destruct Hfree.
+ rewrite H. trivial.
+ destruct H as (c & Hc & HV). destruct HV as [HV´ | [HV´ | HV´]]; rewrite HV´.
× eapply get_free_GET_NOW; eauto.
× eapply get_free_HOLD_LOCK; eauto.
× simpl.
rewrite ZMap.gi in Hfrom.
pose proof Hget as Hget´. unfold get_free_qlock in Hget´.
unfold get_free_qlock. intros.
destruct Hincr as (prefix & Hprefix).
destruct prefix.
{
simpl in ×. inv Hprefix. simpl in ×.
subdestruct; inv Hcal.
- eapply fair_free in Hdestruct; eauto.
destruct Hdestruct; subst.
+ rewrite H. trivial.
+ destruct H as (_ & (q´ & Heq)); subst. inv Heq. elim Hc; trivial.
- eapply fair_free in Hdestruct; eauto.
destruct Hdestruct; subst.
+ rewrite H. trivial.
+ destruct H as (_ & (q´ & Heq)); subst. inv Heq. elim Hc; trivial.
}
{
simpl in Hprefix. inv Hprefix. unfold get_free_qlock in ×.
exploit Hget; eauto.
}
- unfold LogReplay.valid_multi_oracle_pool_H.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H1.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H1.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H1.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold LogReplay.valid_multi_oracle_pool_H1.
unfold LogReplay.valid_multi_oracle_domain, LogReplay.valid_multi_oracle_hqueue; simpl.
split; intros.
+ rewrite ZMap.gi in Hin. inversion Hin.
+ unfold LogReplay.valid_hlock in Hin. destruct Hin as (self_c & b & q & Hcal).
∃ self_c, b, q.
rewrite ZMap.gi. simpl. trivial.
- unfold GlobalOracleProp.valid_AT_oracle_pool.
unfold GlobalOracleProp.valid_AT_oracle, GlobalOracleProp.valid_AT_log; simpl.
intros. rewrite ZMap.gi in H0. simpl in H0. eauto.
- unfold LogReplay.valid_AT_oracle_pool_H.
unfold LogReplay.valid_AT_oracle_H, LogReplay.valid_AT_log_H; simpl.
intros. rewrite ZMap.gi. simpl. eauto.
- unfold LogReplay.valid_AT_oracle_pool_H.
unfold LogReplay.valid_AT_oracle_H, LogReplay.valid_AT_log_H; simpl.
intros. rewrite ZMap.gi. simpl. eauto.
- unfold GlobalOracleProp.valid_TCB_oracle_pool.
unfold GlobalOracleProp.valid_TCB_oracle, GlobalOracleProp.valid_TCB_log; simpl.
intros. rewrite ZMap.gi in Hshared. simpl in Hshared. eauto.
- unfold LogReplay.valid_AT_oracle_pool_H.
unfold LogReplay.valid_AT_oracle_H, LogReplay.valid_AT_log_H; simpl.
intros. rewrite ZMap.gi. simpl. eauto.
- unfold GlobalOracleProp.valid_ABTCB_oracle_pool.
unfold GlobalOracleProp.valid_ABTCB_oracle, GlobalOracleProp.valid_ABTCB_log; simpl.
intros. rewrite ZMap.gi. simpl.
unfold GlobalOracleProp.valid_SABTCB_log.
split; intros; eauto.
- unfold LogReplay.valid_AT_oracle_pool_H.
unfold LogReplay.valid_AT_oracle_H, LogReplay.valid_AT_log_H; simpl.
intros. rewrite ZMap.gi. simpl. eauto.
- unfold GlobalOracleProp.valid_ABTCB_oracle_pool.
unfold GlobalOracleProp.valid_ABTCB_oracle, GlobalOracleProp.valid_ABTCB_log; simpl.
intros. rewrite ZMap.gi. simpl.
unfold GlobalOracleProp.valid_SABTCB_log.
split; intros; eauto.
- unfold BigStepLogReplay.valid_big_oracle.
unfold BigStepLogReplay.valid_big_oracle_domain, BigStepLogReplay.valid_TCB_oracle_B, BigStepLogReplay.valid_AT_oracle_B, BigStepLogReplay.valid_lock_oracle_B; simpl.
repeat split; intros; trivial. inversion Hin.
- unfold GlobalOracleProp.valid_big_oracle_cpu_id. simpl; intros.
rewrite ZMap.gi in H. inversion H.
Defined.
Instance thread_conf_instances: SingleOracle.ThreadsConfigurationOps.
constructor.
exact 1%Z.
exact 2%Z.
exact 2%Z.
exact 2%Z.
exact (cons 17%Z (cons 18%Z (cons 19%Z (cons 20%Z (cons 21%Z nil))))).
exact 2%Z.
exact (100%nat).
Defined.
Instance single_oracle_ops_instances: SingleOracle.SingleOracleOps.
constructor.
exact nil.
repeat constructor.
exact 1000%positive.
exact 1%positive.
Defined.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Existing Instance AuxSingleAbstractDataType.single_data.
Existing Instance SingleOracleImpl.s_oracle_prf.
Require Import CommonTactic.
Instance thread_configuration_instances: SingleOracle.ThreadsConfiguration.
constructor.
-
intros; induction l.
+ simpl; auto.
+ simpl.
case_eq (ObjPHBThreadReplayFunction.apply_event a (ObjPHBThreadReplayFunction.update init_shared_adt l));
intros; simpl; auto.
unfold ObjPHBThreadReplayFunction.apply_event in H.
destruct a.
destruct l0; try auto.
× subdestruct.
inversion H; simpl; auto.
× destruct (syncch); [ | inversion H].
Opaque BigStepLogReplay.B_CalLock.
Opaque BigStepLogReplay.B_CalTCB_log_real.
subdestruct.
inversion H; auto.
× destruct (ObjPHBThreadReplayFunction.prim_id_num id); try congruence.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H.
subdestruct.
inversion H; auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in H.
Opaque BigLogThreadConfigFunction.B_GetContainerUsed.
Opaque List.in_dec.
Opaque BigStepLogReplay.B_CalTCB_log_real.
subdestruct.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in H.
subdestruct.
destruct p; simpl in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in Hdestruct7.
simpl in ×.
subdestruct.
inversion Hdestruct7.
subst.
inversion H; simpl.
auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; auto.
inversion H; auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct choice; simpl; try (inversion H; fail).
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; auto.
destruct p; simpl; auto.
inversion H.
inversion H.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; auto.
destruct p; simpl; auto.
inversion H; auto.
inversion H; auto.
inversion H; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
inversion H; simpl; auto.
inversion H; simpl; auto.
× inversion H.
simpl in *; auto.
-
simpl; auto.
-
simpl.
unfold init_real_cidpool.
replace ((8 - 1)%Z) with 7%Z; try omega.
simpl.
rewrite ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gss; auto.
-
simpl; auto.
-
simpl.
omega.
-
simpl.
auto.
-
simpl.
unfold init_real_cidpool.
replace ((8 - 1)%Z) with 7%Z; try omega.
simpl.
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gso; [ | intro contra; inversion contra].
rewrite Maps.ZMap.gss; auto.
-
intros.
simpl.
simpl in H.
destruct H; [right; simpl; auto | ].
left.
try omega.
-
intros; induction l.
+ simpl; auto.
+ Opaque SingleOracle.full_thread_list.
simpl.
case_eq (ObjPHBThreadReplayFunction.apply_event a (ObjPHBThreadReplayFunction.update init_shared_adt l));
intros; simpl; auto.
unfold ObjPHBThreadReplayFunction.apply_event in H.
destruct a.
destruct l0; try auto.
× subdestruct.
inversion H.
simpl.
rewrite Maps.ZMap.gss.
unfold ObjPHBThreadReplayFunction.z_check in Hdestruct10.
revert Hdestruct10.
clear.
simpl in *; intros.
unfold Coqlib.proj_sumbool in Hdestruct10.
subdestruct.
auto.
× destruct (syncch); [ | inversion H].
Opaque BigStepLogReplay.B_CalLock.
Opaque BigStepLogReplay.B_CalTCB_log_real.
subdestruct.
inversion H.
simpl.
rewrite Maps.ZMap.gss.
unfold ObjPHBThreadReplayFunction.z_check in Hdestruct13.
revert Hdestruct13.
clear.
simpl in *; intros.
unfold Coqlib.proj_sumbool in Hdestruct13.
subdestruct.
auto.
× destruct (ObjPHBThreadReplayFunction.prim_id_num id); try congruence.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H.
subdestruct.
inversion H; auto.
simpl.
rewrite Maps.ZMap.gss.
Transparent SingleOracle.full_thread_list.
simpl; auto.
Opaque SingleOracle.full_thread_list.
unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in H.
Opaque BigLogThreadConfigFunction.B_GetContainerUsed.
Opaque List.in_dec.
Opaque BigStepLogReplay.B_CalTCB_log_real.
subdestruct.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; auto.
destruct p; simpl; try (inversion H; fail).
destruct p; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in H.
subdestruct.
destruct p; simpl in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in Hdestruct7.
simpl in ×.
subdestruct.
inversion Hdestruct7.
subst.
inversion H; simpl.
auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; auto.
inversion H; auto.
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct l0; simpl; try (inversion H; fail).
destruct args; simpl; try (inversion H; fail).
destruct choice; simpl; try (inversion H; fail).
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; auto.
destruct p; simpl; auto.
inversion H.
inversion H.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
destruct p; simpl; auto.
destruct p; simpl; auto.
inversion H; auto.
inversion H; auto.
inversion H; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; auto.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
inversion H; simpl; auto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H.
subdestruct.
inversion H; simpl; auto.
inversion H; simpl; auto.
inversion H; simpl; auto.
× inversion H.
simpl in *; auto.
-
Transparent SingleOracle.full_thread_list.
unfold SingleOracle.full_thread_list.
simpl.
constructor.
intro contra.
simpl in contra.
destruct contra; try omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
intro contra.
simpl in contra; inv contra; omega.
constructor.
Defined.
Instance single_oracle_basic_prop_instances: SingleOracleImpl.SingleOracleBasicProp.
constructor.
-
simpl; auto.
-
simpl; auto.
-
simpl; intros; auto.
-
simpl; intros.
elim H.
auto.
Defined.
Existing Instance SingleOracleImpl.s_config.
Definition certikos_instance : Errors.res LAsm.module
:= (@certikos waittime_instances
oracle_ops0_instances
oracle_ops1_instances
oracle_ops2_instances
oracle_ops3_instances
oracle_ops4_instances
oracle_ops5_instances
oracle_ops6_instances
oracle_ops_instances
big_ops_instances
multi_oracle_prop_instances
single_oracle_ops_instances
thread_conf_instances
thread_configuration_instances
single_oracle_basic_prop_instances).