Apalache build fails on Apple silicon

[andrey-kuprianov]

Description

Apalache fails to build on Apple ARM due to missing support from Z3 side:

Tests in error: 
 at.forsyte.apalache.tla.assignments.TestSymbTransPass: Unsupported CPU architecture: aarch64
 at.forsyte.apalache.tla.assignments.TestManualAssignments: Could not initialize class com.microsoft.z3.Native

System information

• Apalache version 0.15.2:
• OS: Mac OS
• JDK version: openjdk 11.0.10 2021-01-19 LTS

[konnov]

I just relabelled it as an enhancement, as we could not foresee Apple introducing one more CPU architecture.

Just curious, does it work in docker on M1?

[andrey-kuprianov]

Just checked: as a workaround, running Apalache via Docker on Apple M1 works fine:)
https://apalache.informal.systems/docs/apalache/installation/docker.html

As desribed here --platform linux/amd64 needs to be passed as an additional argument to Docker.

One thing that is nice with docker is how easy it is to experiment with different Apalache versions: you only need to change the version you want to run; it will be downloaded automatically:)

Also, there might be some issues with running Docker images for Intel on Apple M1. E.g., as I have a spec with old-style type annotations, I have tried Apalache versions before Snowcat; version 0.8.3 hangs for some reason at various stages (I was also getting segmentation faults); version 0.8.2 seems to be working fine.

[andrey-kuprianov]

Sorry, I was too fast to celebrate. Some phases work fine; but it seems that as soon as it comes to running Z3, it segfaults.

[andrey-kuprianov]

Here is a more precise info when running different Docker images:

v.0.9.0
Non-deterministically halts at different places; I also got a segfault:

  > After preprocessing: UniqueRenamer                            I@08:35:21.478
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x000000401798c3a0, pid=44, tid=47
#
# JRE version: OpenJDK Runtime Environment (9.0+12) (build 9.0.4+12-Debian-4)
# Java VM: OpenJDK 64-Bit Server VM (9.0.4+12-Debian-4, mixed mode, tiered, compressed oops, g1 gc, linux-amd64)
# Problematic frame:
# J 3147 c1 org.bitbucket.inkytonik.kiama.output.PrettyPrinter$$Lambda$248.apply(Ljava/lang/Object;)Ljava/lang/Object; (8 bytes) @ 0x000000401798c3a0 [0x000000401798c380+0x0000000000000020]

v.0.8.3
It starts checking the steps, but then halts

v.0.8.2, v.0.8.0
Sometimes they work fine, and produce the counterexample. But the counterexamples are non-deterministic, which was supposed to be fixed in #318 in v.0.8.0.

Sometimes I get again segfaults:

# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x00000040173048e0, pid=44, tid=47
#
# JRE version: OpenJDK Runtime Environment (9.0+12) (build 9.0.4+12-Debian-4)
# Java VM: OpenJDK 64-Bit Server VM (9.0.4+12-Debian-4, mixed mode, tiered, compressed oops, g1 gc, linux-amd64)
# Problematic frame:
# J 113 c1 java.lang.StringLatin1.indexOf([BII)I [email protected] (61 bytes) @ 0x00000040173048e0 [0x00000040173048e0+0x0000000000000000]

So in general Apalache with Docker on M1 doesn't seem to work reliably.
A separate issue is about determinism; I don't know whether this is an artefact of running on M1 or not.

[andrey-kuprianov]

I have checked with Apalache docker image for 0.8.2 on Linux -- it does behave non-deterministically.

[romac]

From this comment, it sounds like there may still be some issues with Z3 on M1, though they might have been fixed in the z3-turnkey project (which Apalache is using, right?) already: Z3Prover/z3#4979 (comment)

[jtremback]

I tentatively have found a workaround, although I will give it a few days to say for sure.

• Install the jdk for macOS x86 from https://www.azul.com/downloads/?os=macos&architecture=x86-64-bit&package=jdk
• The installer will warn you that M1 is better and you should install that instead
• Confirm:

% java --version
openjdk 16.0.1 2021-04-20
OpenJDK Runtime Environment Zulu16.30+15-CA (build 16.0.1+9)
OpenJDK 64-Bit Server VM Zulu16.30+15-CA (build 16.0.1+9, mixed mode, sharing)

I'll include details on how I installed Apalache as well, since that may have affected things.

• Downloaded apalache.zip from here: https://github.com/informalsystems/apalache/releases
• extract zip and cd apalache
• sudo mv bin/apalache-mc /usr/local/bin
• sudo cp -r mod-distribution /usr/local/

[andrey-kuprianov]

I can confirm that the trick with using x86_64 Java, described above, works on my M1 as well.

Many thanks, @jtremback !

[lemmy]

Given that Apalache comes with Turnkey Z3, have you considered bundling a suitable JVM? Since performance isn't critical for the Scala/Java layer of Apalache, you could even consider creating a native image. That way, users wouldn't have to fiddle with an x86-64 VM on Silicon and could use a native JVM for TLC.

For those familiar with the JVM ecosystem (I don't expect many TLA+ users to be), jenv makes it easy to switch JVMs when working with Apalache and TLC. Haven't checked if it helps in this case.

[konnov]

Shall we close this issue now? @andrey-kuprianov can you confirm that you can Apalache on M1?

[thpani]

I've requested support for aarch64 from upstream in tudo-aqua/z3-turnkey#12

[shonfeder]

I like the idea of creating a native image. If that's feasible for us, I'd be in favor of targeting it.

[thpani]

Apalache (and Z3) now runs on native aarch64 JVMs.
No more need to use an x86_64 JDK and run through Rosetta.

[lemmy]

This is great! I'm curious, do you observe any performance benefits?

[thpani]

I'm curious, do you observe any performance benefits?

I believe our benchmarks currently run on x86 only, and I haven't investigated further. CC @shonfeder
As Apalache's preprocessing runtime is usually negligible compared to SMT solving, I'd expect any significant performance gains to come from Z3 running natively, not from a native JVM.