Linköping University: Students Alumni Trade and Industry/Society Internal Search
ahmre_SAS12

Automatic Fence Insertion in Integer Programs via Predicate Abstraction

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

19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012.

ABSTRACT
We propose an automatic fence insertion and verification framework for concurrent programs running under relaxed memory. Unlike previous approaches 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 finite 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 techniques. We have implemented a prototype based on the framework and run it successfully on all standard benchmarks together with several challenging examples that are beyond the applicability of existing methods.


Related files:
ahmre_SAS12.pdfAdobe Acrobat portable document


[AFCL12] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine, "Automatic Fence Insertion in Integer Programs via Predicate Abstraction", 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)