A wide-spectrum language for verification of programs on weak memory models

TL;DR

This paper introduces a comprehensive language and semantics for verifying programs under weak memory models, enabling reasoning about correctness of data structures and low-level code on modern processors.

Contribution

It develops a wide-spectrum language with operational semantics for weak memory models, and implements a model-checking tool to validate program behaviors against hardware and specifications.

Findings

Validated semantics with hardware litmus tests

Successfully model-checked data structure implementations

Provided a framework for reasoning about weak memory behaviors

Abstract

Modern processors deploy a variety of weak memory models, which for efficiency reasons may (appear to) execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be complex and subtle, and can impact on ensuring correctness. Previous work on the semantics of weak memory models has focussed on the behaviour of assembler-level programs. In this paper we utilise that work to extract some general principles underlying instruction reordering, and apply those principles to a wide-spectrum language encompassing abstract data types as well as low-level assembler code. The goal is to support reasoning about implementations of data structures for modern processors with respect to an abstract specification. Specifically, we define an operational semantics, from which we derive some properties of program refinement, and encode the semantics in the rewriting engine Maude as a model-checking tool. The tool is used to validate the semantics against the behaviour of a set of litmus tests (small assembler programs) run on hardware, and also to model check implementations of data structures from the literature against their abstract specifications.