[CakeML-dev] speed of evaluation in logic

[Anthony Fox]

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.

Cheers,
Anthony

> 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?