[mc] exit() instead of abort() in normal operation

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index ea972cb..c4eb5fd 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -653,6 +653,7 @@ set(MC_SRC
   src/mc/mc_smx.cpp
   src/mc/mc_xbt.hpp
   src/mc/mc_xbt.cpp
   src/mc/mc_smx.cpp
   src/mc/mc_xbt.hpp
   src/mc/mc_xbt.cpp

+  src/mc/mc_exit.h

   )
 
 set(MC_SIMGRID_MC_SRC
   )
 
 set(MC_SIMGRID_MC_SRC

diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh
index b8a1ca2..8e13b82 100644 (file)
--- a/examples/msg/mc/bugged1.tesh
+++ b/examples/msg/mc/bugged1.tesh
@@ -1,6 +1,6 @@
 #! ./tesh
 
 #! ./tesh
 

-! expect signal SIGABRT
+! expect return 1

 ! timeout 20
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
 > [  0.000000] (0:@) Check a safety property
 ! timeout 20
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
 > [  0.000000] (0:@) Check a safety property

diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh
index 5cb0cf0..9f0b7ad 100644 (file)
--- a/examples/msg/mc/bugged1_liveness.tesh
+++ b/examples/msg/mc/bugged1_liveness.tesh
@@ -1,6 +1,6 @@
 #! ./tesh
 
 #! ./tesh
 

-! expect signal SIGABRT
+! expect return 2

 ! timeout 20
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness
 ! timeout 20
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness

diff --git a/examples/msg/mc/bugged1_liveness_sparse.tesh b/examples/msg/mc/bugged1_liveness_sparse.tesh
index 72d4e72..bc96e3b 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_sparse.tesh
+++ b/examples/msg/mc/bugged1_liveness_sparse.tesh
@@ -1,6 +1,6 @@
 #! ./tesh
 
 #! ./tesh
 

-! expect signal SIGABRT
+! expect return 2

 ! timeout 60
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness
 ! timeout 60
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness

diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh
index daaa02e..fd040b4 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_visited.tesh
+++ b/examples/msg/mc/bugged1_liveness_visited.tesh
@@ -1,6 +1,6 @@
 #! ./tesh
 
 #! ./tesh
 

-! expect signal SIGABRT
+! expect return 2

 ! timeout 90
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256  --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness
 ! timeout 90
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256  --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness

diff --git a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
index 77e64a4..9fe46b0 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
+++ b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
@@ -1,6 +1,6 @@
 #! ./tesh
 
 #! ./tesh
 

-! expect signal SIGABRT
+! expect return 2

 ! timeout 90
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes  --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness
 ! timeout 90
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes  --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness

diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh
index cadf32f..4449cbe 100644 (file)
--- a/examples/msg/mc/bugged2.tesh
+++ b/examples/msg/mc/bugged2.tesh
@@ -1,6 +1,6 @@
 #! ./tesh
 
 #! ./tesh
 

-! expect signal SIGABRT
+! expect return 1

 ! timeout 20
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
 > [  0.000000] (0:@) Check a safety property
 ! timeout 20
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
 > [  0.000000] (0:@) Check a safety property

diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index 41a5918..a30cd61 100644 (file)
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -12,6 +12,7 @@
 #include "mc_record.h"
 #include "mc_smx.h"
 #include "mc_client.h"
 #include "mc_record.h"
 #include "mc_smx.h"
 #include "mc_client.h"

+#include "mc_exit.h"

 
 using simgrid::mc::remote;
 
 
 using simgrid::mc::remote;
 


@@ -144,7 +145,7 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int
         xbt_free(initial_global_state->send_diff);
         initial_global_state->send_diff = NULL;
         MC_print_statistics(mc_stats);
         xbt_free(initial_global_state->send_diff);
         initial_global_state->send_diff = NULL;
         MC_print_statistics(mc_stats);

-        xbt_abort(); 
+        exit(SIMGRID_EXIT_NON_DETERMINISM);

       }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
         XBT_INFO("****************************************************");
         XBT_INFO("***** Non-deterministic communications pattern *****");
       }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
         XBT_INFO("****************************************************");
         XBT_INFO("***** Non-deterministic communications pattern *****");


