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; }