Capability violation with tuple recovery

[Praetonus]

From today VUG presentation.

class Foo

actor Main
  new create(env: Env) =>
    let x: (Foo, Foo val) = recover
      let y: Foo = Foo
      (y, y)
    end

This program compiles but is clearly wrong (ref and val aliases to the same object).

[jemc]

#1124 is intended to fix this bug by disallowing tuple recovery in all cases, but I personally wouldn't want to see this happen unless we're sure this is the best solution. I think there are lots of legitimate places where we can recover tuples, and indeed - cases where recovering tuples is the only sane way to recover multiple objects that have to be constructed in the same block, or are otherwise linked in some way.

@Gds12 @sylvanc - are there any relatively-easy-to-implement rules we can use in the compiler to use to determine if a given tuple is safe to recover? Even if we can't be fully permissive, it seems like we could at least allow object references that are provably unrelated to one another (if it's possible to prove this). Any ideas?

[ghost]

I think I've figured out the most permissive way of doing this, which is more or less as we discussed in the call last week with a few amendments:

• If a tuple type only contains immutable capabilities or is only being recovered to an immutable type, recovery proceeds as normal (e.g. let x: (Foo val, Foo box) = recover val (Foo, Foo) end works as expected. Note this also includes that tag recovers to tag, as per usual.
• If the tuple type contains any mutable capabilities then the type recovered is exactly the same as it was before the recovery, (e.g. let x: (Foo ref, Foo val) = recover (Foo, Foo) end fails to compile in the assignment since val is not a subtype of ref). This permits recovery of types containing a tuple: e.g. recovery of a (Foo ref^ | (Foo ref, Foo box)) should be (Foo iso^ | (Foo ref, Foo box)).

Summary of examples:

• recover (Foo ref, Foo ref) = (Foo ref, Foo ref)
• recover val (Foo ref, Foo ref) = (Foo val, Foo val)
• recover tag (Foo ref, Foo ref) = (Foo tag, Foo tag)
• recover (Foo ref | (Foo ref, Foo ref)) = (Foo iso^ | (Foo ref, Foo ref))

Additionally, if the components of the tuple do not share any fields (including fields of fields etc...) then it should be safe to recover both members to iso^ as is currently done. For example a tuple of type (U8, U32) is perfectly safe to recover since neither have any fields.

Thoughts? Since I'm not too familiar with the actual implementation I may be missing something :)

[jemc]

if the components of the tuple do not share any fields (including fields of fields etc...) then it should be safe to recover both members to iso^ as is currently done.

I'd like to be able to allow this, but I'm not sure how this would be checked in practice.

Theoretically, it should be possible for the compiler to determine this, with the caveat that the no-sharing-of-fields would have to be enforced for every branch of conditional logic - the compiler can't know statically which branch will be executed at runtime, so all branches would have to be safe.

However, in practice, this tracing of possible branches of execution would have to be done passing into functions, deeply, and tracking state in the tracing about which references could be common at any point. I don't think this is practically feasible with the current architecture of the compiler, unless someone has a clever trick to avoid this.

So that said, I think we'll have to use only the first two points that @Gds12 suggested. I'll move further discussion of this into #1124, where it looks like @Praetonus has already gotten started.