The virtues of conflict: analysing modern concurrency

Conference/Journal
ACM
Authors
Ganesh Narayanaswamy Saurabh Joshi Daniel Kroening
BibTex
Abstract
Abstract Modern shared memory multiprocessors permit reordering of memory operations for performance reasons. These reorderings are often a source of subtle bugs in programs written for such architectures. Traditional approaches to verify weak memory programs often rely on interleaving semantics, which is prone to state space explosion, and thus severely limits the scalability of the analysis. In recent times, there has been a renewed interest in modelling dynamic executions of weak memory programs using partial orders. However, ...