[CakeML-dev] speed of evaluation in logic

Anthony Fox acjf3 at cam.ac.uk
Tue May 23 13:59:19 UTC 2017

Hi Ramana,

I’ve finally found some time to look into this a bit...

One big problem seems to be the use of ListConv1.ALL_EL_CONV when computing secs_ok. It’s performance seems to be dreadful in comparison to EVAL. Replacing

  ListConv1.ALL_EL_CONV eval_T

with just eval_T gave me a timing for that section of

  sec_ok (par) real: 0.67728s

which was a big improvement. However, there seem to be problems elsewhere as well. For example, flat_bytes is computed slowly. In this case

val flat_bytes =
      listSyntax.mk_flat(rconc map_line_bytes')
      |> (REWRITE_CONV (List.rev bytes_defs) THENC eval)

is nine times faster than current version. Another slow computation is enc_secs_again, so I suspect that this could be improved as well.

It may be simplest to stick with EVAL for to_bytes_x64, as it’s performance seems hard to beat.


> On 18 May 2017, at 07:37, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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?

More information about the Developers mailing list