Library mcertikos.multithread.phbthread.ObjPHBThreadDEV
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Integers.
Require Import Values.
Require Import ASTExtra.
Require Import Constant.
Require Import Constant.
Require Import GlobIdent.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import RealParams.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import ObjInterruptDriver.
Require Import ObjConsole.
Require Import OracleInstances.
Require Import ObjSerialDriver.
Require Import ObjVMMDef.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import AuxSingleAbstractDataType.
Require Import ObjPHBFlatMem.
Require Import AlgebraicMem.
Require Import GlobalOracleProp.
Require Import SingleConfiguration.
Require Import BigLogThreadConfigFunction.
Section PHBSPECSDev.
Context `{real_param_ops : RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{threads_conf_ops: ThreadsConfigurationOps}.
Section SINGLE_SPECS_DEV.
Function single_cli_spec (d: PData): option PData :=
if zeq (ZMap.get (CPU_ID (fst d)) (cid (fst d))) dev_handling_cid then
if init (fst d) then Some (fst d, (snd d) {pv_intr_flag : false}) else None else None.
Function single_sti_spec (d: PData): option PData :=
if zeq (ZMap.get (CPU_ID (fst d)) (cid (fst d))) dev_handling_cid then
if init (fst d) then Some (fst d, (snd d) {pv_intr_flag : true}) else None else None.
Notation CONS_BUFFER_MAX_CHARS := (CONS_BUFFER_SIZE - 1).
Function single_cons_intr_aux (abd: PData): option PData :=
match (ikern (snd abd), ihost (snd abd), init (fst abd), in_intr (snd abd)) with
| (true, true, true, true) ⇒
if zeq 1 (serial_exists (drv_serial (snd abd)))
then
match com1 (snd abd) with
| mkDevData
(mkSerialState _ true true true nil rxbuf false _ _ _ _ _ _) lrx _ _ ⇒
match SerialEnv (lrx - 1) with
| SerialRecv str ⇒
if list_eq_dec Z.eq_dec str rxbuf then
if zle
(Zlength ((snd abd).(console).(cons_buf) ++ rxbuf)) CONS_BUFFER_MAX_CHARS
then Some (fst abd, (snd abd)
{pv_console / cons_buf: (cons_buf (console (snd abd))) ++ rxbuf}
{pv_com1 / l1: (lrx + Zlength rxbuf × 2 + 1)}
{pv_com1 / s / RxBuf: nil}
{pv_com1 / s / SerialIrq: false})
else Some (fst abd, (snd abd)
{pv_console / cons_buf: skipn
(Z.to_nat( Zlength ((cons_buf (console (snd abd))) ++ rxbuf)
- CONS_BUFFER_MAX_CHARS))
((cons_buf (console (snd abd))) ++ rxbuf)}
{pv_console / rpos: ((rpos (console (snd abd))) + Zlength(cons_buf (console (snd abd))
++ rxbuf) + 1)
mod CONSOLE_BUFFER_SIZE}
{pv_com1 / l1: (lrx + Zlength rxbuf × 2 + 1)}
{pv_com1 / s /RxBuf: nil}
{pv_com1 / s /SerialIrq: false})
else None
| _ ⇒ None
end
| _ ⇒ None
end
else
None
| _ ⇒ None
end.
Notation SERIAL_HW_BUF_SIZE := 12%nat.
Function single_serial_trans_env (e: SerialEvent) (s: SerialState): SerialState :=
match s with
| mkSerialState base on irq rxint txbuf rxbuf
dlab baudrate databits
stopbits parity fifo modem ⇒
match e with
| SerialPlugin ⇒ s {SerialOn: true}
| SerialRecv str ⇒ let s´ := s {RxBuf:
skipn (length (rxbuf ++ str) - SERIAL_HW_BUF_SIZE)
(rxbuf ++ str)
} in if rxint then s´ {SerialIrq: true} else s´
| SerialSendComplete ⇒ s {TxBuf: nil}
| _ ⇒ s
end
end.
Function single_serial_intr (d: SerialData): SerialData :=
d {s: single_serial_trans_env (SerialEnv d.(l1)) d.(s)}
{l2: d.(l1) + 1}.
Fixpoint single_serial_intr_disable (n: nat) (masked: bool) (abd: PData) {struct n}
: option PData :=
match n with
| O ⇒ Some abd
| S n´ ⇒
let d0 := (snd abd) {pv_com1: single_serial_intr (com1 (snd abd))} in
if SerialIrq (s (com1 d0)) then
if masked then
single_serial_intr_disable n´ true ((fst abd), d0)
else
match single_cons_intr_aux (fst abd, d0) with
| Some d1 ⇒ single_serial_intr_disable n´ false d1
| None ⇒ None
end
else
Some abd
end.
Function single_serial_intr_disable_spec (adt: PData): option PData :=
if zeq (ZMap.get (CPU_ID (fst adt)) (cid (fst adt))) dev_handling_cid then
match (ikern (snd adt), ihost (snd adt), init (fst adt), intr_flag (snd adt), in_intr (snd adt)) with
| (true, true, true, true, false) ⇒
let masked :=
match nth_error (IoApicIrqs (s (ioapic (snd adt)))) 4 with
| value v ⇒
match nth_error (IoApicEnables (s (ioapic (snd adt)))) 4 with
| value true ⇒
if intr_flag (snd adt) then false
else true
| _ ⇒ true
end
| error ⇒ true
end
in
match single_serial_intr_disable INTR_DISABLE_REC_MAX masked (fst adt, (snd adt) {pv_in_intr: true}) with
| Some d´ ⇒ Some (fst d´, (snd d´) {pv_in_intr: false} {pv_ioapic / s / IoApicEnables [(Z.to_nat 4)]: false})
| None ⇒ None
end
| _ ⇒ None
end
else None.
Fixpoint single_serial_intr_enable (n: nat) (abd: PData) {struct n} : option PData :=
match n with
| O ⇒ Some abd
| S n´ ⇒
if SerialIrq (s (com1 (snd abd))) then
match single_cons_intr_aux abd with
| Some d1 ⇒ single_serial_intr_enable n´ d1
| None ⇒ None
end
else
Some abd
end.
Function single_serial_intr_enable_spec (abd: PData): option PData :=
if zeq (ZMap.get (CPU_ID (fst abd)) (cid (fst abd))) dev_handling_cid then
match (ikern (snd abd), ihost (snd abd), init (fst abd), intr_flag (snd abd), in_intr (snd abd)) with
| (true, true, true, true, false) ⇒
match nth_error (IoApicIrqs (s (ioapic (snd abd)))) 4 with
| value v ⇒
match nth_error (IoApicEnables (s (ioapic (snd abd)))) 4 with
| value true ⇒
match single_serial_intr_enable INTR_ENABLE_REC_MAX (fst abd, (snd abd) {pv_in_intr: true}) with
| Some abd´ ⇒ Some (fst abd´, (snd abd´) {pv_in_intr: false} {pv_ioapic / s / IoApicEnables [(Z.to_nat 4)]: true})
| None ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Notation CHAR_CR := 13.
Notation CHAR_LF := 10.
Function single_serial_putc_spec (c: Z) (d: PData): option PData :=
if zeq (ZMap.get (CPU_ID (fst d)) (cid (fst d))) dev_handling_cid then
match (ikern (snd d), init (fst d), ihost (snd d)) with
| (true, true, true) ⇒
if zeq 1 (serial_exists (drv_serial (snd d)))
then
match (com1 (snd d)) with
| mkDevData
(mkSerialState _ true _ _ txbuf nil false _ _ _ _ _ _) _ ltx _ ⇒
match txbuf with
| nil ⇒
if Z.eq_dec c CHAR_LF
then Some (fst d, (snd d) {pv_com1: (com1 (snd d))
{s/TxBuf: CHAR_LF :: CHAR_CR :: nil}
{l2: ltx + 1}})
else Some (fst d, (snd d) {pv_com1: (com1 (snd d))
{s/TxBuf: c :: nil}
{l2: ltx + 1}})
| _ ⇒
if Z.eq_dec c CHAR_LF
then Some ((fst d), (snd d) {pv_com1: (com1 (snd d))
{s/TxBuf: CHAR_LF :: CHAR_CR :: nil}
{l2: (next_sendcomplete ltx)}})
else Some ((fst d), (snd d) {pv_com1: (com1 (snd d))
{s/TxBuf: c :: nil}
{l2: (next_sendcomplete ltx)}})
end
| _ ⇒ None
end
else
Some d
| _ ⇒ None
end
else None.
Function single_cons_buf_read_spec (abd: PData): option (PData × Z) :=
if zeq (ZMap.get (CPU_ID (fst abd)) (cid (fst abd))) dev_handling_cid then
match (ikern (snd abd), ihost (snd abd), init (fst abd)) with
| (true, true, true) ⇒
let s := console (snd abd) in
let b := cons_buf s in
let r := rpos s in
match b with
| nil ⇒ Some (abd, 0)
| c :: tl ⇒
Some (fst abd, (snd abd) {pv_console: (s {cons_buf: tl}{rpos: ((r + 1) mod CONS_BUFFER_SIZE)})}, c)
end
| _ ⇒ None
end
else None.
Function single_hostin_spec (adt: PData): option PData :=
match (init (fst adt), ikern (snd adt), ihost (snd adt)) with
| (true, true, false) ⇒ Some ((fst adt), (snd adt) {pv_ihost: true})
| _ ⇒ None
end.
Function single_hostout_spec (adt: PData): option PData :=
match (ikern (snd adt), init (fst adt), pg (fst adt), ihost (snd adt)) with
| (true, true, true, true) ⇒ Some (fst adt, (snd adt) {pv_ihost: false})
| _ ⇒ None
end.
Definition single_trap_info_get_spec (d: PData): int := fst (ti (snd d)).
Definition single_trap_info_ret_spec (d: PData): val := snd (ti (snd d)).
Function single_uctx_get_spec (i ofs: Z) (d: PData) : option Z :=
let sh_adt := fst d in
let pv_adt := snd d in
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
let cpu := CPU_ID (fst d) in
if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) i then
match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt, ipt pv_adt) with
| (true, true, true, true, true) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
if zle_lt 0 i num_proc then
if is_UCTXT_ptr ofs then
None
else
match (ZMap.get ofs (uctxt pv_adt)) with
| Vint n ⇒ Some (Int.unsigned n)
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function single_uctx_set_spec (i ofs n: Z) (d : PData) : option PData :=
let sh_adt := fst d in
let pv_adt := snd d in
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
let cpu := CPU_ID (fst d) in
if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) i then
match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt, ipt pv_adt) with
| (true, true, true, true, true) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
if zle_lt 0 i num_proc then
if is_UCTXT_ptr ofs then
None
else
let uctx´:= ZMap.set ofs (Vint (Int.repr n)) (uctxt pv_adt) in
Some (sh_adt, pv_adt {pv_uctxt: uctx´})
else None
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function single_proc_start_user_spec (d: PData) : option (PData × UContext) :=
let sh_adt := fst d in
let pv_adt := snd d in
let curid := ZMap.get (CPU_ID sh_adt) (cid sh_adt) in
let cpu := CPU_ID (fst d) in
match (ikern pv_adt, pg sh_adt, ihost pv_adt, ipt pv_adt, init sh_adt) with
| (true, true, true, true, true) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
Some ((sh_adt, pv_adt {pv_ikern: false} {pv_ipt: false} {pv_PT: curid}), (uctxt pv_adt))
else None
| _ ⇒ None
end
| _ ⇒ None
end.
primitive: save user context
Function single_proc_exit_user_spec (d : PData) (rs : UContext) : option PData :=
let sh_adt := fst d in
let pv_adt := snd d in
let curid := ZMap.get (CPU_ID sh_adt) (cid sh_adt) in
let cpu := CPU_ID (fst d) in
match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
| (true, false, true, true) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
Some (sh_adt, pv_adt {pv_ikern: true} {pv_PT: 0} {pv_ipt: true} {pv_uctxt: rs})
else None
| _ ⇒ None
end
| _ ⇒ None
end.
End SINGLE_SPECS_DEV.
End PHBSPECSDev.
let sh_adt := fst d in
let pv_adt := snd d in
let curid := ZMap.get (CPU_ID sh_adt) (cid sh_adt) in
let cpu := CPU_ID (fst d) in
match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
| (true, false, true, true) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
Some (sh_adt, pv_adt {pv_ikern: true} {pv_PT: 0} {pv_ipt: true} {pv_uctxt: rs})
else None
| _ ⇒ None
end
| _ ⇒ None
end.
End SINGLE_SPECS_DEV.
End PHBSPECSDev.