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