Towards a Grainless Semantics of Shared-Variable Concurrency
Professor John Reynolds, Carnegie Mellon University and visiting
University of Edinburgh
Conventional semantics for shared-variable concurrency suffers from
the "grain of time" problem, i.e., the necessity of specifying a
default level of atomicity. We propose a semantics that avoids any
such choice by regarding all interference that is not controlled by
explicit critical regions as catastrophic. It is based on three
principles:
- Operations have duration and can overlap one another
during execution.
- If two overlapping operations touch the same location, the
meaning of the program execution is "wrong".
- If, from a given starting state, execution of a program can
give "wrong", then no other possibilities need be considered.