@@ -156,7 +157,7 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int
         xbt_free(initial_global_state->recv_diff);
         initial_global_state->recv_diff = NULL;
         MC_print_statistics(mc_stats);
         xbt_free(initial_global_state->recv_diff);
         initial_global_state->recv_diff = NULL;
         MC_print_statistics(mc_stats);

-        xbt_abort();
+        exit(SIMGRID_EXIT_NON_DETERMINISM);

       } 
     }
   }
       } 
     }
   }

diff --git a/src/mc/mc_exit.h b/src/mc/mc_exit.h
new file mode 100644 (file)
index 0000000..0b17cac
--- /dev/null
+++ b/src/mc/mc_exit.h
@@ -0,0 +1,13 @@
+#ifndef SIMGRID_MC_EXIT_HPP
+#define SIMGRID_MC_EXIT_HPP
+
+#define SIMGRID_EXIT_SUCCESS  0
+#define SIMGRID_EXIT_SAFETY   1
+#define SIMGRID_EXIT_LIVENESS 2
+#define SIMGRID_EXIT_DEADLOCK 3
+#define SIMGRID_EXIT_NON_TERMINATION 4
+#define SIMGRID_EXIT_NON_DETERMINISM 5
+
+#define SIMGRID_ERROR         63
+
+#endif

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index 927692d..953f138 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -18,6 +18,7 @@
 #include "mc_client.h"
 #include "mc_replay.h"
 #include "mc_safety.h"
 #include "mc_client.h"
 #include "mc_replay.h"
 #include "mc_safety.h"

+#include "mc_exit.h"

 
 extern "C" {
 
 
 extern "C" {
 


@@ -251,7 +252,7 @@ static void MC_modelcheck_liveness_main(void)
           MC_dump_stack_liveness(mc_stack);
           MC_print_statistics(mc_stats);
           XBT_INFO("Counter-example depth : %d", counter_example_depth);
           MC_dump_stack_liveness(mc_stack);
           MC_print_statistics(mc_stats);
           XBT_INFO("Counter-example depth : %d", counter_example_depth);

-          xbt_abort();
+          exit(SIMGRID_EXIT_LIVENESS);

         }
       }
 
         }
       }
 

diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp
index d5fd9ba..f4ff0b7 100644 (file)
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/mc_safety.cpp
@@ -13,6 +13,7 @@
 #include "mc_record.h"
 #include "mc_smx.h"
 #include "mc_client.h"
 #include "mc_record.h"
 #include "mc_smx.h"
 #include "mc_client.h"

+#include "mc_exit.h"

 
 #include "xbt/mmalloc/mmprivate.h"
 
 
 #include "xbt/mmalloc/mmprivate.h"
 


