Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings

TL;DR

This paper identifies counterexamples and a proof loophole in the assumed correctness of compiler mappings for C/C++ atomics on Power and ARMv7 architectures, highlighting potential memory model inconsistencies.

Contribution

It uncovers counterexamples and a loophole in the proof of trailing-sync mappings, challenging previous assumptions of their correctness.

Findings

Counterexamples show the mappings are not always correct.

A loophole in the proof was identified.

Implications for compiler correctness and architecture design.

Abstract

The C and C++ high-level languages provide programmers with atomic operations for writing high-performance concurrent code. At the assembly language level, C and C++ atomics get mapped down to individual instructions or combinations of instructions by compilers, depending on the ordering guarantees and synchronization instructions provided by the underlying architecture. These compiler mappings must uphold the ordering guarantees provided by C/C++ atomics or the compiled program will not behave according to the C/C++ memory model. In this paper we discuss two counterexamples to the well-known trailing-sync compiler mappings for the Power and ARMv7 architectures that were previously thought to be proven correct. In addition to the counterexamples, we discuss the loophole in the proof of the mappings that allowed the incorrect mappings to be proven correct. We also discuss the current state of compilers and architectures in relation to the bug.