Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improved Java phantom references #7131

Merged
merged 7 commits into from
Feb 21, 2024

Conversation

ThomasHaas
Copy link
Contributor

@ThomasHaas ThomasHaas commented Feb 17, 2024

This PR reworks the handling of phantom references in the Z3 API.

The previous implementation used N different reference queues, each with a IdentityHashMap to associate to each phantom reference the native z3 object it reference counts.
In some extreme cases, the IdentityHashMap's performance could degenerate, for example, if a user propagator creates millions of formulas in a short time (every fixed-callback creates at least 2 phantom references right now!)
Furthemore, Java's IdentityHashMap does not implement shrinking, so that the map can permanently consume a lot of memory even if emptied.

The new implementation replaces the hashmap with a doubly-linked list consisting of custom subclasses of phantom references.

Advantages:

  • The doubly-linked list has a strictly smaller memory footprint in all cases and has no issues with shrinking. It also avoids the boxing of a long.
  • The new phantom references have true constant-time handling as opposed to amortized constant time (no O(n) map enlargements, and no high access times in degenerate cases with high number of hash collisions)
  • The N different reference queues are combined into a single reference queue for all objects (managed by Context). Instead, there are N different implementations(*) of PhantomReference all of which are directly inlined in the class they reference count (e.g. AST contains ASTRef). This puts the implementation of incRef and decRef in the same class for better maintainability.

Disadvantages:

  • None. As far as I see, the new implementation is superior in every aspect: performance, memory, and maintainability.

(*) There is an even easier implementation that uses a single PhantomReference implementation that stores a method reference to the decRef implementation (rather than using subclassing). This variant stores an extra pointer per reference which increases memory consumption by ~14% and makes the implementation not strictly more memory efficient than IdentityHashMap (in most practical cases it will still be better) (EDIT: it is still strictly better since it avoids the boxing of a long).

Disclaimer: I have not yet tested the correctness of this new implementation. However, I have implemented and tested a slightly easier version in JavaSMT (this version reference counts only AST objects). Still, some testing should be done before merging.

 - Replaced IDecRefQueue with a new Z3ReferenceQueue class
 - Z3ReferenceQueue manages custom subclasses of phantom references in a doubly-linked list
 - Replaced all subclasses of IDecRefQueue with subclasses of Z3ReferenceQueue.Reference. These custom reference classes are embedded in the class they reference count.
 - Context now owns a single Z3ReferenceQueue for all types of references.
@ThomasHaas
Copy link
Contributor Author

Do I need to change update the python scripts that build the .jar (I don't know why the CI fails)?

@NikolajBjorner
Copy link
Contributor

NikolajBjorner commented Feb 17, 2024

Need to update CMakeLists.txt for cmake build

@NikolajBjorner
Copy link
Contributor

Thanks, I will check with java examples manually around Tuesday. I am not sure they get tested on the build.

@NikolajBjorner NikolajBjorner merged commit a3d00ce into Z3Prover:master Feb 21, 2024
17 checks passed
NikolajBjorner pushed a commit that referenced this pull request Feb 21, 2024
* Reworked phantom reference handling.
 - Replaced IDecRefQueue with a new Z3ReferenceQueue class
 - Z3ReferenceQueue manages custom subclasses of phantom references in a doubly-linked list
 - Replaced all subclasses of IDecRefQueue with subclasses of Z3ReferenceQueue.Reference. These custom reference classes are embedded in the class they reference count.
 - Context now owns a single Z3ReferenceQueue for all types of references.

* Made Statistics.Entry a static subclass

* Made Context.close idempotent (as recommended)

* Update CMakeLists.txt for building the Java API.

* Updated CMakeLists.txt again.

* Use correct SuppressWarning annotation to silence the compiler

* Formatting
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants