Explaining relaxed memory models with program transformations

DOI10.1007/978-3-319-48989-6_29MaRDI QIDQ2281648zbMATH OpenOpenAlexFDO

Authors Ori Lahav, Viktor Vafeiadis

Publication date 3 January 2020

Full work available at URL http://hdl.handle.net/11858/00-001M-0000-002C-EBF9-6

Mathematics Subject Classification ID

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

Recommendations

• Effective Program Verification for Relaxed Memory Models
• Software verification for weak memory via program transformation
• Compositional verification of compiler optimisations on relaxed memory
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Publication:3490929

Cited in

(7)

• Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP
• Automatic Memory Management Based on Program Transformation Using Ownership
• CCA-secure keyed-fully homomorphic encryption
• Common compiler optimisations are invalid in the C11 memory model and what we can do about it
• A load-buffer semantics for total store ordering
• Parallelized sequential composition and hardware weak memory models
• Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models

This page was built for publication: Explaining relaxed memory models with program transformations

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