Fences in weak memory models

DOI10.1007/S10703-011-0135-ZMaRDI QIDQ453523zbMATH OpenOpenAlexFDO

Authors Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell

Publication date 27 September 2012

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-011-0135-z

zbMATH Keywords

formal proofsfencesgeneric frameworkpowerPCtesting toolweak memory models

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Computer system organization (68M99)

Recommendations

• Trading fences with RMRs and separating memory models
• A formal hierarchy of weak memory models
• On the verification problem for weak memory models
• Owicki-Gries reasoning for weak memory models
• Compartment Models with Memory
• A framework for correctness criteria on weak memory models

Cites work

• scientific article; zbMATH DE number 107700 (Why is no real title available?)
• Effective Program Verification for Relaxed Memory Models
• Fences in weak memory models
• The Java memory model

Cited in

(11)

• A formal hierarchy of weak memory models
• Taming release-acquire consistency
• Model checking concurrent programs
• Mending fences with self-invalidation and self-downgrade
• Trading fences with RMRs and separating memory models
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• Abstract semantic dependency
• A program logic for C11 memory fences
• Fences in weak memory models
• Overhauling SC atomics in C11 and OpenCL
• Brief announcement: Fence insertion for straight-line programs is in P

Describes a project that uses

Uses Software

• Coq
• TSOTool
• UMM

This page was built for publication: Fences in weak memory models

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