[CakeML-dev] speed of evaluation in logic

[Ramana Kumar]

Hello again,

I have done some more detailed experiments timing evaluation in the logic
of different parts of the compiler (on a small section of the hello world
program - basically an initial segment of the basis library).
The comparison is (roughly) between the [BOOT] custom
parallelised-where-possible evaluation strategy originally used in the
bootstrap evaluation, and the [EVAL] strategy of calling
computeLib.CBV_CONV without any customisation (but using the compiler
compset).
Here are the takeaway points:
- For compilation from source to labLang, the BOOT method is consistently
faster by a small amount (10-30%)
- For compilation from labLang to target, EVAL is _much_ faster, like 8x.

So: we can split the evaluation and use BOOT for compilation down to
labLang then EVAL for the rest, to get the best of both methods.

I am confused about how EVAL is getting so much speed in lab_to_target.
Bear in mind that this is without parallelisation (afaik), which BOOT uses
a lot in this phase of compilation. My current guess is that there must be
some very smart custom conversions installed for lab_to_target that don't
fire under BOOT's strategy. For example, did anyone write custom
conversions for calculating sec_ok for previously encoded instructions?
Calculating sec_ok under BOOT's strategy, even in parallel, often takes
longer than EVAL on the entire lab_to_target evaluation. I know there are
custom conversions for memoising the encoder (which both strategies benefit
from), but are those custom conversions doing more than I'm aware of?

Cheers,
Ramana

On 1 May 2017 at 23:52, Magnus Myreen <magnus.myreen at gmail.com> wrote:

> If I remember correctly, the standard kernel has special combined
> primitives and other tricky for fast EVAL. Maybe your conversions
> weren't using the right things in the kernel. -- Magnus
>
> On 1 May 2017 at 15:16, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> > Hi all,
> >
> > On the cleanup branch I've been making the compilation-in-logic method
> used
> > by the bootstrap into a library to be used for compiling in the logic
> > generally. (This is issue #249.) The bootstrap method involves lots of
> > custom conversions and parallelised evaluation where possible.
> Preliminary
> > use of it to compile the characteristic examples suggests, however, that
> it
> > might be a lot slower than what was used before (essentially EVAL using
> the
> > compiler compset).
> >
> > While we might expect some slowdown due to additional printing and
> > intermediate definitions, I would have overall expected a speedup. I'm
> just
> > noticing this based on my recollection of building the examples the EVAL
> way
> > (15 mins I thought) and so may be totally wrong about the slowdown. More
> > careful experiments would need to be done. And if EVAL really is faster,
> I'd
> > want to understand why! Or how to exploit it further!
> >
> > Systematic experiments on various strategies for evaluation in the logic
> > could be interesting. We have a big program (the compiler) to do them
> with.
> > I tried various strategies for one compilation phase once (it's still in
> the
> > comments of x64BootstrapScript.sml) and could never beat EVAL and never
> > understood why not, because I was doing the most direct efficient custom
> > conversion I thought possible.
> >
> > On a separate note, I will be out of contact (and not working on CakeML -
> > I'll be at an intensive training camp) from Wednesday for a week. I hope
> > nothing urgent comes up, and if you want to plan for any contingencies
> > beforehand, email me. (I will probably still have email during the week,
> but
> > not much access.)
> >
> > Cheers,
> > Ramana
> >
> > _______________________________________________
> > Developers mailing list
> > Developers at cakeml.org
> > https://lists.cakeml.org/listinfo/developers
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170518/bdc17a39/attachment.html>