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 this work, we propose a technique that combines model checking and static analysis to analyse specifications of multi-threaded software. For a given weak memory architecture, it identifies a set of fences to be placed in the corresponding code produced by our code generator. This set guarantees that the resulting software will be sequentially consistent. In cases where fences are not sufficient, our technique suggests where to use stronger mechanisms, such as locking or the use of transactional memory. In comparison, static analysis techniques are less precise, and model checking techniques have worse scalability.

This is joint work with Sander de Putter.