Abstract: Weak memory adds many behaviors in a concurrent program that are unexpected by the most programmers. The weak memory behaviors can be removed by placing memory fences in the programs. For performance, one should only add minimal number of fences such that there are no unwanted behaviors. In this paper, we present a novel method for synthesizing fences that disallow behaviors that are due to week memory and violate a safety property of a straight line concurrent program. Our method constructs a formula that encodes all violating executions of the program under weak memory and iteratively constructs a happens-before formula over memory events that represents memory event orderings that leads to error for some inputs. Afterwards, our method searches for event cycles encoded in the formula and optimally introduces fences such that the cycles are removed from the program behavior. We have implemented the above method in Tara. Our tool supports TSO, PSO, and RMO memory models. We applied Tara on benchmarks, and compared the performance with fence synthesis tools Glue and Memorax.
