MC-SAT Thread Safety (#456)

* Correct debug code.

* Avoid deadlocks in MC-SAT.

---------

Co-authored-by: Mark Mitchell <mark.mitchell@sri.com>

configure.ac

@@ -870,10 +870,6 @@ fi
 AC_SUBST(THREAD_SAFE)
 if test "x$thread_safe" = xyes ; then
    THREAD_SAFE=1
-   # iam: the aim is to eventually eliminate this restriction, but not before the 2.6.2 release.
-   if test $use_mcsat = yes ; then
-      AC_MSG_ERROR([Building with both --enable-mcsat and --enable-thread-safety is currently not supported.])
-   fi
 fi
 
 dnl

src/api/yices_api.c

@@ -8669,10 +8669,10 @@ static inline bool yices_assert_formula_checks(term_t t) {
   MT_PROTECT(bool,  __yices_globals.lock, _o_yices_assert_formula_checks(t));
 }
 
-EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) {
+int32_t _o_yices_assert_formula(context_t *ctx, term_t t) {
   int32_t code;
 
-  if (! yices_assert_formula_checks(t)) {
+  if (! _o_yices_assert_formula_checks(t)) {
     return -1;
   }
 
@@ -8711,7 +8711,7 @@ EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) {
 
   assert(context_status(ctx) == STATUS_IDLE);
 
-  code = assert_formula(ctx, t);
+  code = _o_assert_formula(ctx, t);
   if (code < 0) {
     // error during internalization
     convert_internalization_error(code);
@@ -8722,6 +8722,10 @@ EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) {
   return 0;
 }
 
+EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) {
+  MT_PROTECT(int32_t, __yices_globals.lock,
+	     _o_yices_assert_formula(ctx, t));
+}
 
 
 
@@ -9054,23 +9058,19 @@ static bool _o_unsat_core_check_assumptions(uint32_t n, const term_t a[]) {
   return check_good_terms(__yices_globals.manager, n, a) && check_boolean_args(__yices_globals.manager, n, a);
 }
 
-static bool unsat_core_check_assumptions(uint32_t n, const term_t a[]) {
-  MT_PROTECT(bool,  __yices_globals.lock, _o_unsat_core_check_assumptions(n, a));
-}
-
 /*
  * Check context with assumptions
  * - n = number of assumptions
  * - a[0] ... a[n-1] = n assumptions. All of them must be Boolean terms.
  */
-EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t a[]) {
+smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t a[]) {
   param_t default_params;
   ivector_t assumptions;
   smt_status_t stat;
   uint32_t i;
   literal_t l;
 
-  if (!unsat_core_check_assumptions(n, a)) {
+  if (!_o_unsat_core_check_assumptions(n, a)) {
     return STATUS_ERROR; // Bad assumptions
   }
 
@@ -9113,8 +9113,6 @@ EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const
 
   assert(context_status(ctx) == STATUS_IDLE);
 
-  yices_obtain_mutex();
-
   // convert the assumptions to n literals
   init_ivector(&assumptions, n);
   for (i=0; i<n; i++) {
@@ -9130,8 +9128,6 @@ EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const
   }
   assert(assumptions.size == n);
 
-  yices_release_mutex();
-
   // set parameters
   if (params == NULL) {
     yices_default_params_for_context(ctx, &default_params);
@@ -9150,6 +9146,9 @@ EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const
   return stat;
 }
 
+EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t a[]) {
+  MT_PROTECT(smt_status_t, __yices_globals.lock, _o_yices_check_context_with_assumptions(ctx, params, n, a));
+}
 
 /*
  * CHECK WITH A MODEL

src/api/yices_api_lock_free.h

@@ -575,9 +575,16 @@ extern context_t *_o_yices_new_context(const ctx_config_t *config);
 
 extern void _o_yices_free_context(context_t *ctx);
 
-//iam: this one is defined in context.c
+extern int32_t _o_yices_assert_formula(context_t *ctx, term_t t);
+
+//Defined in context.c.
 extern int32_t _o_assert_formulas(context_t *ctx, uint32_t n, const term_t *f);
 
+extern int32_t _o_assert_formula(context_t *ctx, term_t);
+
+extern smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param_t *params,
+									   uint32_t n, const term_t t[]);
+
 /****************
  *  UNSAT CORE  *
  ***************/

src/context/context.c

@@ -6291,8 +6291,12 @@ int32_t assert_formulas(context_t *ctx, uint32_t n, const term_t *f) {
  * - otherwise, the code is negative. The assertion could
  *   not be processed.
  */
+int32_t _o_assert_formula(context_t *ctx, term_t f) {
+  return _o_assert_formulas(ctx, 1, &f);
+}
+
 int32_t assert_formula(context_t *ctx, term_t f) {
-  return assert_formulas(ctx, 1, &f);
+  MT_PROTECT(int32_t, __yices_globals.lock, _o_assert_formula(ctx, f));
 }
 
 

src/mcsat/bv/bv_explainer.c

@@ -38,6 +38,7 @@
 #include "explain/full_bv_trivial.h"
 
 #include "yices.h"
+#include "api/yices_api_lock_free.h"
 #include <inttypes.h>
 
 void bv_subexplainer_construct(bv_subexplainer_t* exp, const char* name, plugin_context_t* ctx, watch_list_manager_t* wlm, bv_evaluator_t* eval) {
@@ -169,10 +170,10 @@ void bv_explainer_normalize_conflict(bv_explainer_t* exp, ivector_t* conflict_ou
 }
 
 void bv_explainer_check_conflict(bv_explainer_t* exp, const ivector_t* conflict) {
-  context_t* ctx = yices_new_context(NULL);
+  context_t* ctx = _o_yices_new_context(NULL);
   uint32_t i;
   for (i = 0; i < conflict->size; ++ i) {
-    yices_assert_formula(ctx, conflict->data[i]);
+    _o_yices_assert_formula(ctx, conflict->data[i]);
   }
   smt_status_t result = yices_check_context(ctx, NULL);
   (void) result;

src/mcsat/bv/bv_utils.h

@@ -35,6 +35,7 @@
 #include "mcsat/tracing.h"
 #include "mcsat/value.h"
 #include "yices.h"
+#include "api/yices_api_lock_free.h"
 
 /** Types of bitvector terms */
 typedef enum {
@@ -467,8 +468,8 @@ static inline
 bool check_rewrite(plugin_context_t* ctx, term_t old, term_t t){
   if (t == old) return true;
   term_manager_t* tm   = ctx->tm;
-  context_t* yctx      = yices_new_context(NULL);
-  yices_assert_formula(yctx, mk_neq(tm, old, t));
+  context_t* yctx      = _o_yices_new_context(NULL);
+  _o_yices_assert_formula(yctx, mk_neq(tm, old, t));
   smt_status_t output = yices_check_context(yctx, NULL);
   bool result = (output == STATUS_UNSAT);
   if (!result && ctx_trace_enabled(ctx, "mcsat::bv::arith::ctz")) {
@@ -479,7 +480,7 @@ bool check_rewrite(plugin_context_t* ctx, term_t old, term_t t){
     ctx_trace_term(ctx, t);
     assert(false);
   }
-  yices_free_context(yctx);
+  _o_yices_free_context(yctx);
   return result;
 }
 

src/mcsat/bv/explain/eq_ext_con.c

@@ -33,6 +33,7 @@
 #include "mcsat/eq/equality_graph.h"
 
 #include "yices.h"
+#include "api/yices_api_lock_free.h"
 #include "eq_ext_con.h"
 
 
@@ -1543,7 +1544,7 @@ term_t explain_propagation(bv_subexplainer_t* this, const ivector_t* reasons_in,
   if (ok) {
     // Concat the terms
     if (to_concat.size > 1) {
-      result_subst = yices_bvconcat(to_concat.size, to_concat.data);
+      result_subst = _o_yices_bvconcat(to_concat.size, to_concat.data);
     } else {
       result_subst = to_concat.data[0];
     }

src/mcsat/bv/explain/full_bv_sat.c

@@ -142,8 +142,8 @@ void bb_sat_solver_add_variable(bb_sat_solver_t* solver, variable_t var, bool wi
     term_t var_fresh;
     term_kind_t kind = term_kind(solver->yices_ctx->terms, var_term);
     if (kind != UNINTERPRETED_TERM) {
-      type_t var_type = yices_type_of_term(var_term);
-      var_fresh = yices_new_uninterpreted_term(var_type);
+      type_t var_type = _o_yices_type_of_term(var_term);
+      var_fresh = _o_yices_new_uninterpreted_term(var_type);
     } else {
       var_fresh = var_term;
     }
@@ -163,7 +163,7 @@ void bb_sat_solver_assert_term(bb_sat_solver_t* solver, variable_t assertion_ter
     fprintf(out, "  previously \n");
     ctx_trace_term(solver->ctx, assertion_term);
   }
-  yices_assert_formula(solver->yices_ctx, assertion_term);
+  _o_yices_assert_formula(solver->yices_ctx, assertion_term);
 }
 
 /**
@@ -276,7 +276,7 @@ void bb_sat_solver_solve_and_get_core(bb_sat_solver_t* solver, term_vector_t* co
   }
 
   // Check the assumptions (should be unsat)
-  smt_status_t status = yices_check_context_with_assumptions(solver->yices_ctx, NULL, assumptions.size, assumptions.data);
+  smt_status_t status = _o_yices_check_context_with_assumptions(solver->yices_ctx, NULL, assumptions.size, assumptions.data);
   (void) status;
   assert(status == STATUS_UNSAT);
 

src/mcsat/conflict.c

@@ -29,19 +29,20 @@
 #include "mcsat/tracing.h"
 
 #include "yices.h"
+#include "api/yices_api_lock_free.h"
 #include <inttypes.h>
 
 #define CONFLICT_DEFAULT_ELEMENT_SIZE 100
 
 void conflict_check(conflict_t* conflict) {
   ctx_config_t* config = yices_new_config();
-  context_t* ctx = yices_new_context(config);
+  context_t* ctx = _o_yices_new_context(config);
   uint32_t i;
   const ivector_t* literals = &conflict->disjuncts.element_list;
   for (i = 0; i < literals->size; ++i) {
     term_t literal = literals->data[i];
     literal = opposite_term(literal);
-    int32_t ret = yices_assert_formula(ctx, literal);
+    int32_t ret = _o_yices_assert_formula(ctx, literal);
     if (ret != 0) {
       // unsupported by regular yices
       fprintf(stderr, "skipping conflict (ret)\n");
@@ -52,7 +53,7 @@ void conflict_check(conflict_t* conflict) {
   smt_status_t result = yices_check_context(ctx, NULL);
   (void) result;
   assert(result == STATUS_UNSAT);
-  yices_free_context(ctx);
+  _o_yices_free_context(ctx);
   yices_free_config(config);
 }
 

src/mcsat/preprocessor.c

@@ -34,6 +34,7 @@
 #include "context/context_types.h"
 
 #include "yices.h"
+#include "api/yices_api_lock_free.h"
 
 void preprocessor_construct(preprocessor_t* pre, term_table_t* terms, jmp_buf* handler, const mcsat_options_t* options) {
   pre->terms = terms;
@@ -459,8 +460,8 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
                 size = 0;
               }
             }
-            current_pre = yices_bvconcat(n_vars, vars);
-            term_t eq = yices_eq(current, current_pre);
+            current_pre = _o_yices_bvconcat(n_vars, vars);
+            term_t eq = _o_yices_eq(current, current_pre);
             preprocessor_mark_eq(pre, eq, current);
           }
         }
@@ -598,7 +599,7 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
       } else {
         type_t arg_pre_type = term_type(pre->terms, arg_pre);
         term_t arg_pre_is_positive = mk_arith_term_geq0(&pre->tm, arg_pre);
-        term_t arg_negative = yices_neg(arg_pre);
+        term_t arg_negative = _o_yices_neg(arg_pre);
         current_pre = mk_ite(&pre->tm, arg_pre_is_positive, arg_pre, arg_negative, arg_pre_type);
       }
       break;
@@ -718,7 +719,7 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
             trace_term_ln(pre->tracer, terms, arg_pre);
           }
           // For simplification purposes use API
-          current_pre = yices_bitextract(arg_pre, index);
+          current_pre = _o_yices_bitextract(arg_pre, index);
           assert(current_pre != NULL_TERM);
         }
       }

src/mt/yices_locks_posix.c

@@ -20,30 +20,38 @@
 #include <stdio.h>
 #include <assert.h>
 #include <errno.h>
+#include <string.h>
 
 #include "yices_locks.h"
 
-//I see NDEBUG and DEBUG in the code; which is it?
-#ifdef DEBUG
-static pthread_mutexattr_t mta;
-static pthread_mutexattr_t* mattr = &mta;
-#else
-static pthread_mutexattr_t* mattr = NULL;
-#endif
+static void print_error(const char *caller, const char *syscall, int errnum) {
+  char buffer[64];
 
+  strerror_r(errnum, buffer, sizeof(buffer));
+  fprintf(stderr, "%s failed: %s returned %d: %s\n", caller, syscall,
+	  errnum, buffer);
+}
 
 int32_t create_yices_lock(yices_lock_t* lock){
   int32_t retcode;
-#ifdef DEBUG
-  retcode = pthread_mutexattr_settype(&mta, PTHREAD_MUTEX_ERRORCHECK);
-  if(retcode){
-    fprintf(stderr, "create_yices_lock failed: pthread_mutexattr_settype returned %d\n", retcode);
-  }
+#ifndef NDEBUG
+  pthread_mutexattr_t mta;
+  pthread_mutexattr_t *mattr = &mta;
+#else
+  pthread_mutexattr_t *mattr = NULL;
+#endif
+
+#ifndef NDEBUG
+  retcode = pthread_mutexattr_init(mattr);
+  if(retcode)
+    print_error("create_yices_lock", "pthread_mutexattr_init", retcode);
+  retcode = pthread_mutexattr_settype(mattr, PTHREAD_MUTEX_ERRORCHECK);
+  if(retcode)
+    print_error("create_yices_lock", "pthread_mutextattr_settype", retcode);
 #endif
   retcode = pthread_mutex_init(lock, mattr);
-  if(retcode){
-    fprintf(stderr, "create_yices_lock failed: pthread_mutex_init returned %d\n", retcode);
-  }
+  if(retcode)
+    print_error("create_yices_lock", "pthread_mutex_init", retcode);
   assert(retcode == 0);
   return retcode;
 }
@@ -54,7 +62,7 @@ int32_t try_yices_lock(yices_lock_t* lock){
     if(retcode == EBUSY){
       return 1;
     } else {
-      fprintf(stderr, "try_yices_lock failed: pthread_mutex_trylock returned %d\n", retcode);
+      print_error("try_yices_lock", "pthread_mutex_trylock", retcode);
     }
     return -1;
   }
@@ -65,7 +73,7 @@ int32_t try_yices_lock(yices_lock_t* lock){
 int32_t get_yices_lock(yices_lock_t* lock){
   int32_t retcode = pthread_mutex_lock(lock);
   if(retcode){
-    fprintf(stderr, "get_yices_lock failed: pthread_mutex_lock returned %d\n", retcode);
+    print_error("get_yices_lock", "pthread_mutex_lock", retcode);
   }
   assert(retcode == 0);
   return retcode;
@@ -74,7 +82,7 @@ int32_t get_yices_lock(yices_lock_t* lock){
 int32_t release_yices_lock(yices_lock_t* lock){
   int32_t retcode = pthread_mutex_unlock(lock);
   if(retcode){
-    fprintf(stderr, "release_yices_lock failed: pthread_mutex_unlock returned %d\n", retcode);
+    print_error("release_yices_lock", "pthread_mutex_unlock", retcode);
   }
   assert(retcode == 0);
   return retcode;
@@ -83,7 +91,7 @@ int32_t release_yices_lock(yices_lock_t* lock){
 void destroy_yices_lock(yices_lock_t* lock){
   int32_t retcode = pthread_mutex_destroy(lock);
   if(retcode){
-    fprintf(stderr, "destroy_yices_lock failed: pthread_mutex_destroy returned %d\n", retcode);
+    print_error("destroy_yices_lock", "pthread_mutex_destroy", retcode);
   }
   assert(retcode == 0);
 }