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

fencesformal proofsgeneric frameworkpowerPCtesting toolweak memory models

Mathematics Subject Classification ID

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

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

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

Cited in

(11)

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

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)