Towards a Grainless Semantics for Shared Variable Concurrency
John C. Reynolds
Conventional semantics for shared variable concurrency imposes
a default choice of the level of atomicity that is often
unrealistic for an actual implementation - this is commonly
called the "grain of time" phenomenon. We propose a semantics
that avoids any such choice. It is based on three principles:
All operations have duration and can overlap one another
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.
The slides for this lecture are available online.