Fences in weak memory models

DOI10.1007/S10703-011-0135-ZzbMATH Open1247.68155OpenAlexW2066615989MaRDI QIDQ453523FDOQ453523

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

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

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)

Cites Work

• Effective Program Verification for Relaxed Memory Models
• Title not available (Why is that?)
• Fences in weak memory models
• The Java memory model

Cited In (11)

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

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)