Projections and Undefined Behavior

[dabrahams]

Definitions

• A projection is a sink, set, inout or let access. ^{1 2}
• A projection of type T is an access to an object of type T.
• Projections are active when they are created.
• A projection can become inactive during its lifetime. For example, in x: inout T = &y, y becomes inactive, and if still alive, becomes active again when the lifetime of x ends.
• An object is initialized at the first completion of a set access on it (an init function is a set access on self).
• An object is complete when all parts³ are initialized.
• An initialized or complete object becomes incomplete (and uninitialized ⁴) when any part is passed as a sink parameter, and returns to its prior state whenever all of its parts have returned to an initialized state.

Laws

In entirely safe code, the compiler upholds these properties:

• An active non-set projection of type T always refers to a complete object of type T.
• if x is an active sink, set, or inout projection of an object y, no other projection that includes y is active.

Note: the compiler also ensures that only active projections of complete objects are used in expressions other than those that narrow active projections of incomplete objects to their stored parts, e.g. in x.y, x may project an incomplete object.

The behavior of a program that violates either property (e.g., using pointers) is undefined. For example:

let i = 3
let p = pointer[to: i] // i becomes inactive
let q = p.copy()       // projection of p ends; i becomes active
let j = q.unsafe[]     // UB: active projection `j` includes the object bound to active `sink` projection `i`

Note: this post reflects revisions based on the discussion below.

Footnotes

1. Projections can be bound to names but may also be the temporary unnamed results of expressions. ↩

2. A var declaration creates a bound sink projection. ↩

3. An object's parts all follow from its type declaration and do not depend on the user-defined semantics of operations. For example, they do not include “logical parts” that can only be reached via declared pointers, such as the elements of a dynamic array, even though its == operation implies that they are parts. ↩

4. Every initialized object is complete, so every incomplete object is uninitialized. ↩

[kyouko-taiga]

Very nice laws!

I understand the general meaning of the definitions but I think they require some tweaks. Some comments:

A projection is an inout or let access, whether temporary or bound to a name

A projection can have any access effect, including set and even sink.

In my working lexicon, I use projection to mean an access on (parts of) one or several values. For example, min[x, y.1] is a projection of x and part of y. The effect of that projection could be set or sink depending on the variant being used.

subscript<T is Comparable>(x: auto T, y: auto T) auto -> T {
  sink { if y < x { y } else { x } }
}

public fun main() {
  var x = 1 ; var y = 2
  var z = min[x, y]
  _ = z
}

Here I would call z a projection of x and y, even though it is a sink access.

It may also be interesting to note that T and remote sink T are not exactly the same. The latter denotes a responsibility to deinitialize an instance of T that is stored elsewhere. I have to concede that this feature is a mostly consequence of the calculus. One use case could be for capturing an immovable object, but even then the compiler won't get you very far since a lambda making such a capture would not be allowed to flow into a sink parameter despite having a sink effect on its call operator.

a var declaration is a bound inout access to the value with which it is initialized

A var declaration is a sink access initially uninitialized. That is, the semantics of var x = 1 are the same as that of var x: Int ; &x = 1.

A use of a bound projection is a mention of the binding's name in source.

A "use" is an IR term and thus I think we can't limit ourselves to occurrences visible in sources only. Also I think this definition contradicts the one before it (which incidentally describes more accurately what a use is in the IR). The name to which a temporary projection is bound does not show up in sources.

The issue is that an expression like p.0 (where p is a tuple) is really a use of the first component of p and not of p itself. That works if we say that f(p.0) temporarily binds p.0 to some name that we cannot see in sources. In fact, that is what happens in the IR.

I understand it is inconvenient to bring up the IR but in any case, we'll at least have to consider evaluation order in your laws. For example, this program is legal in safe Hylo:

public fun main() {
  var xs : Array<_> = [1, 2, 3]
  &xs.append(xs[0].copy())
}

There are two temporary projections of xs here. To understand why they do not overlap, one has to think about the specific order in which these projections are formed. You touch on this point with your note.

