lifetime checking design problems

mppf commented 6 years ago

Assumption that formal arguments have same lifetime

With array.push_back, an element with lifetime == this is set to another argument. But, the current analysis assumes that all formal arguments have the same lifetime. That prevents the lifetime checker from detecting errors involving array.push_back such as:

pragma "safe"
module X {

class MyClass {
  var x:int;
}

record BorrowedThing {
  var b: borrowed MyClass;
}

var globalB: BorrowedThing;

proc BorrowedThing.errorSetG(arg: borrowed MyClass) {
  this.b = arg; // this should be an error
}

var globalA: [1..1] borrowed MyClass;

proc errorPushG(arg: borrowed MyClass) {
  globalA.push_back(arg); // this should be an error
}

proc test() {
  var x = new owned MyClass(1);
  globalB.errorSetG(x.borrow());
  errorPushG(x.borrow());
}
test();

}

Writing array.push_back

Were the previous issues resolved, proc array.push_back(value) would cause an error in compilation. How can a version of proc array.push_back(value) be written that does compile?

Brainstorming possible directions:

scope variables can't be stored in arrays / collections
analysis assumes each argument has independent lifetime
lifetime annotation on the arguments indicates this should have lifetime <= value
assumption about argument declaration order - lifetime of 1st arg (this) is <= lifetime of 2nd arg (value) .
assumption that this argument has lifetime <= other arguments
specially mark borrowed arguments that can be saved anywhere in the called function
treat containers differently from other types

Impact

The impact of adding checking for these cases is that where we previously were checking the way values are returned and assigned, now we will also check that values passed to a function have appropriate lifetime constraints. E.g. 5 arguments passed to a function might have some lifetime constraint among them.

bradcray commented 6 years ago

Of the solutions proposed here, this one feels least scary to me:

lifetime annotation on the arguments indicates this should have lifetime >= value

Are there lessons to be learned from prior art (e.g., modern C++ or Rust) here?

mppf commented 6 years ago

When this is resolved, update the following tests which currently use a workaround:

[x] generic-collection-unspecified-with-type.chpl
[x] generic-collection-unspecified.chpl

As well as in module code:

[ ] _add in DefaultAssociative
[x] push_back/push_front
[x] writeEF/writeFF/writeXF.

mppf commented 6 years ago

Generally speaking, a function could take two arguments and it could save borrows from either argument in the other. Or both. E.g.

// supposed this is called with borrows or with records containing borrows
proc swap(ref formalA, ref formalB) {
  var tmp = formalB;  // inferred lifetime of tmp is formalB
  formalB = formalA; // lifetime checker sees formalB storing a borrow from formalA
  formalA = tmp; // lifetime checker sees formalA storing a borrow from formalB
}

I don't think this case is specifically tied to ref since we could imagine a similar situation with a class that contains a borrow:

class StoresBorrow {
  var x: borrow;
}
proc swap2(formalA:StoresBorrow, formalB:StoresBorrow) {
  var tmp = formalB.getBorrowRef(); // inferred lifetime of tmp is formalB
  formalB.getBorrowRef() = formalA.getBorrowRef(); // lifetime checker sees assignment to lifetime formalB from lifetime formalA
  formalA.getBorrowRef() = tmp; // lifetime checker sees assignment to lifetime formalA from lifetime formalB
}

Additionally, the lifetime checker currently uses an inference strategy of using the minimum applicable lifetimes of actual arguments passed to a call as the lifetime of the call result. AFAIK this strategy is OK for returns, but we'll need the checker to store more information if it is to detect situations where a borrow from one argument is stored in another. Consider for example:

proc harderCase( formalA, formalB ) {
  var x = f(formalA, formalB); // lifetime is formalA or formalB according to minimum rule?
  formalA.getBorrowRef() = x;
  formalB.getBorrowRef() = x;
  // the above statements imply formalA lifetime == formalB lifetime but this presumably
  // isn't checked at the call site unless we use an annotation, and there should be an
  // error here to indicate the annotation is necessary.
}

Here I am imagining that perhaps the lifetimes inferred from formal arguments could be handled more specially, where instead of just a minimum lifetime, the lifetime tracker also manages a set of formals that could possibly impact that lifetime. The minimum lifetime could still be used for return checking, but the set of formals impacting the lifetime would be used to check for invalid assignments that borrow between formals.

