Boosting Sequential Consistency Checking Using Saturation

TitreBoosting Sequential Consistency Checking Using Saturation
Publication TypeJournal Article
Year of Publication2020
AuthorsZennou, R, Atig, MF, Biswas, R, Bouajjani, A, Enea, C, Erradi, M
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12302 LNCS
Mots-clésConcurrent program, Fast detections, NP-hard, Polynomial approximation, Polynomial-time, Search spaces, Sequential consistency, Shared memory, Total order, Write operations

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. © 2020, Springer Nature Switzerland AG.




Suivez-nous sur





Avenue Mohammed Ben Abdallah Regragui, Madinat Al Irfane, BP 713, Agdal Rabat, Maroc

  Télécopie : (+212) 5 37 68 60 78

  Secrétariat de direction : 06 61 48 10 97

        Secrétariat général : 06 61 34 09 27

        Service des affaires financières : 06 61 44 76 79

        Service des affaires estudiantines : 06 62 77 10 17 /

        Résidences : 06 61 82 89 77



Education - This is a contributing Drupal Theme
Design by WeebPal.