Unreliable SAT/UNSAT in Multithreaded use

[baierd]

I'm having a problem with the multithreaded usage of Yices 2. I am using the current release version with the compile option for thread safety. When trying to assert a UNSAT formula (formula below) i get varying results in the different threads. i.e. 4 threads: sometimes all return SAT, sometimes 2 SAT and 2 UNSAT etc. (with the same formula that is 100% UNSAT) When trying without threads i get the desired UNSAT reliable. Am i doing something wrong or is this indeed a bug?

The following code is run in multiple threads to reproduce the bug: (May seem a little wierd as it is extracted from a loop. Just treat obvious types like int = int32_t etc.)

      String COUNTER_PREFIX  = "c@";
      String CHOICE_PREFIX = "i@";
      long cfg = yices_new_config();
      yices_set_config(cfg, "solver-type", "dpllt");
      yices_set_config(cfg, "mode", "push-pop");
      long envConc = yices_new_context(cfg);
      yices_context_disable_option(envConc, "var-elim");
      yices_free_config(cfg);
      int intType = yices_int_type();
      int boolType = yices_bool_type();
      int base = yices_eq(yices_named_variable(intType, COUNTER_PREFIX + 0), yices_int32(0));
      int lastIdx = 0;
      int expected = 0;
      int i = 1;
      int selector = yices_named_variable(boolType, CHOICE_PREFIX + i);
      int form1 = yices_or2(mkConstraint(i, 2, selector), mkConstraint(i, 2, yices_not(selector)));
      int form2 =
          yices_or2(mkConstraint(i + 1, 2, yices_not(selector)), mkConstraint(i + 1, 2, selector));
      lastIdx = i + 1;
      expected += 5;
      i += 2;
      int selector2 = yices_named_variable(boolType, CHOICE_PREFIX + i);
      int form3 =
          yices_or2(mkConstraint(i, 2, selector2), mkConstraint(i, 2, yices_not(selector2)));
      int form4 =
          yices_or2(
              mkConstraint(i + 1, 2, yices_not(selector2)),
              mkConstraint(i + 1, 2, selector2));
      lastIdx = i + 1;
      expected += 5;
      int form5 =
          yices_arith_gt_atom(
              yices_named_variable(intType, COUNTER_PREFIX + lastIdx),
              yices_int32(expected));

      int* allConstraints = {base, form1, form2, form3, form4, form5};
      int sat = yices_check_context_with_assumptions(envConc, 0, 6, allConstraints);
      // This sat is unreliable
      yices_free_context(envConc);

[BrunoDutertre]

Thanks. but can you also include the mkConstraint function?

[baierd]

Simply use the formulas in the assert statements in an array with the yices_check_context_with_assumptions() method. I've updated the code above.

Is there any helpful difference in how Yices2 asserts formulas in incremental mode?

(I had to write it out because this example is generated by a function, hence the pseudocode appearance)

[BrunoDutertre]

@baierd. Did you see our previous question: what's mkConstraint?

[baierd]

I am an idiot, sorry.

int mkConstraint(int newIdx, int increment, int selector) {
    String COUNTER_PREFIX  = "c@";
    return yices_and2(
        selector,
        yices_eq(
            yices_named_variable(yices_int_type(), COUNTER_PREFIX + newIdx),
            yices_add(
                yices_named_variable(yices_int_type(), COUNTER_PREFIX + (newIdx - 1)),
                yices_int32(increment))));
  }

[ianamason]

@baierd OK I am gonna take a look.

[ianamason]

I don't see any races. I tried with 100 threads. I was running in a Ubuntu 16.04 vagrant box. This is what I get with 10 threads:

valgrind --tool=helgrind ./problem 10
==21098== Helgrind, a thread error detector
==21098== Copyright (C) 2007-2015, and GNU GPL'd, by OpenWorks LLP et al.
==21098== Using Valgrind-3.11.0 and LibVEX; rerun with -h for copyright info
==21098== Command: ./problem 10
==21098==
10 threads
Logging thread 0 to /tmp/simple_test_0.txt
Logging thread 1 to /tmp/simple_test_1.txt
Logging thread 2 to /tmp/simple_test_2.txt
Logging thread 3 to /tmp/simple_test_3.txt
Logging thread 4 to /tmp/simple_test_4.txt
Logging thread 5 to /tmp/simple_test_5.txt
Logging thread 6 to /tmp/simple_test_6.txt
Logging thread 7 to /tmp/simple_test_7.txt
Logging thread 8 to /tmp/simple_test_8.txt
Logging thread 9 to /tmp/simple_test_9.txt
threads away

