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

DOI10.1007/978-3-031-37703-7_13zbMATH Open1545.68075MaRDI QIDQ6535538FDOQ6535538

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

Publication date: 12 January 2024

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

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)

Cites Work

• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Title not available (Why is that?)
• The Java memory model
• A Shared Memory Computer Display System
• Symbolic partial-order execution for testing multi-threaded programs

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)