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
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/…
Static and Dynamic Threads f(a) Static Threads" fork f(a1) fork f(a2) fork f(an) ●●● "Dynamic Threads" 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens Static and Dynamic Threads f(a) . . . fork f(a1) fork f(a2) fork f(an) … “Static Threads” “Dynamic Threads
Challenges First attempt Check NI between all static threads ■T:(A,G) ■ij.i月→G→A Too rigid to handle changing env. 2005-9-16 NJPLS@Stevens
2005-9-16 NJPLS@Stevens Challenges ◼ First attempt ◼ Check NI between all static threads ◼ Ti : (Ai , Gi ) ◼ i,j. ij Gi Aj Too rigid to handle changing env