TY - GEN
T1 - Boosting Sequential Consistency Checking Using Saturation
AU - Zennou, Rachid
AU - Atig, Mohamed Faouzi
AU - Biswas, Ranadeep
AU - Bouajjani, Ahmed
AU - Enea, Constantin
AU - Erradi, Mohammed
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020/1/1
Y1 - 2020/1/1
N2 - We address the problem of checking that an execution of a shared memory concurrent program is sequentially consistent (SC). This problem is NP-hard due to the necessity of finding a total order between the write operations that induces an acyclic happen-before relation. We propose an approach allowing to avoid falling systematically in the worst case, and to check SCness in polynomial-time in most cases in practice. The approach is based on a simple yet powerful saturation-based procedure for computing write constraints that must hold for SCness, allowing on one hand fast detection of SC violations, and on the other hand reducing drastically the search space for a total order witnessing SCness.
AB - We address the problem of checking that an execution of a shared memory concurrent program is sequentially consistent (SC). This problem is NP-hard due to the necessity of finding a total order between the write operations that induces an acyclic happen-before relation. We propose an approach allowing to avoid falling systematically in the worst case, and to check SCness in polynomial-time in most cases in practice. The approach is based on a simple yet powerful saturation-based procedure for computing write constraints that must hold for SCness, allowing on one hand fast detection of SC violations, and on the other hand reducing drastically the search space for a total order witnessing SCness.
UR - https://www.scopus.com/pages/publications/85093860805
U2 - 10.1007/978-3-030-59152-6_20
DO - 10.1007/978-3-030-59152-6_20
M3 - Conference contribution
AN - SCOPUS:85093860805
SN - 9783030591519
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 360
EP - 376
BT - Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
A2 - Hung, Dang Van
A2 - Sokolsky, Oleg
PB - Springer Science and Business Media Deutschland GmbH
T2 - 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020
Y2 - 19 October 2020 through 23 October 2020
ER -