Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid

[simgrid.git] / src / mc / mc_safety.cpp

diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp
index f4ff0b7..1642b3a 100644 (file)
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/mc_safety.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2014. The SimGrid Team.
+/* Copyright (c) 2008-2015. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -6,16 +6,16 @@
 
 #include <assert.h>
 
-#include "mc_state.h"
-#include "mc_request.h"
-#include "mc_safety.h"
-#include "mc_private.h"
-#include "mc_record.h"
-#include "mc_smx.h"
-#include "mc_client.h"
-#include "mc_exit.h"
+#include "src/mc/mc_state.h"
+#include "src/mc/mc_request.h"
+#include "src/mc/mc_safety.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_record.h"
+#include "src/mc/mc_smx.h"
+#include "src/mc/mc_client.h"
+#include "src/mc/mc_exit.h"
 
-#include "xbt/mmalloc/mmprivate.h"
+#include "src/xbt/mmalloc/mmprivate.h"
 
 extern "C" {
 
@@ -54,7 +54,7 @@ static void MC_pre_modelcheck_safety()
   XBT_DEBUG("Initial state");
 
   /* Wait for requests (schedules processes) */
-  MC_wait_for_requests();
+  mc_model_checker->wait_for_requests();
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
   smx_process_t process;
@@ -73,7 +73,7 @@ static void MC_pre_modelcheck_safety()
 /** \brief Model-check the application using a DFS exploration
  *         with DPOR (Dynamic Partial Order Reductions)
  */
-void MC_modelcheck_safety(void)
+int MC_modelcheck_safety(void)
 {
   MC_modelcheck_safety_init();
 
@@ -119,14 +119,14 @@ void MC_modelcheck_safety(void)
 
       /* Answer the request */
       MC_simcall_handle(req, value);
-      MC_wait_for_requests();
+      mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
       next_state = MC_state_new();
 
       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
           MC_show_non_termination();
-          exit(SIMGRID_EXIT_NON_TERMINATION);
+          return SIMGRID_MC_EXIT_NON_TERMINATION;
       }
 
       if ((visited_state = is_visited_state(next_state)) == NULL) {
@@ -186,7 +186,7 @@ void MC_modelcheck_safety(void)
       /* Check for deadlocks */
       if (MC_deadlock_check()) {
         MC_show_deadlock(NULL);
-        exit(SIMGRID_EXIT_DEADLOCK);
+        return SIMGRID_MC_EXIT_DEADLOCK;
       }
 
       /* Traverse the stack backwards until a state with a non empty interleave
@@ -199,6 +199,9 @@ void MC_modelcheck_safety(void)
       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);
+          if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
+            xbt_die("Mutex is currently not supported with DPOR, "
+              "use --cfg=model-check/reduction:none");
           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
@@ -256,7 +259,7 @@ void MC_modelcheck_safety(void)
 
   XBT_INFO("No property violation found.");
   MC_print_statistics(mc_stats);
-  exit(SIMGRID_EXIT_SUCCESS);
+  return SIMGRID_MC_EXIT_SUCCESS;
 }
 
 static void MC_modelcheck_safety_init(void)
@@ -270,7 +273,7 @@ static void MC_modelcheck_safety_init(void)
     XBT_INFO("Check non progressive cycles");
   else
     XBT_INFO("Check a safety property");
-  MC_wait_for_requests();
+  mc_model_checker->wait_for_requests();
 
   XBT_DEBUG("Starting the safety algorithm");