TY - GEN
T1 - On atomicity in presence of non-atomic writes
AU - Enea, Constantin
AU - Farzan, Azadeh
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2016.
PY - 2016/1/1
Y1 - 2016/1/1
N2 - The inherently nondeterministic semantics of concurrent programs is the root of many programming errors. Atomicity (more precisely conflict serializability) has been used to reduce the magnitude of this nondeterminism and therefore make it easier to understand the behaviour of the concurrent program. Serializability, however, has not been studied well for programs executed under memory models weaker than sequential consistency (SC), where writes are not atomic, i.e., they may be committed to the main memory later than issued. In this paper, we define the notion of conflict serializability for the Total Store Ordering (TSO) memory model, and study the relation between TSO-serializability and the well-known notions of SC-serializability and robustness. We investigate the algorithmic problem of monitoring program executions for violations of serializability, and provide lower bound complexity results for the problem, and new algorithms to perform the monitoring efficiently.
AB - The inherently nondeterministic semantics of concurrent programs is the root of many programming errors. Atomicity (more precisely conflict serializability) has been used to reduce the magnitude of this nondeterminism and therefore make it easier to understand the behaviour of the concurrent program. Serializability, however, has not been studied well for programs executed under memory models weaker than sequential consistency (SC), where writes are not atomic, i.e., they may be committed to the main memory later than issued. In this paper, we define the notion of conflict serializability for the Total Store Ordering (TSO) memory model, and study the relation between TSO-serializability and the well-known notions of SC-serializability and robustness. We investigate the algorithmic problem of monitoring program executions for violations of serializability, and provide lower bound complexity results for the problem, and new algorithms to perform the monitoring efficiently.
UR - https://www.scopus.com/pages/publications/84964091202
U2 - 10.1007/978-3-662-49674-9_29
DO - 10.1007/978-3-662-49674-9_29
M3 - Conference contribution
AN - SCOPUS:84964091202
SN - 9783662496732
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 497
EP - 514
BT - Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings
A2 - Raskin, Jean-François
A2 - Chechik, Marsha
PB - Springer Verlag
T2 - 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2016 and held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
Y2 - 2 April 2016 through 8 April 2016
ER -