@@ -1675,17 +1675,17 @@ Ownership SSA
16751675A SILFunction marked with the ``[ossa] `` function attribute is considered to be
16761676in Ownership SSA form. Ownership SSA is an augmented version of SSA that
16771677enforces ownership invariants by imbuing value-operand edges with semantic
1678- ownership information. All SIL values are statically assigned an ownership kind
1678+ ownership information. All SIL values are assigned a constant ownership kind
16791679that defines the ownership semantics that the value models. All SIL operands
16801680that use a SIL value are required to be able to be semantically partitioned in
1681- between "normal uses" that just require the value to be live and "consuming
1682- uses" that end the lifetime of the value and after which the value can no longer
1683- be used. Since operands that are consuming uses end a value's lifetime,
1684- naturally we must have that the consuming use points jointly post-dominate all
1685- non-consuming use points and that a value must be consumed exactly once along
1686- all reachable program paths, preventing leaks and use-after-frees. As an
1687- example, consider the following SIL example with partitioned defs/uses annotated
1688- inline::
1681+ between "non-lifetime ending uses" that just require the value to be live and
1682+ "lifetime ending uses" that end the lifetime of the value and after which the
1683+ value can no longer be used. Since by definition operands that are lifetime
1684+ ending uses end their associated value's lifetime, we must have that the
1685+ lifetime ending use points jointly post-dominate all non-lifetime ending use
1686+ points and that a value must have exactly one lifetime ending use along all
1687+ reachable program paths, preventing leaks and use-after-frees. As an example,
1688+ consider the following SIL example with partitioned defs/uses annotated inline::
16891689
16901690 sil @stash_and_cast : $@convention(thin) (@owned Klass) -> @owned SuperKlass {
16911691 bb0(%kls1 : @owned $Klass): // Definition of %kls1
@@ -1710,12 +1710,101 @@ inline::
17101710
17111711Notice how every value in the SIL above has a partionable set of uses with
17121712normal uses always before consuming uses. Any such violations of ownership
1713- semantics would trigger a static SILVerifier error allowing us to know that we
1713+ semantics would trigger a SILVerifier error allowing us to know that we
17141714do not have any leaks or use-after-frees in the above code.
17151715
1716+ Ownership Kind
1717+ ~~~~~~~~~~~~~~
1718+
17161719The semantics in the previous example is of just one form of ownership semantics
1717- supported: "owned" semantics. In SIL, we allow for values to have one of four
1718- different ownership kinds:
1720+ supported: "owned" semantics. In SIL, we map these "ownership semantics" into a
1721+ form that a compiler can reason about by mapping semantics onto a lattice with
1722+ the following elements: `None `_, `Owned `_, `Guaranteed `_, `Unowned `_, `Any `. We
1723+ call this the lattice of "Ownership Kinds" and each individual value an
1724+ "Ownership Kind". This lattice is defined as a 3-level lattice with::
1725+
1726+ 1. None being Top.
1727+ 2. Any being Bottom.
1728+ 3. All non-Any, non-None OwnershipKinds being defined as a mid-level elements of the lattice
1729+
1730+ We can graphically represent the lattice via a diagram like the following::
1731+
1732+ +------+
1733+ +-------- | None | ---------+
1734+ | +------+ |
1735+ | | |
1736+ v v v ^
1737+ +-------+ +-----+------+ +---------+ |
1738+ | Owned | | Guaranteed | | Unowned | +--- Value Ownership Kinds and
1739+ +-------+ +-----+------+ +---------+ Ownership Constraints
1740+ | | |
1741+ | v | +--- Only Ownership Constraints
1742+ | +-----+ | |
1743+ +-------->| Any |<----------+ v
1744+ +-----+
1745+
1746+ One moves down the lattice by performing a "meet" operation::
1747+
1748+ None meet OtherOwnershipKind -> OtherOwnershipKind
1749+ Unowned meet Owned -> Any
1750+ Owned meet Guaranteed -> Any
1751+
1752+ and one moves up the lattice by performing a "join" operation, e.x.::
1753+
1754+ Any join OtherOwnershipKind -> OtherOwnershipKind
1755+ Owned join Any -> Owned
1756+ Owned join Guaranteed -> None
1757+
1758+ This lattice is applied to SIL by requiring well formed SIL to:
1759+
1760+ 1. Define a map of each SIL value to a constant OwnershipKind that classify the
1761+ semantics that the SIL value obeys. This ownership kind may be static (i.e.:
1762+ the same for all instances of an instruction) or dynamic (e.x.: forwarding
1763+ instructions set their ownership upon construction). We call this subset of
1764+ OwnershipKind to be the set of `Value Ownership Kind `_: `None `_, `Unowned `_,
1765+ `Guaranteed `_, `Owned `_ (note conspiciously missing `Any `). This is because
1766+ in our model `Any ` represents an unknown ownership semantics and since our
1767+ model is strict, we do not allow for values to have unknown ownership.
1768+
1769+ 2. Define a map from each operand of a SILInstruction, `i `, to a constant
1770+ Ownership Kind, Boolean pair called the operand's `Ownership
1771+ Constraint `_. The Ownership Kind element of the `Ownership Constraint `_
1772+ determines semantically which ownership kind's the operand's value can take
1773+ on. The Boolean value is used to know if an operand will end the lifetime of
1774+ the incoming value when checking dataflow rules. The dataflow rules that each
1775+ `Value Ownership Kind `_ obeys is documented for each `Value Ownership Kind `_
1776+ in its detailed description below.
1777+
1778+ Then we take these two maps and require that valid SIL has the property that
1779+ given an operand, ``op(i) `` of an instruction ``i `` and a value ``v `` that
1780+ ``op(i) `` can only use ``v `` if the ``join `` of
1781+ ``OwnershipConstraint(operand(i)) `` with ``ValueOwnershipKind(v) `` is equal to
1782+ the ``ValueOwnershipKind `` of ``v ``. In symbols, we must have that::
1783+
1784+ join : (OwnershipConstraint, ValueOwnershipKind) -> ValueOwnershipKind
1785+ OwnershipConstraint(operand(i)) join ValueOwnershipKind(v) = ValueOwnershipKind(v)
1786+
1787+ In words, a value can be passed to an operand if applying the operand's
1788+ ownership constraint to the value's ownership does not change the value's
1789+ ownership. Operationally this has a few interesting effects on SIL::
1790+
1791+ 1. We have defined away invalid value-operand (aka def-use) pairing since the
1792+ SILVerifier validates the aforementioned relationship on all SIL values,
1793+ uses at all points of the pipeline until ossa is lowered.
1794+
1795+ 2. Many SIL instructions do not care about the ownership kind that their value
1796+ will take. They can just define all of their operand's as having an
1797+ ownership constraint of Any.
1798+
1799+ Now lets go into more depth upon `Value Ownership Kind `_ and `Ownership Constraint `_.
1800+
1801+ Value Ownership Kind
1802+ ~~~~~~~~~~~~~~~~~~~~
1803+
1804+ As mentioned above, each SIL value is statically mapped to an `Ownership Kind `_
1805+ called the value's "ValueOwnershipKind" that classify the semantics of the
1806+ value. Below, we map each ValueOwnershipKind to a short summary of the semantics
1807+ implied upon the parent value:
17191808
17201809* **None **. This is used to represent values that do not require memory
17211810 management and are outside of Ownership SSA invariants. Examples: trivial
@@ -1739,10 +1828,7 @@ different ownership kinds:
17391828 bitcasting a trivial type to a non-trivial type. This value should never be
17401829 consumed.
17411830
1742- We describe each of these semantics in more detail below.
1743-
1744- Value Ownership Kind
1745- ~~~~~~~~~~~~~~~~~~~~
1831+ We describe each of these semantics in below in more detail.
17461832
17471833Owned
17481834`````
@@ -1912,10 +1998,26 @@ This is a form of ownership that is used to model two different use cases:
19121998 trivial pointer to a class. In that case, since we have no reason to assume
19131999 that the object will remain alive, we need to make a copy of the value.
19142000
2001+ Ownership Constraint
2002+ ~~~~~~~~~~~~~~~~~~~~
2003+
2004+ NOTE: We assume that one has read the section above on `Ownership Kind `_.
2005+
2006+ As mentioned above, every operand ``operand(i) `` of a SIL instruction ``i `` has
2007+ statically mapped to it:
2008+
2009+ 1. An ownership kind that acts as an "Ownership Constraint" upon what "Ownership
2010+ Kind" a value can take.
2011+
2012+ 2. A boolean value that defines whether or not the execution of the operand's
2013+ instruction will cause the operand's value to be invalidated. This is often
2014+ times referred to as an operand acting as a "lifetime ending use".
2015+
19152016Forwarding Uses
19162017~~~~~~~~~~~~~~~
19172018
1918- NOTE: In the following, we assumed that one read the section above, `Value Ownership Kind `_.
2019+ NOTE: In the following, we assumed that one read the section above, `Ownership
2020+ Kind `_, `Value Ownership Kind `_ and `Ownership Constraint `_.
19192021
19202022A subset of SIL instructions define the value ownership kind of their results in
19212023terms of the value ownership kind of their operands. Such an instruction is
0 commit comments