Relaxed Operational Semantics of Concurrent Programming Languages

TL;DR

This paper introduces a new operational framework for modeling concurrent program semantics under relaxed memory models, incorporating a temporary store and write grain concepts, supported by a simulator for litmus tests.

Contribution

It presents a novel formal semantics framework for concurrent languages with relaxed memory models, including a simulator for testing and validation.

Findings

The framework accurately models relaxed memory behaviors.

The simulator successfully runs litmus tests to validate the semantics.

Provides a basis for analyzing concurrent program correctness under relaxed memory models.

Abstract

We propose a novel, operational framework to formally describe the semantics of concurrent programs running within the context of a relaxed memory model. Our framework features a "temporary store" where the memory operations issued by the threads are recorded, in program order. A memory model then specifies the conditions under which a pending operation from this sequence is allowed to be globally performed, possibly out of order. The memory model also involves a "write grain," accounting for architectures where a thread may read a write that is not yet globally visible. Our formal model is supported by a software simulator, allowing us to run litmus tests in our semantics.