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...

Probabilistic Testing for Weak Memory Concurrency

The Probabilistic Concurrency Testing (PCT) algorithm provides theoretical guarantees for the probability of detecting concurrency bugs in a sequential consistency memory model, but its theoretical guarantees do not apply to weak memory concurrency. The weak memory concurrency refers to the modern compiler’s optimization that relaxes the...

Parameterized Verification under Release Acquire is PSPACE-complete

We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. In the non-parameterized setting, access to atomic compare-and-swap (CAS) instructions renders the safety verification problem undecidable. In the light of this result, we consider parameterized systems consisting of an unbounded...

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...