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/…
Our Contributions A new PCC framework:CMAP Verification of general properties Dynamic thread creation/termination Generalize the Rely-Guarantee method Modular verification ■Realistic features Multiple instantiations of thread code Thread argument passing,thread-local data 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens Our Contributions ◼ A new PCC framework: CMAP ◼ Verification of general properties ◼ Dynamic thread creation/termination ◼ Generalize the Rely-Guarantee method ◼ Modular verification ◼ Realistic features ◼ Multiple instantiations of thread code ◼ Thread argument passing, thread-local data
Outline of This Talk Background:the Rely-Guarantee Method Challenges for Dynamic Thread Creation/Termination ■Our Approach The CMAP Framework Conclusion and Future Work 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens Outline of This Talk ◼ Background: the Rely-Guarantee Method ◼ Challenges for Dynamic Thread Creation/Termination ◼ Our Approach ◼ The CMAP Framework ◼ Conclusion and Future Work
The Rely-Guarantee Method Thread 1 (A1,G1) Shared 8÷ A1 Thread 2 (A2,G2) Memory 5152 S3 S4 S5 A1:S2-S3,S4-S51 A2:S1-S2,S3-S41 G1:S1-S2,S3-S4 G2:S2-S3,S4-S51 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens The Rely-Guarantee Method Thread 1 Thread 2 (A1,G1) Shared (A2,G2) Memory S1 S2 S3 S4 S5 A1: S2 – S3, S4 – S5,… G1: S1 – S2, S3 – S4,… A2: S1 – S2, S3 – S4,… G2: S2 – S3, S4 – S5,… G1 A2 G2 A1
The Rely-Guarantee Method Thread Thread Environment ■Rely and Guarantee ■A,G:State→State>Prop Thread Modularity Non-Interference (interface compatibility): ■ij.i月→G,→A Safety of each thread ■T:(A,G) 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens The Rely-Guarantee Method ◼ Thread + Thread Environment ◼ Rely and Guarantee ◼ A, G: State → State → Prop ◼ Thread Modularity ◼ Non-Interference (interface compatibility): ◼ i,j. ij Gi Aj ◼ Safety of each thread ◼ Ti : (Ai , Gi )
GCD Example [Yu&Shao'04] Thread1: Thread2: while(a<>b){ while(a<>b){ if(a b) if(b a) a :a-b b b-a; ] } A1=(a=a)∧(a≥b→b=b)∧(GcD(a,b)=GCD(a',b)) G1=(b=b)∧(a≤b→a=a)∧(GCD(a,b)=GCD(a',b) A2三G1( G2=A1 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens GCD Example [Yu&Shao’04] Thread1: while(a<>b){ if(a > b) a := a-b; } Thread2: while(a<>b){ if(b > a) b := b-a; }