Re: [swift-dev] Proposal: SIL Ownership Model + Verifier

[John McCall via swift-dev]

> On Dec 8, 2016, at 1:53 PM, Andrew Trick  wrote:
>> On Dec 7, 2016, at 11:25 PM, John McCall via swift-dev > > wrote:
>> 
>>> 
>>> On Dec 7, 2016, at 2:13 PM, Michael Gottesman via swift-dev 
>>> mailto:swift-dev@swift.org>> wrote:
>>> 
>>> This is a proposal for a new SIL Ownership Model and verifier. An online 
>>> HTML version of the document is available here:
>>> 
>>> https://gottesmm.github.io/proposals/sil-ownership-model.html 
>>> 
>>> 
>>> and inline below.
>>> 
>>> Michael
>>> 
>>> 
>>> 
>>> # Summary
>>> 
>>> This document defines a SIL ownership model and a compile time static 
>>> verifier
>>> for the model. This will allow for static compile time verification that a 
>>> SIL
>>> program satisfies all ownership model constraints.
>>> 
>>> The proposed SIL ownership model embeds ownership into SIL's SSA def-use
>>> edges. This is accomplished by:
>>> 
>>> 1. Formalizing into SIL API's the distinction in between defs
>>>(e.g. `SILInstruction` and `SILArgument`) and the values produced by defs
>>>(e.g. `SILValue`). This is needed to model values as having ownership and
>>>defs as not having ownership. The main implication here is that the two 
>>> can
>>>no longer be implicitly convertible and the API must enforce this.
> 
> This proposal is simultaneously proposing some specific API details
> while avoiding both the motivation behind it and the eventual features
> that it will support.
> 
> I think the ValueBase/Def renaming is a little
> misunderstanding. "ValueDef" in the proposal was a placeholder (not a
> perfect name) for some perceived need to have a common
> SILArgument/SILInstruction base class. That's probably not necessary
> in which case there's nothing to disagree about.
> 
> John's counter proposal solves that problem by repurposing ValueBase
> to serve as a base class for value definitions (and then goes into
> some detail on implementing multi-result instructions).
> 
>> We currently have two kinds of def: instructions and arguments.  Arguments
>> always define a single value, and I don't see anything in your proposal that
>> changes that.  And the idea that an instruction produces exactly one value is
>> already problematic, because many don't produce a meaningful value at all.
>> All that changes in your proposal is that certain instructions need to be 
>> able
>> to produce multiple values.
> 
> That’s an obvious way of looking at it. I personally am most
> interested in putting an end to the chronic problem of conflating
> instructions and values which literally makes it impossible to have a
> sane discussion about ownership. I insisted that SILInstruction not
> derive from ValueBase, which probably led to the proposed
> renaming. This probably comes across as confusing because the proposal
> is deliberately side-stepping the issue of multi-result instructions.
> 
> What I really want to see at the proposal level is agreement on core concepts:
> - A value has a type, ownership, one def, and 0..n uses
> - Ownership rules are guaranteed simply by evaluating those 0..n uses.
> - A value’s def/use is the point at which it is produced/consumed.
> - Use/def points are demarcated by instructions or block boundaries
> - An instruction produces values via results or consumes them via operands.
> 
> There shouldn't be any debate about these concepts, so why is there so
> much confusion? I think caused by some bad choices in the SIL
> interface, particularly as SILInstruction : ValueBase.
> 
> So we should define a SIL interface that reflects those core
> concepts. We should be able to reimplement multi-result instructions
> without affecting those interfaces and without rewritting SIL passes.

I agree.  I don't think this requires deep changes to how SIL nodes are 
typically
worked with.  As long as single-result instructions can be transparently used as
values, so that e.g. the result of SILBuilder::CreateBitCast can be used as a
SILValue, the number of changes required should be quite modest.

Things like SILCloner will of course need some minor updates to handle the
fact that a single instruction can have multiple uses, but that should be 
straightforward
to do on top of the existing Value->Value mapping.

John.

> 
> -Andy
> 
>> 
>> Moreover, the word "def" clearly suggests that it refers to the definition 
>> of a
>> value that can be used, and that's how the term is employed basically 
>> everywhere.
>> 
>> So allow me to suggest that a much clearer way of saying what you're trying 
>> to
>> say is that we need to distinguish between defs and instructions.  An 
>> instruction
>> may have an arbitrary number of defs, possibly zero, and each def is a value
>> that can be used.  (But the number of defs per instruction is known 
>> statically
>> for most instructions, which is something we can use to make working with
>> defs much less annoying.)
>> 
>> Also this stuff you'

