Model checking race-freedom when ``sequential consistency for data-race-free programs is guaranteed

DOI10.1007/978-3-031-37703-7_13MaRDI QIDQ6535538zbMATH OpenFDO

Authors Wenhao Wu, Jan Hückelheim, Paul D. Hovland, Ziqing Luo, Stephen F. Siegel

Publication date 12 January 2024

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

model checkingOpenMPdata race

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Java Memory Model-Aware Model Checking
• Data-race and concurrent-write freedom are undecidable.
• Local Data Race Freedom with Non-multi-copy Atomicity
• Dataflow analysis for datarace-free programs
• Sound and complete monitoring of sequential consistency for relaxed memory models

Cites work

• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• A Shared Memory Computer Display System
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Symbolic partial-order execution for testing multi-threaded programs
• The Java memory model

This page was built for publication: Model checking race-freedom when ``sequential consistency for data-race-free programs is guaranteed

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535538)