Relaxed-memory concurrency and verified compilation

DOI10.1145/1926385.1926393MaRDI QIDQ5408530zbMATH OpenOpenAlexFDO

Authors Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1926385.1926393

zbMATH Keywords

relaxed memory modelssemanticsverifying compilation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• CompCertTSO
• Verified Compilation for Shared-Memory C
• Verifying optimizations for concurrent programs
• A promising semantics for relaxed-memory concurrency
• Effective Abstractions for Verification under Relaxed Memory Models

Cited in

(10)

• Compositional verification of compiler optimisations on relaxed memory
• Possible values: exploring a concept for concurrency
• Lem: a lightweight tool for heavyweight semantics
• Effective Abstractions for Verification under Relaxed Memory Models
• Verifying optimizations for concurrent programs
• Verified just-in-time compiler on x86
• CompCertTSO
• Mathematizing C++ concurrency
• Verified Compilation for Shared-Memory C
• Computer Algebra in Scientific Computing

This page was built for publication: Relaxed-memory concurrency and verified compilation

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