The Release-Acquire ( \(\texttt{RA}\) ) semantics and its variants are some of the most fundamental models of concurrent semantics for architectures, programming languages, and distributed systems. Several steps have been taken in the direction of testing such semantics, where one is interested in whether a single program execution is consistent with a memory model. The more general verification problem, i.e., checking whether all allowed program runs are consistent with a memory model, has still not been studied as much. The purpose of this work is to bridge this gap. We tackle the verification problem, where, given an implementation described as a register machine, we check if any of its runs violates the . \({\texttt{RA}} \) semantics or its Strong (. \({\texttt{SRA}} \) ) and Weak (. \({\texttt{WRA}} \) ) variants. We show that verifying \({\texttt{WRA}} \) in this setup is in \(\mathcal {O}(n^5)\) , while verifying \({\texttt{RA}} \) and \({\texttt{SRA}} \) is both NP- and coNP-hard, and provide a PSPACE upper bound. This answers some fundamental questions about the complexity of these problems, and provides insights on the expressive power of register machines as a model.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Verification of the Release-Acquire Semantics

  • Parosh Aziz Abdulla,
  • Elli Anastasiadi,
  • Mohamed Faouzi Atig,
  • Samuel Grahn

摘要

The Release-Acquire ( \(\texttt{RA}\) ) semantics and its variants are some of the most fundamental models of concurrent semantics for architectures, programming languages, and distributed systems. Several steps have been taken in the direction of testing such semantics, where one is interested in whether a single program execution is consistent with a memory model. The more general verification problem, i.e., checking whether all allowed program runs are consistent with a memory model, has still not been studied as much. The purpose of this work is to bridge this gap. We tackle the verification problem, where, given an implementation described as a register machine, we check if any of its runs violates the . \({\texttt{RA}} \) semantics or its Strong (. \({\texttt{SRA}} \) ) and Weak (. \({\texttt{WRA}} \) ) variants. We show that verifying \({\texttt{WRA}} \) in this setup is in \(\mathcal {O}(n^5)\) , while verifying \({\texttt{RA}} \) and \({\texttt{SRA}} \) is both NP- and coNP-hard, and provide a PSPACE upper bound. This answers some fundamental questions about the complexity of these problems, and provides insights on the expressive power of register machines as a model.