Re: [swift-dev] Proposal: SIL Ownership Model + Verifier

[Andrew Trick via swift-dev]

> On Dec 7, 2016, at 11:25 PM, John McCall via swift-dev  
> wrote:
> 
>> 
>> On Dec 7, 2016, at 2:13 PM, Michael Gottesman via swift-dev 
>> mailto:swift-dev@swift.org>> wrote:
>> 
>> This is a proposal for a new SIL Ownership Model and verifier. An online 
>> HTML version of the document is available here:
>> 
>> https://gottesmm.github.io/proposals/sil-ownership-model.html 
>> 
>> 
>> and inline below.
>> 
>> Michael
>> 
>> 
>> 
>> # Summary
>> 
>> This document defines a SIL ownership model and a compile time static 
>> verifier
>> for the model. This will allow for static compile time verification that a 
>> SIL
>> program satisfies all ownership model constraints.
>> 
>> The proposed SIL ownership model embeds ownership into SIL's SSA def-use
>> edges. This is accomplished by:
>> 
>> 1. Formalizing into SIL API's the distinction in between defs
>>(e.g. `SILInstruction` and `SILArgument`) and the values produced by defs
>>(e.g. `SILValue`). This is needed to model values as having ownership and
>>defs as not having ownership. The main implication here is that the two 
>> can
>>no longer be implicitly convertible and the API must enforce this.

This proposal is simultaneously proposing some specific API details
while avoiding both the motivation behind it and the eventual features
that it will support.

I think the ValueBase/Def renaming is a little
misunderstanding. "ValueDef" in the proposal was a placeholder (not a
perfect name) for some perceived need to have a common
SILArgument/SILInstruction base class. That's probably not necessary
in which case there's nothing to disagree about.

John's counter proposal solves that problem by repurposing ValueBase
to serve as a base class for value definitions (and then goes into
some detail on implementing multi-result instructions).

> We currently have two kinds of def: instructions and arguments.  Arguments
> always define a single value, and I don't see anything in your proposal that
> changes that.  And the idea that an instruction produces exactly one value is
> already problematic, because many don't produce a meaningful value at all.
> All that changes in your proposal is that certain instructions need to be able
> to produce multiple values.

That’s an obvious way of looking at it. I personally am most
interested in putting an end to the chronic problem of conflating
instructions and values which literally makes it impossible to have a
sane discussion about ownership. I insisted that SILInstruction not
derive from ValueBase, which probably led to the proposed
renaming. This probably comes across as confusing because the proposal
is deliberately side-stepping the issue of multi-result instructions.

What I really want to see at the proposal level is agreement on core concepts:
- A value has a type, ownership, one def, and 0..n uses
- Ownership rules are guaranteed simply by evaluating those 0..n uses.
- A value’s def/use is the point at which it is produced/consumed.
- Use/def points are demarcated by instructions or block boundaries
- An instruction produces values via results or consumes them via operands.

There shouldn't be any debate about these concepts, so why is there so
much confusion? I think caused by some bad choices in the SIL
interface, particularly as SILInstruction : ValueBase.

So we should define a SIL interface that reflects those core
concepts. We should be able to reimplement multi-result instructions
without affecting those interfaces and without rewritting SIL passes.

-Andy

> 
> Moreover, the word "def" clearly suggests that it refers to the definition of 
> a
> value that can be used, and that's how the term is employed basically 
> everywhere.
> 
> So allow me to suggest that a much clearer way of saying what you're trying to
> say is that we need to distinguish between defs and instructions.  An 
> instruction
> may have an arbitrary number of defs, possibly zero, and each def is a value
> that can be used.  (But the number of defs per instruction is known statically
> for most instructions, which is something we can use to make working with
> defs much less annoying.)
> 
> Also this stuff you're saying about values having ownership and defs not 
> having
> ownership is, let's say, misleading; it only works if you're using a 
> meaninglessly
> broad definition of ownership.  It would be better to simply say that the 
> verification
> we want to do for ownership strongly encourages us to allow instructions to 
> introduce multiple defs whose properties can be verified independently.
> 
>> 2. Specifying a set of ownership kinds and specifying a method for mapping a
>>`SILValue` to an ownership kind.
>> 3. Specifying ownership constraints on all `SILInstruction`s and 
>> `SILArgument`s
>>that constrain what ownership kinds their operands and incoming values
>>respectively can possess.
>> 4. Implementing a verifier to ensure that all

