Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination Xinyu Feng Yale University Joint work with Zhong Shao
Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination Xinyu Feng Yale University Joint work with Zhong Shao
Motivation Proof-carrying code (PCC) In principle:verify any property on any code Real binaries no loss of efficiency Embedded OS,device drivers... All safety liveness properties... Formal,machine-checkable proofs In reality:only works for sequential code Can concurrent code ever be supported by the PCC framework 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens Motivation ◼ Proof-carrying code (PCC) ◼ In principle: verify any property on any code ◼ Real binaries & no loss of efficiency ◼ Embedded OS, device drivers… ◼ All safety & liveness properties… ◼ Formal, machine-checkable proofs ◼ In reality: only works for sequential code Can concurrent code ever be supported by the PCC framework ?
Challenges Challenges for Proof-carrying concur.code -A general framework for concurrent assembly code verification Lack of structures(e.g.cobegin/coend blocks) Specification/proof generation Spec inference,proof assistant,theorem prover ■（ Concurrent assembly code verification No directly applicable logic Traditional Hoare-logic:only sequential code Type Systems:no Concurrent Typed Assembly Language (TAL) 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens Challenges ◼ Challenges for Proof-carrying concur. code ◼ A general framework for concurrent assembly code verification ◼ Lack of structures (e.g. cobegin/coend blocks) ◼ Specification/proof generation ◼ Spec inference, proof assistant, theorem prover ◼ Concurrent assembly code verification ◼ No directly applicable logic ◼ Traditional Hoare-logic: only sequential code ◼ Type Systems: no Concurrent Typed Assembly Language (TAL)
Previous work Rely-Guarantee (R-G)Method Shared memory concurrency Thread modular verification Only for higher-level code:cobegin/coend a CCAP[Yu&Shao,ICFP'04] The first PCC framework supporting concurrent assembly code R-G method Only support static threads P1l...IPn 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens Previous work ◼ Rely-Guarantee (R-G) Method ◼ Shared memory concurrency ◼ Thread modular verification ◼ Only for higher-level code: cobegin/coend ◼ CCAP[Yu&Shao, ICFP’04] ◼ The first PCC framework supporting concurrent assembly code ◼ R-G method ◼ Only support static threads ◼ P1 || … || Pn
Concurrency Programming ■cobegin/coend S::=...|cobegin P1 P2 codend .. Higher-level,well-structured Only support properly nested concurrent code fork/join S::=...|tid :fork f(a)join tid... More flexible:improperly nested code OSes/Java/... 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens Concurrency Programming ◼ cobegin/coend ◼ S::=…| cobegin P1 || P2 codend | … ◼ Higher-level, well-structured ◼ Only support properly nested concurrent code ◼ fork/join ◼ S::=…| tid := fork f(a) | join tid | … ◼ More flexible: improperly nested code ◼ OSes/Java/…