An object of nominal type T is initialized when the first T.init (if any exist) has run on it, or when it is complete otherwise

If possible I would like to avoid giving any special status to T.init and T.deinit. Sugar aside, these functions are completely ordinary. What makes T.init an initializer for the underlying calculus is merely the fact that self is a set parameter. Likewise T.deinit is a deinitializer simply because self is a sink parameter.

In my personal mental model I stopped seeing methods as a concept separate from free functions (and subscripts).

An object is deinitialized and incomplete when its deinitializer completes but before the first deinitializer of a part in its contiguous storage (if any) begins.

I don't understand the distinction you draw between deinitialized and incomplete.

[dabrahams]

In my working lexicon, I use projection to mean an access on (parts of) one or several values. For example, min[x, y.1] is a projection of x and part of y. The effect of that projection could be set or sink depending on the variant being used.

OK.

A "use" is an IR term and thus I think we can't limit ourselves to occurrences visible in sources only.

I think it's fine for “use” to have a contextual meaning. Isn't every use in IR derived from some use-as-I-have-defined-it? Regardless, the wording doesn't depend on having a definition of “use” so I just removed it.

one has to think about the specific order in which these projections are formed. You touch on this point with your note.

I don't think the fact that evaluation order is sometimes not lexically left-to-right demands any changes to what I wrote. The point is to lay out what causes UB given the evaluation order rules, whatever they may be. I also don't see where I touch on your point.

If possible I would like to avoid giving any special status to T.init and T.deinit.

IMO the logical conclusion of that is that every piece of memory is always accessible as any type without UB. Think about when we can access a tuple of two Ints. Obviously, it has to be OK to access each of its constituent Ints before we can access the tuple. So when is it OK to access one of its constituent Ints? It has no parts; the only boundary in the order of execution is when its init is complete. If we say init isn't special, the Ints are accessible as soon as the memory exists, and thus the whole tuple is. I don't think we want to say that.

I draw no distinction between deinitialized and incomplete. I say they are the same: an object stops being complete precisely when it becomes deinitialized.

[kyouko-taiga]

If we say init isn't special, the Ints are accessible as soon as the memory exists, and thus the whole tuple is. I don't think we want to say that.

I don't think so, or I am missing something from your point.

Structs behave the same way as tuples do except that the memory state of each individual stored properties cannot be "observed" outside of its declaration. That is, any direct member of a struct enjoys the privilege of treating any instance of Self like a tuple, whether it is called self or something else.

So when I say that init isn't special it's because one can emulate an initializer with any member function:

struct Vec2 {
  public var x: Int
  public var y: Int
  public memberwise init
  public func initialize(_ x: sink Int, _ y: sink Int) set { &self.x = x ; &self.y = y }
}

To me, Vec2.init and Vec2.initialize are doing exactly the same thing. It just happens that the former comes with some sugar. I think it should be possible to allocate and initialize an instance of Vec2 without ever calling Vec2.init:

public fun main() {
  let p = PointerToMutable<Vec2>.allocate(count: 1)
  unsafe pointer.initialize_callee(fun(x) { Vec2.initialize(&x, 1, 2) })
}

Likewise there is nothing special about deinit. It is just a function that takes an instance of Self as a set parameter. Declaring such a function as a member lets it treat that instance like a tuple and therefore it can deinitialize each part individually.

[dabrahams]

Likewise there is nothing special about deinit. It is just a function that takes an instance of Self as a set parameter.

sink, surely.

[kyouko-taiga]

Indeed.

[RishabhRD]

• An object is initialized at the first completion of a set access on it (an init function is a set access on self).
• An object is complete when all parts in its contiguous storage are initialized.

Shouldn't the definition of complete be defined in terms of memory write for parts? I am concerned of the case when set access can do more than just initializing. For example, this code seems okay to me, but doesn't fit the definition of complete:

