An axiomatic specification for sequential memory models

DOI10.1007/978-3-319-21668-3_24MaRDI QIDQ1702905zbMATH OpenOpenAlexFDO

Authors William Mansky, Dmitri Garbuzov, Steve Zdancewic

Publication date 1 March 2018

Full work available at URL https://doi.org/10.1007/978-3-319-21668-3_24

zbMATH Keywords

memory modelsoptimizing compilersdeep specifications

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Relaxed memory models
• A formal hierarchy of weak memory models
• Parameterized Memory Models and Concurrent Separation Logic
• Studying Operational Models of Relaxed Concurrency
• scientific article; zbMATH DE number 1951189

Cited in

(2)

• A calculus for attribute-based memory updates
• A verified specification of TLSF memory management allocator using state monads

This page was built for publication: An axiomatic specification for sequential memory models

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