Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models (Extended Version)

TL;DR

This paper introduces a new theory for verifying thread optimizations in concurrent programs, focusing on thread states at synchronization points, which enables more optimizations and more efficient refinement checking.

Contribution

It formulates a novel theory based on thread states at synchronization, improving optimization support and refinement checking efficiency for the SC-for-DRF model.

Findings

Supports more thread optimizations

Enables more efficient refinement checking

Improves compiler testing performance

Abstract

When optimizing a thread in a concurrent program (either done manually or by the compiler), it must be guaranteed that the resulting thread is a refinement of the original thread. Most theories of valid optimizations are formulated in terms of valid syntactic transformations on the program code, or in terms of valid transformations on thread execution traces. We present a new theory formulated instead in terms of the state of threads at synchronization operations, and show that it provides several advantages: it supports more optimizations, and leads to more efficient and simpler procedures for refinement checking. We develop the theory for the SC-for-DRF execution model (using locks for synchronization), and show that its application in a compiler testing setting leads to large performance improvements.