Compiling on Apple Silicon

[tquatmann]

I propose to document the current state of compiling on apple silicon without emulation in this issue.

How to compile (April 2023)

Storm compiles natively on ARM-based apple silicon processors. However, a few points need to be considered:

• Make sure you have the latest version of Storm (April 2023 or later)
• Dependencies need to be installed using the arm version of homebrew. Skip cln and ginac as they do not have an ARM version supported by homebrew
• Make sure that you use an arm compiled cmake binary (check with where cmake and file path/to/cmake)
• Carl needs to be build without cln and ginac. This should be the default once this PR is merged The latest versions of CLN and GiNaC support Apple Silicon.
• If you previously had an x86 version installed, you need to re-build storm (and carl) from scratch. For this, remove the corresponding build folders and invoke the building steps.
• Examine the cmake output. It might be that cmake found an x86 version of carl or another dependency. Homebrew dependencies should normally be found in /opt/homebrew, not in /usr/local/.
• Contact us at support@stormchecker.org or on github in case of issues.

TODO list for official support:

• merge PR Sylvan upgrade #273
• make installation of carl and storm without cln and ginac more straightforward (ideally, these dependencies are disabled automatically if compiling on M1 is detected).
• Assess if it helps to set CMAKE_OSX_ARCHITECTURES to arm64. Resolved: Appears to work without
• I had problems with setting -DSTORM_FORCE_SHIPPED_CARL=ON when compiling for arm: carl did not compile due to some eigen related issue.
• Some includes are taken from the x86 installation. For example, I ran into a known issue related to boost that should have already been fixed in my boost installation. The "solution" was to upgrade my x86 boost installation. Resolved: Can not be replicated anymore. Might have been an issue with an older or with an x86 cmake version
• clang option -march=native does not seem to work yet which is why -DSTORM_PORTABLE was required for me. Also, the jit engine doesn't work for that reason, which also lets the tests fail (see PR remove jit from current code base #292)
• Check if stormpy works
• The Homebrew formula(s) for Storm and Carl need to be updated as well
• Adapt Website documentation
• fix or work around issue Failing MultiObjectiveModelCheckerTest on Apple Silicon #354

[sjunges]

Hi Tim,

great progress. Could you add an item regarding stormpy on the TODO list. At least it would be good if we have clarity on whether this will work when writing the documentation.

We first need to detect Apple silicon. One option is https://cmake.org/cmake/help/latest/envvar/CMAKE_APPLE_SILICON_PROCESSOR.html#envvar:CMAKE_APPLE_SILICON_PROCESSOR

but that requries CMAKE 3.19.

Thoughts?

[tquatmann]

Since PRs #323 and #273 are finally merged now, natively building on Apple Silicon should kind of work now. This still needs some testing, though.

[sjunges]

Regarding CLN: https://www.ginac.de/pipermail/cln-list/2023-March/000803.html, there seems to be some progress

[tquatmann]

I'm compiling on Apple Silicon just fine and I can no longer reproduce the issues I had before when using a shipped carl version. I guess that problem solved itself.

The test SparseMaPcaaMultiObjectiveModelCheckerTest.serverRationalNumbers fails due to an issue in Eigen v3.3.9. I worked around this in PR #349

[sjunges]

CLN support is still lagging behind; one could appearantly install this from git: https://www.ginac.de/pipermail/cln-list/2023-April/000815.html

[sjunges]

I have been using this with stormpy now for quite some while :-)

[sjunges]

The typical problem that people seem to run into is that libraries compiled for x86/Rosetta are included, which leads to strange errors down the line. I wonder if there is a simple way to spot this during configuration.

It would definitively help resolve #419

[sjunges]

Can we add #354 this to the checklist here?

[volkm]

The latest version of CLN seems to support ARM now, see ChangeLog

[tquatmann]

I just installed storm w/ CLN support. Seems to work so far :)

[sjunges]

Can we add #523 to the issues?

[sjunges]

Bug #523 has been resolved by single-thread sylvan, see #600 which relates to this.