On Rely-Guarantee Reasoning

8 years 6 days ago

Download ttic.uchicago.edu

Rely-Guarantee reasoning is a well-known method for veriﬁcation of shared-variable concurrent programs. However, it is diﬃcult for users to deﬁne rely/guarantee conditions, which specify threads’ behaviors over the whole program state. Recent eﬀorts 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 speciﬁed. This greatly limits the reuse of veriﬁed program modules. In this paper, we propose LRG, a new Rely-Guarantee-based logic that brings local reasoning and information hiding to concurrency veriﬁcation. Our logic, for the ﬁrst time, supports a frame rule over rely/guarantee conditions so that speciﬁcations of program modules only need to talk about the resources used locally, and the veriﬁed modules can be reused in diﬀerent threads without redoing the proof. Moreover, we introduce a new hiding rule to hide the resources shared by a subse...

Stephan van Staden

Real-time Traffic