Library language
This file contains the formalization of the low-level language for
implementing preemptive OS kernels and the high-level specification language
for specifying OS kernels. The low-level language is a practical subset
of C plus assembly primitives, while the high-level specification language
is a simple imperative language parametrized with abstract schedulers and
kernel operations. The implementation corresponds to Sec.3 of the paper.
The low-level language is concurrent, with multiple continuations (i.e., control stacks)
in the state, each corresponding to a task. All tasks share memory, but each has
its own local variables and local interrupt states. We also separate the program state
(including memory and variables) into two disjoint parts, one for the application
code and the other for the kernel code. The only way for client code to
access kernel states is to call system APIs, and kernel APIs cannot access
application states.
The high-level specification language provides some abstract statements to specify
the system APIs and interrupt handlers. It not only allows users to write
abstract statements to specify the functionality of kernel APIs but also configure
the abstract scheduler. Specifying details of the scheduling policies
(instead of using a more abstract non-deterministic scheduler that may pick any task)
allows us to specify and verify scheduling properties such as PIF at the high level.
Require Import include.
Require Import memdata.
Require Import memory.
Require Import val.
Set Implicit Arguments.
task idenifier
Definition tid := addrval.
Definition beq_tid (n m : tid) : bool :=
match n, m with
| (b, i), (b´, i´) => andb (beq_pos b b´) (Int.eq i i´)
end.
Definition blt_tid (n m : tid) : bool :=
match n, m with
| (b, i), (b´, i´) => if blt_pos b b´
then true
else if beq_pos b b´
then Int.lt i i´
else false
end.
Definition beq_tid (n m : tid) : bool :=
match n, m with
| (b, i), (b´, i´) => andb (beq_pos b b´) (Int.eq i i´)
end.
Definition blt_tid (n m : tid) : bool :=
match n, m with
| (b, i), (b´, i´) => if blt_pos b b´
then true
else if beq_pos b b´
then Int.lt i i´
else false
end.
the task identifier module for the range of maps
Module tidspec.
Definition A := tid.
Definition B := tid.
Definition beq : A -> A -> bool := beq_tid.
Definition blt : A -> A -> bool := blt_tid.
Lemma beq_true_eq : forall a a´ : A,
beq a a´ = true -> a = a´.
Lemma beq_false_neq : forall a a´ : A,
beq a a´ = false -> a <> a´.
Lemma eq_beq_true : forall a a´ : A,
a = a´ -> beq a a´ = true.
Lemma neq_beq_false : forall a a´ : A,
a <> a´ -> beq a a´ = false.
Lemma blt_trans : forall a a´ a´´ : A,
blt a a´ = true -> blt a´ a´´ = true -> blt a a´´ = true.
Lemma blt_irrefl : forall a : A,
blt a a = false.
Lemma blt_asym : forall a b : A,
blt a b = true -> blt b a = false.
Lemma blt_beq_dec : forall a b : A,
{blt a b = true} + {beq a b = true} + {blt b a = true}.
End tidspec.
function names
INUM represents the total number of interrupt handlers, which is configurable
interrupt identifiers
C expressions
We use 'enull' to represent the special expression which is used for initializing
a pointer with 'vnull'. Both a variable x and a integer n can be an expression.
The expression 'ederef e' is used to dereference a memory location obtained from 'e',
while 'eaddrof e' calculates and returns the memory address of 'e'. The expression
'efield e id' is used for accessing a field of a “struct” type. 'earrayelem e1 e2'
returns the value of an element of an array. 'ecast e t' cast the type of 'e' into 't'.
Inductive expr:=
| enull : expr
| evar : var -> expr
| econst32 : int32 -> expr
| eunop : uop -> expr -> expr
| ebinop : bop -> expr -> expr -> expr
| ederef : expr -> expr
| eaddrof : expr -> expr
| efield : expr -> ident -> expr
| ecast : expr -> type -> expr
| earrayelem : expr -> expr -> expr.
expression list
value list
address list
free list
type list
low-level primitives
The built-in primitive statements is defined as below, 'exint' represents the assembly code
which is used to return from interrupt handlers. 'eoi n' represents the assembly
statement that clears a bit of Interrupt Service Register(isr). 'cli' and 'sti'
are used for enable and disable the interrupt handlers respectively. 'encrit' and
'excrit' are used for enter and exit critical region respectively. Their semantics
support nested critical region in μC/OS-II, and they are implemented with the assembly
instructions like pushf, cli and popf. 'switch x' is used to do context switch, and the
variable 'x' represents the target task scheduled to. To support reasoning about nested
and multi-level interrupt handlers, we use the primitive 'checkis' to obtain the
depth of the nested interrupt handlers. In μC/OS-II, there is a global variable
“intnesting” to record the depth of the nested interrupt handlers, and context
switch could only be done when the depth is 1 (intnesting is 1). To reason about
nested interrupt handlers, instead of specifying this global variable, we introduce
an abstract stack to record the trace of the interrupt handlers, and the primitive
'checkis' is used to read the depth of the stack.
Inductive prim :=
| exint : prim
| switch : var -> prim
| eoi : int32 -> prim
| excrit : prim
| encrit : prim
| cli : prim
| sti : prim
| checkis : var -> prim .
task priority
identifier of event control block
message
the length of messages
os time
waiting list
states of tasks
Inductive tcbstats:=
| os_stat_sem: ecbid -> tcbstats
| os_stat_q: ecbid -> tcbstats
| os_stat_time: tcbstats
| os_stat_mbox: ecbid -> tcbstats
| os_stat_mutexsem: ecbid -> tcbstats.
Inductive taskstatus :=
| rdy: taskstatus
| wait : tcbstats -> int32 -> taskstatus.
Module abstcb.
Definition B : Set := ( priority * taskstatus * msg)%type.
End abstcb.
Module TcbMod := MapLib.MapFun tidspec abstcb.
Module abssem.
Definition B : Set := prod Z waitset.
End abssem.
Module SemMod := MapLib.MapFun tidspec abssem.
Module absmsgq.
Definition B : Set := prod (prod (list msg) maxlen) waitset.
End absmsgq.
Module MsgqMod := MapLib.MapFun tidspec absmsgq.
Definition owner:= option (tid * int32).
Inductive edata:=
| abssem: int32 -> edata
| absmsgq : list msg -> maxlen -> edata
| absmbox: msg -> edata
| absmutexsem: int32 -> owner -> edata.
Module absecb.
Definition B : Set := prod edata waitset.
End absecb.
Module EcbMod := MapLib.MapFun tidspec absecb.
Inductive absdataid:=
| abstcblsid : absdataid
| absecblsid: absdataid
| ostmid : absdataid
| curtid:absdataid.
Definition absdataid_eq (id1 id2:absdataid):=
match id1, id2 with
| abstcblsid, abstcblsid => true
| absecblsid,absecblsid => true
| ostmid, ostmid => true
| curtid,curtid => true
| _,_ => false
end.
Definition absdataid_lt (id1 id2:absdataid):=
match id1, id2 with
| abstcblsid, abstcblsid => false
| abstcblsid, _ => true
| absecblsid, abstcblsid => false
| absecblsid, absecblsid => false
| absecblsid, _ =>true
| ostmid, abstcblsid =>false
| ostmid, absecblsid => false
| ostmid, ostmid => false
| ostmid, _ => true
| curtid, _ => false
end.
Module absdataidspec.
Definition A := absdataid.
Definition beq := absdataid_eq.
Definition blt := absdataid_lt.
Lemma beq_true_eq : forall a a´ : A,
beq a a´ = true -> a = a´.
Lemma beq_false_neq : forall a a´ : A,
beq a a´ = false -> a <> a´.
Lemma eq_beq_true : forall a a´ : A,
a = a´ -> beq a a´ = true.
Lemma neq_beq_false : forall a a´ : A,
a <> a´ -> beq a a´ = false.
Lemma blt_trans :
forall a a´ a´´ : A,
blt a a´ = true -> blt a´ a´´ = true -> blt a a´´ = true.
Lemma blt_irrefl :
forall a : A,
blt a a = false.
Lemma blt_asym :
forall a b : A,
blt a b = true -> blt b a = false.
Lemma blt_beq_dec :
forall a b : A,
{blt a b = true} + {beq a b = true} + {blt b a = true}.
End absdataidspec.
Inductive absdata:=
| abstcblist: TcbMod.map -> absdata
| absecblist : EcbMod.map -> absdata
| ostm: ostime -> absdata
| oscurt: addrval -> absdata.
Module absdatastru.
Definition B := absdata.
End absdatastru.
Module OSAbstMod := MapLib.MapFun absdataidspec absdatastru.
Definition osabst:= OSAbstMod.map.
| os_stat_sem: ecbid -> tcbstats
| os_stat_q: ecbid -> tcbstats
| os_stat_time: tcbstats
| os_stat_mbox: ecbid -> tcbstats
| os_stat_mutexsem: ecbid -> tcbstats.
Inductive taskstatus :=
| rdy: taskstatus
| wait : tcbstats -> int32 -> taskstatus.
Module abstcb.
Definition B : Set := ( priority * taskstatus * msg)%type.
End abstcb.
Module TcbMod := MapLib.MapFun tidspec abstcb.
Module abssem.
Definition B : Set := prod Z waitset.
End abssem.
Module SemMod := MapLib.MapFun tidspec abssem.
Module absmsgq.
Definition B : Set := prod (prod (list msg) maxlen) waitset.
End absmsgq.
Module MsgqMod := MapLib.MapFun tidspec absmsgq.
Definition owner:= option (tid * int32).
Inductive edata:=
| abssem: int32 -> edata
| absmsgq : list msg -> maxlen -> edata
| absmbox: msg -> edata
| absmutexsem: int32 -> owner -> edata.
Module absecb.
Definition B : Set := prod edata waitset.
End absecb.
Module EcbMod := MapLib.MapFun tidspec absecb.
Inductive absdataid:=
| abstcblsid : absdataid
| absecblsid: absdataid
| ostmid : absdataid
| curtid:absdataid.
Definition absdataid_eq (id1 id2:absdataid):=
match id1, id2 with
| abstcblsid, abstcblsid => true
| absecblsid,absecblsid => true
| ostmid, ostmid => true
| curtid,curtid => true
| _,_ => false
end.
Definition absdataid_lt (id1 id2:absdataid):=
match id1, id2 with
| abstcblsid, abstcblsid => false
| abstcblsid, _ => true
| absecblsid, abstcblsid => false
| absecblsid, absecblsid => false
| absecblsid, _ =>true
| ostmid, abstcblsid =>false
| ostmid, absecblsid => false
| ostmid, ostmid => false
| ostmid, _ => true
| curtid, _ => false
end.
Module absdataidspec.
Definition A := absdataid.
Definition beq := absdataid_eq.
Definition blt := absdataid_lt.
Lemma beq_true_eq : forall a a´ : A,
beq a a´ = true -> a = a´.
Lemma beq_false_neq : forall a a´ : A,
beq a a´ = false -> a <> a´.
Lemma eq_beq_true : forall a a´ : A,
a = a´ -> beq a a´ = true.
Lemma neq_beq_false : forall a a´ : A,
a <> a´ -> beq a a´ = false.
Lemma blt_trans :
forall a a´ a´´ : A,
blt a a´ = true -> blt a´ a´´ = true -> blt a a´´ = true.
Lemma blt_irrefl :
forall a : A,
blt a a = false.
Lemma blt_asym :
forall a b : A,
blt a b = true -> blt b a = false.
Lemma blt_beq_dec :
forall a b : A,
{blt a b = true} + {beq a b = true} + {blt b a = true}.
End absdataidspec.
Inductive absdata:=
| abstcblist: TcbMod.map -> absdata
| absecblist : EcbMod.map -> absdata
| ostm: ostime -> absdata
| oscurt: addrval -> absdata.
Module absdatastru.
Definition B := absdata.
End absdatastru.
Module OSAbstMod := MapLib.MapFun absdataidspec absdatastru.
Definition osabst:= OSAbstMod.map.
abstract step
abstract expression used in spec_assume
the high-level specification language
'spec_prim vl osabstep' is a relation that takes vl as arguments and maps an abstract
state to another. Users can instantiate it to specify any atomic transitions over abstract
states. 'spec_assume absexpr' asserts that the predicate 'absexpr' holds over the current
abstract state, 'absexpr' is a prop of abstract state. 'spec_end opv' represents the end of
abstract APIs with optional return values or interrupt handlers. 'spec_seq s1 s2' and
'spec_choice s1 s2' are statements for sequential composition and non-deterministic
choices respectively.
Inductive spec_code:=
| spec_prim : vallist-> osabstep -> spec_code
| sched : spec_code
| spec_done : option val -> spec_code
| spec_seq : spec_code -> spec_code -> spec_code
| spec_choice : spec_code -> spec_code -> spec_code
| spec_assume : absexpr -> spec_code.
Notation " x ´(|´ vl ´|)´ " := (spec_prim vl x) (at level 40).
Notation " ´END´ v " := (spec_done v)(at level 40).
Notation " x ´;;´ y " := (spec_seq x y) (right associativity, at level 44).
Notation " x ´??´ y " := (spec_choice x y) (right associativity, at level 45).
Notation " ´ASSUME´ b " := (spec_assume b) (at level 40).
C statements
'sassign e1 e2' is used to assign the right value of e2
to the memory address obtained from e1 . 'scall f el' is a function call with arguments
evaluated from expression list 'el'. The similar function call statement 'scalle e f el'
assigns the return value to the memory address obtained from 'e'. The print statement
'sprint e' allows us to observe the execution results of the low-level programs. The return
statements 'sret' and 'sret e' are used in a function body which return with a value or not.
The other structural statements have standard meanings, we omit their explanation here.
For the dynamical statements, 'sskip opv' is used to indicate the end of executing a statement,
and the optional value v records the value generated by the statement if it has.
The 'sfexec f vl tl' statement is an intermediate statement for running the function body.
When a function call statement is executed, it first calculates all the expressions to get
the value list of the arguments, then is executed to 'sfexec' before the execution of the
function body. 'sfree fl opv' is used to free the memory blocks of local variables
and formal parameters after finishing the execution of the statements of function
bodies, while 'salloc vl dl' allocates memory blocks for local variables and formal
parameters before entering the function body. Note that all the dynamical state-
ments never appear in the programs written by users. They are only used for
giving the fine-grained small-step operational semantics.
The current implementation mixes the primitives, the standard
C statements, the high-level api statements and the dynamical statements together. We need to introduce
additional constraints to specify the OS functions bodies which do not contain
dynamical statements. Also the client functions cannot have both built-in prim-
itives or dynamical statements.
Inductive stmts :=
| sskip : option val -> stmts
| sassign : expr -> expr -> stmts
| sif : expr -> stmts -> stmts -> stmts
| sifthen:expr->stmts->stmts
| swhile : expr -> stmts -> stmts
| sret : stmts
| srete : expr -> stmts
| scall : fid -> exprlist -> stmts
| scalle : expr -> fid -> exprlist -> stmts
| sseq : stmts -> stmts -> stmts
| sprint : expr -> stmts
| sfexec : fid -> vallist -> typelist -> stmts
| sfree : freelist -> option val -> stmts
| salloc : vallist -> decllist -> stmts
| sprim : prim -> stmts
| hapi_code:spec_code -> stmts .
Open Scope type_scope.
function definitions
the set of functions
the set of interrupt handlers
the low-level kernel code
low-level program
The whole low-level program 'lprog' (progunit * oscode) consists of client
function definitions 'progunit' and the OS code 'oscode' (progunit * progunit * intunit),
where the first 'progunit' represents the definitions of API functions,
the second 'progunit' means the definitions of the internal functions and
'intunit' contains all the interrupt handlers.
APIs and internal functions map function identifiers to the definitions of functions,
while the interrupt handlers maps the handler identifiers to statements.
Function definitions 'function' consist of the type of the return value,
the declaration of parameters, the declaration of local variables and the
statement of the function body. For convinience, we define client statements
and kernel statements with the same syntax, A statement can be either
built-in primitive statements (sprim prim), high-level spec-code
(hapi_code spec_code), the standard C statements or dynamical statements
which are only used for defining the operational semantics.
the current evaluation
Inductive cureval:=
|cure : expr -> cureval
|curs : stmts -> cureval.
Notation "´SKIP´ " := (curs (sskip None)) (at level 0).
Notation "´[´ v ´]´" := (curs (sskip (Some v))) (at level 0).
|cure : expr -> cureval
|curs : stmts -> cureval.
Notation "´SKIP´ " := (curs (sskip None)) (at level 0).
Notation "´[´ v ´]´" := (curs (sskip (Some v))) (at level 0).
Definition of continuation, which is a pair of expression continuation and statement continuation
Inductive exprcont:=
| kenil : exprcont
| keop1 : uop -> type -> exprcont -> exprcont
| keop2r : bop -> expr -> type -> type -> exprcont -> exprcont
| keop2l: bop -> val -> type -> type ->exprcont -> exprcont
| kederef : type -> exprcont -> exprcont
| keoffset: int32 -> exprcont -> exprcont
| kearrbase: expr -> type -> exprcont -> exprcont
| kearrindex: val -> type -> exprcont -> exprcont
| kecast: type -> type -> exprcont -> exprcont.
Inductive stmtcont:=
| kstop : stmtcont
| kseq : stmts -> stmtcont -> stmtcont
| kcall : fid -> stmts -> env -> stmtcont -> stmtcont
| kint : cureval -> exprcont -> env -> stmtcont -> stmtcont
| kassignr: expr -> type -> stmtcont -> stmtcont
| kassignl : val -> type -> stmtcont -> stmtcont
| kfuneval : fid -> vallist -> typelist -> exprlist -> stmtcont -> stmtcont
| kif : stmts -> stmts -> stmtcont -> stmtcont
| kwhile : expr -> stmts -> stmtcont -> stmtcont
| kret : stmtcont -> stmtcont
| kevent : cureval -> exprcont -> stmtcont -> stmtcont.
Definition cont := (exprcont * stmtcont).
| kenil : exprcont
| keop1 : uop -> type -> exprcont -> exprcont
| keop2r : bop -> expr -> type -> type -> exprcont -> exprcont
| keop2l: bop -> val -> type -> type ->exprcont -> exprcont
| kederef : type -> exprcont -> exprcont
| keoffset: int32 -> exprcont -> exprcont
| kearrbase: expr -> type -> exprcont -> exprcont
| kearrindex: val -> type -> exprcont -> exprcont
| kecast: type -> type -> exprcont -> exprcont.
Inductive stmtcont:=
| kstop : stmtcont
| kseq : stmts -> stmtcont -> stmtcont
| kcall : fid -> stmts -> env -> stmtcont -> stmtcont
| kint : cureval -> exprcont -> env -> stmtcont -> stmtcont
| kassignr: expr -> type -> stmtcont -> stmtcont
| kassignl : val -> type -> stmtcont -> stmtcont
| kfuneval : fid -> vallist -> typelist -> exprlist -> stmtcont -> stmtcont
| kif : stmts -> stmts -> stmtcont -> stmtcont
| kwhile : expr -> stmts -> stmtcont -> stmtcont
| kret : stmtcont -> stmtcont
| kevent : cureval -> exprcont -> stmtcont -> stmtcont.
Definition cont := (exprcont * stmtcont).
Definition of low-level and high-level code
Definition code := (cureval * cont).
Module CodeSpec.
Definition B:= code.
End CodeSpec.
Import MapLib.
Module TasksMod := MapFun tidspec CodeSpec.
Module CodeSpec.
Definition B:= code.
End CodeSpec.
Import MapLib.
Module TasksMod := MapFun tidspec CodeSpec.
Definition of task pool of low-level and high-level machine
Definition tasks :=TasksMod.map.
Module EnvSpec.
Definition B:= env.
End EnvSpec.
Module CltEnvMod:= MapFun tidspec EnvSpec.
Module EnvSpec.
Definition B:= env.
End EnvSpec.
Module CltEnvMod:= MapFun tidspec EnvSpec.
Definition of local symbol table
Definition of C states, which consist of global symbol table, local symbol tables and memory
'ie' is a boolean flag used to turn on/off interrupts.
'isr' is a sequence of boolean flags, one for each interrupt. The stack 'cs' records
the historical values of 'ie', which are pushed whenever the execution enters a
critical region. It is used to support nested critical regions. The task-local stack
'is' records the sequence of interrupts that interrupt the execution of this task. It is
auxiliary data introduced for verification purpose. Then the task-local interrupt
status 'localst' is defined as a triple (ie, is, cs). 'ltaskstset' records the 'localst'
of each task. The kernel-level state 'osstate' consists of the general C state 'clientst',
the global 'isr' register and the set 'localst' of task-local interrupt status.
the local states of interrupts
Definition localst := (ie * is * cs).
Module LocalStSpec.
Definition B:= localst.
End LocalStSpec.
Module TaskLStMod:= MapFun tidspec LocalStSpec.
Definition ltaskstset:= TaskLStMod.map.
Module LocalStSpec.
Definition B:= localst.
End LocalStSpec.
Module TaskLStMod:= MapFun tidspec LocalStSpec.
Definition ltaskstset:= TaskLStMod.map.
the isr register
Definition isr := hid -> bool.
Definition isrupd (r : isr) (x : hid) (b : bool):=
fun (y : hid) => if beq_nat x y then b else r y.
Fixpoint leb_nat (m : nat) : nat -> bool :=
match m with
| O => fun _ : nat => true
| S m´ => fun n : nat => match n with
| O => false
| S n´ => leb_nat m´ n´
end
end.
Fixpoint highpri´ (r : isr) (n : nat) : hid :=
match n with
| O => INUM
| S n´ => let y := highpri´ r n´ in
if r n´ then
if (leb_nat n´ y) then n´ else y
else y
end.
Definition highpri (r:isr) := highpri´ r INUM.
Definition higherint (r:isr) (i:hid) := forall i´, i´<= i -> r i´ = false.
Definition empisr := fun (x : hid) => false.
Definition isrupd (r : isr) (x : hid) (b : bool):=
fun (y : hid) => if beq_nat x y then b else r y.
Fixpoint leb_nat (m : nat) : nat -> bool :=
match m with
| O => fun _ : nat => true
| S m´ => fun n : nat => match n with
| O => false
| S n´ => leb_nat m´ n´
end
end.
Fixpoint highpri´ (r : isr) (n : nat) : hid :=
match n with
| O => INUM
| S n´ => let y := highpri´ r n´ in
if r n´ then
if (leb_nat n´ y) then n´ else y
else y
end.
Definition highpri (r:isr) := highpri´ r INUM.
Definition higherint (r:isr) (i:hid) := forall i´, i´<= i -> r i´ = false.
Definition empisr := fun (x : hid) => false.
the low-level kernel state
Definition osstate := (clientst * isr * ltaskstset).
Definition smem := (env * env * mem).
Definition taskst := (smem * isr * localst).
Definition get_smem (ts : taskst) :=
match ts with
(m, _, _) => m
end.
Definition smem := (env * env * mem).
Definition taskst := (smem * isr * localst).
Definition get_smem (ts : taskst) :=
match ts with
(m, _, _) => m
end.
the low-level world
The whole program configuration 'lworld' consists of the program 'lprog',
the task pool 'tasks', the client state 'clientst', the kernel state 'osstate',
and the identifier t of the current task. Note that W contains two pieces of 'clientst',
one for user applications (clients), the other inside 'osstate' for the kernel.
Separating the data into two parts prevents user applications from accessing kernel data.
Definition lworld := (lprog * tasks * clientst * osstate * tid).
Definition funtype : Set := prod type typelist.
Definition api_code := vallist -> spec_code.
Definition osapi := prod api_code funtype.
Definition osapispec := fid -> option osapi.
Definition int_code := spec_code.
Definition osintspec := hid -> option int_code.
Definition ossched := osabst -> tid -> Prop.
Definition osspec := (osapispec * osintspec * ossched).
the high-level program
the whole high-level program 'hprog' consists of the application code and the abstract
specification of the kernel 'osspec'. The application code is the same as in the low-level
language. 'osspec' contains the specifications 'osapispec' for kernel APIs, 'osintspec' for
interrupt handlers, and 'ossched' for the scheduler. The high-level program configuration
'hworld' consists of the high-level program 'hprog', the task pool 'tasks', the client state
'clientst', and the abstract kernel state 'osabst'. Programmers at this level have no control
over interrupts (e.g., enabling or disabling interrupts). Always enabled, interrupts are modeled
implicitly as abstract external events that may occur non-deterministically at any program
points. Handlers of the events are also specified as 'osintspec' in 'osspec'.
At the high level an incoming level-k event is always handled by executing 'osintspec k'.
The interrupt handlers are specified as an abstract statement 'spec_code' and
The system APIs (osapi,funtype) consist of the type of the API 'funtype' and the abstract
spec 'osapi' which maps the values of arguments to a 'spec_code'.
the high-level world