Last year there was a paper published, on a mode system for OCaml to reduce memory allocation. Early this year there was another, an extension of that system to prevent data races. I’ve been in correspondence with one of the authors of that paper, and we agreed there were some rough spots in it. I had my own ideas of how to extend the mode system in the original paper to prevent data races, and I present them here.
Axes
As well as the three axes proposed in the first paper, the new mode axes are Mutability and Ordering, a conjugate pair. Mutability captures whether the referenced memory can be mutated through this reference, whereas Ordering captures the dependence of a closure on operations around it.
On the Mutability axis, in submode order:
- Mutable means the memory can be mutated through this reference regardless of its Uniqueness. A closure over this value must be Volatile.
- Exclusively Mutable means the memory can be mutated if this reference is Exclusive or lower. A closure over this value must be Sequential or higher.
- Immutable means this reference cannot be used to mutate the memory. A closure over this value may be Pure.
On the Ordering axis, in submode order:
- Pure means that invocations of this closure do not depend on any program state, or for values, that this memory has no Mutable references to it.
- Sequential means that invocations of this closure must be ordered relative to each other, or for values, that this memory has no mutable aliases (but may be mutable through this reference).
- Volatile means that invocations of this closure must be ordered relative to every other program operation, or for values, that this memory may have mutable aliases.
The relation between this axis pair is reversed relative to Uniqueness and Affinity: it’s the value axis that restricts loosening of the closure axis: a Volatile value can be made Immutable, but a Pure Immutable value must remain Pure.
When aliased, Exclusively Mutable becomes Immutable, and Mutable and Sequential become Volatile. To be shared with another thread, a value must be Pure, or it must be Exclusive and Sequential; this allows mutable state to be shared across threads, as long as this would not lead to a data race, as well as preventing data races caused by aliased immutable state.