The translator seems to be fairly slow.

CakeML / cakeml

CakeML: A Verified Implementation of ML

https://cakeml.org

Other

964 stars 84 forks source link

The translator seems to be fairly slow. #527

Closed talsewell closed 5 years ago

talsewell commented 6 years ago

In some recent regression runs, the translator is the first "really slow" task.

For instance, in regression 491, the time taken was approximately 5-6 hours for proofs, 5-6 hours for translation, and 10-15 hours each for the 32/64 bit self-bootstraps.

Of those, it looks like the translation might be the easiest to try to speed up.

The idea of this issue is to gather thoughts on what might be improved.

It was suggested that manipulating the value environment repeatedly is an issue. I've done an experiment which suggests that this isn't a big issue. I don't know if the progress so far on the "abstract translator" (see #202 ) is relevant or not.

It was also suggested that the treatment of EqualityType left room for improvement. That will be the next place I look.

talsewell commented 6 years ago

On advice from @agomezl I scraped the regression history. There's no interesting trend in the translation times, they're pretty constant, though there are some strange outliers I don't understand (specifically 455).

formrre commented 6 years ago

I have just looked at 455 and am suspecting the translation looks faster because its timing was taken since the resumption, not since the the start.

talsewell commented 6 years ago

Some updates about this:

some information was extracted from run 502. I can attach the file here if anyone wants to look.
by the time the translation is working in compiler64ProgScript, it is pretty slow, taking 10-30secs per function.
nearly all the elapsed time is spent during the three-way split in translate_options (rec/fun/val).
naively, the candidate issues could be the various ml_prog_updates and add_v_thms
@oskarabrahamsson and I had a chat about this, and our money is on the work done processing the theorem 'th' in add_Dlet/add_Dletrec etc.

talsewell commented 6 years ago

There's some progress on this in PR 551: https://github.com/CakeML/cakeml/pull/551

Some of the above summary was wrong. I'll include more of an explanation of the current state if/when the above PR is merged.

xrchz commented 5 years ago

@talsewell is this done now?

talsewell commented 5 years ago

Yes, I think that all the obvious major issues have been addressed. If anyone's using the translator interactively and comes across particular things that are annoying, we can investigate them specifically.