Robustness against Power is PSpace-complete

DOI10.1007/978-3-662-43951-7_14MaRDI QIDQ5167835zbMATH OpenOpenAlexFDO

Authors Egor Derevenetc, Roland Meyer

Publication date 1 July 2014

Published in Automata, Languages, and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1404.7092

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Formal languages and automata (68Q45)

Abstract: Power is a RISC architecture developed by IBM, Freescale, and several other companies and implemented in a series of POWER processors. The architecture features a relaxed memory model providing very weak guarantees with respect to the ordering and atomicity of memory accesses. Due to these weaknesses, some programs that are correct under sequential consistency (SC) show undesirable effects when run under Power. We call these programs not robust against the Power memory model. Formally, a program is robust if every computation under Power has the same data and control dependencies as some SC computation. Our contribution is a decision procedure for robustness of concurrent programs against the Power memory model. It is based on three ideas. First, we reformulate robustness in terms of the acyclicity of a happens-before relation. Second, we prove that among the computations with cyclic happens-before relation there is one in a certain normal form. Finally, we reduce the existence of such a normal-form computation to a language emptiness problem. Altogether, this yields a PSPACE algorithm for checking robustness against Power. We complement it by a matching lower bound to show PSPACE-completeness.

Recommendations

• Deciding Robustness against Total Store Ordering
• Checking and enforcing robustness against TSO
• On the verification problem for weak memory models
• Reasoning about TSO programs using reduction and abstraction
• Capturing Register and Control Dependence in Memory Consistency Models with Applications to the Itanium Architecture

Cited in

(9)

• Checking robustness between weak transactional consistency models
• Robustness of PSPACE-complete sets
• CCA-secure keyed-fully homomorphic encryption
• A theory of partitioned global address spaces
• Tackling real-life relaxed concurrency with FSL++
• A load-buffer semantics for total store ordering
• Checking and enforcing robustness against TSO
• scientific article; zbMATH DE number 7327945 (Why is no real title available?)
• Robustness Against Transactional Causal Consistency.

This page was built for publication: Robustness against Power is PSpace-complete

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