Re: [swift-dev] Proposal: SIL Ownership Model + Verifier

[John McCall via swift-dev]

> On Dec 7, 2016, at 2:13 PM, Michael Gottesman via swift-dev 
>  wrote:
> 
> This is a proposal for a new SIL Ownership Model and verifier. An online HTML 
> version of the document is available here:
> 
> https://gottesmm.github.io/proposals/sil-ownership-model.html 
> 
> 
> and inline below.
> 
> Michael
> 
> 
> 
> # Summary
> 
> This document defines a SIL ownership model and a compile time static verifier
> for the model. This will allow for static compile time verification that a SIL
> program satisfies all ownership model constraints.
> 
> The proposed SIL ownership model embeds ownership into SIL's SSA def-use
> edges. This is accomplished by:
> 
> 1. Formalizing into SIL API's the distinction in between defs
>(e.g. `SILInstruction` and `SILArgument`) and the values produced by defs
>(e.g. `SILValue`). This is needed to model values as having ownership and
>defs as not having ownership. The main implication here is that the two can
>no longer be implicitly convertible and the API must enforce this.

We currently have two kinds of def: instructions and arguments.  Arguments
always define a single value, and I don't see anything in your proposal that
changes that.  And the idea that an instruction produces exactly one value is
already problematic, because many don't produce a meaningful value at all.
All that changes in your proposal is that certain instructions need to be able
to produce multiple values.

Moreover, the word "def" clearly suggests that it refers to the definition of a
value that can be used, and that's how the term is employed basically 
everywhere.

So allow me to suggest that a much clearer way of saying what you're trying to
say is that we need to distinguish between defs and instructions.  An 
instruction
may have an arbitrary number of defs, possibly zero, and each def is a value
that can be used.  (But the number of defs per instruction is known statically
for most instructions, which is something we can use to make working with
defs much less annoying.)

Also this stuff you're saying about values having ownership and defs not having
ownership is, let's say, misleading; it only works if you're using a 
meaninglessly
broad definition of ownership.  It would be better to simply say that the 
verification
we want to do for ownership strongly encourages us to allow instructions to 
introduce multiple defs whose properties can be verified independently.

> 2. Specifying a set of ownership kinds and specifying a method for mapping a
>`SILValue` to an ownership kind.
> 3. Specifying ownership constraints on all `SILInstruction`s and 
> `SILArgument`s
>that constrain what ownership kinds their operands and incoming values
>respectively can possess.
> 4. Implementing a verifier to ensure that all `SILInstruction` and 
> `SILArgument`
>are compatible with the ownership kind propagated by their operand
>`SILValue`s and that pseudo-linear dataflow constraints are maintained.

I'll tackle these other sections in another email.  Let's go one at a time.

> # Cleanly separating Value and Def APIs in SIL
> 
> All values in SIL are defined via an assignment statement of the form: ` 
> = `.
> In English, we say `foo` is a value that is defined by the def
> `bar`. Originally, these two concepts were distinctly represented by the 
> classes
> `SILValue` and `ValueBase`. All `ValueBase` defined a list of `SILValue` that
> were related, but not equivalent to the defining `ValueBase`. With the 
> decision
> to represent multiple return values as instruction projections instead of as a
> list of `SILValue`, this distinction in between a def and the values was lost,
> resulting in `SILValue` being used interchangeably with `ValueBase` throughout
> the swift codebase. This exposes a modeling issue when one attempts to add
> ownership to SIL, namely that values have ownership, while the defs that 
> define
> the values do not. This implies that defs and values *should not* be
> interchangeable.

Again, I do not understand what you're trying to say about ownership here.
Just drop it.

> In order to model that values, not defs, have ownership, we separate the
> `SILValue` and `ValueBase` APIs. This is done by:

Almost all of this is based on what I consider to be a really unfortunate use
of the term "def".

Allow me to suggest this:

1. You do not need to rename ValueBase.  Let's stick with the term "Value"
instead of "Def" in the source code.

2. There are only three subclasses of ValueBase for now:
  - SILArgument
  - SingleInstructionResult
  - MultiInstructionResult
This means that the Kind can probably be packed into the use-list pointer.

3. SingleInstructionResult will only be used for instructions that are known to
produce exactly one value.  All such instructions can derive from a single
class, of which SingleInstructionResult can be a superclass.  This will make
it possible to construct a SILVal

[swift-dev] Proposal: SIL Ownership Model + Verifier

