Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Predicate Abstraction For Relaxed Memory Models
event speaker icon
Yuri Meshman (M.Sc. Thesis Seminar)
event date icon
Tuesday, 17.12.2013, 10:30
event location icon
Taub 601
event speaker icon
Advisor: Prof. E. Yahav
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.