#380 support multiple architectures for solver binaries z3 #395

kfriedberger · 2024-09-17T20:13:03Z

This branch / pull request exists for tracking some steps towards supporting multiple architectures. I will use Z3 as example, because it was requested several times. Some explanation can be found in #380 .

I will not yet commit binaries to any public archive (Ivy or Maven) until we can make sure that the new approach is backwards-compatible (e.g. default architecture x86 can be used as before) and we have a maintainable code base (including scripts and documentation for publication and testing).

kfriedberger · 2024-09-29T09:01:14Z

This PR is currently blocked by sosy-lab/java-common-lib#43 to test execution on ARM64.

// UPDATE: The wording "blocked" is too much. Z3 is still not available for ARM64 on Linux, so local development is not affected and we could merge this PR.

kfriedberger · 2024-09-29T21:14:16Z

The current state seems to work as expected. I tested:

publishing solver Z3 to Ivy and Maven, including x64 and arm64 for several operating systems ✔️
downloading from Ivy is backwards-compatible for Z3 (e.g., just increment the version of Z3). This works without changing the ivy-settings. We still need to find a way for publishing JavaSMT itself with a reasonable configuration.
downloading from Maven requires more smaller changes. For example, as shown in this change: 958dbc3

Z3 is already published in Maven and Ivy, and works well with JavaSMT 5.0.1.
Feel free to test and give feedback.

As I do not have an ARM-based Apple machine available, maybe @ThomasHaas and @hernanponcedeleon can test whether it works as expected. Thanks.

kfriedberger · 2024-09-29T21:18:17Z

If there is positive feedback, I will also publish Z3 in its latest version 4.13.2 to Ivy and Maven. The publication of Z3 is even more automated now than it was before.

ThomasHaas · 2024-10-03T13:21:27Z

It seems to work on ARM-based Macs now. Good job :)

kfriedberger · 2024-10-12T23:00:22Z

Z3 was published to Ant/Ivy and Maven in versions 4.13.2 and 4.13.3.

There are some smaller issues that are currently blocking this PR from merging:

JavaSMT uses outdated CI images for Linux, e.g., Z3 has removed support for Ubuntu 20.* and requires newer GLIBC version. We will exclude those systems and update the CI in another branch in the future.
Z3 has a smaller regression when parsing formulas (due to a new feature that allows to compare formulas of incompatible types like Int/Bool):
Regression: theory mismatch no longer recognized when parsing SMTLIB, 0/1 are booleans. Z3Prover/z3#7419
(our fix from 8e2f3b0 might be changed/reverted in the future, if Z3 provides a bugfix)
Z3 DLL on Windows x64 crashes:
Regression: Windows x64 DLL crashes for Z3 4.13.2 and 4.13.3 Z3Prover/z3#7420

Not tested, not finished, just a draft.

… for backwards compatibility.

This should keep the existing cache valid and re-usable. Otherwise, we would create a new cache structure within the existing cache, with redundant entries. With this change, we limit the redundancy to arch- or classifier-specific entries.

We could include x64 and ARM64 dependencies for Z3. However, the default stays by only x64.

…rs, but only all other files. This cleanup aligns better with Maven guidelines. This is a small change for all upcoming publications to Maven and the Maven users.

…cture. Additionally, we upload Java sources and JavaDoc for z3 to the Maven repository. We need to test whether the uploaded files work as expected.

Let the user decide what to load, e.g. on a minimal system only load for one specific OS and arch.

See Z3Prover/z3#7419 for details. If required, the Z3 parser automatically converts Boolean formulas `f` to e.g. `ITE(f 1 0)`, which makes them comparable to Integer symbols and numbers 0/1.

… instead of JavaSMT root directory.

…ure-solver-binaries-z3

…ture-solver-binaries-z3

…into 380-multi-architecture-solver-binaries-z3

…l FP sizes.

…cripts, like Bitwuzla.

…and improve the linking process.

OpenSMT can be compiled for ARM in two simple steps: - provide GMP for ARM64 (we use the version that we provide for MathSAT anyway) - replace GCC with the cross-compiler for ARM64

…ure-solver-binaries-z3

kfriedberger · 2025-01-19T19:45:45Z

@daniel-raffler and @baierd : could you take a look and provide feedback? I would like to merge this PR in near time.

Beside Java-based solvers SMTInterpol and Princess, we now have 4 native solvers that are working on ARM64 platform:

with Linux on ARM64: Z3, MathSAT5, Bitwuzla, and OpenSMT.
with Windows and MacOS on ARM64: Z3

