[Pitch] Region Based Isolation

[hborla (Holly Borla)]

@FranzBusch

While the iterator here is transferred across isolation regions due to the law of exclusivity there should not be any concurrent access to the iterator since the next method us mutating.

Your contrived example will technically compile under this proposal, but remember that iterator is in the same region as stream and all of its results that are non-Sendable; if you do anything to merge the stream or the results into the actor's region -- such as using a parameter in the expression that initializes stream or storing one of the results into a variable that's already in the actor's region -- then the compiler must assume that the actor can reference iterator. In order to fully solve the Sendable issues with AsyncSequence iterators, I believe we need the future direction of this proposal to specify that a result value is disconnected, and then annotate both makeIterator() and next() with that attribute.

@gregtitus

I assume the update of the disconnected state (x in the examples) must not only happen along all control flow paths but in order to be safe it must also happen before any potential suspension point (an await in the following code). Otherwise the actor could be re-entered and the old x accessed by some other task. Is that correct?

Yes, that's correct!