nuSMV and nuXmv on Apple M2

21

file command can tell you the architecture of an executable. For example, the nusmv from Homebrew is an arm64 binary:

file $(which nusmv)
/opt/homebrew/bin/nusmv: Mach-O 64-bit executable arm64

But the FBK binaries are universal:

file ./nuXmv
./nuXmv: Mach-O universal binary with 2 architectures: [x86_64:Mach-O 64-bit executable x86_64] [arm64]
./nuXmv (for architecture x86_64):	Mach-O 64-bit executable x86_64
./nuXmv (for architecture arm64):	Mach-O 64-bit executable arm64

file ./NuSMV
./NuSMV: Mach-O universal binary with 2 architectures: [x86_64:Mach-O 64-bit executable x86_64] [arm64]
./NuSMV (for architecture x86_64):	Mach-O 64-bit executable x86_64
./NuSMV (for architecture arm64):	Mach-O 64-bit executable arm64

I supposed that maybe for some reason Alloy is running it in x86_64 mode, so I mvā€™d the original executable to NuSMV-universal and made a wrapper NuSMV to force it to run in arm64:

#!/bin/sh

arch -arm64 NuSMV-universal "$@"

It worked!

Option Solver changed to Electrod/NuSMV
Executing "Check restore_after_delete"
   Solver=NuSMV Steps=1..10 Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 Mode=batch
   No translation information available. 39ms.
   No counterexample found. Assertion may be valid. 1097ms.
1 Like
22

Extracted and checked electrod and it is indeed a x86_64 binary:

file ./electrod
./electrod: Mach-O 64-bit executable x86_64
23

Thanks for the investigation. Iā€™m not completely sure to follow the end of your reasoning though, as I donā€™t really master the intricacies of various Mac architectures (the only Mac I have ever used was the first one :wink: ). Do you suggest that the issue when running nuXmv from electrod would be the difference of target architecture between the two? Currently, the latter is built by Github or by @nmacedo (canā€™t remember). I suppose we should try to build a universal (if possible) or arm64 (at worst) version of electrod?

24

No. I would have had suspected that if I didnā€™t already succeed in running the arm64 nusmv from homebrew. I am quite surprised by the mix of architectures here:

  1. Alloy runs in arm64 Java11 JVM (by Zulu)
  2. electrod, an x86_64 binary, is invoked from arm64 JVM
  3. nusmv, an arm64 binary, is invoked from x86_64 electrod

If the mix of architecture is a problem I expect step 2 to fail already. Or that step 3 would fail with an arm64 binary. But bizarrely this sandwich of a mixture works.

x86_64 binaries on M1 macOS runs via Rosetta translation. According to Apple documentation:

Rosetta translates all x86_64 instructions, but it doesnā€™t support the execution of some newer instruction sets and processor features, such as AVX, AVX2, and AVX512 vector instructions. If you include these newer instructions in your code, execute them only after verifying that they are available.

Maybe the x86_64 version makes use of advanced instruction sets?

Yes, a universal or arm64 electrod is likely to fix it. The arm64 JVM should invoke the arm64 version in the universal electrod, which should then invoke the arm64 version in the universal NuSMV.

Until then, a quick workaround can be to distribute a wrapper along with the universal, to launch the proper binary depending on hardware information:

#!/bin/sh

case "$(sysctl machdep.cpu.brand_string)" in
  *"Apple"*) arch -arm64 NuSMV-universal "$@" ;;
  *) NuSMV-universal "$@" ;;
esac