On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning Xinyu Feng Yale University Joint work with Rodrigo Ferreira and Zhong Shao
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning Xinyu Feng Yale University Joint work with Rodrigo Ferreira and Zhong Shao
Motivation Concurrency verification is challenging! Exponential state space caused by interleaving of execution. Memory aliasing makes it harder to ensure non-interference. Modularity is the key!
Motivation Concurrency verification is challenging! T1 T1 T1 T2 T2 T2 Exponential state space caused by interleaving of execution. Memory aliasing makes it harder to ensure non-interference. Modularity is the key!
Two kinds of modularity 。Control modularity -a.k.a.thread-modularity each thread is verified independently of others 。Data modularity -a.k.a.information hiding -each thread only cares about data it uses
Two kinds of modularity • Control modularity – a.k.a. thread-modularity – each thread is verified independently of others • Data modularity – a.k.a. information hiding – each thread only cares about data it uses
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 regions
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 2004] ☺ thread modularity ☺ data modularity: local reasoning restrictive synchronization pattern shared resources can be accessed only inside critical regions
Our Contributions SAGL:combining CSL and A-G reasoning - extend A-G logic with local reasoning better data modularity (than A-G reasoning) thread modularity no restriction over synchronization pattern A formal study of the relationship between CSL and A-G reasoning
Our Contributions • SAGL: combining CSL and A-G reasoning – extend A-G logic with local reasoning ☺ better data modularity (than A-G reasoning) ☺ thread modularity ☺ no restriction over synchronization pattern • A formal study of the relationship between CSL and A-G reasoning
Outline of this talk 。Background Concurrent Separation Logic -Assume-Guarantee reasoning SAGL:combination of CSL A-G reasoning Interpretation of CSL in SAGL
Outline of this talk • Background – Concurrent Separation Logic – Assume-Guarantee reasoning • SAGL: combination of CSL & A-G reasoning • Interpretation of CSL in SAGL
Concurrent Separation Logic Assertions capture ownerships of resources 1→n Cannot access resource without ownership ● Shared resources are protected by critical regions (CRs) Transfer of ownership at boundary of CR
Concurrent Separation Logic • Assertions capture ownerships of resources • Cannot access resource without ownership • Shared resources are protected by critical regions (CRs) • Transfer of ownership at boundary of CR l n
CSL assertions emp empty heap 1→1 n 1→ n p*q P g P∧g P∧g
CSL assertions l n l n p q p q emp empty heap p q p q
Locks and Critical Regions Lock-based critical regions (CR): Lacq(); Lrel() Invariants about memory protected by locks: Γ={化→，ln→rn} 1* *In
Locks and Critical Regions Lock-based critical regions (CR): l.acq(); … … … … l.rel() Invariants about memory protected by locks: = {l1 r1 , …, ln rn } r1 rn . . . l1 ln
Concurrent Separation Logic T4) E()p2' P2 1.rel() T(2) *p2 1.acq() T(2)
p1 (l2 ) p2 (l1 ) p1 (l2 ) (l1 ) p2 Concurrent Separation Logic p1 (l2 ) p2 (l1 ) l1 .acq() l1 .rel() … p1 (l2 ) (l1 ) p2