The current changes to Ivy are backwards-compatible and allow to use and update existing JavaSMT integrations without further changes (such as in CPAchecker). If the user wants to use binary solvers for ARM64, he can modify his Ivy dependency to load the corresponding files.

We already provide the corresponding files in Maven, so the user specify them via the pom-file..

baierd

Overall very nice. I will test this PR on my Windows machine later today.

I have some small questions/suggestions, but did not find anything mayor.

build/build-maven-publish.xml

build/build-publish-solvers/macros.xml

build/build-maven-publish.xml

src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java

baierd · 2025-01-25T12:07:56Z

Something that might be worth a try is adding a static info() method that tries to read your OS and gives you information about available solvers, dependencies and requirements (e.g. copy the Windows binaries for a Dev build), or possibly even checks those requirements for you.

kfriedberger · 2025-01-25T13:41:24Z

I would not expect such a info-feature from a library, but only in the main application.

The compilation will fail, because JavaSMT is not yet released in a new version, and some library names have been changed.

kfriedberger · 2025-01-25T20:01:03Z

For executing and testing the ARM-based binaries, you can apply Podman/Docker with Qemu.
A corresponding Dockerfile would look like this:

FROM arm64v8/ubuntu:22.04

ENV DEBIAN_FRONTEND=noninteractive
ENV TZ=UTC
ENV LANG=C.UTF-8

RUN apt-get update && apt-get install -y --no-install-recommends \
  wget curl \
  ant git \
  openjdk-17-jre-headless \
  openjdk-17-jdk-headless \
  libgomp1

Build with:

podman build --platform=linux/arm64 - < ubuntu2204-arm64.Dockerfile

The output will contain the ID in the last line.

Run with:

podman run -it \
    --mount type=bind,source=${HOME}/workspace,target=/workspace \
    --workdir /workspace/java-smt \
    ID

Podman/Docker with qemu is emulating ARM64 on x64 about 3-10 times slower than normal execution. I am thinking about an ARM-based CI, however Podman/Docker with Qemu might be too slow for that.

baierd

Looks good. Thanks for incorporating my suggestions!

Do we want to document the Podman/Docker info in some file or issue?

kfriedberger · 2025-01-26T08:00:36Z

The Podman/Docker file might be interesting for additional CI jobs. We will surely come across that topic in #384.

kfriedberger added enhancement Documentation solver Maven labels Sep 22, 2024

kfriedberger requested a review from baierd September 29, 2024 21:19

kfriedberger mentioned this pull request Sep 29, 2024

support for Mac with M series chips #380

Closed

kfriedberger marked this pull request as ready for review October 12, 2024 11:43

kfriedberger added 18 commits October 13, 2024 12:21

initial steps to provide multiple binaries of Z3.

2b5e801

Not tested, not finished, just a draft.

configure Ivy with a new classifier for 'arch', tested for Z3 binary.

2349bae

#380: reduce manual steps for publishing Z3, create copies of library…

68bab2b

… for backwards compatibility.

fix typo in property usage.

a3021ab

update Z3 to v4.13.0.

5d70c5f

We could include x64 and ARM64 dependencies for Z3. However, the default stays by only x64.

Maven: change publication pattern, do not use classifier for plain Ja…

ddc9977

…rs, but only all other files. This cleanup aligns better with Maven guidelines. This is a small change for all upcoming publications to Maven and the Maven users.

#380: rewrite Maven publication step to support x64 and arm64 archite…

14699d6

…cture. Additionally, we upload Java sources and JavaDoc for z3 to the Maven repository. We need to test whether the uploaded files work as expected.

update Maven examples as expected to work. Not yet tested.

78a298e

#380: update readme to show our support for ARM64.

a55cfe7

#380: make basic configurations for Z3 public.

9d68306

Let the user decide what to load, e.g. on a minimal system only load for one specific OS and arch.

Z3: update to v4.13.2

321da34

Z3: update build-scripts for v4.13.3

bbfb727

Z3: avoid regression error.

d6019c6

See Z3Prover/z3#7419 for details. If required, the Z3 parser automatically converts Boolean formulas `f` to e.g. `ITE(f 1 0)`, which makes them comparable to Integer symbols and numbers 0/1.

fix paths for Windows-based CI.

8a2cddb

Z3: update to v4.13.3

32d5b71

exclude Z3 on some older Linux systems.

9c6867f

use platform-independent solver for simple test.

316d99e

Z3, MathSAT5, Bitwuzla: use separate directory 'dist' for publication…

cd2529a

… instead of JavaSMT root directory.

This was referenced Jan 7, 2025

Update OpenSMT to version 2.8.0 #426

Merged

Update Bitwuzla to version 0.7.X #427

