Relaxed-memory concurrency and verified compilation

DOI10.1145/1926385.1926393zbMATH Open1284.68152OpenAlexW4247648759MaRDI QIDQ5408530FDOQ5408530

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

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

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)

Cited In (8)

• 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
• Verifying Optimizations for Concurrent Programs
• Lem: a lightweight tool for heavyweight semantics
• Effective Abstractions for Verification under Relaxed Memory Models

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)