Library mcertikos.objects.cpulocaldef.GlobalOracle
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.
Notation ID_AT := 0.
Notation ID_TCB := 1.
Notation ID_SC := 2.
Notation ID_range := 3.
Definition local_lock_bound := (10 % nat).
Inductive TicketOracleEvent :=
| INC_TICKET (n: nat)
| INC_NOW
| GET_NOW
| CAS_TICKET
| SWAP_TAIL (n : nat) (is_null : bool)
| CAS_TAIL (success : bool)
| GET_NEXT
| SET_NEXT (old_tail: Z)
| GET_BUSY (busy : bool)
| SET_BUSY
| HOLD_LOCK
| WAIT_LOCK (n: nat)
| GET_LOCK
| REL_LOCK
| TRY_LOCK.
Inductive head_status:=
| LEMPTY | LGET | LHOLD.
Section CONDITION_VARIABLE.
Record FIFOBBQ :=
mkFIFOBBQ {
max: Z;
front: Z;
next: Z;
whead: ZMap.t (Z × Z);
wq: ZMap.t (list Z)
}.
Definition init_FIFOBBQ :=
mkFIFOBBQ max_resource_size 0 0 (ZMap.init (num_proc, num_proc)) (ZMap.init nil).
Inductive FIFOCV :=
| CV_Undef
| CV_Valid (cv: FIFOBBQ).
Definition FIFOCVPool := ZMap.t FIFOCV.
Inductive ID_QNode :=
| IDQ_Undef
| IDQ_Valid (prev next: Z).
Definition ID_Q := ZMap.t ID_QNode.
Definition update_max (a : FIFOBBQ) b :=
mkFIFOBBQ b (front a) (next a) (whead a) (wq a).
Definition update_front (a : FIFOBBQ) b :=
mkFIFOBBQ (max a) b (next a) (whead a) (wq a).
Definition update_next (a : FIFOBBQ) b :=
mkFIFOBBQ (max a) (front a) b (whead a) (wq a).
Definition update_in_whead (a : FIFOBBQ) b :=
mkFIFOBBQ (max a) (front a) (next a) b (wq a).
Definition update_in_wq (a : FIFOBBQ) b :=
mkFIFOBBQ (max a) (front a) (next a) (whead a) b.
End CONDITION_VARIABLE.
Notation "a {max : b }" := (update_max a b) (at level 1).
Notation "a {front : b }" := (update_front a b) (at level 1).
Notation "a {next : b }" := (update_next a b) (at level 1).
Notation "a {whead : b }" := (update_in_whead a b) (at level 1).
Notation "a {wq : b }" := (update_in_wq a b) (at level 1).
Inductive SharedMemEvent :=
| OMEME (l: list Integers.Byte.int)
| OBUFFERE (msg : PageBuffer)
| OPULL
| OATE (a: ATable)
| OTCBE (t: TCBPool) (q: TDQueuePool)
| OABTCBE (t: AbTCBPool) (q: AbQueuePool)
| OSCE (c: SyncChanPool)
| OPALLOCE (b: Z)
| OTDSPAWN (new_id: Z)
| OTDYIELD (cur_id: Z)
| OTDSLEEP (slp_id cv_id: Z) (s: SyncChanPool)
| OTDWAKE (cv_id: Z)
| OTDWAKE_DIFF (wk_id cpu_id: Z).
Inductive MultiOracleEventUnit :=
| TTICKET (e: TicketOracleEvent)
| TSHARED (e: SharedMemEvent).
Inductive MultiOracleEvent :=
| TEVENT (i: Z) (e: MultiOracleEventUnit).
Inductive MultiOracleEventType :=
| ETICKET
| ESHARED.
Function GetMultiOracleEventType (e: MultiOracleEventUnit) :=
match e with
| TTICKET _ ⇒ ETICKET
| TSHARED _ ⇒ ESHARED
end.
Definition MultiLog := list MultiOracleEvent.
Definition MultiOracle := Z → MultiLog → MultiLog.
Definition MultiOraclePool := ZMap.t MultiOracle.
Inductive MultiLogType :=
| MultiUndef
| MultiDef (l: MultiLog).
Definition MultiLogPool := ZMap.t MultiLogType.
Definition Sleeper := ZMap.t Z.
Definition init_sleeper := ZMap.init 0.
Class WaitTime :=
{
fairness: nat;
positive_fairness: (0 < fairness)%nat
}.
Class MultiOracleOps :=
{
current_CPU_ID: Z;
current_CPU_ID_range: 0 ≤ current_CPU_ID < TOTAL_CPU;
current_curid: Z;
current_curid_range: 0 ≤ current_curid < num_proc;
sleep_waittime: nat
}.
Inductive LockStatus :=
| LockFalse
| LockOwn (b: bool).
Definition Lock := ZMap.t LockStatus.
Definition init_lock := ZMap.init LockFalse.
Fixpoint ByteList (l: list Integers.Byte.int) :=
match l with
| nil ⇒ nil
| a :: l ⇒ (Byte a) :: (ByteList l)
end.
Lemma list_forall2_bytelist_inject:
∀ l f,
list_forall2 (memval_inject f) (ByteList l) (ByteList l).
Proof.
induction l; intros.
- constructor.
- simpl. constructor. constructor.
eauto.
Qed.
Lemma list_forall2_bytelist_lessdef:
∀ l,
list_forall2 memval_lessdef (ByteList l) (ByteList l).
Proof.
induction l; intros.
- constructor.
- simpl. constructor. constructor.
eauto.
Qed.
Lemma ByteList_eq:
∀ l l´,
ByteList l = ByteList l´ →
l = l´.
Proof.
induction l; simpl; intros; trivial.
- destruct l´; trivial.
inv H.
- destruct l´; inv H.
exploit IHl; eauto.
intros →. trivial.
Qed.
Lemma list_forall2_bytelist_inject_eq:
∀ l l´ f,
list_forall2 (memval_inject f) (ByteList l) l´ →
l´ = ByteList l.
Proof.
induction l; intros.
- inv H. trivial.
- inv H. inv H2.
exploit IHl; eauto.
intros →. trivial.
Qed.
Lemma list_forall2_bytelist_lessdef_eq:
∀ l l´,
list_forall2 memval_lessdef (ByteList l) l´ →
l´ = ByteList l.
Proof.
induction l; intros.
- inv H. trivial.
- inv H. inv H2.
exploit IHl; eauto.
intros →. trivial.
Qed.
Section MULTIPROCESSOR.
Section Range.
Definition ID_AT_range := 1.
Definition ID_TCB_range := num_chan.
Definition ID_SC_range := num_chan.
Function index_range (i: Z) :=
match i with
| ID_AT ⇒ Some ID_AT_range
| ID_TCB ⇒ Some ID_TCB_range
| ID_SC ⇒ Some ID_SC_range
| _ ⇒ None
end.
Definition lock_TCB_range := ID_AT_range + ID_TCB_range.
Definition lock_range := ID_AT_range + ID_TCB_range + ID_SC_range.
Definition lock_AT_start := 0.
Definition lock_TCB_start := ID_AT_range.
Definition lock_SC_start := lock_TCB_range.
Function index_incrange (i: Z) :=
match i with
| ID_AT ⇒ Some 0
| ID_TCB ⇒ Some ID_AT_range
| ID_SC ⇒ Some lock_TCB_range
| _ ⇒ None
end.
Function index2Z (index ofs: Z) :=
match index_range index, index_incrange index with
| Some r, Some base ⇒
if zle_lt 0 ofs r then
Some (base + ofs)
else
None
| _, _ ⇒ None
end.
End Range.
Section SHARED_ID.
Section ID0.
Function Shared2ID0 (i: Z) :=
match i with
| ID_AT ⇒ Some AT_LOC
| ID_TCB ⇒ Some TCBPool_LOC
| ID_SC ⇒ Some SYNCCHPOOL_LOC
| _ ⇒ None
end.
Function CheckID0 (i: positive) :=
if peq i AT_LOC then true
else if peq i TCBPool_LOC then true
else if peq i SYNCCHPOOL_LOC then true
else false.
Lemma Shared2ID_valid0:
∀ i id,
Shared2ID0 i = Some id →
CheckID0 id = true.
Proof.
intros. functional inversion H; trivial.
Qed.
End ID0.
Section ID1.
Function Shared2ID1 (i: Z) :=
match i with
| ID_TCB ⇒ Some TCBPool_LOC
| ID_SC ⇒ Some SYNCCHPOOL_LOC
| _ ⇒ None
end.
Lemma Shared2ID1_AT:
∀ i e,
Shared2ID1 i = Some e →
e ≠ AT_LOC.
Proof.
intros. functional inversion H; red; intro HF; inv HF.
Qed.
Function CheckID1 (i: positive) :=
if peq i TCBPool_LOC then true
else if peq i SYNCCHPOOL_LOC then true
else false.
Lemma Shared2ID_valid1:
∀ i id,
Shared2ID1 i = Some id →
CheckID1 id = true.
Proof.
intros. functional inversion H; trivial.
Qed.
End ID1.
Section ID2.
Function Shared2ID2 (i: Z) :=
match i with
| ID_SC ⇒ Some SYNCCHPOOL_LOC
| _ ⇒ None
end.
Lemma Shared2ID2_neq:
∀ i e,
Shared2ID2 i = Some e →
e ≠ AT_LOC ∧ e ≠ TCBPool_LOC.
Proof.
intros. functional inversion H; split; red; intro HF; inv HF.
Qed.
Function CheckID2 (i: positive) :=
if peq i SYNCCHPOOL_LOC then true
else false.
Lemma Shared2ID_valid2:
∀ i id,
Shared2ID2 i = Some id →
CheckID2 id = true.
Proof.
intros. functional inversion H; trivial.
Qed.
End ID2.
End SHARED_ID.
End MULTIPROCESSOR.