Port native_compute to OCaml 5 (using tag 0).

[silene]

This is a variant of #20396, except that we keep using tag 0 for accumulators, instead of switching to tag 247. As a consequence, this pull request does not modify the code generated by native_compute at all. So, any difference in performance is purely due to intrinsic changes between OCaml 4 and OCaml 5. (And there is no noticeable difference if one stays on OCaml 4.)

The trick is as follows. Since OCaml 5 no longer accepts naked pointers in blocks with tag 0, we just need to make sure that the closures that represent accumulators only contain non-naked pointers. The main offender is the first field of a closure, which is the code pointer, but we can solve the issue by putting the code inside an out-of-heap block. Obviously, this will cause the garbage collector to instantly segfault on any R^X-enabled kernel. (No idea whether OCaml supports them.)

This approach is extremely fragile. (Much more than #20396.) Indeed, the OCaml compiler is sometimes very creative in the way it compiles the simple closure fun x -> accumulate data x. This is the reason why Landin's knot is used here instead of a standard recursive definition. A different approach, less fragile, would be to add the following three lines to the assembly block, so that we no longer depend on the way the compiler compiled the closure, at the expense of a deeper knowledge of OCaml's calling convention:

mov %rax, %rdi
mov 16(%rbx), %rax
mov %rdi, %rbx

Anyway, as with #20396, this pull request is not meant to be applied and is just there for people to experiment with native_compute on OCaml 5. @gasche

EDIT: Since I finally went for the less fragile variant, this pull request is actually release-worthy.

[ppedrot]

@coqbot bench native

[SkySkimmer]

Bench won't work, this is based on some too old commit

[silene]

I finally went for the longer, more robust, version. As a consequence, with OCaml 4, the only difference before and after this pull request is that, when accumulating something on top of an open term, the execution of

jmp camlNativevalues__accumulate_xxx@PLT

is replaced by the execution of

mov coq_accumulate_addr@GOTPCREL(%rip), %rdi
jmp *(%rdi)

Everything else is strictly identical.

If we had some way of guessing the hash xxx produced by the OCaml compiler, then we could directly jump to the correct function (instead of having to first load its address from coq_accumulate_addr) and the code executed by native_compute would thus be exactly the same. But this difference does not matter much in practice. First, this path is only executed when manipulating open terms, and second, the jump is perfectly predicted by the processor, since the target never changes.

Another way to see it is that the only difference ends up being the two lines

.align 8
.quad 3067

If the OCaml compiler had inserted them itself, then we would never have add to do anything. The original code would have worked both on OCaml 4 and OCaml 5.

[ppedrot]

This is not meant for merging, so let's close.

[silene]

Actually, the comment was on the original fragile version. The robust version of the pull request could actually be applied. (I should have removed the sentence when I dropped the old version.)

[ppedrot]

This is not very portable, isn't it? What about the M1 users for instance?

[silene]

If an M1 user wants to use native_compute with OCaml 5, they need to provide the equivalent five lines of assembly code. So, it is a political decision. Do we want to forbid x86-64 users from using native_compute because M1 users cannot?

(To be fair, I should be able to write the corresponding code for Arm. It is just that I have no way of testing it. It is better that it is someone who can test it who does the job.)

[ppedrot]

Also we didn't test the performance difference because this PR was based on an old commit. Maybe you should rebase before we assess the protocol.

[silene]

Or maybe do the opposite? That is, we should assess the protocol before I rebase. For instance, if you want to be able to test the performance on some representative use case of native_compute (e.g., the BB(5) challenge, which I did), then rebasing is counterproductive.

Anyway, the point is kind of moot for now, because I will not be able to hack on Rocq until early October.

[silene]

@coqbot run full ci

[silene]

I have rebased the pull request on top of master. It have also added support for x86-32, in addition to the original support for x86-64. For Windows on x86-64, the code compiles, but I do not know if it runs correctly. (Does the Windows CI test native_compute?)

The full CI went through successfully (https://gitlab.inria.fr/coq/coq/-/pipelines/1275426), except for the job test-suite:base+32bit, since there was no support for x86-32 at the time.

The one thing that is missing (in addition to people implementing dedicated code for non-x86 architectures) is a proper way to disable native_compute at configure time, if the architecture is not supported. (I do not know how to detect the architecture from an OCaml file.) As a consequence, the configure script currently enables native_compute if asked to, which then fails with assert false at runtime if the user tries to invoke the tactic. (Hence the failure in the native_compute tests of the aforementioned 32bit testsuite.)

[rlepigre]

You can detect the architecture using dune, and select among two implementations. The typical way to do that is to use (enabled_if ...) in your (library ...), and to then choose between two variants of a .ml file depending on whether your library is available or not. You can see an example in the perf support, which only works on Linux (see here and here).

In your case, I think that the enabled_if part could look like the following.

  (enabled_if
   (or
    (= %{architecture} "x86_64")
    (= %{architecture} "i386")))

[ppedrot]

I tried this PR on the famous UnsaturatedSolinasHeuristics/Tests.v fiat-crypto file that was very sensitive to the choice of representation of accumulators, and on OCaml 4.14.2 on x86-64 it doesn't seem to change anything performance-wise.

The one thing that is missing (in addition to people implementing dedicated code for non-x86 architectures) is a proper way to disable native_compute at configure time, if the architecture is not supported.

We're not really forced to do this though. We could instead fall back gracefully on the alternative encoding of accumulators as closures, which is less efficient than the trick used here but would still be better than falling back to the VM. Also, there may be a not-so-distant future where we don't have to rely on hacks at all and instead have an efficient closure pattern in OCaml flambda internals.

[silene]

encoding of accumulators as closures, which is less efficient than the trick used here but would still be better than falling back to the VM

Do you mean putting something like if Obj.tag v = Obj.closure_tag then ... else match ... before every match construct? My memory is a bit fuzzy, but I seem to remember that it was slow enough that it was no longer a net gain compared to the VM. Indeed, Obj.tag is really slow, because it requires a full context switch from OCaml to C and back. If the branch predictor correctly guesses the result of the test, some of the cost of this context switch will be masked by various cache misses, but not completely. The situation would be quite different if Obj.tag was a builtin function known by the compiler.

In fact, I just tried the following microbenchmark. Branch prediction is perfect (only 4k misses, presumably during startup and exit) and there are no cache misses, so all the processor units are running at full throttle (about 7 instructions are retired per cycle). The code using Obj.tag is twice as slow: 26 billion instructions (1.02s) vs 12 billion instructions (0.45s).

let b = ref (Either.Left 0)

let () = b := Either.Right 1

let f () =
  let j = ref 0 in
  for i = 0 to 999_999_999 do
    if Obj.tag (Obj.repr !b) = 0 then incr j
  done;
  exit (if !j = 0 then 0 else 1)

let g () =
  let j = ref 0 in
  for i = 0 to 999_999_999 do
    match !b with Left _ -> incr j | _ -> ()
  done;
  exit (if !j = 0 then 0 else 1)

let () = g () (* or f () *)

[ppedrot]

Obj.tag is really slow, because it requires a full context switch from OCaml to C

I was thinking instead about the version were we have a low-level C function that expects its argument to be an actual OCaml value and just does a field access + some arithmetic. This is much more efficient than Obj.tag and with the proper external annotations we can probably remove the overheads of the context switch.

[proux01]

FWIW, when developing primitive floats, a major source of inefficiency of the first implem for native_compute came out to be calls to Obj.tag that we had to replace with a custom rocq_is_double C implem.

[ppedrot]

See #14048 for the kind of fallback I had in mind.

[gasche]

I could try to implement a type-based optimization for Obj.tag in the compiler upstream where, when the type of the value is known to be an inductive without immediate integers or lazy values, then we perform a direct tag access.

Which version of OCaml should I start from to make this easy for you to test?

[ppedrot]

I could try to implement a type-based optimization for Obj.tag in the compiler upstream where, when the type of the value is known to be an inductive without immediate integers or lazy values, then we perform a direct tag access.

This is extremely dangerous given that the first thing the native compiler does is to ignore all typing information. We really should not rely on type-based optimization for anything that is remotely linked to the Rocq native compiler.

[silene]

I am certainly not asking for a type-based optimization. Just a dumb "%tag" builtin that would avoid the compiler from having to save unclobbered registers on the stack and to perform a full stack switch would already be a great gain, even if it ends up executing the same instructions as the current C code.

[ppedrot]

@silene I want to proceed with this PR, but it lacks a little improvement. The configure check is now too lax, as it claims to support native compilation for all architectures. You should refine the test following the same analysis as in rocq_values.c. I could do it myself but I'm not really skilled enough with dune to write this complex interplay of C stubs, if that's even possible.

[silene]

I do not understand what you are suggesting. I do not see anything architecture-specific in rocq_values.c. The code was just doing

#if OCAML_VERSION >= 50000
// Placeholder used by native_compute
  abort();

and the related configure check was just as simple:

if caml_version_nums >= [5;0;0] && prefs.nativecompiler <> NativeNo then
  let () = cprintf prefs "Your version of OCaml is %s." caml_version in
  die "You have enabled Rocq's native compiler, however it is not compatible with OCaml >= 5.0.0"

Here we need some way for the configure script to ask the C compiler what kind of assembly dialect it supports. (I know how to do that with the autoconf machinery in the C world, but here I am at a loss.)

[ppedrot]

I'll try to cook up a hack to show you.

[ppedrot]

@silene I force-pushed a patch atop of your PR that implements the configure-time check as a small C stub.

[ppedrot]

@coqbot run full ci

[silene]

I see. But now I am wondering, why not directly link with rocq_values.c? That way, we would not have another file that we need to keep synchronized. Or does Dune forbid it because it is in a distant directory?

[SkySkimmer]

That would be a recursive dep since rocq_values.c is compiled with flags generated by configure

[ppedrot]

If everybody is happy with this hack, we can merge this PR. Anybody against?

[ppedrot]

Shouldn't we use the GC-aware macros for this function and its i386 version? AFAIU nothing prevents the GC from moving clos under our feet in the caml_alloc_small call below. The code pointer should be allocated statically so maybe it does not matter, but just in case it does not hurt to double-down on invariants.

[silene]

The code no longer cares about clos once its field 2 has been read, so there is no reason to keep it alive by registering it as a GC root. As for the code pointer (the content of that field), "should be allocated" is the wrong way to look at it. Indeed, this is just an address in the text segment; it is never allocated, or only with a very loose definition, that is, it is in a block allocated by the dynamic linker when it loaded Rocq in memory. This whole pull request would be reduced to almost nothing if we had a portable way to know how OCaml names anonymous functions (i.e., nm _build/default/kernel/.kernel.objs/native/nativevalues.o | grep __fun_).

[ppedrot]

this is just an address in the text segment; it is never allocated, or only with a very loose definition

That's what I meant by statically, but indeed. If you're confident that in the OCaml 5.0 model all these operations are safe, then it's fine. I never trust C and much less the OCaml semantics w.r.t. memory.

[silene]

My confidence does not lie in the semantics of C or OCaml. It is just that the code pointer points to some executable code by definition, but the heap (be it C or OCaml) is not executable for obvious security reasons.

[gasche]

This whole pull request would be reduced to almost nothing if we had a portable way to know how OCaml names anonymous functions.

Is this something worth discussing at the OCaml-compiler level? (Would a "compiler-libs" API function that provides this be okay, or a dependency too much?)

ocamlopt supports a -save-ir-after scheduling option that will serialize the "linear" representation of the IR (as pretty-printed with the -dlinear debug option), and can be passed again to the compiler:

$ ocamlopt -save-ir-after scheduling -c test.ml # produces test.cmir-linear
$ ocamlopt test.cmir-linear # finishes the compilation from that file, as if test.ml was passed but without duplicate work

It would be possible to inspect the cmir-linear file, whose format depends on the OCaml version but is portable across operating systems and architectures. (The type definition for the values encoded in this file are in file_formats/linear_format.mli, the lowest-churn approach if you don't want to depend on compiler-libs may be to copy the definition, use conditional directives if the format ever changes, and write the small unmarshaller for those files yourself, it's ten lines of code .)

[silene]

I don't think the dependency on compiler-libs is much of an issue. I am more worried about writing the Dune code that will make it possible to inspect the generated files in order to recover the symbol.

To be more precise, what would make the pull request simpler is to know the generated name for the arity-1 function that corresponds to a given arity-2 function that has been partly applied (here accumulate).

But now that I think about it, it might be possible to make the code much simpler. Indeed, there already exists one such arity-1 function whose name is well-known: caml_curry2_1. So, it might be possible to just use it. This would make the code a bit slower (every time an argument is accumulated, caml_curry2_1 + accumulate would be called instead of just partially_applied_accumulate), but it might become a lot more maintainable.

[ppedrot]

the generated name for the arity-1 function that corresponds to a given arity-2 function that has been partly applied

Can't we just get this information at runtime and do a little bit of metaprogramming in C? We're already generating OCaml files for the native compiler, it would not hurt to have a trivial C file with the right autogenerated code...

[silene]

Can't we just get this information at runtime and do a little bit of metaprogramming in C?

We could, but unfortunately, it does not really help. This time, the issue comes from an inadequacy from modern processors. Indeed, their instruction sets usually do not provide an instruction for branching to an absolute 64-bit address (for various reasons, most of them good). So, even if you can recover at runtime the actual address of the function you are interested in, you cannot directly call it by lack of a suitable instruction. Therefore, you still need a chunk of assembly code to perform a somewhat indirect branch. So, you will not gain much from a maintainability point of view.

In case you wonder why this lack of branching instruction is not an ubiquitous problem, that is because, when the linker links the object files together, it knows both the source and the target of every local branch, so it can use a relative branch, which is supported everywhere. Similarly, here, by knowing the actual name of accumulate (or of its partially applied variant), we could let the linker do its magic.

[silene]

By the way, if someone needs help to port the code to their favorite architecture, just send me the output of ocamlopt -S for the following OCaml progam:

let accumulate data x = data - x
let foo data = accumulate data
let bar accu x = accu x

[silene]

So, I have been experimenting a bit with caml_curry2_1. It certainly makes the C/ASM code much simpler. On x86-64, it is reduced to the following snippet.

asm(".align 8\n\t"
    ".quad 3067\n"
    "rocq_curry2_1_addr:\n\t"
    "jmp caml_curry2_1\n");

value rocq_curry2_1(value) {
  extern void rocq_curry2_1_addr();
  return (value)&rocq_curry2_1_addr;
}

The C part would be shared by every architecture. The assembly part would be different for every architecture, but almost identical, e.g., s/jmp/br/.

[silene]

Closing in favor of #21540 which is a much more maintainable version.