uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Optimal stateless model checking for reads-from equivalence under sequential consistency
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.ORCID iD: 0000-0001-6832-6611
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.ORCID iD: 0000-0001-8229-3481
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Show others and affiliations
2019 (English)In: Proceedings of the ACM on programming languages, ISSN 2475-1421Article in journal (Refereed) Published
Abstract [en]

We present a new approach for stateless model checking (SMC) of multithreaded programs under Sequential Consistency (SC) semantics.  To combat state-space explosion, SMC is often equipped with a partial-order reduction technique, which defines an equivalence on executions, and only needs to explore one execution in each equivalence class.  Recently, it has been observed that the commonly used equivalence of Mazurkiewicz traces can be coarsened but still cover all program crashes and assertion violations.  However, for this coarser equivalence, which preserves only the reads-from relation from writes to reads, there is no SMC algorithm which is (i) optimal in the sense that it explores precisely one execution in each reads-from equivalence class, and (ii) efficient in the sense that it spends polynomial effort per class.  \end{inparaenum} We present the first SMC algorithm for SC that is both optimal and efficient in practice, meaning that it spends polynomial time per equivalence class on all programs that we have tried.  This is achieved by a novel test that checks whether a given reads-from relation can arise in some execution.  Our experimental results show that Nidhugg/rfsc, although slower than the fastest SMC tools in programs where tools happen to examine the same number of executions, always scales similarly or better than them, and outperforms them by an exponential factor in programs where the reads-from equivalence is coarser than the standard one. We also present two non-trivial use cases where the new equivalence is particularly effective, as well as the significant performance advantage that Nidhugg/rfsc offers compared to state-of-the-art SMC and systematic concurrency testing tools.

Place, publisher, year, edition, pages
2019.
Keywords [en]
concurrent programs, sequential consistency, program verification, stateless model checking, dynamic partial order reduction
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-396320DOI: 10.1145/3360576OAI: oai:DiVA.org:uu-396320DiVA, id: diva2:1367334
Available from: 2019-11-03 Created: 2019-11-03 Last updated: 2019-11-03

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full texthttps://dl.acm.org/citation.cfm?doid=3366395.3360576

Authority records BETA

Abdulla, ParoshAtig, Mohamed FaouziJonsson, BengtNgo, Tuan-PhongSagonas, Konstantinos

Search in DiVA

By author/editor
Abdulla, ParoshAtig, Mohamed FaouziJonsson, BengtNgo, Tuan-PhongSagonas, Konstantinos
By organisation
Computer SystemsComputing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 6 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf