Synthesis of memory fences via refinement propagation

Abstract. We address the problem of fence inference in infinite-state concur-rent programs running on relaxed memory models such as TSO and PSO. We present a novel algorithm that can automatically synthesize the necessary fences for infinite-state programs. Our technique is based on two main ideas: (i) verification with numerical do-mains: we reduce verification under relaxed models to verification under sequen-tial consistency using integer and boolean variables. This enables us to combine abstraction refinement over booleans with powerful numerical abstractions over the integers. (ii) synthesis with refinement propagation: to synthesize fences for a program P, we combine abstraction refinements used for successful synthesis of programs coarser than P into a new candidate abstraction for P. This “proof reuse ” approach dramatically reduces the time required to discover a proof for P. We implemented our technique and successfully applied it to several challenging concurrent algorithms, including state of the art concurrent work-stealing queues.