Fences in weak memory models

DOI10.1007/s10703-011-0135-zzbMath1247.68155OpenAlexW2066615989MaRDI QIDQ453523

Susmit Sarkar, Jade Alglave, Luc Maranget, 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

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

Related Items (4)

Model Checking Concurrent Programs ⋮ A formal hierarchy of weak memory models ⋮ Fences in weak memory models ⋮ An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model

Uses Software

• Coq
• TSOTool
• UMM

Cites Work

• Fences in weak memory models
• Effective Program Verification for Relaxed Memory Models
• The Java memory model
• Unnamed Item

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