[CakeML-dev] speed of evaluation in logic
acjf3 at cam.ac.uk
Tue May 23 13:59:19 UTC 2017
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
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 =
|> (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