+-- Note [Soundness of inlining]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- In the Hoopl paper, the soundness condition on rewrite functions is
+-- described as follows:
+--
+-- "If it replaces a node n by a replacement graph g, then g must
+-- be observationally equivalent to n under the assumptions
+-- expressed by the incoming dataflow fact f. Moreover, analysis of
+-- g must produce output fact(s) that are at least as informative
+-- as the fact(s) produced by applying the transfer function to n."
+--
+-- We consider the second condition in more detail here. It says given
+-- the rewrite R(n, f) = g, then for any incoming fact f' consistent
+-- with f (f' >= f), then running the transfer function T(f', n) <= T(f', g).
+-- For inlining this is not necessarily the case:
+--
+-- n = "x = a + 2"
+-- f = f' = {a = y}
+-- g = "x = y + 2"
+-- T(f', n) = {x = a + 2, a = y}
+-- T(f', g) = {x = y + 2, a = y}
+--
+-- y + 2 and a + 2 are not obviously comparable, and a naive
+-- implementation of the lattice would say they are incomparable.
+-- At best, this means we may be over-conservative, at worst, it means
+-- we may not terminate.
+--
+-- However, in the original Lerner-Grove-Chambers paper, soundness and
+-- termination are separated, and only equivalence of facts is required
+-- for soundness. Monotonicity of the transfer function is not required
+-- for termination (as the calculation of least-upper-bound prevents
+-- this from being a problem), but it means we won't necessarily find
+-- the least-fixed point.
+
+-- Note [Coherency of annotations]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- Is it possible for our usage annotations to become invalid after we
+-- start performing transformations? As the usage info only provides
+-- an upper bound, we only need to consider cases where the usages of
+-- a register may increase due to transformations--e.g. any reference
+-- to a local register in an AlwaysInline or AlwaysSink instruction, whose
+-- originating assignment was single use (we don't care about the
+-- many use case, because it is the top of the lattice). But such a
+-- case is not possible, because we always inline any single use
+-- register. QED.
+--
+-- TODO: A useful lint option would be to check this invariant that
+-- there is never a local register in the assignment map that is
+-- single-use.
+
+-- Note [Soundness of store rewriting]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- Its soundness depends on the invariant that no assignment is made to
+-- the local register before its store is accessed. This is clearly
+-- true with unoptimized spill-reload code, and as the store will always
+-- be rewritten first (if possible), there is no chance of it being
+-- propagated down before getting written (possibly with incorrect
+-- values from the assignment map, due to reassignment of the local
+-- register.) This is probably not locally sound.
+
projects / ghc-hetmet.git / commitdiff