@@ -21,6 +22,8 @@ extern "C" {
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 

+}
+

 static int is_exploration_stack_state(mc_state_t current_state){
 
   xbt_fifo_item_t item;
 static int is_exploration_stack_state(mc_state_t current_state){
 
   xbt_fifo_item_t item;


@@ -35,6 +38,8 @@ static int is_exploration_stack_state(mc_state_t current_state){
   return 0;
 }
 
   return 0;
 }
 

+static void MC_modelcheck_safety_init(void);
+

 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */


@@ -68,8 +73,10 @@ static void MC_pre_modelcheck_safety()
 /** \brief Model-check the application using a DFS exploration
  *         with DPOR (Dynamic Partial Order Reductions)
  */
 /** \brief Model-check the application using a DFS exploration
  *         with DPOR (Dynamic Partial Order Reductions)
  */

-static void MC_modelcheck_safety_main(void)
+void MC_modelcheck_safety(void)

 {
 {

+  MC_modelcheck_safety_init();
+

   char *req_str = NULL;
   int value;
   smx_simcall_t req = NULL;
   char *req_str = NULL;
   int value;
   smx_simcall_t req = NULL;


@@ -119,7 +126,7 @@ static void MC_modelcheck_safety_main(void)
 
       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
           MC_show_non_termination();
 
       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
           MC_show_non_termination();

-          return;
+          exit(SIMGRID_EXIT_NON_TERMINATION);

       }
 
       if ((visited_state = is_visited_state(next_state)) == NULL) {
       }
 
       if ((visited_state = is_visited_state(next_state)) == NULL) {


@@ -179,7 +186,7 @@ static void MC_modelcheck_safety_main(void)
       /* Check for deadlocks */
       if (MC_deadlock_check()) {
         MC_show_deadlock(NULL);
       /* Check for deadlocks */
       if (MC_deadlock_check()) {
         MC_show_deadlock(NULL);

-        return;
+        exit(SIMGRID_EXIT_DEADLOCK);

       }
 
       /* Traverse the stack backwards until a state with a non empty interleave
       }
 
       /* Traverse the stack backwards until a state with a non empty interleave


@@ -246,12 +253,13 @@ static void MC_modelcheck_safety_main(void)
       }
     }
   }
       }
     }
   }

+

   XBT_INFO("No property violation found.");
   MC_print_statistics(mc_stats);
   XBT_INFO("No property violation found.");
   MC_print_statistics(mc_stats);

-  return;
+  exit(SIMGRID_EXIT_SUCCESS);

 }
 
 }
 

-void MC_modelcheck_safety(void)
+static void MC_modelcheck_safety_init(void)

 {
   if(_sg_mc_termination)
     mc_reduce_kind = e_mc_reduce_none;
 {
   if(_sg_mc_termination)
     mc_reduce_kind = e_mc_reduce_none;


@@ -276,11 +284,4 @@ void MC_modelcheck_safety(void)
   /* Save the initial state */
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = MC_take_snapshot(0);
   /* Save the initial state */
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = MC_take_snapshot(0);

-
-  MC_modelcheck_safety_main();
-
-  xbt_abort();
-  //MC_exit();
-}
-

 }
 }

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index 2c83424..ba80984 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -21,6 +21,7 @@
 #include "mc_private.h"
 #include "mc_ignore.h"
 #include "mcer_ignore.h"
 #include "mc_private.h"
 #include "mc_ignore.h"
 #include "mcer_ignore.h"

+#include "mc_exit.h"

 
 using simgrid::mc::remote;
 
 
 using simgrid::mc::remote;
 


@@ -238,7 +239,7 @@ bool s_mc_server::handle_events()
 
       case MC_MESSAGE_ASSERTION_FAILED:
         MC_report_assertion_error();
 
       case MC_MESSAGE_ASSERTION_FAILED:
         MC_report_assertion_error();

-        xbt_abort();
+        ::exit(SIMGRID_EXIT_SAFETY);

         break;
 
       default:
         break;
 
       default:

diff --git a/src/mc/mc_server.h b/src/mc/mc_server.h
index a6fc2f8..e1ed05d 100644 (file)
--- a/src/mc/mc_server.h
+++ b/src/mc/mc_server.h
@@ -18,10 +18,11 @@
 #include <xbt/misc.h>
  
 #include "mc_process.h"
 #include <xbt/misc.h>
  
 #include "mc_process.h"

+#include "mc_exit.h"

 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 

-#define MC_SERVER_ERROR 127
+#define MC_SERVER_ERROR SIMGRID_ERROR

 
 typedef struct s_mc_server s_mc_server_t, *mc_server_t;
 
 
 typedef struct s_mc_server s_mc_server_t, *mc_server_t;
 

diff --git a/teshsuite/mc/replay/random_bug.tesh b/teshsuite/mc/replay/random_bug.tesh
index 59e995b..c418e24 100644 (file)
--- a/teshsuite/mc/replay/random_bug.tesh
+++ b/teshsuite/mc/replay/random_bug.tesh
@@ -1,5 +1,5 @@
 #!/usr/bin/env tesh
 #!/usr/bin/env tesh

-!expect signal SIGABRT
+! expect return 1

 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random_bug ${srcdir:=.}/../../../examples/platforms/small_platform.xml ${srcdir:=.}/random_bug.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/record:1
 > [  0.000000] (0:@) Check a safety property
 > [  0.000000] (0:@) **************************
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random_bug ${srcdir:=.}/../../../examples/platforms/small_platform.xml ${srcdir:=.}/random_bug.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/record:1
 > [  0.000000] (0:@) Check a safety property
 > [  0.000000] (0:@) **************************