Add allocation-free variants of the nextup and nextdown floating-point operations.

Floating-point values are boxed, which means that any operation causes an
allocation. While short-lived, they nonetheless cause the minor heap to
fill, which in turn triggers the garbage collector.

To reduce the number of allocations, I initially went with a shadow stack
mechanism for storing floating-point values. But assuming the CoqInterval
library is representative, this was way too complicated in practice, as
most stack-located values ended up being passed to nextdown and nextup
before being stored in memory.

So, this commit implements a different mechanism. Variants of nextdown and
nextup are added, which reuse the allocation of their input argument.
Obviously, this is only correct if there is no other reference to this
argument. To ensure this property, the commit only uses these opcode
during a peephole optimization. If two primitive operations follow one
another, then the second one can reuse the allocation of the first one,
since it never had time to even reach the stack.

For CoqInterval, this divides the number of allocations due to
floating-point operations by about two.

The following snippet is made 4% faster by this commit (and 13% faster if
we consider only the floating-point operations).

    From Coq Require Import Int63 BinPos PrimFloat.
    Definition foo n :=
      let eps := sub (next_up one) one in
      Pos.iter (fun x => next_down (add x eps)) two n.
    Time Eval vm_compute in foo 100000000.

1 files changed, 14 insertions, 0 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0f7713a6bb..3c3f45f7e6 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1753,6 +1753,20 @@ value coq_interprete
         Next;
       }
 
+      Instruct (CHECKNEXTUPFLOATINPLACE) {
+        print_instr("CHECKNEXTUPFLOATINPLACE");
+        CheckFloat1();
+        Store_double_val(accu, nextafter(Double_val(accu), INFINITY));
+        Next;
+      }
+
+      Instruct (CHECKNEXTDOWNFLOATINPLACE) {
+        print_instr("CHECKNEXTDOWNFLOATINPLACE");
+        CheckFloat1();
+        Store_double_val(accu, nextafter(Double_val(accu), -INFINITY));
+        Next;
+      }
+
       Instruct(CHECKCAMLCALL2_1) {
         // arity-2 callback, the last argument can be an accumulator
         value arg;