Lock correctness

Locks are a frequently used synchronisation mechanism in shared memory concurrent programs. They are used to enforce atomicity of certain code portions, avoid undefined behaviour due to data races, and hide weak memory effects of the underlying hardware architectures (i.e., they provide the illusion of interleaved execution). To provide these guarantees, the correct interplay of a number of subsystems is required. We distinguish between the application level, the transformation level, and the hardware level. On the application level, the programmer is required to correctly use the locks. This amounts to avoiding data races, deadlocks, and other errors in using the locking primitives, such as unlocking a lock that is not currently held. On the transformation level, the compiler needs to correctly optimise the program and correctly map its operations to machine code. This requires knowing, for example, when it is safe to move a code statement in a thread past a lock operation such that the resulting thread is a refinement of the original thread. On the hardware level, the lock operations themselves need to be implemented correctly, by usage of low-level primitives such as memory fences and read-modifywrite operations. This requires knowing the relaxations of memory ordering that could occur on the target hardware, and the effect of the primitives that can be used to restore consistency (such as memory fences). In this thesis, we address an aspect of each of the three levels of correctness mentioned above. On the application level, we provide a sound static approach for deadlock analysis of C/Pthreads programs. The approach is based on a contextand thread-sensitive abstract interpretation framework, and uses a lightweight dependency analysis to identify statements relevant to deadlock analysis. To quantify scalability, we have applied our approach to a large number of concurrent programs from the Debian GNU/Linux distribution. On the transformation level, we provide a new theory of refinement between threads, which is phrased in terms of state transitions between lock operations. We show that the theory is more precise than existing approaches, and that its application in a compiler testing setting leads to large performance gains compared to a previous approach. On the hardware level, we provide a toolchain to test the memory model of GPUs and the behaviour of code running on them. We automatically generate short concurrent code snippets that, when run on hardware, reveal interesting properties about the underlying memory model. These code snippets include idioms that typically appear in implementations of synchronisation operations. We further manually test several GPU locking primitives. Our testing has revealed surprising hardware behaviours and bugs in lock implementations.