Permission-Based Separation Logic for Message-Passing Concurrency

摘要

We develop local reasoning techniques for message passing concurrent programsbased on ideas from separation logics and resource usage analysis. We extendprocesses with permission- resources and define a reduction semantics for thisextended language. This provides a foundation for interpreting separationformulas for message-passing concurrency. We also define a sound proof systempermitting us to infer satisfaction compositionally using local,separation-based reasoning.