Merged

kfriedberger added 14 commits January 11, 2025 23:58

Merge remote-tracking branch 'origin/master' into 380-multi-architect…

abaedf5

…ure-solver-binaries-z3

fix test: OpenSMT requires newer GLIBC, from Ubuntu 22.04 or newer.

6af4b41

Merge branch 'update_bitwuzla_for_sbv_bugfix' into 380-multi-architec…

7a0dc38

…ture-solver-binaries-z3

Bitwuzla: update version to latest bugfix release.

ad13270

Merge remote-tracking branch 'origin/update_bitwuzla_for_sbv_bugfix' …

7451e8b

…into 380-multi-architecture-solver-binaries-z3

Bitwuzla: update library version to compiled with enabled experimenta…

ebd7030

…l FP sizes.

Bitwuzla: fix typo and rename task to avoid naming conflicts.

9156cee

OpenSMT: refactor build-script to align with other Swig-based build-s…

320434a

…cripts, like Bitwuzla.

OpenSMT: replace GMP from Docker image with externally compiled GMP, …

478ac33

…and improve the linking process.

OpenSMT: add compilation step for Linux on ARM64.

e7b03ef

OpenSMT can be compiled for ARM in two simple steps: - provide GMP for ARM64 (we use the version that we provide for MathSAT anyway) - replace GCC with the cross-compiler for ARM64

OpenSMT: rename library, i.e., shorten "java" to "j".

d7a3059

OpenSMT: update dependency to use x64/arm64 version of OpenSMT.

3d81fe2

Merge remote-tracking branch 'origin/master' into 380-multi-architect…

f5e4276

…ure-solver-binaries-z3

OpenSMT: enrich test with info about GLIBC dependency.

13b3f12

AppVeyor: improve Windows build

657ee3c

baierd requested changes Jan 25, 2025

View reviewed changes

build/build-maven-publish.xml Show resolved Hide resolved

build/build-publish-solvers/macros.xml Show resolved Hide resolved

build/build-maven-publish.xml Show resolved Hide resolved

src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java Show resolved Hide resolved

update Readme.

244467c

update Maven example projects with new library versions.

937b917

The compilation will fail, because JavaSMT is not yet released in a new version, and some library names have been changed.

kfriedberger requested a review from baierd January 25, 2025 20:04

baierd approved these changes Jan 25, 2025

View reviewed changes

kfriedberger merged commit ba42ae4 into master Jan 26, 2025
2 of 3 checks passed

kfriedberger deleted the 380-multi-architecture-solver-binaries-z3 branch January 26, 2025 08:02

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

#380 support multiple architectures for solver binaries z3 #395

#380 support multiple architectures for solver binaries z3 #395

kfriedberger commented Sep 17, 2024 •

edited

Loading

kfriedberger commented Sep 29, 2024 •

edited

Loading

kfriedberger commented Sep 29, 2024 •

edited

Loading

kfriedberger commented Sep 29, 2024 •

edited

Loading

ThomasHaas commented Oct 3, 2024

kfriedberger commented Oct 12, 2024 •

edited

Loading

kfriedberger commented Jan 19, 2025 •

edited

Loading

baierd left a comment

baierd commented Jan 25, 2025

kfriedberger commented Jan 25, 2025

kfriedberger commented Jan 25, 2025

baierd left a comment

kfriedberger commented Jan 26, 2025

#380 support multiple architectures for solver binaries z3 #395

#380 support multiple architectures for solver binaries z3 #395

Conversation

kfriedberger commented Sep 17, 2024 • edited Loading

kfriedberger commented Sep 29, 2024 • edited Loading

kfriedberger commented Sep 29, 2024 • edited Loading

kfriedberger commented Sep 29, 2024 • edited Loading

ThomasHaas commented Oct 3, 2024

kfriedberger commented Oct 12, 2024 • edited Loading

kfriedberger commented Jan 19, 2025 • edited Loading

baierd left a comment

Choose a reason for hiding this comment

baierd commented Jan 25, 2025

kfriedberger commented Jan 25, 2025

kfriedberger commented Jan 25, 2025

baierd left a comment

Choose a reason for hiding this comment

kfriedberger commented Jan 26, 2025

kfriedberger commented Sep 17, 2024 •

edited

Loading

kfriedberger commented Sep 29, 2024 •

edited

Loading

kfriedberger commented Sep 29, 2024 •

edited

Loading

kfriedberger commented Sep 29, 2024 •

edited

Loading

kfriedberger commented Oct 12, 2024 •

edited

Loading

kfriedberger commented Jan 19, 2025 •

edited

Loading