Lifetimes + different properties of an aggregate

Using Swift
, ,
1

As I understand it, to enforce the Law of Exclusivity, accesses to properties stored in an aggregate (like p.x) in general are treated as accesses to the aggregate itself (in this case, p itself). There is a special case when statically enforcing exclusivity for properties known to be stored is tracked on a per-property basis, allowing simultaneous access to (say) p.x and p.y for some Point2D-like struct.

It appears as if such a special case is not present when performing lifetime checks. For example,

struct Point2D {
    var x, y: Int
}

struct NEBox: ~Escapable {
    let val: Int;
}

func mutate(_ n: inout Int) {
    n = 42;
}

@_lifetime(&n)
func depend(on n: inout Int) -> NEBox {
  return NEBox(val: n);
}

func doit() {
    var p = Point2D(x: 4, y: 2);
    let NEBox = depend(on: &p.x);

    // this correctly raises an error, since exclusivity is violated
    mutate(&p.x);
    // this raises an error too, though (I believe) it need not
    mutate(&p.y);

    // ensure that NEBox is still alive
    print(NEBox.val);
}

This was surprising to me, likely because I have been thinking of the types of checks performed to statically enforce the Law of Exclusivity as being very similar to those used to check lifetimes.

Do the analyses required to bring this special-cased, finer-grained tracking to lifetime checking seem possible? Is this change intended for the future? As I understand it, more language-level features relating properties of a struct and lifetime annotations are planned, but this seems to be more about the implementation of an analysis.

1 Like
2

could you elaborate on what the special case to which you’re referring is?

edit: ah, i think i might understand – do you mean this sort of thing:

func use(_ x: inout Int, _ y: inout Int) { x += 1; y -= 1 }
var p = Point2D()
use(&p.x, &p.y) // no exclusivity violation
3

Yes, your edit exactly describes the behavior I had in mind. From the Ownership Manifesto,

Thus, while there is a scheme which allows independent access to different properties of the same aggregate value, it requires us to be using static enforcement for the aggregate access and to know that both properties are stored. This is an important special case, but it is just a special case. In all other cases, we must fall back on the general rule that an access to a property is also an access to the aggregate.

If x and y were instead computed properties of Point2D, the special case would not apply the code in the snippet would be rejected with an overlapping exclusive access error.

4

For your record, there's already a related section in the current design doc: swift-evolution/proposals/NNNN-lifetime-dependency.md at f75af2e13fd133e1c28e97a9c3be3996de6d4d99 · swiftlang/swift-evolution · GitHub.

5

Hmm. I think that what is described in the document (which is useful btw, thanks!) is notably different from the case that I describe here. The proposed extension here is to track the lifetimes of components of an aggregate separately from each other. The case that I observe above does not ever aggregate multiple non-escapable values.

Though, I do think that a version of the example I present could be written using the component lifetimes proposal:

@_lifetime(&p.x)
func depend(on p: inout Point2D) → NEBox {
  return NEBox(val: p.x)
}

I would imagine that (in a post-component lifetimes world) this should work—but then again, I already imagine that the pre-component lifetimes example above should work too. These two approaches seem comparable in complexity to implement, so maybe that answers my question as to why the example I want to borrow-check currently does not…