A Certified Data Race Analysis for a Java-like Language
From MaRDI portal
Recommendations
- Formalising Java’s Data Race Free Guarantee
- Java and the Java memory model -- a unified, machine-checked formalisation
- A shared-variable concurrency analysis of multi-threaded object-oriented programs
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Conditional must not aliasing for static race detection
Cites work
- Conditional must not aliasing for static race detection
- Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors
- Extracting a data flow analyser in constructive logic
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Formalising Java’s Data Race Free Guarantee
- Oracle Semantics for Concurrent Separation Logic
- The Java memory model
Cited in
(7)- Checking data-race freedom of GPU kernels, compositionally
- Dynamic inference of polymorphic lock types
- Formalising Java’s Data Race Free Guarantee
- Memory access protocols: certified data-race freedom for GPU kernels
- scientific article; zbMATH DE number 1728452 (Why is no real title available?)
- Associating synchronization constraints with data in an object-oriented language
- Conditional must not aliasing for static race detection
Describes a project that uses
Uses Software
This page was built for publication: A Certified Data Race Analysis for a Java-like Language
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183531)
