Library mcertikos.objects.cpulocaldef.GlobalOracleProp
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Memory.
Require Import AuxLemma.
Require Import Constant.
Require Import GlobIdent.
Require Export GlobalOracle.
Require Export BigStepGlobalOracle.
Require Export BigStepLogReplay.
Require Export LogReplay.
Require Export OracleCHANRel.
Require Export OracleATRel.
Require Export OracleATHRel.
Require Export OracleABTCBRel.
Require Export OracleTCBRel.
Require Export HTicketLockOpGenDef.
Require Export CalMCSLock.
Require Export QMCSLockOpGenDef.
Require Export HMCSLockOpGenDef.
Require Export BThreadGenDef.
Require Export QThreadGenDef.
Section ORACLE1.
Definition valid_AT_log (l: MultiLog) (n: Z) :=
∀ a, GetSharedAT l = Some a →
AT_kern a n ∧ AT_usr a n.
Definition valid_AT_log_pool (l: MultiLogPool) (n: Z) :=
∃ q, ZMap.get lock_AT_start l = MultiDef q
∧ valid_AT_log q n.
Definition valid_AT_oracle (o: MultiOracle) :=
∀ q i n, valid_AT_log q n →
valid_AT_log ((o i q) ++ q) n.
Definition valid_AT_oracle_pool (o: MultiOraclePool) :=
valid_AT_oracle (ZMap.get lock_AT_start o).
Lemma valid_AT_log_pool_gso:
∀ l e q n,
valid_AT_log_pool l n →
e ≠ lock_AT_start →
valid_AT_log_pool (ZMap.set e q l) n.
Proof.
unfold valid_AT_log_pool.
intros.
rewrite ZMap.gso; auto.
Qed.
Lemma valid_AT_log_pool_gss:
∀ l o q i n,
valid_AT_log_pool l n →
valid_AT_oracle_pool o →
ZMap.get lock_AT_start l = MultiDef q →
let o´ := ZMap.get lock_AT_start o in
valid_AT_log_pool (ZMap.set lock_AT_start (MultiDef ((o´ i q) ++ q)) l) n.
Proof.
unfold valid_AT_log_pool.
unfold valid_AT_oracle_pool.
intros. rewrite ZMap.gss.
destruct H as (q0 & Heq & Hvalid).
rewrite H1 in Heq. inv Heq.
esplit. split; trivial.
eapply H0. trivial.
Qed.
Class MultiOracleOps1 :=
{
multi_oracle_init1 : MultiOraclePool
}.
End ORACLE1.
Section ORACLE2.
Class MultiOracleOps2 :=
{
multi_oracle_init2 : MultiOraclePool
}.
End ORACLE2.
Section ORACLE3.
Class MultiOracleOps3 :=
{
multi_oracle_init3 : MultiOraclePool
}.
End ORACLE3.
Section ORACLE4.
Definition valid_TCB_log l :=
∀ t tq
(Hshared: GetSharedTCB l = Some (t, tq)),
TCBCorrect_range t ∧ TDQCorrect_range tq.
Definition valid_TCB_log_pool l :=
∀ i q (Hrange: 0 ≤ i < num_chan)
(Hdef: ZMap.get (i + ID_AT_range) l = MultiDef q),
valid_TCB_log q.
Definition valid_TCB_oracle (o: MultiOracle) :=
∀ q i
(Hvalid: valid_TCB_log q),
valid_TCB_log ((o i q) ++ q).
Definition valid_TCB_oracle_pool (o: MultiOraclePool) :=
∀ i (Hrange: 0 ≤ i < num_chan),
valid_TCB_oracle (ZMap.get (i + ID_AT_range) o).
Class MultiOracleOps4 :=
{
multi_oracle_init4 : MultiOraclePool
}.
End ORACLE4.
Section ORACLE5.
Definition valid_ABTCB_log l :=
∀ t tq
(Hshared: GetSharedABTCB l = Some (t, tq)),
AbTCBCorrect_range t
∧ AbQCorrect_range tq
∧ QCount t tq
∧ InQ t tq.
Definition valid_SABTCB_log l :=
∀ t tq
(Hshared: GetSharedABTCB l = Some (t, tq)),
AbTCBStrong_range t
∧ AbQCorrect_range tq
∧ QCount t tq
∧ InQ t tq.
Definition valid_ABTCB_log_pool l :=
∀ i q (Hrange: 0 ≤ i < num_chan)
(Hdef: ZMap.get (i + ID_AT_range) l = MultiDef q),
valid_ABTCB_log q.
Definition valid_ABTCB_oracle (o: MultiOracle) :=
∀ q i,
(valid_ABTCB_log q → valid_ABTCB_log ((o i q) ++ q))
∧ (valid_SABTCB_log q → valid_SABTCB_log ((o i q) ++ q)).
Definition valid_ABTCB_oracle_pool (o: MultiOraclePool) :=
∀ i (Hrange: 0 ≤ i < num_chan),
valid_ABTCB_oracle (ZMap.get (i + ID_AT_range) o).
Class MultiOracleOps5 :=
{
multi_oracle_init5 : MultiOraclePool
}.
End ORACLE5.
Section ORACLE6.
Definition valid_big_oracle_cpu_id `{MultiOracleOps} (o: MultiOraclePool) :=
∀ l e cpu,
In (TEVENT cpu e) (ZMap.get lock_range o current_CPU_ID l) →
cpu ≠ current_CPU_ID.
Class MultiOracleOps6 :=
{
multi_oracle_init6 : MultiOraclePool;
multi_oracle_init7 : MultiOraclePool;
multi_oracle_init8 : MultiOraclePool
}.
End ORACLE6.
Class MultiOracleOps0 :=
{
multi_oracle_init0 : MultiOraclePool
}.
Class MCSOracleOps :=
{
mcs_oracle_init0 : MultiOraclePool
}.
Section With_Oracle.
Require Import RealParams.
Class MultiOracleProp
`{waittime: WaitTime}
`{oracle_ops0 : MultiOracleOps0} `{oracle_ops1 : MultiOracleOps1} `{oracle_ops2 : MultiOracleOps2}
`{oracle_ops3 : MultiOracleOps3}
`{oracle_ops4 : MultiOracleOps4}
`{oracle_ops5 : MultiOracleOps5}
`{oracle_ops6 : MultiOracleOps6}
`{oracle_ops : MultiOracleOps}
`{big_ops : BigOracleOps} :=
{
valid_ticket_oracle0: valid_multi_oracle_pool multi_oracle_init0;
get_free_qlock_oracle0: get_free_qlock_oracle_pool multi_oracle_init0;
valid_ticket_oracle1: valid_multi_oracle_pool_H multi_oracle_init1;
valid_ticket_oracle2: valid_multi_oracle_pool_H multi_oracle_init2;
valid_ticket_oracle3: valid_multi_oracle_pool_H1 multi_oracle_init3;
valid_ticket_oracle4: valid_multi_oracle_pool_H1 multi_oracle_init4;
valid_ticket_oracle5: valid_multi_oracle_pool_H1 multi_oracle_init5;
valid_ticket_oracle6: valid_multi_oracle_pool_H1 multi_oracle_init6;
valid_AT_oracle_pool2: valid_AT_oracle_pool multi_oracle_init2;
valid_AT_oracle_pool3 `{real_params_ops: RealParamsOps}: valid_AT_oracle_pool_H multi_oracle_init3;
valid_AT_oracle_pool4 `{real_params_ops: RealParamsOps}: valid_AT_oracle_pool_H multi_oracle_init4;
valid_TCB_oracle_pool4: valid_TCB_oracle_pool multi_oracle_init4;
valid_AT_oracle_pool5 `{real_params_ops: RealParamsOps}: valid_AT_oracle_pool_H multi_oracle_init5;
valid_ABTCB_oracle_pool5: valid_ABTCB_oracle_pool multi_oracle_init5;
valid_AT_oracle_pool6 `{real_params_ops: RealParamsOps}: valid_AT_oracle_pool_H multi_oracle_init6;
valid_ABTCB_oracle_pool6: valid_ABTCB_oracle_pool multi_oracle_init6;
valid_big_oracle0 `{real_params_ops: RealParamsOps}: valid_big_oracle big_oracle0;
valid_global_oracle7: valid_big_oracle_cpu_id multi_oracle_init7
}.
Class MCSOracleProp
`{waittime: WaitTime}
`{multi_oracle_ops: MultiOracleOps}
`{mcs_oracle_ops : MCSOracleOps}
`{oracle_ops1 : MultiOracleOps1}
`{big_ops : BigOracleOps} :=
{
valid_mcs_oracle1: valid_multi_oracle_pool_H multi_oracle_init1;
get_free_qslock_oracle0: get_free_qslock_oracle_pool mcs_oracle_init0;
valid_mcs_oracle0: valid_multi_oracle_pool_mcs mcs_oracle_init0;
valid_mcs_oracle11: valid_qs_oracle_pool mcs_oracle_init0;
valid_mcs_oracle12: relate_mcs_qs_oracle_pool mcs_oracle_init0
}.
End With_Oracle.
Section With_MEM_Oracle.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Class MultiOracleLink `{multi_oracle_prop : MultiOracleProp}:=
{
relateticket: relate_ticket_oracle_pool multi_oracle_init1 multi_oracle_init0;
relateat: ∀ s, relate_AT_Oracle_Pool s multi_oracle_init2 multi_oracle_init1;
relateath `{real_params_ops: RealParamsOps}: relate_ATH_Oracle_Pool multi_oracle_init3 multi_oracle_init2;
relatetcb: ∀ s, relate_TCB_Oracle_Pool s multi_oracle_init4 multi_oracle_init3;
relateabtcb: relate_ABTCB_Oracle_Pool multi_oracle_init5 multi_oracle_init4;
relatesc: ∀ s, relate_SC_Oracle_Pool s multi_oracle_init6 multi_oracle_init5;
relate_big: relate_big_small_oracle big_oracle0 multi_oracle_init7;
relate_thread: relate_Thread_Oracle_Pool multi_oracle_init7 multi_oracle_init6
}.
Class MCSOracleLink `{mcs_oracle_prop : MCSOracleProp}:=
{
relatemcs: relate_mcs_oracle_pool multi_oracle_init1 mcs_oracle_init0
}.
End With_MEM_Oracle.