Existing work Assume-Guarantee (A-G)reasoning [Misra&Chandy'81,Jones'83] ©thread modularity general:no restriction over synchronization pattern spec of A&G requires global data invariants Concurrent Separation Logic (CSL)[o'Hearn,Brookes 20041 ©thread modularity data modularity:local reasoning restrictive synchronization pattern shared resources can be accessed only inside critical regionsExisting work • Assume-Guarantee (A-G) reasoning [Misra&Chandy’81, Jones’83] ☺ thread modularity ☺ general: no restriction over synchronization pattern  spec of A&G requires global data invariants • Concurrent Separation Logic (CSL) [O’Hearn, Brookes 2004] ☺ thread modularity ☺ data modularity: local reasoning  restrictive synchronization pattern shared resources can be accessed only inside critical regions