Compositional reasoning advances verify complex concurrent algorithms
The Complexity of Interference: When Rely/Guarantee Does Not Work
Logic in Computer Science
Summary
Some computer programs run multiple parts at the same time, which can make checking if they work correctly very hard. The rely/guarantee method is a popular way to do this but struggles with some complicated programs because their parts interfere too much. The paper looks at a specific example, a concurrent garbage collector, and shows a new way to verify it by focusing on properties shared by all instances of a variable. This new approach breaks down complex interactions into simpler parts, making it easier to understand why the program works even when the usual method fails.
What this means in practice
- •For software verification teams: Check correctness of complex concurrent algorithms that resist traditional rely/guarantee verification methods.
- •For concurrent system developers: Design more reliable concurrent systems by understanding core properties needed for correct component interactions.
Authors
Nisansala P. Yatapanage
Abstract
Rely/Guarantee is a well-known verification technique for reasoning about concurrent programs. However, for some algorithms, devising suitable rely and guarantee conditions is challenging, due to the strong interference exhibited in these algorithms. The Ben-Ari concurrent garbage collector is an algorithm where the complex interactions between the components prevent the construction of compositional rely and guarantee conditions. This paper investigates an approach for verifying the Ben-Ari algorithm, which enables reasoning to be performed in a more compositional manner in cases where compositional reasoning would not otherwise be possible. This is accomplished by reasoning that a given property holds for all instances of a particular variable and then instantiating the variable to the local variable required. As well as providing a reasoning approach which is more compositional, the result is the identification of the core property required of a component, thus enabling a deeper understanding about the reasons why the algorithm works correctly. This helps to reveal the reasons why the rely/guarantee approach does not work directly for some problems.