Challenges Extensibility and openness not designed for certain specific interoperations But can we just use MLFs, e.g.Coq? Expressiveness type safety,concurrency properties,partial correctness,.. A general and uniform model of control flow Allow functions certified in different systems to call each other the key for modularity:separate verification proof reuse Principled interoperation with clear meta-property properties of the whole system composed of modules Not readily supported in Coq!
Challenges ◼ Extensibility and openness ◼ not designed for certain specific interoperations But can we just use MLFs, e.g. Coq? ◼ Expressiveness ◼ type safety, concurrency properties, partial correctness, … ◼ A general and uniform model of control flow ◼ Allow functions certified in different systems to call each other ◼ the key for modularity: separate verification & proof reuse ◼ Principled interoperation with clear meta-property ◼ properties of the whole system composed of modules Not readily supported in Coq!
Our contributions OCAP:an open framework Embedding of different systems TAL,non-CPS Hoare-logic,A-G reasoning,.. ■Open&Extensible Modularity with first-class code pointers [Ni&shao POPL06] ■Soundness Type safety,preservation of invariants in foreign systems ▣Applications TAL memory allocation libs. Threads Scheduler The first time to modularly certify both sides ■
Our contributions ◼ OCAP: an open framework ◼ Embedding of different systems ◼ TAL, non-CPS Hoare-logic, A-G reasoning, … ◼ Open & Extensible ◼ Modularity with first-class code pointers [Ni&Shao POPL’06] ◼ Soundness ◼ Type safety, & preservation of invariants in foreign systems ◼ Applications ◼ TAL + memory allocation libs. ◼ Threads + Scheduler ◼ The first time to modularly certify both sides ◼ …
Outline ■OCAP Framework Certifying Threads Schedulers
Outline ◼ OCAP Framework ◼ Certifying Threads & Schedulers
OCAP:Overview ! C1 …2 Cn L1 Cr [o on Sound Sound [on OCAP Rules OCAP Soundness Modeling of the machine TCB Mechanized Meta-Logic(CiC)
OCAP Rules … Ln OCAP : Overview OCAP Soundness Mechanized Meta-Logic (CiC) Modeling of the machine TCB Sound L1 ( )L1 ( )Ln Sound Mechanized Meta-Logic (CiC) Modeling of the machine … C1 Cn
The Machine (data heap) f 工1 pc addu f2: 2 0 12 lw … SW fa: 工3 ￥1 r2 r3 jf (register file)R (code heap)c (state)s:=(H,R) (instr.seq.)I ::={f→工}* (program)P:=(c,s,pc)
The Machine I1 f1: I2 f2: I3 f3: … (code heap) C 0 r1 1 2 … r2 r3 … rn (data heap) H (register file) R (state) S addu … lw … sw … … j f (instr. seq.) I (program) P::=(C,S,pc) ::=(H,R) ::={f I}* pc