Predicate abstraction for relaxed memory models

30Citations
Citations of this article
12Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We present a novel approach for predicate abstraction of programs running on relaxed memory models. Our approach consists of two steps. First, we reduce the problem of verifying a program P running on a memory model M to the problem of verifying a program PM that captures an abstraction of M as part of the program. Second, we present a new technique for discovering predicates that enable verification of PM. The core idea is to extrapolate from the predicates used to verify P under sequential consistency. A key new concept is that of cube extrapolation: it successfully avoids exponential state explosion when abstracting PM. We implemented our approach for the x86 TSO and PSO memory models and showed that predicates discovered via extrapolation are powerful enough to verify several challenging concurrent programs. This is the first time some of these programs have been verified for a model as relaxed as PSO. © 2013 Springer-Verlag.

Cite

CITATION STYLE

APA

Dan, A. M., Meshman, Y., Vechev, M., & Yahav, E. (2013). Predicate abstraction for relaxed memory models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7935 LNCS, pp. 84–104). https://doi.org/10.1007/978-3-642-38856-9_7

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free