Stream: Coq Platform devs & users

Topic: 32 bit cygwin will discontinue next year

Michael Soegtrop (Nov 02 2021 at 14:45):

There was recently a message on the cygwin mailing list, that support for 32 bit will be discontinued. In principle one can also install the 32 bit MinGW toolchain on a 64 bit cygwin, it is quite tricky though because Windows has the property that the contents of system DLLs depend on if a 32 bit or 64 bit process looks at it. So a 64 bit MinGW 32 linker would see the 64 bit DLLs and go wild. One can get around this by copying the DLLs with a 32 bit copy program somewhere else ... it is a bit messy.

In short: what do you think? Should we discontinue the 32 bit version of Coq?

Some people say that the 32 bit version is faster, because Coq is mostly pointers and these need less cache in 32 bit, but in CI the difference doesn't look significant.

Karl Palmskog (Nov 02 2021 at 14:49):

I believe @Andrew Appel has been a proponent of 32-bit Coq (for the performance reasons stated by Michael), maybe we want to get his opinion on discontinuing it.

Would also be interesting to know what it actually requires on, say, Linux side of things to get 32 bit. Could be worth to keep 32 bit as a niche experimental thing on Linux without any official support.

Guillaume Melquiond (Nov 02 2021 at 14:52):

Note that, sooner or later, the OCaml developers will make the choice for us, as discontinuing OCaml for x86-32 is on the drawing board.

Enrico Tassi (Nov 02 2021 at 14:54):

At least for Linux there is a "mixed" architecture called x32 IIRC (which is 32 bits pointers but 64bits instructions/registers). OCaml has a patch for this one around. @Guillaume Melquiond do you know what they think about that?

Enrico Tassi (Nov 02 2021 at 14:55):

(x32 is really what Appel's use case needs IMO)

Guillaume Melquiond (Nov 02 2021 at 14:57):

My understanding is that it is not worth the effort, especially with OCaml 5.0/Multicore needing lots of virtual memory to accommodate minor heaps. But I follow OCaml's development from very far away, so take my interpretation with a grain of salt.

Théo Zimmermann (Nov 02 2021 at 15:08):

I suggest the reading of this thread, especially around the place where @Emilio Jesús Gallego Arias mentions the users of Coq who like the 32 bit version and the response of @Xavier Leroy to that. IMHO if @Xavier Leroy wishes to drop 32 bit OCaml (despite his proximity with @Andrew Appel), I think we should follow suit: https://discuss.ocaml.org/t/jane-street-packages-dropping-support-for-32-bit/8621

Théo Zimmermann (Nov 02 2021 at 15:09):

More precise link: https://discuss.ocaml.org/t/jane-street-packages-dropping-support-for-32-bit/8621/13

Enrico Tassi (Nov 02 2021 at 15:23):

OK, then it seems really that the world is going to be a better place ;-)

Andrew Appel (Nov 02 2021 at 15:42):

I have already said, in other forums, that I don't expect that 32-bit Coq will be supported just for me if I'm the only user. But here are some things I believe:

1. Running Coq with 32-bit pointers really can be twice as fast as with 64-bit pointers; several years ago I published measurements documenting this.
2. At the time of those measurements, OCaml on Windows could support only a 2.0 gigabyte heap, even though the address space should naturally be 4 gigabytes (2^32). More recently than those measurements, OCaml became even more limited; now you can't really get a heap bigger than 1.2 gigabytes before OCaml blows up. I suspect that the OCaml maintainers are tuning their memory management to the 64-bit case, to the detriment of the 32-bit case.
3. The consequence of that is that, even when the heap is only 1 gigabyte, Coq runs slower in 32-bit mode than it should, because there are too many major-generation garbage collections. (That's conjecture; to prove it, I would have to run a Coq with garbage-collection statistics, and I haven't done that.)
4. The "mixed" architecture x32 sounds like exactly what I need. But it shouldn't be just me -- perhaps there are many other users who are willing to organize their Coq developments so that any individual .v file requires no more than 500 million words (that is, 2 gigabytes in 32-bit mode or 4 gigabytes in 64-bit mode), and such developments should build in x32.

