[foreign-memaccess] RFC: to scope or not to scope?

[John Rose]

On Jun 1, 2019, at 8:50 AM, Jorn Vernee <jbvernee at xs4all.nl> wrote:
> 
> an idea I had been thinking about; make thread confined-ness a more local, temporary state. e.g. you call asConfined which creates a segment that is confined to the current thread, but then add a release() method that invalidates the confined copy and makes the root segment valid again.

This is a good line of thought, but be careful with it, because if you
do the "simple" thing you won't be able to prove freedom from races.

For example, if the root segment allows writing, then any thread can
initiate a racy write to it.  Unless this is provably under a mutex of
some sort, this racy write can still be "handing around" when the
segment transitions back to the confined state.  This means that the
confined state can suffer "hangovers" from previous states, when a
write from that state is not yet completed.

And it's even worse:  Reads *from* the root state are also racy, in
almost as bad a sense as writes.  A read from a root state won't
scribble on a confined state, but it will (potentially) see invariant
breaking states which confined states are careful to make invisible.

This is why, when thinking about versions of scopes and/or memory
segments that can change state over time, I like to stay away from
the normal Java state (any thread can read or write at any time)
because it cannot be adjoined to the cleaner states (like thread
confined) without spoiling those states.

Basically, as a bottom line observation, the Java memory model
cannot be *extended* to make race-free protocols.  It must be
*restricted* at *all* points, in order to create conditions for
excluding races.  You can't have a protocol where some actors
are careful and others are (legacy-style) free-running readers
and writers.

So what's to be done?  Well, the intermediate "neutral" state
between confined states should *not be* business as usual
(racy reads and writes) or even new-fangled immutable
data structures, but *zero access* data structures.  When
I have written or spoken at times about a "queued" state
to adjoin to thread confined states, this is what I mean.

When a memory segment is in the queued state, it is neither
readable nor writable.  A thread must acquire (exclusive)
access for confined reading and writing, *or* the memory
segment must make a *permanent* transition to globally
*read only* (which is also race-free).  If at any moment
uncontrolled writes, or uncontrolled reads not fully ordered
against writes, are allowed, there is no way to (safely)
restore provable race-free conditions.  Once the horse
races out of the barn, you can't lead it back in.  Only
non-racing horses can exit the barn and safely re-enter.
(If you will…)

Now, there may be ways to compromise this very strict
model.  But I think the above is the only way to *safely*
and *provably* exclude races.  So it should be a starting
point in these designs.

Surely one compromise is to give *system code* an unsafe
method to *force* a state transition even when that requires
trusting the caller to certify that the transition is safe.
But this kind of compromise must be reserved to power
users and platform implementors, because (if used by
random people) it will undermine all correctness proofs.
The situation is analogous to sun.misc.Unsafe:  It exists
to allow platform implementors to break the rules
for a moment in the name of affirming the rules in
more flexible ways over time, but it is only available
to (or supposed to be available to) "rule-implementing"
users, not end-users.  End users have a right to strong
correctness invariants (temporal and spatial and type-ful
confinement of data references), and at the same time
giving them ways to break those invariants, without
requiring them to rebuild them for *everyone* defeats
the invariants.

Which is all to say, be careful how you design the
"neutral" or "global" state.  If you design it in the "obvious"
Java-legacy way, you may well make the confined states
unenforceable.

My $0.02.

— John