Concurrent library correctness on the TSO memory model

Abstract. Linearizability is a commonly accepted notion of correctness for li-braries of concurrent algorithms. Unfortunately, it is only appropriate for se-quentially consistent memory models, while the hardware and software platforms that algorithms run on provide weaker consistency guarantees. In this paper, we present the first definition of linearizability on a weak memory model, Total Store Order (TSO), implemented by x86 processors. We establish that our definition is a correct one in the following sense: while proving a property of a client of a con-current library, we can soundly replace the library by its abstract implementation related to the original one by our generalisation of linearizability. This allows ab-stracting from the details of the library implementation while reasoning about the client. We have developed a tool for systematically testing concurrent libraries against our definition and applied it to several challenging algorithms.