Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Weak Memory Demands Model-based Compiler Testing

Luke Geeson

TL;DR

The paper addresses the risk of compiler bugs when concurrency semantics observed on relaxed hardware diverge from the source language model. It advocates model-based testing with tooling parameterized over source and architecture models, exemplified by the Téléchat tool and its use with a known LLVM bug revealed through updates to the herd memory model. The case study demonstrates a bug caused by LLVM's code generation and a dead-register optimization that makes an Arm SWP-based path appear to violate the C11 model, highlighting a new class of Heisenbugs. The work argues that testing practices and test generators must adapt to hardware relaxations and that automated industry-scale testing can uncover such issues, motivating broader adoption of model-aware testing.

Abstract

A compiler bug arises if the behaviour of a compiled concurrent program, as allowed by its architecture memory model, is not a behaviour permitted by the source program under its source model. One might reasonably think that most compiler bugs have been found in the decade since the introduction of the C/C++ memory model. We observe that processor implementations are increasingly exploiting the behaviour of relaxed architecture models. As such, compiled programs may exhibit bugs not seen on older hardware. To account for this we require model-based compiler testing. While this observation is not surprising, its implications are broad. Compilers and their testing tools will need to be updated to follow hardware relaxations, concurrent test generators will need to be improved, and assumptions of prior work will need revisiting. We explore these ideas using a compiler toolchain bug we reported in LLVM.

Weak Memory Demands Model-based Compiler Testing

TL;DR

The paper addresses the risk of compiler bugs when concurrency semantics observed on relaxed hardware diverge from the source language model. It advocates model-based testing with tooling parameterized over source and architecture models, exemplified by the Téléchat tool and its use with a known LLVM bug revealed through updates to the herd memory model. The case study demonstrates a bug caused by LLVM's code generation and a dead-register optimization that makes an Arm SWP-based path appear to violate the C11 model, highlighting a new class of Heisenbugs. The work argues that testing practices and test generators must adapt to hardware relaxations and that automated industry-scale testing can uncover such issues, motivating broader adoption of model-aware testing.

Abstract

A compiler bug arises if the behaviour of a compiled concurrent program, as allowed by its architecture memory model, is not a behaviour permitted by the source program under its source model. One might reasonably think that most compiler bugs have been found in the decade since the introduction of the C/C++ memory model. We observe that processor implementations are increasingly exploiting the behaviour of relaxed architecture models. As such, compiled programs may exhibit bugs not seen on older hardware. To account for this we require model-based compiler testing. While this observation is not surprising, its implications are broad. Compilers and their testing tools will need to be updated to follow hardware relaxations, concurrent test generators will need to be improved, and assumptions of prior work will need revisiting. We explore these ideas using a compiler toolchain bug we reported in LLVM.
Paper Structure (1 section, 6 figures)

This paper contains 1 section, 6 figures.

Table of Contents

  1. Introduction

Figures (6)

  • Figure 1: Message Passing Litmus Test. We reported swp this bug in LLVM's implementation of atomic_exchange. We found this using the Téléchat compiler testing tool.
  • Figure 2: Outcomes of running Fig. \ref{['exc']} under the C/C++ memory model C11. Note the absense of {P1:r0=0; y=2}.
  • Figure 3: Compiled version swp of Fig. \ref{['exc']}. Note the destination register of the SWPL is the zero register (WZR).
  • Figure 4: Outcomes of running Fig. \ref{['exc2']} under the Arm AArch64 model aarch64. Note the presence of {P1:r0=0; y=2}.
  • Figure 5: Compiled version of Fig. \ref{['exc']} (fixed). Note the destination register of the SWPL is not the zero register WZR, but rather register W15. We recommended this fix in our bug report swp.
  • ...and 1 more figures