Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion

When targeting modern parallel hardware architectures, constructing correct and high-performing software is complex and time-consuming. In particular, reorderings of memory accesses that violate intended sequentially consistent behaviour are a major source of bugs. Applying synchronisation mechanisms to repair these should be done sparingly, as they negatively impact performance. In the past, both static analysis approaches and techniques based on explicit-state model checking have been proposed to identify where synchronisation fences have to be placed in a program. The former are fast, but the latter more precise, as they tend to insert fewer fences. Unfortunately, the model checking techniques suffer a form of state space explosion that is even worse than the traditional one. In this work, we propose a technique using a combination of state space exploration and static analysis. This combination is in terms of precision comparable to purely model checking-based techniques, but it reduces the state space explosion problem to the one typically seen in model checking. Furthermore, experiments show that the combination frequently outperforms both purely model checking and static analysis techniques. In addition, we have added the capability to check for atomicity violations, which is another major source of bugs.