Xavier Leroy

icon indicating a website link https://xavierleroy.org/

icon company Collège de France and Inria icon location Paris, France icon location Professor of software sciences at Collège de France, Paris. Member of Inria research team Cambium. Interested in all scientific aspects of computer programming

Results 360 comments of Xavier Leroy

OCaml 5 performance regression for unmarshal-heavy workloads

Thanks for the detailed analysis. Allocation of multiple blocks (as opposed to OCaml 4's "allocate one big block and carve sub-blocks inside" strategy) is probably unavoidable in OCaml 5, but...

[5.3] Compiling C++ code using the OCaml C API results in name-mangled caml_state on Cygwin

Yes, let's fix this for 5.3. But the problem has been there since 5.0, right?

Use WinAPI concurrency primitives on Windows ports (remove winpthreads)

I need to be convinced this is not a regression compared to just using winpthreads, or a more modern implementation of the POSIX API for Win32. There are benefits to...

A standard reporting format for ocamltest, with a Github Action UI

Somewhat related (but not directly): #12243 .

A standard reporting format for ocamltest, with a Github Action UI

I hope ocamltest's output format can be made not only more suitable for CI tools, but also more readable for humans. What about having only one line of output for...

Stdlib: make the Hashtbl per default seeded, unless OCAMLRUNPARAM includes "R=0"

When I implemented hash table randomization back in 2012, I wanted to make it the default (and actually the only) mode. I was quickly dissuaded by two serious industrial users...

aarch64 assembler error: conditional branch out of range

Well spotted, thank you for the report. I think the main offenders here are the `tbz` and `tbnz` instructions, since they are limited to +/- 32K. The other conditional branches...

aarch64 assembler error: conditional branch out of range

@monniaux : thanks for the Chamois plug, but branch relaxation for PowerPC was implemented 14 years ago in 14b44ae202de640f2a7a6e973e5fb912b736c002, so nothing is new under the sun. @bagnalla: thanks for the...

Support x86 Indirect Branch Tracking.

Note that the runtime library functions in `runtime/x86_64` are not annotated with `endbr64` instructions, as these functions are intended to be called directly, but not through a function pointer.

Support x86 Indirect Branch Tracking.

Also: IBT support is for 64-bit x86 only. Intel processors support IBT in 32-bit mode as well, but I don't think it's worth supporting in CompCert.