Local Rely-Guarantee Reasoning
Authors
Xinyu Feng
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 possible 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 concurrency verification.
Our logic, for the first time, supports a frame rule over rely/guarantee
conditions so that specifications of program modules only need to talk
about the resources used locally, and the verified modules can be reused
in different threads without 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 sharing of dynamically allocated resources, which requires adjustment
of rely/guarantee conditions.
Published
Copyright © 2008 Xinyu Feng
|