Example:List T={I→List(X)} getNode(): -emp} 1.acq(); y一 -emp List(x)}; 日日 {Node(y)List(x)} L.rel(); Node(y)}
Example: List x = { … l List(x) } getNode(): l.acq(); … l.rel(); -{emp} -{emp * List(x)}; -{Node(y) * List(x)} -{Node(y)} x … y
Concurrent Separation Logic ·Thread modularity r(p}c (a} Data modularity by local reasoning do not need knowledge of other threads'data Ownership transfer is bound with CRs requires built-in critical regions hard to support ad-hoc synchronizations
Concurrent Separation Logic • Thread modularity • Data modularity by local reasoning – do not need knowledge of other threads’ data Ownership transfer is bound with CRs – requires built-in critical regions – hard to support ad-hoc synchronizations ┝ {p} C {q}
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
Assume-Guarantee Reasoning Thread T and its environment Environment:the collection of all other threads except T A:assumption about environment's transition G:guarantee to the environment 。a:precondition
Assume-Guarantee Reasoning • Thread T and its environment – Environment: the collection of all other threads except T • A: assumption about environment’s transition • G: guarantee to the environment • a: precondition