SIL Ownership Model

Table of Contents

Abstract

Today, SIL does not express or validate ownership properties internally to a SILFunction. This increases the difficulty of SILGening “ownership correct” SIL and optimizing ownership in an effective, safe way. This document proposes an ownership model for SIL based around an augmented form of SSA called Ownership SSA (OSSA). This in combination with SIL expressing ownership semantics along call graph edges will allow for entire Swift programs to be verified as statically preserving ownership invariants. We describe OSSA below:

Ownership SSA Formally

Let f be a SIL function. A SSA value v in f is immortal and can be referenced at any point dominated by v’s definition. When SIL is in OSSA form, we extend SSA by requiring that all such v provide a static map from any point p dominated by v to a boolean discriminator that defines whether or not a use of v at p results in f being ill-formed. We call this the availability map for v at p and write Availability(v)(p). We require Availability(v)(p) to have the following properties:

By specifying properties of a value’s availability map, we can define ownership semantics for the value and enforce them in SIL. The first kind of ownership semantic that we define is that of the “owned” value. Let v be an owned value in f. Then v must have the following properties:

Given an owned value o, we can derive scoped “borrowed” values from o via “borrow operations”. We require any such b to have the following properties:

Naturally, we can iterative apply additional borrow operations to b to get additional b’ that have dependent lifetime on b (and thus o as well). An owned value and the associated borrow values in OSSA form a semantic value. Define a semantic value, s, as a rooted subgraph of the def-use graph of f with a singular owned value root, Root(s) and for which the set of all non-root values, Borrow(s), are derived from Root(s) via iterative borrow operations. Conceptually all values in s refer to the same underlying semantic program entity (e.g. a class instance or a struct with non-trivial fields). Via corrolaries to our previous definitions, it is easy to see that:

  1. Root(s) must be available if any Borrow(s) is available. This follows from borrowed values having dependent availability.

Now that we have our abstract model of Ownership SSA, we define how this is implemented in SIL.

Ownership SSA In SIL

In order to define this model in SIL, we begin by defining our owned and borrowed values. We extend the categorization slightly since in SIL we must also consider objc-bridging and trivial values. This results in us classifying values in the following four categories:

In code, these are modeled as cases of the enum ValueOwnershipKind. Just like we categorize the ownership semantics of values, we categorize the ownership semantics of the effects of these upon their operand values:

While Point and Consuming only effect the incoming value to the instruction, Forwarding and Reborrow operands additionally constrain the results of instructions as follows:

These categories will be modeled in the compiler via the enum OperandOwnershipUseKind.

SIL Changes for OSSA

To implement this proposal, several structural changes must be made to SIL. We go through each below:

Functions

To distinguish in between functions in OSSA form and those that are not, we define a new SILFunction attribute called [ossa] that signifies that a function is in OSSA form and must pass the ownership verifier.

SILValue

We add two new methods to SILValue’s API:

ValueOwnershipKind SILValue::getOwnershipKind() const;
bool SILValue::verifyOwnership() const;

The first API returns the ownership kind associated with the value. This is implemented via a visitor struct that statically can map a value via its ValueKind to the relevant ownership semantics.

The second API returns true if the value considered as a def is compatible with its users.

Operand

The only changed required of Operand is the addition of a new API:

OperandOwnershipUseKind Operand::getOwnershipUseKind() const;

This returns the statically mapped use semantics of this operand.

Instruction

The addition of ownership does not change the textual or in memory representation of SILInstructions but semantically adds new requirements upon each instruction. Each of these ownership semantics will be documented in SIL.rst and will be enforced via the ownership verifier. We describe the more important categories of instructions below.

Borrow Instructions

The instructions are used to introduce new borrow values:

Lifetime Maintenance Instructions

These instructions are used to manipulate the lifetime of non-trivial values. Specifically:

Function Application/Coroutine Instructions

Function Application instructions such as apply, try_apply generally have OperandOwnershipUseKind semantics that one would expect except for one special case: function parameters that are passed @guaranteed. In this case since the use of the @guaranteed value is immediate upon function application, we treat the use as a point use.

In constrast, since coroutines are not evaluated instantaneously, we require that coroutine instructions perform a form of “pseudo” reborrowing. Specifically:

ForwardOrReborrow Instructions

There are certain classes of instructions that we allow to have either Forwarding or Reborrow operands. To ensure consistency, we only allow for this property to be set when the instruction is constructed. Some examples of these types of instructions:

NOTE: That unchecked_enum_data is a special case since enums always contain conceptually a single tuple as their payload.

Value Projections and Destructures

Value projections such as tuple_extract, struct_extract that allow for one to access the internal fields of a value without destroying the value. This implies that the original value can not be destroyed. As such we model these as instructions with Reborrow semantics. In contrast, destructure operations such as destructure_struct and destructure_tuple take in a single value and split it up into the constituant first level fields of the value. As such, we model destructure operations as having Forwarding ownership.

SILArgument

In order to support the ownership model, we require the following changes to SILArgument:

  1. All SILArguments must specify a fixed ValueOwnershipKind on construction.

  2. All SILPhiArguments are treated like an instruction result of the set of predecessor terminators. This means that the rules around Forwarding and Reborrow operands apply to any such SILPhiArguments.

  3. Any SILArgument with Borrowed ownership is not required to have pairing end_borrows. This is because a SILFunctionArgument naturally has an end_borrow like scope (the function itself) and SILPhiArguments with Guaranteed ownership rely on the end_borrow set of its incoming values.