The meaning of concurrent programs

TL;DR

This paper explores the semantics of assignment and mutual exclusion in concurrent systems, emphasizing low-level architectural details to enhance realism and using recursive functions on event sequences for defining state-dependent functions.

Contribution

It introduces a realistic semantic framework for concurrent programs that incorporates low-level architectural features and employs recursive functions on event sequences.

Findings

Provides a detailed semantic model for assignment and mutual exclusion.

Uses recursive functions to define state-dependent behaviors.

Bridges formal semantics with architectural realism.

Abstract

The semantics of assignment and mutual exclusion in concurrent and multi-core/multi-processor systems is presented with attention to low level architectural features in an attempt to make the presentation realistic. Recursive functions on event sequences are used to define state dependent functions and variables in ordinary (non-formal-method) algebra.