Skip to main content
Department of Information Technology

Dual Semantics for Total Store Order

Speaker:
Parosh Abdulla

Date and Time
Friday, March 24th, 2017 at 14:15.

Location
Polacksbacken, ITC, room 1145.

Abstract
Modelling the behaviors of concurrent programs has traditionally relied on a fundamental assumption, namely that of Sequential Consistency (SC). Under the SC semantics, an instruction performed by a process will become immediately visible to all the other processes in the system. However, recent developments in system design imply that the SC semantics is no longer valid. For instance, modern computer architectures such as TSO, POWER, and ARM, allow the re-ordering of program instructions in order to gain efficiency and limit power consumption. Geo-replicated systems allow application programs on different nodes to execute autonomously so that the system can survive data-center failures, and so that services move closer to end users. The emergence of such *weakly consistent* systems calls for a new generation of methods and tools for the modelling, analysis, and verification of programs.

The study of weakly consistent systems is one of the main research challenges currently addressed by the algorithmic verification group. In this lecture, I will illustrate some of the problems that arise in this context, and give examples of potential solutions through our recent work on the verification of concurrent programs running under the classical TSO (Total Store Order) memory model. The model allows "write to read" relaxation corresponding to the addition of an unbounded store buffer (that contains pending store operations) between each processor and the main memory. In this work, we introduce a novel semantics which we call the *dual TSO semantics* that replaces each store buffer by a *load buffer* that contains pending load operations. The flow of information is also reversed, i.e., store operations are performed by the processes atomically on the main memory, while values of variables are propagated from the memory to the load buffers of the processes. We show that the two semantics are equivalent in the sense that a program will reach identical sets of states when run under the two semantics. Furthermore, we present a simple and effective reachability algorithm for checking safety properties of programs running under the dual semantics.

Finally, I will describe a few directions for future work, including the verification of TSO-coherence (e.g., for cache protocols), and the challenges we face when considering more general forms of weak consistence than the one induced TSO.

The seminar will be self-contained and accessible even to people with no background in program verification. Joint work with Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo.

Back to the seminar page

Updated  2017-03-16 11:26:06 by Philipp Rümmer.