Automatic Fence Insertion in Integer Programs via Predicate Abstraction

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine

We propose an automatic fence insertion and verification framework for concurrent programs running under relaxed memory. Unlike previous ap- proaches to this problem, which allow only variables of finite domain, we target programs with (unbounded) integer variables. The problem is difficult because it has two different sources of infiniteness: unbounded store buffers and unbounded integer variables. Our framework consists of three main components: (1) a fi- nite abstraction technique for the store buffers, (2) a finite abstraction technique for the integer variables, and (3) a counterexample guided abstraction refinement loop of the model obtained from the combination of the two abstraction tech- niques. We have implemented a prototype based on the framework and run it successfully on all standard benchmarks together with several challenging exam- ples that are beyond the applicability of existing methods.

In Proceedings of the 19th International Static Analysis Symposium, 2012

Last version (pdf) 2012