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

semanticsrelaxed memory modelsverifying 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)

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

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)