Concurrent programs are challenging to reason about due to their unpredictable behaviour. Even relatively simple concurrent programs can be difficult to reason about if their processes interfere a lot. Linearisability provides a way to verify the correctness of concurrent programs by analysing the observable states in a program's execution. If two consecutive states do not correspond to a valid step at the sequential level then the behaviour is considered non-linearisable.

The Treiber stack is a non-blocking concurrent stack algorithm, and a common example to motivate linearisability. Numerous techniques have been used to prove linearisability of the Treiber stack, however, describing its interference using the rely/guarantee approach remains a challenge. The rely/guarantee method reasons about concurrent systems in a compositional way by separating the program from its environment. In this method, the 'rely' condition represents the interference that can be tolerated from the environment, while the 'guarantee' condition defines the interference that the program will adhere to. A key step to finding suitable rely/guarantee conditions for the Treiber stack is to identify categories of invalid behaviour and ensure that the chosen conditions prevent these behaviours. Once suitable conditions are established, the rely/guarantee rules are used to prove that two processes can safely execute concurrently.

This presentation discusses the key ideas in the concepts of linearisability and rely/guarantee, identifies categories of invalid behaviour, and outlines the initial steps in the rely/guarantee proof for the Treiber stack.