The Taub Faculty of Computer Science Events and Talks

In this talk 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 P_M that captures an abstraction of M as part of the program. Second, we show how to discover new predicates that enable verification of P_M. 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 explosion when abstracting P_M. 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. We show that our cube extrapolation approach introduces a x100 reduction in the number of SMT calls for several programs, enabling their verification. This is the first time some of these programs have been verified for a model as relaxed as PSO.