native compute · Miscellaneous · Zulip Chat Archive

@Maxime Dénès We've run a big computation in Coq with native_compute (36h) and the extracted code with ocamlopt (14h). The code is fairly simple, little use of dependent types. Does the difference of timings seem correct?

Guillaume Melquiond (Mar 25 2021 at 09:10):

You cannot expect native_compute to run as fast as extracted code. Indeed, it has to handle the case of open terms. For instance, while fst x is basically free for extracted code, it is quite costly for native_compute. I am not sure it can incur such a slowdown, but it should not be that far.

Pierre-Marie Pédrot (Mar 25 2021 at 09:12):

I think @Jason Gross did a bit of benchmarking for this situation, and indeed the difference was somewhere in the 2-3x range.

Bas Spitters (Mar 25 2021 at 09:14):

To be sure, I'm not complaining, just trying so see whether the numbers are expected.

Pierre-Marie Pédrot (Mar 25 2021 at 09:19):

for higher-order code, expect even more slowdown: https://github.com/coq/coq/issues/8019

Guillaume Melquiond (Mar 25 2021 at 09:31):

Did you mean dependent types? Because higher-order is not an issue, as far as I know. But computing types is.

Enrico Tassi (Mar 25 2021 at 09:53):

Out of curiosity, which ocaml version are you using @Bas Spitters ?

Maxime Dénès (Mar 25 2021 at 10:07):

@Bas Spitters Hi ! This not entirely unexpected, but sill in the high range of what I'd expect. Of course, it depends a lot of the nature of the code. Performance overhad can come from the handling of open terms or computing in types, as @Guillaume Melquiond wrote, or even in some cases from explicit polymorphism: sometimes having a lot of arguments can make the use of registers less smart, even when the values are not really useful. Extraction erases some of these arguments.

Pierre-Marie Pédrot (Mar 25 2021 at 10:29):

@Guillaume Melquiond in HO code you'll pay for closure normalization, which doesn't happen in weak-head CBV.

Pierre-Marie Pédrot (Mar 25 2021 at 10:30):

BTW, I am currently trying to get a working POC removing the naked pointer use of accumulators following Xavier Leroy's proposal, and I am quite afraid this will have terrible consequences on perfs.

Guillaume Melquiond (Mar 25 2021 at 10:41):

Pierre-Marie Pédrot said:

in HO code you'll pay for closure normalization, which doesn't happen in weak-head CBV.

If the final results contains closures, then I agree. But, hopefully, that is not what is being computed here, and the result is a just a plain concrete value.