For 64-bit targets, array bound checking assembly code could be more compact #5360
Original bug ID: 5360
Consider the following module:
let f (a: t array) =
Here is a diff between the code generated by OCaml 3.12.1 and the code that could be expected for bounds checking, when values have the same size as double-precision floating-point numbers :
--- t.orig.s 2011-09-25 14:43:16.000000000 +0200
The minimally tested attached patch implements the new version.
The text was updated successfully, but these errors were encountered:
Comment author: pascal_cuoq
This is not a performance optimization, it is a code size optimization. In realistic function f above, the same three-instruction sequence appears at the beginning of each of two branches, making the code of this function three instructions longer than necessary. This is stupid and can be fixed with the same "if wordsize_shift = numfloat_shift" test that's already used elsewhere in cmmgen.ml.
I have no doubt that this is entirely absorbed by other inefficiencies in the compiler, if that's what you are getting at. The only hard facts I have at hand are that the Frama-C core (excluding most functionality) compiles to a 10MB binary and that compiling with -compact makes it smaller and faster, hinting that code bloat does influence performance.
Comment author: @gasche
I compiled frama-C without -compact on my trunk, and here are the size of toplevel.opt:
The difference is rather small.
That said, in the process I discovered that this optimization is already performed in the Parraylength case, so applying it in the Parrayref and Parrayset cases does not seem preposterous.
PS: Oh, and Frama-C doesn't compile as is against trunk, because you have some Datatype.Hashtbl functor with input signature Hashtbl.S, to which you pass your Inthash module, but the signature of stdlib's Hashtbl changed in trunk (a new "stats" function is available). It is not future-proof to depend contravariantly on a stdlib interface.
Comment author: @xavierleroy
Patch #2 applied in SVN trunk (commit 11932).
I agreee more compact code is better, and optimizations specific to 64-bit targets are welcome since these targets are getting dominant.
For Parraylength, the 64-bit case saves one run-time test, while for Parrayrefs and Parraysets we have the same number of tests executed (2), but produce one fewer. So, the benefits will be much smaller.
Comment author: pascal_cuoq
All together, the patches here and from entry #5345 (including the assembly-level patch 0002 that was rejected) applied to OCaml 3.12.1 appear to make the sha1.c benchmark from http://blog.frama-c.com/index.php?post/2011/08/29/CompCert-gets-a-safe-interpreter-mode 1.5% faster (same protocol as in the blog post, sha1.c modified to run the same computations 5 times). This is pretty cool even if it does not nearly bridge the gap with CompCert's interpreter.
Other Frama-C use cases would use a smaller proportion of array operations, but yet other use cases would use more. I think the sha1.c benchmark is average in this respect.