SE-0414: Region Based Isolation

This is a great point; I'd had this sticking in the back of my mind as a potential problem, and you're absolutely right to drag it out as something we need to deal with.

The basic problem here can be summarized as follows:

  1. Region-based isolation adds a new capability in which non-Sendable values can be transferred between concurrency domains if they're currently in an independent region.
  2. There is an assumption in region-based isolation that non-isolated functions that have access to a non-Sendable value are limited in the effect they can have on that value's region. Basically, we assume that these functions can merge the value's region with the regions of other non-Sendable parameters (e.g. by making references from one to the other), but we assume they cannot merge the value's region with other regions (e.g. by creating a reference to the value from actor-isolated state).
  3. assumeIsolated does not currently limit the flow of non-Sendable values between the formally non-isolated caller and the formally isolated body of the function it's passed, and this effectively allows the arbitrary merger of regions with the actor's region.

One of these points needs to change to eliminate this soundness hole. (1) is really the whole point of region-based isolation, so we don't want to change that. We could remove the assumptions in (2), but that would make region-based isolation pretty useless without a ton of annotations. So ideally we find a way to change (3).

Changing (3) is theoretically source-breaking, since we don't currently limit the flow of non-Sendable values at all with this function. However:

  • developers have generally been informed that we're still closing holes with some of these concurrency APIs, so we do have some room to change the rules retroactively, and
  • it's not a hard source break because we're still only enforcing concurrency with warnings; at worst we're talking about people seeing extra warnings around assumeIsolated, not a completely broken build.

The only thing that's a little grating is that the current behavior of assumeIsolated is actually perfectly sound in the current sendability model — it's just these extra rules of region-based isolation that make it unsound. But it's still a sort of synchronization/isolation primitive, making it something of an edge case that hopefully isn't getting written afresh all the time. I don't think it's unreasonable for us to rebase our understanding of sendability around the goal of enabling the region-transfer capability, especially if that just turns into adding a carefully-chosen attribute to the callback parameter.

It's interesting to note that we get basically the same situation with locks. In an API like OSAllocatedLock.withLock, the callback is not actually sent — it's going to run synchronously with the current context — but it still needs a certain amount of Sendable enforcement to prevent values from being used concurrently. In particular, the lock-protected state is a "rigid" region that cannot be merged with other rigid regions, such as those of parameters from the surrounding context. Similarly, with assumeIsolated, the isolated region of the actor is a rigid region that cannot be unified with other rigid regions. We can merge non-rigid regions into these rigid regions, e.g. if we just created a non-Sendable value and it's currently independent, but we can't do true peer-merges of them.

Now, withLock doesn't have this hole because we require the function passed in to be Sendable. This is a conservatively correct way of closing this hole, because non-Sendable values can't flow either in or out of a Sendable closure at all.[1] We could do the same thing to assumeIsolated by making its parameter function Sendable.

That fix would be quite a bit more conservative than necessary. I think we can start with it, but if we find it's restricting code too much, we may need to add some ability to mark a function as some kind of Sendable barrier without actually making it Sendable. That would also probably be useful for withLock.


  1. Technically, we can allow values in independent regions to be captured by a Sendable closure as a transfer of the region. However, since we don't know how many times the function will be invoked, and in particular if it might be invoked concurrently, we wouldn't actually be able to use these captured values in the closure. We would need @calledOnce / @calledSequentially annotations to make this useful. ↩︎

12 Likes