@@ -1675,17 +1675,17 @@ Ownership SSA
1675
1675
A SILFunction marked with the ``[ossa] `` function attribute is considered to be
1676
1676
in Ownership SSA form. Ownership SSA is an augmented version of SSA that
1677
1677
enforces 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
1679
1679
that defines the ownership semantics that the value models. All SIL operands
1680
1680
that 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::
1689
1689
1690
1690
sil @stash_and_cast : $@convention(thin) (@owned Klass) -> @owned SuperKlass {
1691
1691
bb0(%kls1 : @owned $Klass): // Definition of %kls1
@@ -1710,12 +1710,101 @@ inline::
1710
1710
1711
1711
Notice how every value in the SIL above has a partionable set of uses with
1712
1712
normal 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
1714
1714
do not have any leaks or use-after-frees in the above code.
1715
1715
1716
+ Ownership Kind
1717
+ ~~~~~~~~~~~~~~
1718
+
1716
1719
The 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:
1719
1808
1720
1809
* **None **. This is used to represent values that do not require memory
1721
1810
management and are outside of Ownership SSA invariants. Examples: trivial
@@ -1739,10 +1828,7 @@ different ownership kinds:
1739
1828
bitcasting a trivial type to a non-trivial type. This value should never be
1740
1829
consumed.
1741
1830
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.
1746
1832
1747
1833
Owned
1748
1834
`````
@@ -1912,10 +1998,26 @@ This is a form of ownership that is used to model two different use cases:
1912
1998
trivial pointer to a class. In that case, since we have no reason to assume
1913
1999
that the object will remain alive, we need to make a copy of the value.
1914
2000
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
+
1915
2016
Forwarding Uses
1916
2017
~~~~~~~~~~~~~~~
1917
2018
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 `_.
1919
2021
1920
2022
A subset of SIL instructions define the value ownership kind of their results in
1921
2023
terms of the value ownership kind of their operands. Such an instruction is
0 commit comments