Stream: Coq devs & plugin devs

Topic: native compiler bench

Pierre-Marie Pédrot (Apr 01 2021 at 15:17):

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

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

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

Pierre-Marie Pédrot (Apr 01 2021 at 15:20):

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

Enrico Tassi (Apr 01 2021 at 15:21):

on your machine?

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

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:21):

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

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

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:22):

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

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:22):

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

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

Pierre-Marie Pédrot (Apr 01 2021 at 15:23):

@Enrico Tassi what development are you talking about precisely?

Pierre-Marie Pédrot (Apr 01 2021 at 15:24):

before thrashing the bench I'd like to check locally

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

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

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.

Pierre-Marie Pédrot (Apr 01 2021 at 15:41):

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

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

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).

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.

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 13 2024 at 01:02 UTC