Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads Xinyu Feng Toyota Technological Institute at Chicago Joint work with Zhong Shao (Yale),Yuan Dong (Tsinghua Univ.)and Yu Guo (USTC)
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads Xinyu Feng Toyota Technological Institute at Chicago Joint work with Zhong Shao (Yale), Yuan Dong (Tsinghua Univ.) and Yu Guo (USTC)
How to verify safety correctness of OS kernels /Hypervisors? Many challenges: Is verification possible? Low-level C/Assembly code Code loading Concurrency How to do it in a Interrupts clean modular way? Device drivers l/O
How to verify safety & correctness of OS kernels / Hypervisors? Code loading Many challenges: Interrupts … Device drivers & I/O Concurrency Low-level C/Assembly code Is verification possible? How to do it in a clean & modular way?
Layering of Simplified Kernel Code A ） 1 一R0 10 -IR1 ∩∩ u∩U∩∩ ←—R2 B locks cond var. 1/O 1 4一1R3 1 ←—R4 ←—R5 ←—IR6 〉 scheduler ctxt switching &.. —IR7 B:concurrent code with explicit interrupts How to verify ??
Layering of Simplified Kernel Code scheduler & ctxt switching & ... . . . locks cond var. I/O . . . . . . . . . A B C 1 1 0 1 1 0 1 0 IR0 IR1 IR2 IR3 IR4 IR5 IR6 IR7 B: concurrent code with explicit interrupts How to verify ???
Concurrency with Interrupts:Challenges Thread X Handler 0 Thread Y irq0 sti Handler 1 switch irq1 4) cli iret switch cli iret sti _switch sti Asymmetric preemption between handlers and non-handler code Intertwining between threads and handlers Asymmetric synchronization:cli/sti are different from locks
Concurrency with Interrupts: Challenges . . . . . . cli . . . switch . . . sti . . . Thread X switch iret . . . . . . Handler 0 . . . cli . . . switch . . . sti . . . . . . sti . . . Thread Y iret . . . Handler 1 Asymmetric preemption between handlers and non-handler code Intertwining between threads and handlers Asymmetric synchronization: cli/sti are different from locks
Our Contributions A Hoare-style program logic for modular verification of low-level programs with interrupts and concurrency. Locks Condition Variables yield/sleep void acq_m(Lock *1); void wait_m(Lock *I,CV *cv); timer_handler void rel_m(Lock *I); void signal_m(CV *cv); void yield() cli/ void acq_h(Lock *1); void wait_h(Lock *I,CV *cv); void sleep() sti void rel_h(Lock *1); void signal_h(Lock *I,CV *cv); void acq_spin(Lock *I); void wait_bh(Lock *I,CV *cv); void rel_spin(Lock *I); void signal_bh(Lock *I,CV *cv); scheduler block unblock void scheduler() void blk(queue *q) int unblk(queue *q) node*deQueue(queue *q) void enQueue(queue q,node *n) ctxt switching code
Our Contributions A Hoare-style program logic for modular verification of low-level programs with interrupts and concurrency
AIM -I Single Threaded-Code with Interrupts (data heap)H f1: 工1 pc addu… f2: 2 012 cli sti iret ih: ISR ￥2 ￥3 … (register file)R ie jf (code heap)c (state)s :=(H,R,ie) ::={f→I」* (program)P::=(c,s,pc)
AIM – I : Single Threaded-Code with Interrupts I1 f1: I2 f2: ih: ISR … (code heap) C 0 r1 1 2 … r2 r3 … rn (data heap) H (register file) R (state) S addu … cli sti iret … j f (program) P::=(C,S,pc) ::=(H,R,ie) ::={f I}* pc ie
Example:Teeter-Totter left right while(true){ 50 50 cli; timer: if([right]=0){ if([1eft]==0){ sti; print("right wins!"); break; iret; } [right]:=[right]-1; [left] :=[1eft]-1; [1eft]:=[1eft]+1; [right][right]+1; sti; iret; print("left wins！"); How to guarantee non-interference?
Example: Teeter-Totter while(true){ cli; if([right] == 0){ sti; break; } [right] := [right]-1; [left] := [left]+1; sti; } print(“left wins!”); timer: if([left] == 0){ print(“right wins!”); iret; } [left] := [left]-1; [right] := [right]+1; iret; 50 50 left right How to guarantee non-interference?
Non-Interference? Program invariant: There is always a partition of memory among concurrent entities, and each concurrent entity only access its own part. But note: The partition is dynamic:ownership of memory can be dynamically transferred. cli/sti can be modeled as operations that trigger memory ownership transfer
Non-Interference? Program invariant: There is always a partition of memory among concurrent entities, and each concurrent entity only access its own part. But note: The partition is dynamic: ownership of memory can be dynamically transferred. cli/sti can be modeled as operations that trigger memory ownership transfer
AIM -I:The Memory Model INV Memory B A Non-handler Handler INV sti cli iret The memory partition is logical,not physical!
- { PINVh } AIM – I : The Memory Model Non-handler sti iret Handler B A cli … Memory … - INV { Ph } The memory partition is logical, not physical!
Separation Logic to Enforce Partition [lthtiaq O'Hearn'01,Reynolds'02] emp empty heap 1→ n 1→ n p*q P q P∧g P∧g
Separation Logic to Enforce Partition l n l n p q p q emp empty heap p q p q [Ithtiaq & O’Hearn’01, Reynolds’02]