On 11 Aug 2023, at 12:51, Stuart Henderson <[email protected]> wrote: > > yes, for amd64 it's intel Tiger Lake (11th gen) and newer, models of the > format iX-11XXX, iX-12XXX, iX-13XXX. no AMD CPUs. On ark.intel.com, look > for "Control-Flow Enforcement Technology" (the intel term which covers > both shadow stacks and indirect branch tracking). > > for arm64 currently only on Apple M2.
Thanks for all the pointers! Every machine for 100 miles around me seems to be an AMD these days, so I've ordered myself a Raptor Lake NUC to be my new OpenBSD desktop. As soon as that arrives I'll take a look at the native code compiler output (unless someone else beats me to it). In the meanwhile I think we should go for updating the OCaml ports to 5.1.0 so that a patch against trunk will be manageable... The only roadbump is from Daniel Dickman, who wrote: > Fine with me so long as compcert continues to work on i386. I think the > only impact is potentially running slower? That’s fine with me. > > That being said I think there were some challenges with newer coq on > i386. So maybe the end is close for compcert on that platform? Indeed, I think it's time to move to a 64-bit license after so many years. I strongly suspect you're the only user of OpenBSD/i386 compcert these days, so it's worth just asking for an upgrade of the license to shift to 64-bit. OCaml 5 will definitely be bytecode-only for 32-bit architectures for the foreseeable future. This in turn pushes up memory requirements (due to the extra boxing of values), which makes it more likely that Compcert/Coq will hit the 4GB process limit. Anil
