Local Data Race Freedom with Non-multi-copy Atomicity

DOI10.1007/978-3-319-94111-0_12MaRDI QIDQ5883581zbMATH OpenOpenAlexFDO

Authors Tatsuya Abe

Publication date 21 March 2023

Published in Model Checking Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-94111-0_12

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Data-race and concurrent-write freedom are undecidable.
• Dataflow analysis for datarace-free programs
• Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
• Java Memory Model-Aware Model Checking
• Non-preemptive semantics for data-race-free programs

Cites work

• Dynamic partial-order reduction for model checking software
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Observation-based concurrent program logic for relaxed memory consistency models
• Resources, concurrency, and local reasoning

Cited in

(4)

• Data-race and concurrent-write freedom are undecidable.
• Pointer race freedom
• Dataflow analysis for datarace-free programs
• Model checking race-freedom when ``sequential consistency for data-race-free programs is guaranteed

This page was built for publication: Local Data Race Freedom with Non-multi-copy Atomicity

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