Using temporal logics for specifying weak memory consistency models

摘要

The formal verification of multithreaded programs is not just more difficult due to the concurrent behaviours, but also due to the used underlying weak memory consistency models. Weak memory models arise from techniques like store buffering that were introduced to increase the performance. However, all of these techniques weaken the memory consistency, and may result in unintuitive behaviours where processors may disagree on the order in which write operations occurred. Requirements for verification are therefore unambiguous and complete specifications of such memory consistency models. In the past, specifications based on different formalisms have been presented which often lacked of comparability and the direct usability for model checking. In this paper, we therefore introduce the use of temporal logic to describe the behaviour of memory systems. In particular, we use linear temporal logic (LTL) to define the weak memory models. Thereby, we can easily check the properties of a multithreaded program against several different consistency models and determine the weakest consistency guarantees required to fulfil the given specification.