At the call site, checking is easier in that we could assume no relationship between the lifetimes of the actuals need exist (and the minimum lifetime is still OK for the purposes of validating returns of borrows) - unless there is an annotation that relatively explicitly indicates a required ordering on the lifetimes of the actuals (as we would need for push_back).

mppf commented 5 years ago

analysis assumes each argument has independent lifetime

Trying this out, with an exception for =, all but these tests passed quickstart:

[Error matching compiler output for analysis/alias/array-of-classes (compopts: 1)] [Error matching compiler output for analysis/alias/array-of-classes (compopts: 2)] [Error matching compiler output for classes/delete-free/swap-managed] [Error matching compiler output for classes/dinan/parent_class_cast] [Error matching compiler output for functions/diten/refIntents-workaround] [Error matching compiler output for functions/ferguson/ref-pair/ifexpr/ifexpr2-1]

mppf commented 5 years ago

Main remaining TODOs:

figure out what's going on in the ifexpr test (temporary lifetime is inferred to be c and then set to b)
develop a plan for swap
enable lifetime inference for assign based on lifetime annotations

mppf commented 5 years ago

There are some problems with records that both own and borrow. This comes up because arrays fall into this category (they own their domain, say, but the elements might be borrows).

class C { var x: int; }

record R {
  var own: owned C;
  var bor: borrowed C;
}

proc makeA(arg: borrowed C) {
  var ret: R;
  ret.own = new owned C(0);
  ret.bor = arg;
  return ret;
}

proc main() {
  var ownC = new owned C(1);
  var outerb: borrowed C;
  {
    var b = ownC.borrow();
    var A = makeA(b);
    outerb = A.bor;
  }
}

That causes certain patterns where a copy of the record is made to not compile where it would compile without the copy. The above is an example. This can come up with records/classes containing arrays; the outer scope in main might really be fields.

I don't have a good solution to this problem. The lifetime checker does differentiate between "intrinsic" and "inferred" lifetime and this distinction could allow the above case to compile, but it would require that the author of the type R mark which methods are returning a borrow from the owned field (i.e. should use the "intrinsic" lifetime) vs which are returning a borrow from the contained data (i.e. should use the "inferred" lifetime).

This is the array form of exactly the same problem:

class C { var x: int; }

proc makeA(arg: borrowed C) {
  var ret: [1..1] borrowed C;
  ret[1] = arg;
  return ret;
}

proc main() {
  var ownC = new owned C(1);
  var outerb: borrowed C;
  var outerA: [1..1] borrowed C;
  {
    var b = ownC.borrow();
    var A = makeA(b);
    outerb = A[1];
    outerA[1] = A[1];
  }
}

Edit: here is another case that has some similarities:

class C { var x: int; }

class B { var bor: borrowed C; }

record R {
  var own: owned B;
  proc init() {
    own = new owned B(nil);
  }
}

proc main() {
  var steal: owned B;
  {
    var r:R;
    var ownC = new owned C(2);
    r.own.bor = ownC.borrow();
    steal = r.own;
  }

  writeln(steal.bor.x);
}

Here the compiler doesn't track that steal = r.own can make a borrow escape. Could it? I'm not so sure. It's related to the issue with tracking arrays of borrows though.

Here's the same issue with returns:

class C { var x: int; }

class B { var bor: borrowed C; }

record R {
  var own: owned B;
  proc init() {
    own = new owned B(nil);
  }
}

proc test() {
  var r:R;
  var ownC = new owned C(2);
  r.own.bor = ownC.borrow();
  return r.own;
}

{
  var steal = test();
  writeln(steal.bor.x);
}

mppf commented 5 years ago

Two more tricky cases:

class C { var x: int; }

proc main() {
  var A:[1..0] owned C;

  {
    var own = new owned C();
    A.push_back(own);
  }
}

class C { var x: int; }

class B { var bor: borrowed C; }

record R {
  var impl: owned B;
  proc init() {
    impl = new owned B(nil);
  }
}

proc doit(ref a:R, const ref b:owned C) lifetime a < b {
  a.impl.bor = b.borrow();
}

proc main() {
  var r: R;

  {
    var ownC = new owned C(1);
    doit(r, ownC);
  }

  writeln(r.impl.bor.x);
}

At issue here is whether a lifetime constraint (as push_back will have) only applies to types that contain borrows. The first example above indicates that's probably what we'd want, but the second example is a counter-argument.

chapel-lang / chapel