An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models

Alexander Linden
Université de Liège
Friday, 17 December, 2010 - 16:00
NO Building Floor 5, Salle Solvay

In this talk, we consider the problem of verifying programs for the relaxed memory models implemented in modern processors. We first introduce memory models, starting with the classical sequential consistency model, and than moving to its relaxations, in particular the TSO (Total Store Order) relaxation. The proposed verification approach uses an operational store-buffer based semantics of the chosen relaxed memory model and proceeds by using finite automata for symbolically representing the possible contents of the buffers. Store, load, commit and other synchronization operations then correspond to operations on these finite automata. The advantage of this approach is that it operates on (potentially infinite) sets of buffer contents, rather than on individual buffer configurations. This provides a way to tame the explosion of the number of possible buffer configurations, while preserving the full generality of the analysis. It is thus possible to check even designs that exploit the relaxed memory model in unusual ways. An experimental implementation has been used to validate the feasibility of the approach.