Title: Using temporal logics for specifying weak memory consistency models

Authors: Maximilian Senftleben; Klaus Schneider

Addresses: Department of Computer Science, University of Kaiserslautern, Germany ' Department of Computer Science, University of Kaiserslautern, Germany

Abstract: 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.

Keywords: weak memory model; memory model; weak memory consistency; memory consistency; weak consistency; memory specification; specification; temporal logic; model checking; verification; LTL.

DOI: 10.1504/IJCCBS.2018.096187

International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.2, pp.214 - 229

Received: 11 Sep 2017
Accepted: 21 May 2018
Published online: 15 Nov 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article