Replace finalizers with PhantomReferences in Java API

[cheshire]

Hi,

This pull request replaces very inefficient finalizers usage with PhantomReferences, as described in #442.
The new solution relies on ReferenceQueues, and does not require any locking at all.

I have tested this code with our rather extensive JavaSMT test suite, however it does not poke around specific Z3 areas JavaSMT does not cover (e.g. goals, datatype sorts, etc).

This pull request might require a few more iterations:

1. What should be the copyright header for the newly created files? I'm fine with whatever.
2. There were many sever style issues in Java API bindings, I have fixed many of them in this pull request as well, albeit in a different commit.
   If absolutely needed I can split it into different pull requests as well, but I think the process would be much easier if we can treat them atomically.

Without fixing some of those style issues it would have been very difficult to write a new solution.

[NikolajBjorner]

Cool,

1. There is a paragraph regarding copyright on https://github.com/Z3Prover/z3/wiki/Contribution-Guidelines. If the question is about credit, one approach is to add your name to files you create. Git also tracks this in an indirect way.
2. Moving { around is fine if this is how Java does it (we use 4 spaces elsewhere https://www.youtube.com/watch?v=K5WW7JOBSjg). Removing redundant casts is even better.

[NikolajBjorner]

be always -> always be

[cheshire]

changed.

[wintersteiger]

No problem if multiple things are adressed in one PR; the main issue from my point of view is that we don't break old applications too severly. It seems you mostly tried to achieve that though. I'll run our Java example through it, that one also runs some simple tests involving goals and tactics.

Regarding the lock on context creation, I think I added that because at one point there was a concurrency bug in the Context creation/initialization, but that may (and should have been) fixed by now. Either way, I don't expect many applications will need thousands of Contexts per second, so performance shouldn't be critical there.

Generally I'm happy with style fixes. None of us is a full-time (or even part-time) Java programmer and we don't have the resources to become one either. At the current stage, we can think about marking some old bad-style things as deprecated (to not break existing applications) and to introduce new concepts that make more sense to Java programmers.

Ideally I would like to get a pro-Java hacker to take over the official maintenance of the Java API, so if you or someone in your sphere of influence is keen on giving this a try let us know!

[wintersteiger]

BTW, does anybody have a good test for concurrency issues in the Java API? Does the JavaSMT test suite contain some stress tests for that?

[wintersteiger]

So, at the moment, our JavaExample doesn't compile because:

..\examples\java\JavaExample.java:187: error: constructor Context in class Context cannot be applied to given types;
    Context ctx = new Context();

Is that a required/recommend style change? If it's easy I'd rather not break this one.

Also:

..\examples\java\JavaExample.java:1059: error: incompatible types: HashMap<String,String> cannot be converted to long
     Context ctx = new Context(cfg);

I think there's no downside whatsoever to keeping the HashMap constructor next to the Map constructor, could you add that back?

[NikolajBjorner]

I would also be inclined to add back Context as an accessible constructor as it isn't a factory creating contexts.

[cheshire]

@NikolajBjorner @wintersteiger I've changed this back. In general, I would say that indeed in Java static methods are mostly preferred over constructors, as they can be given names, and don't contain arbitrary restrictions on chaining (super() has to be the first call in a method, etc).

IIRC the reason for the initial change was to make the native field final (which is indeed a very good idea most of the time).
Without the lock this approach is not required, and the old API works just fine.

In general, I was trying to minimize the number of API changes.
IIRC the only API changes are:

• Changed constructors to static methods in some classes, in order to make fields final.
• Changed "update" method on Expr to return a new expression object instead of modifying the existing one in order to make the field final.

[cheshire]

@wintersteiger I have relatively few concurrency tests in JavaSMT, but I most probably will add more soon. Before that I should try to figure out how to communicate the interrupt leading to segfault issue.

[NikolajBjorner]

I've changed this back.
If it makes sense to have both for beautifying client code, then why not.

[cheshire]

@NikolajBjorner I've started concurrency testing with hundred different threads.

There seems to be two issues:

1. Z3 gets very slow, generating random formula + solving it on hundred different context concurrently takes 23 seconds on my laptop (for comparison, 2 seconds for Princess and 300 ms for SMTInterpol, and normally Z3 is much faster than either of those solvers).
2. When enabling phantom-referenced based GC, I sometimes non-determenistically "get double free or corruption (fasttop)". I do not know yet whether the same problem occurs with old bindings, but I suspect it does.

[cheshire]

Somewhat unhelpful log is available at metaworld.me/concurrent_z3_crash.log

[wintersteiger]

@cheshire: Can you share the test program with us?

[NikolajBjorner]

Regarding the pull request, though, seems ready to integrate.
As we concluded elsewhere, the logs are generally not very useful for the multi-threaded case.

[cheshire]

@wintersteiger yes, it basically creates a random formula, checks it for satisfiability, modifies by traversal, and checks again, doing that in parallel on 100 different contexts.
I was just trying to say that I'm not sure how useful concurrent testing will be for this pull request, as there seems to be many problems associated with multiple thread usage as it is.

  private static class ConcurrencyTester implements Callable<Boolean> {

    private final int threadNo;
    private final SolverContext runnableContext;

    private ConcurrencyTester(int pThreadNo, SolverContext pRunnableContext) {
      threadNo = pThreadNo;
      runnableContext = pRunnableContext;
    }

    @Override
    public Boolean call() {
      try {
        FormulaManager rMgr = runnableContext.getFormulaManager();
        Fuzzer f = new Fuzzer(rMgr, new Random(0));
        BooleanFormula random = f.fuzz(100, 3);
        boolean ans1, ans2;
        try (ProverEnvironment e = runnableContext.newProverEnvironment()) {
          e.push(random);
          ans1 = e.isUnsat();
        }
        BooleanFormula lowercased = rMgr.transformRecursively(new FormulaTransformationVisitor(rMgr) {
          @Override
          public Formula visitFreeVariable(
              Formula f, String name) {
            return rMgr.makeVariable(rMgr.getFormulaType(f), name.toLowerCase());
          }
        }, random);
        try (ProverEnvironment e = runnableContext.newProverEnvironment()) {
          e.push(random);
          ans2 = e.isUnsat();
        }
        assertThat(ans1).isEqualTo(ans2);
        return ans1;
      } catch (SolverException | InterruptedException pE) {
        throw new UnsupportedOperationException("fail");
      }
    }
  }

  @Test
  public void concurrencyTest() throws Exception {
    SolverContextFactory localFactory = new SolverContextFactory(config, logger, shutdownNotifierToUse());

    int poolSize = 100;
    ExecutorService executor = Executors.newFixedThreadPool(poolSize);
    List<Callable<Boolean>> callables = new ArrayList<>(poolSize);

    for (int i = 0; i < poolSize; i++) {
      callables.add(new ConcurrencyTester(i, localFactory.generateContext()));
    }

    List<Future<Boolean>> out = executor.invokeAll(callables);
    executor.shutdown();
    executor.awaitTermination(30, TimeUnit.SECONDS);

    for (Future<Boolean> future :  out) {
      assertThat(future.isDone()).isTrue();
    }
  }

[cheshire]

Right, so what should I do to get this merged?

[wintersteiger]

We can merge that now, but I expect new bug reports will trickle in shortly after that and I won't be available for any testing for bugfixing for about 2 weeks from now. Will you be available to fix at least the simple issues?

[cheshire]

Yes, I would be available for that in the next two weeks (and in general
after as well, but can't give hard guarantees too far ahead).

On Fri, Jun 24, 2016 at 2:39 PM, Christoph M. Wintersteiger <
[email protected]> wrote:

We can merge that now, but I expect new bug reports will trickle in
shortly after that and I won't be available for any testing for bugfixing
for about 2 weeks from now. Will you be available to fix at least the
simple issues?

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
#648 (comment), or mute
the thread
https://github.com/notifications/unsubscribe/AAVTH1zXecXjt9jJGNIyxD-nNJyxVUqzks5qO8__gaJpZM4Iz3Dm
.

[wintersteiger]

That's fantastic, thanks for making room for this! No hard guarantees needed, but it's good to know somebody will look at it if needed.

I'm merging this right now and I'll at least check to see whether the JavaExample produces anything unexpected.

[NikolajBjorner]

Super! Thanks a lot for the substantial contribution.