type Atom: Deinitializable, Movable {
  public var x: Int
  public memberwise init
  public fun initialize(_ p: let Pointer<Composed>) set {
    &x = 2
    inout c = p.unsafe[] // Currently `Atom` is not initialized(as per definition) and thus `Composed` is not complete. So, is illegal.
  }
}

type Composed: Deinitializable {
  public var x: Atom
  public var y: Atom
  public memberwise init
  public fun initialize() set { 
     &x = Atom(x: 2)
     &y = Atom(x: 3)
     let p = pointer[to: self]
     let q = p.copy()
     y.deinit()
     &y.initialize(q)
  }
}

(The compiler also ensures that only active projections are used in expressions, other than to narrow them to stored parts, e.g. in x.y, x may be inactive).

I think compiler disallows the "other than" part. For example:

public struct Composed {
  public var x: Int
  public var y: Int
  public memberwise init
}

public fun g( c: inout Composed) {}

public fun f( c: inout Composed) {
  inout c1 = &c
  inout x = &c.x // c.x is illegal to use, use c1.x
  &x = 2
  g(&c1)
}

The compiler also ensures that only active projections are used in expressions

Also this rule is from where, I got the idea of pointer provenance. Consider following program:

public fun main() {
  var x: Int = 1
  let p = mutable_pointer[to: &x]
  let q = p.copy()
  inout x1 = &x
  inout x2 = q.unsafe[]
  &x1 = 2
}

On line inout x2 = q.unsafe[], to me it seems like using pointer to cheat compiler to use the inactive binding x . In a "purer" program, p and q would have been created using x1.

But from our last discussion, I think you meant to say, we should not treat pointer as something more than a memory address. And any binding created from pointer dereference, should be logically assumed to be created from latest active binding?

[dabrahams]

@kyouko-taiga please see if you agree with all this:

• IMO there's no reason we need to allow the first example. There's lots of code that makes sense but we are going to say is UB in order to have simple rules.
• I think you may be right about the “other than” part. I think it should say:

  The compiler also ensures that only active projections of complete objects are used in expressions, other than to narrow active projections of incomplete objects to their stored parts, e.g. in x.y, x may project an incomplete object

• I think we should not make UB rules about pointers. I assume that is what you mean by “not treat them as anything more than a memory address.”
• You could say that any binding created from a pointer dereference should be logically assumed to be created from latest active binding of an overlapping object, but you don't need to say anything like that, and shouldn't, because it just complicates things. The point of these rules is that “created from” doesn't appear anywhere. So pointer or projection provenance is irrelevant to these rules.
• The only place where provenance comes up is that a dereferenced pointer can only point into the allocation it was initialized from.

[kyouko-taiga]

I don't mind if we rule out the first example, but it is true that the condition for an object to be complete may be too strong. I think it disallows using self after its parts have been initialized without first returning from the function, which is too strict and ultimately arbitrary since we can just write this without violating the rules:

fun use<T>(x: T) {}
fun initialize(p: set {Int, Int}) {
  set q =  &p
  &q.0 = 0 ; &q.1 = 1
  use(p)
}

Your amendment to the rule about disallowing uses of incomplete objects seems correct.

I don't have a strong opinion about the last example. AFAICT the only think that truly matters is that it should be illegal to project pointees out of pointers in such a way that it creates two active mutable bindings that overlap. It would not shock me if using pointers provides ways to uphold this principle that would not be possible to replicate with ordinary accesses.

@RishabhRD If your examples work with tuples, could you use those instead of nominal types? That would eliminate some of of the "noise" coming from declarations that are irrelevant to your points (e.g., memberwise initializers).

[dabrahams]

…the condition for an object to be complete may be too strong. I think it disallows using self after its parts have been initialized without first returning from the function

How? The definition of “complete” is precisely that all the parts are initialized, so it does not require returning from an initializer (or any other set access). In fact, the desire to use self immediately after its parts are initialized is the very raison d'être of “complete.” Otherwise we would define everything in terms of “initialized” alone.