thread 0 returned 3
thread 1 returned 3
thread 2 returned 3
thread 3 returned 3
thread 4 returned 3
thread 5 returned 3
thread 6 returned 3
thread 7 returned 3
thread 8 returned 3
thread 9 returned 3
==21098==
==21098== For counts of detected and suppressed errors, rerun with: -v
==21098== Use --history-level=approx or =none to gain increased speed, at
==21098== the cost of reduced accuracy of conflicting-access information
==21098== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 244 from 27)

What platform are you running on?

Are you sure the yices library your java is loading is built with --enable-thread-safety

Here is the code that I was running. Note that the Makefile has hard links to my yices build. So will need futzing. bug.zip

[baierd]

I can confirm that there is no "SAT" problem in your program on my machine(I've tested your program with my lib). The problem could be the build/recompilation used after creating the Yices2 lib that is causing my problem. Edit: You are using yices specific API for threading. Is Yices2 thread safe if i were to not use it, but use another multithreading API?

[ianamason]

I think it is the locking that makes it thread-safe, not the actual code to create threads.

[ianamason]

If you would like to package up a small java example that exhibits the problem, I will happily look into it.

[baierd]

A little context: I work at the JavaSMT project. We are providing a unified API for multiple SMT-Solvers. We use a selfmade JNI wrapper that simply handels input/output into Yices2. The example above is basicly the code that fails in our project (its an excerpt of a concurrency test boiled down to the failing parts) but ill post the full version of my code below. We compile gmp and gperf with options: --enable-cxx --with-pic --disabled-shared --enable-fat And Yices2 with: --enable-thread-safety --with-pic-gmp=/pathToGmp

After that we use a script (in the linked project above: /lib/native/source/yices2j/compile.sh ) to recompile with the JNI wrapper (also present in the same folder). In the current repository version there are some missing -pthread flags that i used for the concurrency tests. Note that the Yices2 implementation is work in progress.

Maybe you see something obvious as to why its failing. Thank you for your assistance.

Code (JUnit-Test that is unreliable):

  @Before
  public void createEnvironment() {
    yices_init();
    long cfg = yices_new_config();
    yices_set_config(cfg, "solver-type", "dpllt");
    yices_set_config(cfg, "mode", "push-pop");
    env = yices_new_context(cfg);
    yices_context_disable_option(env, "var-elim");
    yices_free_config(cfg);
  }

  @After
  public void freeEnvironment() {
    yices_free_context(env);
    yices_exit();
  }

  @Test
  public void simpleConcurrentUNSAT() {
    assertThat(yices_is_thread_safe()).isEqualTo(1);

    assertConcurrency(
        "testIntConcurrencyWithConcurrentContext",
        () -> {
          long cfg = yices_new_config();
          yices_set_config(cfg, "solver-type", "dpllt");
          yices_set_config(cfg, "mode", "push-pop");
          long envConc = yices_new_context(cfg);
          yices_context_disable_option(envConc, "var-elim");
          yices_free_config(cfg);
          int intType = yices_int_type();
          int boolType = yices_bool_type();

          int base = yices_eq(yices_named_variable(intType, COUNTER_PREFIX + 0), yices_int32(0));
          int lastIdx = 0;
          int expected = 0;
          int i = 1;
          int selector = yices_named_variable(boolType, CHOICE_PREFIX + i);
          int form1 =
              yices_or2(mkConstraint(i, 2, selector), mkConstraint(i, 2, yices_not(selector)));

          int form2 =
              yices_or2(
                  mkConstraint(i + 1, 2, yices_not(selector)), mkConstraint(i + 1, 2, selector));
          lastIdx = i + 1;
          expected += 5;

          i += 2;
          int selector2 = yices_named_variable(boolType, CHOICE_PREFIX + i);
          int form3 =
              yices_or2(mkConstraint(i, 2, selector2), mkConstraint(i, 2, yices_not(selector2)));

          int form4 =
              yices_or2(
                  mkConstraint(i + 1, 2, yices_not(selector2)), mkConstraint(i + 1, 2, selector2));
          lastIdx = i + 1;
          expected += 5;

          int form5 =
              yices_arith_gt_atom(
                  yices_named_variable(intType, COUNTER_PREFIX + lastIdx), yices_int32(expected));

          int[] allConstraints = {base, form1, form2, form3, form4, form5};

          boolean sat =
              yices_check_sat_with_assumptions(envConc, 0, allConstraints.length, allConstraints);
          assertThat(sat).isEqualTo(false);

          yices_free_context(envConc);
        });
  }

  int generate(int n) {
    int intType = yices_int_type();
    int boolType = yices_bool_type();
    Preconditions.checkArgument(n >= 2);
    List<Integer> clauses = new ArrayList<>();
    clauses.add(yices_eq(yices_named_variable(intType, COUNTER_PREFIX + 0), yices_int32(0)));
    int lastIdx = 0;
    int expected = 0;
    for (int i = 1; i < 2 * n; i += 2) {
      int selector = yices_named_variable(boolType, CHOICE_PREFIX + i);
      clauses.add(yices_or2(mkConstraint(i, 2, selector), mkConstraint(i, 2, yices_not(selector))));
      clauses.add(
          yices_or2(mkConstraint(i + 1, 2, yices_not(selector)), mkConstraint(i + 1, 2, selector)));
      lastIdx = i + 1;
      expected += 5;
    }
    clauses.add(
        yices_arith_gt_atom(
            yices_named_variable(intType, COUNTER_PREFIX + lastIdx), yices_int32(expected)));

    return recursiveClauses(clauses);
  }

  private int recursiveClauses(List<Integer> clauses) {
    if (clauses.size() == 1) {
      return clauses.get(0);
    }
    int clause = clauses.get(0);
    clauses.remove(0);
    return yices_and2(clause, recursiveClauses(clauses));
  }

  private int mkConstraint(int newIdx, int increment, int selector) {
    return yices_and2(
        selector,
        yices_eq(
            yices_named_variable(yices_int_type(), COUNTER_PREFIX + newIdx),
            yices_add(
                yices_named_variable(yices_int_type(), COUNTER_PREFIX + (newIdx - 1)),
                yices_int32(increment))));
  }

  /** just a small lambda-compatible interface. */
  private interface Run {
    void run() throws SolverException, InterruptedException, InvalidConfigurationException;
  }

  // ** Simply assures that all threads are started simultaneously and end after 30s by force. */
  private static void assertConcurrency(String testName, Run runnable) {
    int numberofThreads = 4;
    final ExecutorService threadPool = Executors.newFixedThreadPool(numberofThreads);
    final List<Throwable> exceptionsList = Collections.synchronizedList(new ArrayList<>());

    // Waits for all threads to be started
    final CountDownLatch allExecutorThreadsReady = new CountDownLatch(numberofThreads);
    // Syncs start of tests after all threads are already created
    final CountDownLatch afterInitBlocker = new CountDownLatch(1);
    // Syncs end of tests (And prevents Deadlocks in test-threads etc.)
    final CountDownLatch allDone = new CountDownLatch(numberofThreads);
    for (int i = 0; i < numberofThreads; i++) {
      @SuppressWarnings("unused")
      Future<?> future =
          threadPool.submit(
              () -> {
                allExecutorThreadsReady.countDown();
                try {
                  afterInitBlocker.await();
                  runnable.run();
                } catch (Throwable e) {
                  exceptionsList.add(e);
                } finally {
                  allDone.countDown();
                }
              });
    }
    try {
      assertWithMessage("Timeout initializing the Threads for " + testName)
          .that(allExecutorThreadsReady.await(numberofThreads * 10, TimeUnit.MILLISECONDS))
          .isTrue();
      afterInitBlocker.countDown();
      assertWithMessage("Timeout in " + testName)
          .that(allDone.await(30, TimeUnit.SECONDS))
          .isTrue();
    } catch (Throwable e) {
      exceptionsList.add(e);
    } finally {
      threadPool.shutdownNow();
    }
    assertWithMessage("Test %s failed with exception(s): %s", testName, exceptionsList)
        .that(exceptionsList.isEmpty())
        .isTrue();
  }```

[ianamason]

OK so why are you creating a context in the CreateEnvironment. That looks scary, especially if you use it from other threads.

Our notion of thread safety is that a context should only be accessed by the thread that created it. Are you obeying that?

By the way we have Java bindings for yices2. But Darpa fine print prevents us from flicking the public switch, though hopefully soon.

[baierd]

The context created in CreateEnvironment is not used by the concurrency test below (Its simply ignored and deleted later. We use that for the other tests but they are not run at the same time as the concurrency test).

The test creates 4 threads and each of them creates its own config and context. The contexts never get accessed by another thread.

That's actually nice to hear with the Java bindings, we are looking forward to that.

[BrunoDutertre]

I'm more worried about the calls to yices_init and yices_exit.
You shouldn't call them more than once per JVM. Are there other @Test methods running concurrently?

[ianamason]

Yes, that would be very bad, if each test got is own CreateEnvironment.

[baierd]

yices_init and yices_exit are called only once at the beginning of a test and at the very end. The concurrency is handled inside the @Test. So from the point of view of Java there is a CreateEnvironment once, then the @Test gets started, after the test is done freeEnvironment() calls yices_exit once. Only inside the @Test concurrency is created and handled.

[ianamason]

I suppose I should write a similar test for our bindings...