Stream: Coq devs & plugin devs

Topic: native compiler bench


view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 15:17):

do we have a reasonable set of micro-benchmarks for the native compiler?

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 15:18):

I've written a patch to get rid of the naked pointer hack and would like to see how terrible it is

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:19):

@Guillaume Melquiond uses native compute on real examples, I think this is better than a micro bench

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 15:20):

but I have no easy way to bench it, haven't I?

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:21):

on your machine?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 15:21):

@Pierre-Marie Pédrot patch for the bench should be pretty simple tho, basically add

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 15:21):

https://github.com/coq/coq/pull/12974

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 15:21):

actually I have no idea anymore what is going on the bench due to the way it was merged wihtout review

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 15:22):

should be okish tho if it is using opam to build Coq

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 15:22):

I will add the default support for native once we get coqnative merged

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 15:23):

As I wrote on https://github.com/coq/coq/pull/13287 I'd really like to it unstuck and merged

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 15:23):

@Enrico Tassi what development are you talking about precisely?

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 15:24):

before thrashing the bench I'd like to check locally

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 15:25):

Actually the bench will only test the performance of the ocaml compiler, not sure there are a lot of calls to native_compute there actually

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:25):

I think it was the interval one, but I'm not 100 sure. anyway, grep native_compute should tell you

view this post on Zulip Guillaume Melquiond (Apr 01 2021 at 15:38):

Yes, CoqInterval makes use of native_compute, if asked to. So, you could opam pin your Coq build, then build CoqInterval. Then I can give you some lengthy computations.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 15:41):

I pushed my PR there: https://github.com/coq/coq/pull/14048

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 15:41):

I'll try to compile interval without having to boot up a fresh OPAM switch though

view this post on Zulip Guillaume Melquiond (Apr 01 2021 at 15:51):

Here is an example:

From Coq Require Import Reals.
From Coquelicot Require Import Coquelicot.
From Interval Require Import Tactic.
Goal True.
(* just in case native_compute is "ondemand" *)
integral_intro (RInt (fun x => sin (x + exp x)) 0 8) with (i_delay, i_native_compute) as _.
(* it takes about 1 second per 1k fuel, change the fuel amount accordingly *)
Time integral_intro (RInt (fun x => sin (x + exp x)) 0 8)
  with (i_width (-40), i_fuel 10000, i_delay, i_native_compute).

view this post on Zulip Jason Gross (Apr 01 2021 at 22:23):

@Pierre-Marie Pédrot https://github.com/mit-plv/fiat-crypto/blob/master/src/UnsaturatedSolinasHeuristics/Tests.v is one of the few cases I've seen where native_compute is much, much faster than vm_compute. The current tests are supposed to take about 40s in native_compute, though by just adjusting the filter on line 145 from 2^350 to 2^401 you can double the length of the test. We have tests set up all the way up to 2^521, but expect these to be very very slow.

view this post on Zulip Jason Gross (Apr 01 2021 at 22:24):

If you want to factor this out into a standalone benchmark, I expect the fully inlined file will only be 1000--2000 loc.


Last updated: Oct 21 2021 at 21:03 UTC