Counter-Example Guided Fence Insertion under TSO

DOI10.1007/978-3-642-28756-5_15MaRDI QIDQ2894272zbMATH OpenOpenAlexFDO

Authors Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine, Parosh A. Abdulla

Publication date 29 June 2012

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28756-5_15

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Polynomial-time fence insertion for structured programs
• scientific article; zbMATH DE number 2038762
• A simplified adaptive fence procedure

Cited in

(15)

• Stateless model checking for TSO and PSO
• Trading fences with RMRs and separating memory models
• CCA-secure keyed-fully homomorphic encryption
• Mending fences with self-invalidation and self-downgrade
• A load-buffer semantics for total store ordering
• Verification of Concurrent Programs on Weak Memory Models
• Context-bounded analysis of TSO systems
• View abstraction -- a tutorial (invited paper)
• Checking and enforcing robustness against TSO
• A verification-based approach to memory fence insertion in PSO memory systems
• Brief announcement: Fence insertion for straight-line programs is in P
• Polynomial-time fence insertion for structured programs
• TSO games -- on the decidability of safety games under the total store order semantics
• Reachability and safety games under TSO semantics
• TSO games -- on the decidability of safety games under the total store order semantics

Describes a project that uses

Uses Software

• Checkfence

This page was built for publication: Counter-Example Guided Fence Insertion under TSO

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