For many years now I have been running a 64-bit operating system, 64-bit applications, and just 32-bit Coq for improved memory performance. It would not be a major problem for me to install 64-bit Coq instead.

Karl Palmskog (Nov 02 2021 at 15:51):

if we actually start to advertise the x32 arch and provide it in Docker images and show the performance gains, I think we could convince a lot of users.

For sure, x32 would work fine on tens of projects in coq-community.

Andrew Appel (Nov 02 2021 at 17:37):

By the way, I think there are important applications of 32-bit architectures in embedded platforms. So it would be a shame if CompCert were to drop support for 32-bit architectures, because then we could not have verified compilation for those platforms (and also VST would have to drop 32-bit architecture support). But that's not at all the same question as "do we need to run Coq in 32-bit mode."

Karl Palmskog (Nov 02 2021 at 17:44):

ah, then I think someone has to invest time in figuring out CompCert cross-compilation, because last time someone checked, Xavier said:

My advice is to not bother with cross-compilation and build only the version of CompCert that corresponds to the host platform.

Paolo Giarrusso (Nov 02 2021 at 23:19):

just for the record, I think even the super-optimized Hotspot supports something x32-like — “compressed pointers”. With objects aligned to 8 bytes, the 3 low-order bits can be skipped, so you can support 32GB heaps with 32-bit pointers: https://www.baeldung.com/jvm-compressed-oops

Paolo Giarrusso (Nov 02 2021 at 23:23):

of course shifting pointers at dereference has some (small) cost, but shifts could be pretty cheap when you’re stalled waiting for memory.

Michael Soegtrop (Nov 03 2021 at 06:48):

Andrew Appel said:

By the way, I think there are important applications of 32-bit architectures in embedded platforms.

I still have it on my ToDO list to add an Opam packages for 32 bit ARM CompCert+VST. As cross environment this should be independent of the OS. I don't think it will be a lot of effort to support it - afair from my discussion with Xavier on this last time the main issue he saw was with setting up the required cross linker in a reliable way - this shouldn't be much of an issue with opam and depext.

Michael Soegtrop (Nov 03 2021 at 07:11):

Regarding the speed ratio: I had a look at recent CI runs and indeed the 32 bit version seems to be about 30..40% faster, see e.g. (https://github.com/coq/platform/actions/runs/1413458927). The majority of the CI run time are Coq calls. Maybe the speed ratio reduced a bit in recent years because CPUs have larger and more advanced caches. Of course 30..40% is still substantial.

Emilio Jesús Gallego Arias (Nov 03 2021 at 14:00):

@Andrew Appel @Michael Soegtrop , it is good to hear this numbers, let's try to forward them to OCaml maintainers (cc @Xavier Leroy ) ; regarding Coq, I volunteer to maintain the 32-bit version as long of course as OCaml still does support 32 bits.

This should be a while, Coq would need to drop support for OCaml 4 at all.

A different issue is Cygwin of course, but maybe WSL can work here.

Michael Soegtrop (Nov 03 2021 at 16:02):

I am not a fan of WSL, because it requires a rather invasive hypervisor - much worse than VirtualBox & Co. If you use WSL, no other virtualization system will work any more. Also I have seen quite a few bad side effects of the hypervisor, say Windows blue screen core dumps are corrupted when you have WSL.

The Windows issue is solvable - worst case by archiving a 32 bit cygwin, but as I said one can get around the linker issues in 64/32 cross builds - I have done it before.

Michael Soegtrop (Nov 04 2021 at 12:55):

One note on the 32 vs 64 bit timing I gave: they are flawed because in 32 bit mode I don't compile Unimath - which needs more heap than possible in 32 bit OCaml. So I would have to run tests where this is rectified.

Last updated: Jun 03 2023 at 04:30 UTC