[MLton-devel] linearity related optimizations

[Matthew Fluet]

> Consider an analysis that determines a boxing criteria for every
> heap-allocated object based on the intuition that a value is boxed if it has
> at least 2 outstanding references *at any given instant*.  This means that an
> object may in fact during its lifetime be referenced by many different
> objects; provided that not more than 1 reference exists at any given point,
> this  object can take on an unboxed representation.
>
> So, in the contrived example,
>
> let val x = (a,b)
>     fun g( (a,b), z) = if odd? z
>                               then a
>                             else b
>     fun f (z) = g (x,z)
>     val h = f 13
>     val j = f 14
> in h + j
> end
>
> x would be a candidate for an unboxed representation.

I'm not sure where x is being flattented into?  The closure of f?  I guess
that makes sense.  But I'm not sure where that is a linearity analysis
versus a closure representation decision (with a possible coercion at g's
call site).  Is there another motivating example you have in mind?

> I'm wondering whether there's likely to be substantial benefit to such
> transformations in the new RSSA world that represents objects via
> memory chunks, and whether it's worth exploring the application (suitably
> modified) of linearity-based analyses on an RSSA target.

I'll chime in with the linearity/mutability analysis I'd most like to see
in MLton.  Something along the lines of Clean's uniqueness types with the
idea of identifying compile-time garbage collection opportunities.  The
motivating example is the basis implementation of List.map, which builds
the mapped list in reverse order (in constant stack) and then reverses the
resulting list (also in constant stack). Clearly, that intermediate list
is used ephemerally, and it's also used linearly.  We'd like to identify
the "top" cons cell during the reverse as being dead and therefore reuse
the space.  Essentially, you'd get a tail-reversing implementation.
The mutability in RSSA is key: you'd initially allocate a tuple with all
mutable fields.  A coercion to immutable would need to be accompanied with
a proof of linearity.  (This would have the side effect of "proving" that
the basis library implementation of vectors on top of mutable arrays was
correct.)  Normally, you'd use the "trivial" linearity analysis of doing
the coercion immediately after allocation.  But, in the list case above,
you'd let the list exist with a mutable tail field so that during the
reversal you could avoid the second allocation.  After the tail update,
you'd then coerce it to immutable, so that the rest of the program uses it
as a "normal" immutable list.



-------------------------------------------------------
This sf.net email is sponsored by: To learn the basics of securing 
your web site with SSL, click here to get a FREE TRIAL of a Thawte 
Server Certificate: http://www.gothawte.com/rd524.html
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel