Absolutely. I have our CI now producing all our build assets with either 4.14.2 or 5.2.0+ox. My local tests are very promising. I’m gonna ping the community to get more feedback but so far it looks like it’s working great. I see similar CPU usage and a slight increase in memory of less than 10%, which is totally acceptable for us.
5 Likes
That’s good to know. If you have more details on the regression, do share that.
Regarding @silene’s issue, I am not sure that the problem has been correctly described. Allocating some virtual address space with PROT_NONE is rather standard and does not need pages to be allocated in a page table. However it was known at the time that switching to a very large memory reservation could break some systems because virtual memory size is sometimes used as a proxy for memory usage (which IIRC under Linux is motivated by the fact that other figures are unreliable).
Removing the dependency on a large reservation for the minor heap is an expected benefit of having a superpage allocator which enables an efficient classification of pointers, among other benefits such as having a proper huge page support (the lack of which was recently shown to be responsible of 1/3rd of the measured slowdown of Coq in a recent analysis of Multicore perfs), or simplifying experimenting with and implementing adaptive sizing strategies for the minor heap (IIUC some of the old multicore experiments). (I now see @silene mentioning on the OCaml github issue another problem which is about having too many mappings, which is controlled by a different parameter than ulimit -v. Another benefit of a superpage allocator is to allocate as few mappings as needed.)
The multicore paper in fact said it took inspiration from the Streamflow allocator which features such a superpage allocator (to benefit from huge pages), but this particular component was never implemented. A prototype of a superpage allocator for OCaml was written before multicore was released (inspired by the one in the Go runtime), but I do not remember any OCaml developer expressing interest in either the prototype or the idea. There was an OCaml workshop talk about it, and it was mentioned several times on GitHub and in person with OCaml developers. They are all the channels available to interact with the OCaml developers.
@gasche’s comment about @silene not reporting the issue sounds like it carries some judgement without checking whether the general issue was known; also I would like to mention that until very recently there was a bot that would attempt to close issues faster than OCaml developers came round to read them, as an example of things where acts could go a longer way in encouraging contributions than post-hoc rationalisations from OCaml devs.
3 Likes
Hi,
We also have some issues with EasyCrypt & OCaml5. After having fixed some timing issue (with big help from the OCaml team), we are now facing a memory blowup issue (from 2G to… well the sky is the limit). oxcaml does not fix the issue.
In our case, the problem seems to come from Why3 (when calling external solvers via the Why3 API - pinging @silene here). A workaround is to change the space_overhead (lowering it to 25) right before calling Why3 (see OCaml 5 memory blowup workaround · EasyCrypt/easycrypt@ba49ccd · GitHub).
It would be interesting to find the root cause.
@strub Could you open an issue on GitHub · Where software is built describing the problem and importantly how to reproduce it? Tag it with Performance if possible. Once I have some reproduction instructions I can spend some time on it.
If running with oxcaml does not fix the issue that is quite interesting and we should understand why the GC pacing changes there are not improving things.
I believe the Goblint project had similar issues, in their case it was caused by weak tables failing to clear unused elements in some cases (typically when hash collisions are common). It is likely that Why3 also uses weak tables or ephemerons, so it could be the same issue.
Yes, Why3 uses weak hashtables (built on top of ephemerons) absolutely everywhere, as it is the core of our hashconsing infrastructure.