Digitala Vetenskapliga Arkivet

Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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
Parsimonious Optimal Dynamic Partial Order Reduction
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, Division of 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. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.ORCID iD: 0000-0001-8229-3481
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.ORCID iD: 0009-0004-7029-1904
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. 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, Division of Computer Systems.ORCID iD: 0000-0001-7897-601X
Show others and affiliations
2024 (English)Conference paper, Published paper (Refereed)
Abstract [en]

Stateless model checking is a fully automatic verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It becomes eective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and reduces the amount of needed exploration. DPOR algorithms that are optimal are particularly effective in that they guarantee to explore exactly one execution from each equivalence class. Unfortunately, existing sequence-based optimal algorithms may in the worst case consume memory that is exponential in the size of the analyzed program. In this paper, we present Parsimonious-OPtimal DPOR (POP), an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency, whose space consumption is polynomial in the worst case. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race, (ii) an eager race reversal strategy to avoid storing initial fragments of to-be-explored executions, and (iii) a space-efficient scheme for preventing redundant exploration, which replaces the use of sleep sets. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption. Comparison to TruSt , a related optimal DPOR algorithm that represents executions as graphs, shows that POP ’s implementation achieves similar performance for smaller benchmarks, and scales much better than TruSt’s on programs with long executions.

Place, publisher, year, edition, pages
2024.
Keywords [en]
Concurrent Programs, Automated Testing, Stateless Model Checking, Dynamic Partial Order Reduction
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-553045OAI: oai:DiVA.org:uu-553045DiVA, id: diva2:1946337
Conference
arXiv
Funder
Swedish Research CouncilAvailable from: 2025-03-21 Created: 2025-03-21 Last updated: 2025-03-21Bibliographically approved

Open Access in DiVA

fulltext(364 kB)23 downloads
File information
File name FULLTEXT01.pdfFile size 364 kBChecksum SHA-512
1b94b8ef8586b6ad6c5221af73f8aec25058c0ed68b97d94a54ae9310ae7f7b8b74b87137b98f6c566fe93cdcec1bb7ed233cca1a02d954011aeca466b6f6e55
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Abdulla, ParoshAtig, Mohamed FaouziDas, SarbojitJonsson, BengtSagonas, Konstantinos
By organisation
Computer SystemsDivision of Computer SystemsComputing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 23 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 340 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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