Local rely-guarantee reasoning

Author:
Open Access
Publisher website
Google Scholar
Abstract
Rely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs. However, it is difficult for users to define rely/guarantee conditions, which specify threads' behaviors over the whole program state. Recent efforts to combine Separation Logic with Rely-Guarantee reasoning have made it pos- sible to hide thread-local resources, but the shared resources still need to be globally known and specified. This greatly limits the reuse of verified program modules. In this paper, we propose LRG, a new Rely-Guarantee-based logic that brings local reasoning and information hiding to concur- rency verification. Our logic, for the first time, supports a frame rule over rely/guarantee conditions so that specifications of pro- gram modules only need to talk about the resources used locally, and the verified modules can be reused in different threads with- out redoing the proof. Moreover, we introduce a new hiding rule to hide the resources shared by a subset of threads from the rest in the system. The support of information hiding not only improves the modularity of Rely-Guarantee reasoning, but also enables the shar- ing of dynamically allocated resources, which requires adjustment of rely/guarantee conditions.

This publication has 17 references indexed in Scilit: