Stream: Coq users

Topic: Overhead of cbv vs. vm_compute

Michael Soegtrop (Mar 29 2021 at 16:04):

I wonder if in case I don't need any special reduction scheme for cbv I should always use vm_compute, or if vm_compute has some one time overhead which depends on the input / output size of the computed term, so that cbv is faster for simple terms.

Guillaume Melquiond (Mar 29 2021 at 16:39):

There is an overhead for compiling the currently evaluated term to bytecode, but as long as your computation takes a few milliseconds, vm_compute should always end up much faster than cbv. Do note, however, that there are implicit rules for cbv, since it respects Opaque, contrarily to vm_compute.

Michael Soegtrop (Mar 30 2021 at 07:51):

@Guillaume Melquiond : thanks for the background information! So the overhead does not depend on the term size (does it for native compute?) but on the complexity of the function to be evaluated.

Is the compilation done dynamically once for each Gallina function as soon as it is hit in vm_compute or does it compile the complete call tree on call of vm_compute? Are the compilations cached at least for the duration of one vernacular command (possibly multiply calls of vm_compute in one high level tactic)?

Guillaume Melquiond (Mar 30 2021 at 08:04):

Compilation is done statically at the time of each Definition (and then stored in .vo files). Then there is a compilation of the current goal at the time of vm_compute. There is also a linking phase at the time of vm_compute to combine all the precompiled definitions. These two are the only overhead of vm_compute with respect to cbv, but it has never been noticeable. I suppose you could make it noticeable by having a very huge goal containing lots of let-in constructs. But nobody ever complained.

For native_compute in ondemand mode, the compilation of every Definition is done dynamically at the time of native_compute, so the overhead can be huge. In yes mode, it behaves similarly to vm_compute. But you still need to pay the overhead of invoking ocamlopt to compile and link the current goal.

Jason Gross (Apr 03 2021 at 11:56):

Beware also that vm_compute does not reduce the indices of inductive constructors. This may be a benefit or a detriment

Cody Roux (Apr 05 2021 at 14:00):

Guillaume Melquiond said:

There is an overhead for compiling the currently evaluated term to bytecode, but as long as your computation takes a few milliseconds, vm_compute should always end up much faster than cbv. Do note, however, that there are implicit rules for cbv, since it respects Opaque, contrarily to vm_compute.

Which can be a huge deal!

Last updated: Sep 26 2023 at 11:01 UTC