Exploring the Boundaries of Rely/Guarantee and Links to Linearisability

Non-blocking concurrent algorithms are particularly challenging to verify. Linearisability is a commonly used technique for verifying such algorithms. Rely/guarantee reasoning provides a compositional approach for reasoning about concurrent systems. This paper explores the relationship between rely/guarantee and linearisability using two well-known examples: the Treiber stack and the Herlihy-Wing queue. Non-linearisable behaviour can be identified by the program making a step where the before and after states do not correspond to a valid step at the sequential level. Therefore, such invalid behaviour relates to a failure of the guarantee condition. The development of these two examples also provides useful insights into the boundaries of rely/guarantee, suggesting that these examples share common properties with another challenging problem, the Ben-Ari garbage collection algorithm studied by Jones and Yatapanage in [JY19].