Tock is an embedded operating system written in the Rust programming language. Rust guarantees memory safety while simultaneously avoiding garbage collection and allowing developers fine control of memory. Unfortunately, kernels inevitably require some unsafe code. One such example is interrupts. Handling interrupts efficiently and correctly is a core responsibility of the kernel, and mistakes in interrupt handlers can cause serious issues such as data loss or device malfunctions.
Tock handles interrupts in a top / bottom half architecture. The top half of an interrupt is responsible for acknowledging an interrupt as fast as possible, and scheduling it for the bottom half. Then, when it is "safer" to do so, the bottom half handles the actual interrupt, executing any necessary logic. Performance is a critical part of these top half handlers, as other interrupts are generally disabled and spending too long in an interrupt handler could quickly degrade system performance. To deal with this, Tock's top half handlers are written in inline assembly.
Writing assembly is hard, and bits of assembly can undermine the type and memory safety - the point of writing a kernel in Rust. A few key challenges are...
- Saving and restoring process state correctly
- ISRs must not clobber registers used in the previous context. If they do, they must save and restore their state.
- Making sure ISRs account for and interact with hardware semantics correctly
- See this long thread about an interrupt issue with ARM devices in Tock
- Dealing with unclear control flow
- Interrupts are asynchronous to the main kernel loop. Therefore, understanding what preconditions and postconditions must hold for an interrupt is difficult.
- Furthermore, the correctness of some ISRs depend on other bits of assembly (for example the assembly responsible for doing context switches)
- Dealing with interrupts interrupting the interrupt handler :)
- For example, in ARM architectures, it is possible for ISRs to be pre-empted by higher priority interrupts.
As part of broader work verifying the Tock OS, we propose verifying the top half interrupt handlers for ARMv6m, ARMv6m, and RISC-V architectures. There is also the option of verifying other assembly (e.g. context switching from the kernel to run processes which involves assembly that saves and restores register values). In fact, this may be necessary to reason about the ISRs themselves.
This will likely involve two lines of work.
- Reasoning about preconditions prior to entering ISRs or other bits of assembly
- For example, the ARMv6m ISR assumes that register R1 is pointing to the previously executing process struct's stored registers field. It is not immediately obvious why this is always the case.
- Reasoning about bits of assembly
- We must make sure that we do not clobber registers or memory accidentally, must make sure the assembly aligns with the hardware's handling of interrupts, and must make sure we can actually deal with ISRs being pre-empted.
One potentially interesting future artifact would be a fully verified ARM or RISC-V emulator. This could be useful for folks needing to write bits of inline assembly in Rust programs. One could first write specifications in a lifted Rust version and add some refinement annotations. For example, here is a really simple contract on a program that moves the value 0 into register r0.
#[flux_rs::sig(fn (arm: &strg Armv7m[@cpu]) ensures arm: Armv7m { v: v.r0 == 0 })]
fn simple_mov_program(armv7m: &mut Armv7m) {
armv7m.mov(GPR::R0, Value::Value(0));
}An example of the specification for mov on an ARMv7m emulator might look roughly like this:
flux_rs::defs! {
fn get_reg(reg: int, cpu: Armv7m) -> int {
if reg == 0 {
cpu.r0
} else if reg == 1 {
cpu.r1
} else if reg == 2 {
cpu.r2
} else if reg == 3 {
cpu.r3
} else if reg == 4 {
cpu.r4
} else if reg == 5 {
cpu.r5
} else if reg == 6 {
cpu.r6
} else if reg == 7 {
cpu.r7
} else if reg == 8 {
cpu.r8
} else if reg == 9 {
cpu.r9
} else if reg == 10 {
cpu.r10
} else if reg == 11 {
cpu.r11
} else if reg == 12 {
cpu.r12
} else if reg == 13 {
cpu.r13
} else if reg == 14 {
cpu.r14
} else {
cpu.r15
}
}
fn value_into_u32(value: Value, cpu: Armv7m) -> int {
if value.is_reg {
get_reg(value.val, cpu)
} else {
value.val
}
}
}
#[flux_rs::refined_by(n: int)]
pub enum GPR {
#[variant(GPR[0])]
R0,
#[variant(GPR[1])]
R1,
#[variant(GPR[2])]
R2,
#[variant(GPR[3])]
R3,
#[variant(GPR[4])]
R4,
#[variant(GPR[5])]
R5,
#[variant(GPR[6])]
R6,
#[variant(GPR[7])]
R7,
#[variant(GPR[8])]
R8,
#[variant(GPR[9])]
R9,
#[variant(GPR[10])]
R10,
#[variant(GPR[11])]
R11,
#[variant(GPR[12])]
R12,
#[variant(GPR[13])]
R13,
// Link Register
#[variant(GPR[14])]
R14,
#[variant(GPR[15])]
R15,
}
#[flux_rs::refined_by(is_reg: bool, val: int)]
pub enum Value {
#[variant({GPR[@n]} -> Value[true, n])]
Register(GPR),
#[variant({u32[@n]} -> Value[false, n])]
Value(u32),
}
#[derive(Debug)]
#[flux_rs::refined_by(
r0: int,
r1: int,
r2: int,
r3: int,
r4: int,
r5: int,
r6: int,
r7: int,
r8: int,
r9: int,
r10: int,
r11: int,
r12: int,
r13: int,
r14: int,
r15: int,
psr: int,
primask: int,
basepri: int,
faultmask: int,
control: int,
)]
pub struct Armv7m {
#[field(u32[r0])]
pub r0: u32,
#[field(u32[r1])]
r1: u32,
#[field(u32[r2])]
r2: u32,
#[field(u32[r3])]
r3: u32,
#[field(u32[r4])]
r4: u32,
#[field(u32[r5])]
r5: u32,
#[field(u32[r6])]
r6: u32,
#[field(u32[r7])]
r7: u32,
#[field(u32[r8])]
r8: u32,
#[field(u32[r9])]
r9: u32,
#[field(u32[r10])]
r10: u32,
#[field(u32[r11])]
r11: u32,
#[field(u32[r12])]
r12: u32,
// r13 is the stack pointer
#[field(u32[r13])]
r13: u32,
// r14 is the link register
#[field(u32[r14])]
r14: u32,
// r15 is the program counter
#[field(u32[r15])]
r15: u32,
//
// Special Registers below
//
// PSR has 3 sub registers:
//
// APSR, IPSR, EPSR
#[field(u32[psr])]
psr: u32,
// Mask registers
//
// primask is 1 bit - the rest being reserved
#[field(u32[primask])]
primask: u32,
// basepri is 8 bit - the rest being reserved
#[field(u32[basepri])]
basepri: u32,
// faultmask is 1 bit - the rest being reserved
#[field(u32[faultmask])]
faultmask: u32,
// Control register (2 bit or 3 bit) depending on the specific processor
#[field(u32[control])]
control: u32,
}
impl Armv7m {
#[flux_rs::sig(fn (&Armv7m[@cpu], &GPR[@reg]) -> u32[get_reg(reg, cpu)])]
fn get_value_from_reg(&self, register: &GPR) -> u32 {
match register {
GPR::R0 => self.r0,
GPR::R1 => self.r1,
GPR::R2 => self.r2,
GPR::R3 => self.r3,
GPR::R4 => self.r4,
GPR::R5 => self.r5,
GPR::R6 => self.r6,
GPR::R7 => self.r7,
GPR::R8 => self.r8,
GPR::R9 => self.r9,
GPR::R10 => self.r10,
GPR::R11 => self.r11,
GPR::R12 => self.r12,
GPR::R13 => self.r13,
GPR::R14 => self.r14,
GPR::R15 => self.r15,
}
}
#[flux_rs::sig(fn (&Armv7m[@cpu], Value[@val]) -> u32[value_into_u32(val, cpu)])]
fn value_into_u32(&self, value: Value) -> u32 {
match value {
Value::Register(register) => self.get_value_from_reg(®ister),
Value::Value(v) => v,
}
}
#[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], u32[@new_val]) ensures self: Armv7m { new_cpu: get_reg(reg, new_cpu) == new_val })]
fn update_reg_with_u32(&mut self, register: GPR, value: u32) {
match register {
GPR::R0 => self.r0 = value,
GPR::R1 => self.r1 = value,
GPR::R2 => self.r2 = value,
GPR::R3 => self.r3 = value,
GPR::R4 => self.r4 = value,
GPR::R5 => self.r5 = value,
GPR::R6 => self.r6 = value,
GPR::R7 => self.r7 = value,
GPR::R8 => self.r8 = value,
GPR::R9 => self.r9 = value,
GPR::R10 => self.r10 = value,
GPR::R11 => self.r11 = value,
GPR::R12 => self.r12 = value,
GPR::R13 => self.r13 = value,
GPR::R14 => self.r14 = value,
GPR::R15 => self.r15 = value,
}
}
#[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], Value[@val])
ensures self: Armv7m {
new_cpu: get_reg(reg, new_cpu) == value_into_u32(val, old_cpu)
}
)]
pub fn mov(&mut self, register: GPR, value: Value) {
// Move immediate - writes a value into destination register
// This does not cause a flag update
let val = self.value_into_u32(value);
self.update_reg_with_u32(register, val);
}
}