How Hard Is Weak-Memory Testing?

Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is consistency testing: is the observed execution of a concurrent program in alignment with the specification of the underlying system? The problem has been studied...

Optimal Reads-From Consistency Checking for C11-Style Memory Models

Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++. One of the most fundamental problems associated with a memory model M is consistency checking: given an execution X, is X consistent with M? This problem lies at the heart of numerous applications, including specification testing and...

Fencing off unwanted behavior: Improving and evaluating the Fency static analysis tool

Computer architectures with weak memory models, such as ARMv8 and ARMv7, allow memory accesses to be reordered in many situations.<br/>Therefore, weak memory models may cause a program to exhibit more behavior than a strong memory model, such as x86.<br/>Fency is a static analysis tool that inserts memory fences to ensure that a program exhibits...

Robustness between Weak Memory Models

Robustness of a concurrent program ensures that its behaviors on a weak concurrency model are indistinguishable from those on a stronger model. Enforcing robustness is particularly useful when porting or migrating applications between architectures. Existing tools mostly focus on ensuring sequential consistency (SC) robustness which is a...