search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
451 stars 149 forks source link

Update mpfr_java package #3753

Open dwightguth opened 1 year ago

dwightguth commented 1 year ago

It has come to my attention that Java 18 deprecated finalizers for removal in a future Java release. We do not directly use finalizers anywhere in the K frontend or Maude backend, but there is one indirect code path through which we make use of finalization in a project that we maintain.

This is the mpfr-java project: https://github.com/runtimeverification/mpfr-java

We use this to represent arbitrary precision floating point numbers (as represented as the Float sort in K) when we need to be able to perform floating point operations on them in the frontend. I believe the llvm backend also makes use of this type in its scala code for pattern matching.

This package makes use of finalizers to deal with the fact that it has classes that maintain raw pointers to memory allocated in C++ via JNI. The finalizer exists in order to free the memory allocated by the mpfr library when the BigFloat instance becomes unreachable by the garbage collector, so as to avoid the need to implement AutoCloseable and perform try-with-resources on every single BigFloat instance.

Java 9 provides a new API intended to replace finalization for this use case: https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/lang/ref/Cleaner.html

We need to replace our use of finalization with this API in order to be conformant with future versions of Java. This is not by any means urgent, as to my knowledge, finalization is still possible as of Java 21, which we haven't even updated to using on CI yet. However, eventually the finalize method will be removed from Java and thus our code will start leaking memory if we do not update it.

A side note: at the time the mpfr_java package was created, mpfr was not otherwise being installed on machines that installed K. As such, the design choice was made to use JNI and statically link MPFR and GMP into the jars that are distributed with the package. It is a testament to how carefully this process was performed that we have not had to rebuild these binaries more than twice in the past ten years. However, this process is somewhat complicated. It may be worth considering the design choice to replace our use of JNI with JNA and simply rely on the user to have globally installed MPFR and GMP as dynamic libraries. This is at the discretion of the person who takes this task, however.

Baltoli commented 1 year ago

This is a time bomb of sorts, but won't start breaking things for a few years (Java LTS after 21 ends up in our LTS Linux - maybe Ubuntu 26.04??)

Baltoli commented 1 year ago

We shouldn't forget about this though, and should aim to fix it before it becomes annoying.

Baltoli commented 7 months ago

It might be worth doing some automation and cleanup on the MPFR-Java repository more generally so that we can have proper tests, versioning etc. - would be good to be confident we don't break anything when doing this refactoring.