[Michael Gottesman via swift-dev]

This is a proposal for a new SIL Ownership Model and verifier. An online HTML 
version of the document is available here:

https://gottesmm.github.io/proposals/sil-ownership-model.html 


and inline below.

Michael



# Summary

This document defines a SIL ownership model and a compile time static verifier
for the model. This will allow for static compile time verification that a SIL
program satisfies all ownership model constraints.

The proposed SIL ownership model embeds ownership into SIL's SSA def-use
edges. This is accomplished by:

1. Formalizing into SIL API's the distinction in between defs
   (e.g. `SILInstruction` and `SILArgument`) and the values produced by defs
   (e.g. `SILValue`). This is needed to model values as having ownership and
   defs as not having ownership. The main implication here is that the two can
   no longer be implicitly convertible and the API must enforce this.
2. Specifying a set of ownership kinds and specifying a method for mapping a
   `SILValue` to an ownership kind.
3. Specifying ownership constraints on all `SILInstruction`s and `SILArgument`s
   that constrain what ownership kinds their operands and incoming values
   respectively can possess.
4. Implementing a verifier to ensure that all `SILInstruction` and `SILArgument`
   are compatible with the ownership kind propagated by their operand
   `SILValue`s and that pseudo-linear dataflow constraints are maintained.

# Cleanly separating Value and Def APIs in SIL

All values in SIL are defined via an assignment statement of the form: ` = 
`.
In English, we say `foo` is a value that is defined by the def
`bar`. Originally, these two concepts were distinctly represented by the classes
`SILValue` and `ValueBase`. All `ValueBase` defined a list of `SILValue` that
were related, but not equivalent to the defining `ValueBase`. With the decision
to represent multiple return values as instruction projections instead of as a
list of `SILValue`, this distinction in between a def and the values was lost,
resulting in `SILValue` being used interchangeably with `ValueBase` throughout
the swift codebase. This exposes a modeling issue when one attempts to add
ownership to SIL, namely that values have ownership, while the defs that define
the values do not. This implies that defs and values *should not* be
interchangeable.

In order to model that values, not defs, have ownership, we separate the
`SILValue` and `ValueBase` APIs. This is done by:

1. Renaming `ValueBase` to `ValueDef`. This makes it clear from a naming
perspective that a `ValueDef` is not a value, but may define values.
2. Eliminate all operator methods on `SILValue` that allow one to work with the
`ValueDef` API via a `SILValue` in favor of an explicit method for getting the
internal `ValueDef` of a `SILValue`, i.e.:

class SILValue {
  ...
  ValueDef *operator->() const; // deleted
  ValueDef &operator*() const; // deleted
  operator ValueDef *() const; // deleted

  bool operator==(ValueDef *RHS) const; // deleted
  bool operator!=(ValueDef *RHS) const; // deleted
  ...
  ValueDef *SILValue::getDef() const; // new
  ...
};

3. Use private access control and friend classes to only allow for `SILValue`s
   to be constructed and vended by their defining `ValueDef` via a new method on
   `ValueDef`:

class SILValue {
  friend class SILUndef; // new
  friend class SILArgument; // new
  friend class SILInstruction; // new
public:
  SILValue(ValueDef *); // deleted
private:
  SILValue(ValueDef *); // new
};

class ValueDef {
  ...
  SILValue getValue() const; // new
  ...
};

To see how specific common code patterns change in light of these changes,
please see the [appendix](#changes-to-silvalue-api-for-sil-ownership).

# Values and ValueOwnershipKinds

Define `ValueOwnershipKind` as the enum with the following cases:

enum class ValueOwnershipKind {
  Trivial,
  Unowned,
  Owned,
  Guaranteed,
}

Our approach to mapping a `SILValue` to a `ValueOwnershipKind` is to use a
`SILVisitor` called `ValueOwnershipKindVisitor`. This works well since if one
holds `ValueKind` constant, `SILValue` have well defined ownership
constraints. Thus we can handle each case individually via the visitor. We use
SILNodes.def to ensure that all `ValueKind` have a defined visitor method. This
will ensure that when a new `ValueKind` is added, the compiler will emit a
warning that the visitor must be updated, ensuring correctness.

The visitor will be hidden in a *.cpp file and will expose its output via a new
API on `SILValue` :

ValueOwnershipKind SILValue::getOwnershipKind() const;

Since the implementation of `SILValue::getOwnershipKind()` will be out of line,
none of the visitor code will be exposed t