Observational models for linearizability checking on weak memory models

Weak memory models are used to increase the performance of concurrent programs by allowing program instructions to be executed on the hardware in a different order to that specified by the software. This places a challenge on the verification of concurrent programs running on weak memory models since the variations in the executions need to be considered.Many approaches of modelling weak memory behaviour focus on architectural models to capture aspects of the hardware's architecture. In this paper, we investigate observational models of weak memory model behaviour which abstract from the underlying hardware architecture, and are instead derived from instruction reordering rules. This enables existing proof methods and tool support for linearizability to be reused. Specifically, we show how one existing proof method and associated model checking approach can be used to reason about programs running on the TSO and XC weak memory models