64 F.Xu et al. (AErpr) e ::nlxl sel&ele.id ele]l... (AppStmts)d ::e=elf(e)d;d|while (e)dl if (e)d else dreturn el... (App Code）A={fhwd,.…,fndn (LPrim) ::switch z|encrt|excrt eoi iext... (LStmts) s ::dts;s while (e)s... (ItrpCode)0 ::[so,...,sN-1] (ProgUnit)n::={f1s1,...,fnsn} (LOSCode)O ::(na,ni,0) (LProg) P:=(A,O) (BitVal) b,ie∈{0,1} (ISRReg)isr ::[bo,...,bN-1] (CrtStk) cs ::nil ie::cs (ItrpStk)is ::nil k::is (ItrpTaskSt)::=(ie,is,cs) (ItpS0π={t161,·,tnw6n} Fig.2.The language for applications and kernel implementation Note that the correctness of OS kernels are independent of the implemen- tation language of A.Here we pick the C language for A to simplify the for- malization because the applications and the kernel are now implemented in the same language and we do not have to consider the interaction between different languages when defining the whole system (AO])behaviors. Low-Level Language for OS Kernels.The middle of Fig.2 shows the low-level language for the concrete implementation of OS kernels.Usually the kernels are implemented in C with inline assembly.However,giving semantics directly to C with inline assembly requires us to expose stacks and registers,which make the semantics overly complex.To avoid this problem,we extend the C statements with assembly primitives t to encapsulate the assembly code.Semantics of these primitives will be given below. switch x switches to the target task z.encrt enters a critical region by disabling interrupts.It also saves the old IF onto the stack to allow nested critical regions.Note we use ie to model the IF flag and abstract away other bits in the hardware EFLAGS register.excrt exits the current critical region by popping the stack to recover ie.Since we hide stacks in our state model,we use an abstract stack cs to save the historical ie bits (see Fig.2,which is explained below).eoi k clears the k-th bit in isr,indicating that the k-th interrupt is no longer in service.iext enables interrupts and returns to the interrupted program. The kernel implementation O consists of the system API implementation na, the internal functions ni and the interrupt handlers 0.The internal functions are called only by code in na or 0.6 is a sequence of N interrupt handlers,where N is the maximum number of interrupts we support.The handler with the lower identifier has the higher priority.Then a complete low-level program P is defined as a pair of the application code A and the kernel code O. Operational Semantics.The language is concurrent,with multiple continuations (i.e.,control stacks)in the state,each corresponding to a task.All tasks share64 F. Xu et al. (AExpr) e ::= n | x | ∗ e | &e | e.id | e[e] | ... (AppStmts) d ::= e=e | f(¯e)| d; d | while (e) d | if (e) d else d | return e | ... (AppCode) A ::= {f1 d1,...,fn dn} (LPrim) ι ::= switch x | encrt | excrt | eoi k | iext | ... (LStmts) s ::= d |ι| s; s | while (e) s | ... (ItrpCode) θ ::= [s0,...,sN−1] (ProgUnit) η ::= {f1 s1,...,fn sn} (LOSCode) O ::= (ηa, ηi, θ) (LProg) P ::= (A, O) (BitVal) b, ie ∈ {0, 1} (ISRReg) isr ::= [b0,...,bN−1] (CrtStk) cs ::= nil | ie::cs (ItrpStk) is ::= nil | k ::is (ItrpTaskSt) δ ::= (ie, is, cs) (ItrpSt) π ::= {t1 δ1,...,tn δn} Fig. 2. The language for applications and kernel implementation Note that the correctness of OS kernels are independent of the implemen￾tation language of A. Here we pick the C language for A to simplify the for￾malization because the applications and the kernel are now implemented in the same language and we do not have to consider the interaction between different languages when defining the whole system (A[O]) behaviors. Low-Level Language for OS Kernels. The middle of Fig. 2 shows the low-level language for the concrete implementation of OS kernels. Usually the kernels are implemented in C with inline assembly. However, giving semantics directly to C with inline assembly requires us to expose stacks and registers, which make the semantics overly complex. To avoid this problem, we extend the C statements with assembly primitives ι to encapsulate the assembly code. Semantics of these primitives will be given below. switch x switches to the target task x. encrt enters a critical region by disabling interrupts. It also saves the old IF onto the stack to allow nested critical regions. Note we use ie to model the IF flag and abstract away other bits in the hardware EFLAGS register. excrt exits the current critical region by popping the stack to recover ie. Since we hide stacks in our state model, we use an abstract stack cs to save the historical ie bits (see Fig. 2, which is explained below). eoi k clears the k-th bit in isr, indicating that the k-th interrupt is no longer in service. iext enables interrupts and returns to the interrupted program. The kernel implementation O consists of the system API implementation ηa, the internal functions ηi and the interrupt handlers θ. The internal functions are called only by code in ηa or θ. θ is a sequence of N interrupt handlers, where N is the maximum number of interrupts we support. The handler with the lower identifier has the higher priority. Then a complete low-level program P is defined as a pair of the application code A and the kernel code O. Operational Semantics. The language is concurrent, with multiple continuations (i.e., control stacks) in the state, each corresponding to a task. All tasks share