Explicit Stabilisation for Modular Rely-Guarantee Reasoning

Abstract. We propose a new formalisation of stability for Rely-Guarantee, in which an assertion's stability is encoded into its syntactic form. This allows two advances in modular reasoning. Firstly, it enables RelyGuarantee, for the first time, to verify concurrent libraries independently of their clients' environments. Secondly, in a sequential setting, it allows a module's internal interference to be hidden while verifying its clients. We demonstrate our approach by verifying, using RGSep, the Version 7 Unix memory manager, uncovering a twenty-year-old bug in the process.

• Type: Conference
• Year: 2010
• Where: ESOP
• Authors: John Wickerson, Matthew J. Parkinson, Mike Dodds
• Keywords: ESOP 2010, Module's Internal Interference, Programming Languages, Twenty-year-old Bug, Unix Memory Manager