Your amendment to the rule about disallowing uses of incomplete objects seems correct.

👍 applied

[kyouko-taiga]

The definition of “complete” is precisely that all the parts are initialized

You are right, sorry!

Also I confirm that we should not allow the first example from Rishab, but not because of any problem related to the "completeness" of the object.
I think the following is simpler program that captures the same setup:

fun f(pair: set {Int,}) {
  &pair = (1,2)
  // ^ 'pair' is complete
  let p = pointer[to_mutable: &pair].copy()
  // ^ 'p' points to the object bound by 'pair' and 'pair' is back to be active; all good
  _ = pair.0
  // ^ 'pair' is incomplete
  g(&pair.0, p)
}

fun g(x: set Int, p: PointerToMutable<{Int, Int}>) {
  &x = 3
  // ^ 'pair' (bound in the caller) is complete
  inout pair_at = &p.unsafe[]
  // ^ UB: there are two active mutating projections that overlap, violating uniqueness
}

Unless I missed something Dave's laws do not describe what uniqueness (or exclusivity) means. An attempt from my part is:

Any code leading a program to a situation where there exist two or more active mutable bindings that overlap triggers UB. Two bindings overlap if they can be used to access the same part(s) of a single object.

Note that I didn't use contiguous storage because it occurred to me that the term might be slightly incorrect since it is possible to store properties indirectly, in both enums and structs. Isn't enough to say "parts of an object"? Even if we're talking about an array, it should not be possible to access the same part (i.e., position in the out-of-line buffer) from two different bindings. And I would claim that CoW representations involve a peer relationship between the container and its storage, meaning that the latter would not be considered "part of" the former.

[dabrahams]

My text doesn't include the terms “uniqueness” or “exclusivity” because it doesn't need to. It's all there in the 2nd bullet. And the text you propose doesn't prevent active immutable bindings from overlapping active mutable ones.

I will remove the “contiguous storage” part. It was intended as a clarification for the casual reader who wonders about “logical parts.” In the domain of objects those don't exist so it's strictly unneeded but then you have to be aware of the technical meaning of object. I can add a footnote.

Even if we're talking about an array, it should not be possible to access the same part (i.e., position in the out-of-line buffer) from two different bindings.

If you mean a dynamic array, parts are irrelevant to the rules that prevent that access. It's already covered. Parts are only used to define completeness and to talk about allowed narrowing (in a note, which should be considered non-normative—it exists to help the reader understand how upholding those properties leads to safety). I don't know what you mean about CoW, but I claim all that is above the level of these rules and these rules are sufficient to ensure that it works and is safe.

[dabrahams]

I got rid of the “contiguous storage” thing and moved more explanatory text into footnotes.

[kyouko-taiga]

My text doesn't include the terms “uniqueness” or “exclusivity” because it doesn't need to. It's all there in the 2nd bullet. And the text you propose doesn't prevent active immutable bindings from overlapping active mutable ones.

Indeed, my bad.

If you mean a dynamic array, parts are irrelevant to the rules that prevent that access.

The footnote clarifies. I have no outstanding concern.

I don't know what you mean about CoW, but I claim all that is above the level of these rules and these rules are sufficient to ensure that it works and is safe.

I was playing devil's advocate for someone who would claim anything about the whole/part relationship between a container and its CoW contents. But really I was saying that this case is irrelevant to the current discussion, and I think we agree.

[dabrahams]

I had to make one more small adjustment to the definitions of incomplete and uninitialized to account for the case where a part of a complete-but-uninitialized object is sunk.

[RishabhRD]

In my working lexicon, I use projection to mean an access on (parts of) one or several values. For example, min[x, y.1] is a projection of x and part of y. The effect of that projection could be set or sink depending on the variant being used.

OK.

Does this OK mean, the above definition should be changed accordingly? Asking as this would impact the shape of my data structure.

[dabrahams]

That OK meant I was going to make sure the text at the top was consistent with Dimi's working lexicon (which I have done AFAIK).