Merge pull request #457 from markpmitchell/mcsat-thread-safety

Improve thread-safety

src/Makefile

@@ -276,6 +276,7 @@ core_src_c := \
 	utils/csets.c \
 	utils/cputime.c \
 	utils/dep_tables.c \
+	utils/error.c \
 	utils/gcd.c \
 	utils/generic_heap.c \
 	utils/hash_functions.c \
@@ -494,7 +495,6 @@ bin_src_c := \
 	frontend/yices_sat_new.c \
 	frontend/yices_smt.c \
 	frontend/yices_smt2.c \
-	frontend/yices_smt2_mt.c \
 	frontend/yices_smtcomp.c \
 
 #

src/api/yices_api.c

@@ -1108,6 +1108,11 @@ EXPORTED void yices_exit(void) {
     delete_sparse_array(&the_root_types);
   }
 
+  free_parameter_list();
+  free_config_list();
+  free_model_list();
+  free_context_list();
+
   delete_parsing_objects();
   delete_fvars();
 
@@ -1123,11 +1128,6 @@ EXPORTED void yices_exit(void) {
   free_bvarith64_buffer_list();
   free_arith_buffer_list();
 
-  free_context_list();
-  free_model_list();
-  free_config_list();
-  free_parameter_list();
-
   delete_list_locks();
 
   q_clear(&r0);

src/frontend/smt2/smt2_commands.c

@@ -2653,8 +2653,13 @@ static void init_search_parameters(smt2_globals_t *g) {
 static void timeout_handler(void *data) {
   smt2_globals_t *g;
 
+#ifndef THREAD_SAFE
   assert(data == &__smt2_globals);
-
+#else
+  /* In the multi-threaded case there are multiple copies of the
+     global data. */
+#endif /* THREAD_SAFE */
+
   g = data;
   if (g->efmode && g->ef_client.efsolver != NULL && g->ef_client.efsolver->status == EF_STATUS_SEARCHING) {
     ef_solver_stop_search(g->ef_client.efsolver);
@@ -2679,14 +2684,13 @@ static smt_status_t check_sat_with_timeout(smt2_globals_t *g, const param_t *par
    * We call init_timeout only now because the internal timeout
    * consumes resources even if it's never used.
    */
-  if (! g->timeout_initialized) {
-    init_timeout();
-    g->timeout_initialized = true;
+  if (! g->to) {
+    g->to = init_timeout();
   }
   g->interrupted = false;
-  start_timeout(g->timeout, timeout_handler, g);
+  start_timeout(g->to, g->timeout, timeout_handler, g);
   stat = check_context(g->ctx, params);
-  clear_timeout();
+  clear_timeout(g->to);
 
   /*
    * Attempt to cleanly recover from interrupt
@@ -2725,15 +2729,14 @@ static smt_status_t check_sat_with_assumptions(smt2_globals_t *g, const param_t
    * We call init_timeout only now because the internal timeout
    * consumes resources even if it's never used.
    */
-  if (! g->timeout_initialized) {
-    init_timeout();
-    g->timeout_initialized = true;
+  if (! g->to) {
+    g->to = init_timeout();
   }
   g->interrupted = false;
-  start_timeout(g->timeout, timeout_handler, g);
+  start_timeout(g->to, g->timeout, timeout_handler, g);
   stat = check_with_assumptions(g->ctx, params, a->assumptions.size, a->assumptions.data, &a->core);
   a->status = stat;
-  clear_timeout();
+  clear_timeout(g->to);
 
   /*
    * Attempt to cleanly recover from interrupt
@@ -2773,14 +2776,13 @@ static smt_status_t check_sat_with_model(smt2_globals_t *g, const param_t *param
    * We call init_timeout only now because the internal timeout
    * consumes resources even if it's never used.
    */
-  if (! g->timeout_initialized) {
-    init_timeout();
-    g->timeout_initialized = true;
+  if (! g->to) {
+    g->to = init_timeout();
   }
   g->interrupted = false;
-  start_timeout(g->timeout, timeout_handler, g);
+  start_timeout(g->to, g->timeout, timeout_handler, g);
   stat = check_with_model(g->ctx, params, n, vars, values);
-  clear_timeout();
+  clear_timeout(g->to);
 
   /*
    * Attempt to cleanly recover from interrupt
@@ -3026,7 +3028,7 @@ static void add_delayed_assertion(smt2_globals_t *g, term_t t) {
 /*
  * Check satisfiability of all assertions
  */
-static void check_delayed_assertions(smt2_globals_t *g) {
+static void check_delayed_assertions(smt2_globals_t *g, bool report) {
   int32_t code;
   smt_status_t status;
   model_t *model;
@@ -3036,12 +3038,14 @@ static void check_delayed_assertions(smt2_globals_t *g) {
 
   if (g->trivially_unsat) {
     trace_printf(g->tracer, 3, "(check-sat: trivially unsat)\n");
-    report_status(g, STATUS_UNSAT);
+    if (report)
+      report_status(g, STATUS_UNSAT);
   } else if (trivially_true_assertions(g->assertions.data, g->assertions.size, &model)) {
     trace_printf(g->tracer, 3, "(check-sat: trivially true)\n");
     g->trivially_sat = true;
     g->model = model;
-    report_status(g, STATUS_SAT);
+    if (report)
+      report_status(g, STATUS_SAT);
   } else {
     /*
      * check for mislabeled benchmarks: some benchmarks
@@ -3105,7 +3109,8 @@ static void check_delayed_assertions(smt2_globals_t *g) {
 	status = check_sat_with_timeout(g, &g->parameters);
       }
 
-      report_status(g, status);
+      if (report)
+	report_status(g, status);
     }
   }
 }
@@ -3312,18 +3317,17 @@ static void efsolve_cmd(smt2_globals_t *g) {
   if (g->efmode) {
     efc = &g->ef_client;
     if (g->timeout != 0) {
-      if (! g->timeout_initialized) {
-        init_timeout();
-        g->timeout_initialized = true;
+      if (! g->to) {
+        g->to = init_timeout();
       }
       g->interrupted = false;
-      start_timeout(g->timeout, timeout_handler, g);
+      start_timeout(g->to, g->timeout, timeout_handler, g);
     }
 
     ef_solve(efc, g->assertions.size, g->assertions.data, &g->parameters,
 	     qf_fragment(g->logic_code), ef_arch_for_logic(g->logic_code),
              g->tracer, &g->term_patterns);
-    if (g-> timeout != 0) clear_timeout();
+    if (g-> timeout != 0) clear_timeout(g->to);
 
     if (efc->efcode != EF_NO_ERROR) {
       // error in preprocessing
@@ -4577,7 +4581,7 @@ static void init_smt2_globals(smt2_globals_t *g) {
   init_params_to_defaults(&g->parameters);
   g->nthreads = 0;
   g->timeout = 0;
-  g->timeout_initialized = false;
+  g->to = NULL;
   g->interrupted = false;
   g->delegate = NULL;
   g->avtbl = NULL;
@@ -4629,8 +4633,8 @@ static void init_smt2_globals(smt2_globals_t *g) {
  * - delete the timeout object if it's initialized
  */
 static void delete_smt2_globals(smt2_globals_t *g) {
-  if (g->timeout_initialized) {
-    delete_timeout();
+  if (g->to) {
+    delete_timeout(g->to);
   }
   delete_info_table(g);
   if (g->logic_name != NULL) {
@@ -6598,7 +6602,7 @@ static yices_thread_result_t YICES_THREAD_ATTR check_delayed_assertions_thread(v
   g->out = output;   // /tmp/check_delayed_assertions_thread_<thread index>.txt
   g->err = output;   // /tmp/check_delayed_assertions_thread_<thread index>.txt
 
-  check_delayed_assertions(g);
+  check_delayed_assertions(g, /*report=*/false);
 
   return yices_thread_exit();
 }
@@ -6621,18 +6625,22 @@ static smt_status_t get_status_from_globals(smt2_globals_t *g) {
 static void check_delayed_assertions_mt(smt2_globals_t *g) {
   bool success;
   uint32_t i, n;
+  bool verbose;
 
   n = g->nthreads;
   assert(n > 0);
 
+  verbose = g->verbosity > 0;
+
   smt2_globals_t *garray =  (smt2_globals_t *) safe_malloc(n * sizeof(smt2_globals_t));
   for(i = 0; i < n; i++) {
     garray[i] = __smt2_globals;  // just copy them for now.
     garray[i].tracer = NULL;     // only main thread can use this.
   }
-  launch_threads(n, garray, sizeof(smt2_globals_t), "check_delayed_assertions_thread", check_delayed_assertions_thread, true);
-  fprintf(stderr, "All threads finished. Now computing check_delayed_assertions in main thread.\n");
-  check_delayed_assertions(g);
+  launch_threads(n, garray, sizeof(smt2_globals_t), "check_delayed_assertions_thread", check_delayed_assertions_thread, verbose);
+  if (verbose)
+    fprintf(stderr, "All threads finished. Now computing check_delayed_assertions in main thread.\n");
+  check_delayed_assertions(g, /*report=*/true);
 
   //could check that they are all OK
 
@@ -6646,11 +6654,9 @@ static void check_delayed_assertions_mt(smt2_globals_t *g) {
     //free the model if there is one, and free the context.
     //IAM: valgrind says there is no leak here. This is puzzling.
   }
-  if (success) {
-    fprintf(stderr, "SUCCESS: All threads agree.\n");
-  } else {
-    fprintf(stderr, "FAILURE: Threads disagree.\n");
-  }
+  if (verbose)
+    fprintf(stderr,
+	    success ? "SUCCESS: All threads agree.\n" : "FAILURE: Threads disagree.\n");
   safe_free(garray);
 }
 #endif
@@ -6679,10 +6685,10 @@ void smt2_check_sat(void) {
       } else {
 	//	show_delayed_assertions(&__smt2_globals);
 #ifndef THREAD_SAFE
-        check_delayed_assertions(&__smt2_globals);
+        check_delayed_assertions(&__smt2_globals, /*report=*/true);
 #else
         if (__smt2_globals.nthreads == 0) {
-          check_delayed_assertions(&__smt2_globals);
+          check_delayed_assertions(&__smt2_globals, /*report=*/true);
         } else {
 	  check_delayed_assertions_mt(&__smt2_globals);
 	}

src/frontend/smt2/smt2_commands.h

@@ -50,6 +50,7 @@
 #include "utils/int_vectors.h"
 #include "utils/ptr_vectors.h"
 #include "utils/string_hash_map.h"
+#include "utils/timeout.h"
 #include "parser_utils/lexer.h"
 #include "parser_utils/term_stack2.h"
 #include "io/tracer.h"
@@ -401,7 +402,7 @@ typedef struct smt2_globals_s {
 
   // timeout
   uint32_t timeout;           // default = 0 (no timeout)
-  bool timeout_initialized;   // initially false. true once init_timeout is called
+  timeout_t *to;              // initially NULL. Non-NULL once init_timeout is called
   bool interrupted;           // true if the most recent call to check_sat timed out
 
   // optional: delegate sat solver for QF_BV

src/frontend/yices/yices_reval.c

@@ -138,7 +138,7 @@
  * OTHER
  * - timeout: timeout value in second (applies to check)
  *   timeout value = 0 means no timeout
- * - timeout_initialized: true once init_timeout is called
+ * - to: the timeout structure
  *
  * COMMAND-LINE OPTIONS:
  * - logic_name: logic to use (option --logic=xxx)
@@ -175,7 +175,7 @@ static int32_t verbosity;
 static tracer_t *tracer;
 
 static uint32_t timeout;
-static bool timeout_initialized;
+static timeout_t *to;
 
 static char *logic_name;
 static char *arith_name;
@@ -262,8 +262,6 @@ static pp_area_t pp_area = {
   140, UINT32_MAX, 0, false, false
 };
 
-
-
 /**************************
  *  COMMAND-LINE OPTIONS  *
  *************************/
@@ -2542,11 +2540,10 @@ static void timeout_handler(void *data) {
  */
 static void set_timeout(void) {
   if (timeout > 0) {
-    if (!timeout_initialized) {
-      init_timeout();
-      timeout_initialized = true;
+    if (!to) {
+      to = init_timeout();
     }
-    start_timeout(timeout, timeout_handler, context);
+    start_timeout(to, timeout, timeout_handler, context);
   }
 }
 
@@ -2555,8 +2552,8 @@ static void set_timeout(void) {
  */
 static void reset_timeout(void) {
   if (timeout > 0) {
-    assert(timeout_initialized);
-    clear_timeout();
+    assert(to);
+    clear_timeout(to);
     timeout = 0;
   }
 }
@@ -3999,7 +3996,7 @@ int yices_main(int argc, char *argv[]) {
    */
   interactive = false;
   timeout = 0;
-  timeout_initialized = false;
+  to = NULL;
   include_depth = 0;
   ready_time = 0.0;
   check_process_time = 0.0;
@@ -4111,8 +4108,8 @@ int yices_main(int argc, char *argv[]) {
 
   yices_exit();
 
-  if (timeout_initialized) {
-    delete_timeout();
+  if (to) {
+    delete_timeout(to);
   }
 
   return exit_code;

src/frontend/yices_smt.c

@@ -182,6 +182,7 @@ static arith_solver_t arith_solver;
  */
 static uint32_t timeout;
 
+static timeout_t *to;
 
 /*
  * Filename given on the command line
@@ -2040,15 +2041,15 @@ static int process_benchmark(char *filename) {
     start_search_time = get_cpu_time();
 
     if (timeout > 0) {
-      init_timeout();
-      start_timeout(timeout, timeout_handler, &context);
+      to = init_timeout();
+      start_timeout(to, timeout, timeout_handler, &context);
     }
     code = check_context(&context, search_options);
     clear_handler();
 
     if (timeout > 0) {
-      clear_timeout();
-      delete_timeout();
+      clear_timeout(to);
+      delete_timeout(to);
     }
 
     print_results();