Effective abstractions for verification under relaxed memory models

摘要

We present a new abstract interpretation based approach for automatically verifying concurrent programs running on relaxed memory models. Our approach is based on three key insights: (i) Although the behaviors of relaxed memory models (e.g., TSO and PSO) are naturally captured by store buffers, directly using such encodings substantially decreases the accuracy of program analysis due to shift operations on buffer contents. The scalability and accuracy of program analysis can be greatly improved by eliminating the expensive shifting of store buffer contents, and we present a new abstraction of the memory model that accomplishes this goal. (ii) The precision of the analysis can be further improved by an encoding of store buffer sizes using leveraged knowledge of the abstract interpretation domain. (iii) A novel source-to-source transformation that realizes the above two techniques makes it possible to use of state-of-the-art analyzers directly under sequential consistency (SC): given a program P and a relaxed memory model M, it produces a new program PM where the behaviors of P running on M are over-approximated by the behavior of PM running on SC.