model-checker : really (?) fix SIMCALL_MUTEX_LOCK and UNLOCK with MC

diff --git a/buildtools/Cmake/AddTests.cmake b/buildtools/Cmake/AddTests.cmake
index 45c74e5..103b33e 100644 (file)
--- a/buildtools/Cmake/AddTests.cmake
+++ b/buildtools/Cmake/AddTests.cmake
@@ -487,8 +487,7 @@ IF(NOT enable_memcheck)
       ADD_TESH(smpi-replay                       --setenv srcdir=${CMAKE_HOME_DIRECTORY}/examples/smpi --cd ${CMAKE_BINARY_DIR}/examples/smpi ${CMAKE_HOME_DIRECTORY}/examples/smpi/replay/smpi_replay.tesh)
     ENDIF()
     IF(HAVE_MC)
-      ADD_TESH(smpi-mc-non-determinism                  --setenv srcdir=${CMAKE_HOME_DIRECTORY}/examples/smpi/mc --cd ${CMAKE_BINARY_DIR}/examples/smpi/mc ${CMAKE_HOME_DIRECTORY}/examples/smpi/mc/non_deterministic.tesh)
-      ADD_TESH(smpi-mc-send-determinism                  --setenv srcdir=${CMAKE_HOME_DIRECTORY}/examples/smpi/mc --cd ${CMAKE_BINARY_DIR}/examples/smpi/mc ${CMAKE_HOME_DIRECTORY}/examples/smpi/mc/send_deterministic.tesh)
+      ADD_TESH(smpi-mc-only-send-determinism                  --setenv srcdir=${CMAKE_HOME_DIRECTORY}/examples/smpi/mc --cd ${CMAKE_BINARY_DIR}/examples/smpi/mc ${CMAKE_HOME_DIRECTORY}/examples/smpi/mc/only_send_deterministic.tesh)
     ENDIF()
     # END TESH TESTS
   ENDIF()

diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt
index 191d4e7..2119015 100644 (file)
--- a/examples/smpi/CMakeLists.txt
+++ b/examples/smpi/CMakeLists.txt
@@ -29,8 +29,7 @@ if(enable_smpi)
     add_executable(smpi_bugged1 mc/bugged1.c)
     add_executable(smpi_bugged2 mc/bugged2.c)
     add_executable(smpi_bugged1_liveness mc/bugged1_liveness.c)
-    add_executable(smpi_send_deterministic mc/send_deterministic.c)
-    add_executable(smpi_non_deterministic mc/non_deterministic.c)
+    add_executable(smpi_only_send_deterministic mc/only_send_deterministic.c)
     add_executable(smpi_mutual_exclusion mc/mutual_exclusion.c)
     add_executable(smpi_non_termination1 mc/non_termination1.c)
     add_executable(smpi_non_termination2 mc/non_termination2.c)
@@ -40,8 +39,7 @@ if(enable_smpi)
     target_link_libraries(smpi_bugged1 simgrid)
     target_link_libraries(smpi_bugged2 simgrid)
     target_link_libraries(smpi_bugged1_liveness simgrid)
-    target_link_libraries(smpi_send_deterministic simgrid)
-    target_link_libraries(smpi_non_deterministic simgrid)
+    target_link_libraries(smpi_only_send_deterministic simgrid)
     target_link_libraries(smpi_mutual_exclusion simgrid)
     target_link_libraries(smpi_non_termination1 simgrid)
     target_link_libraries(smpi_non_termination2 simgrid)
@@ -51,8 +49,7 @@ if(enable_smpi)
     set_target_properties(smpi_bugged1 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     set_target_properties(smpi_bugged2 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     set_target_properties(smpi_bugged1_liveness PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
-    set_target_properties(smpi_send_deterministic PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
-    set_target_properties(smpi_non_deterministic PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
+    set_target_properties(smpi_only_send_deterministic PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     set_target_properties(smpi_mutual_exclusion PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     set_target_properties(smpi_non_termination1 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
     set_target_properties(smpi_non_termination2 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc")
@@ -83,8 +80,7 @@ set(examples_src
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged2.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1_liveness.c
-  ${CMAKE_CURRENT_SOURCE_DIR}/mc/send_deterministic.c
-  ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_deterministic.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/only_send_deterministic.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/mutual_exclusion.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination1.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination2.c
@@ -99,8 +95,7 @@ set(bin_files
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1_liveness
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged2
-  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_send_deterministic
-  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_deterministic
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_only_send_deterministic
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_mutual_exclusion
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_termination
   PARENT_SCOPE

diff --git a/examples/smpi/mc/hostfile_non_deterministic b/examples/smpi/mc/hostfile_only_send_deterministic
similarity index 100%
rename from examples/smpi/mc/hostfile_non_deterministic
rename to examples/smpi/mc/hostfile_only_send_deterministic

diff --git a/examples/smpi/mc/hostfile_send_deterministic b/examples/smpi/mc/hostfile_send_deterministic
deleted file mode 100644 (file)
index 4ae7dab..0000000
--- a/examples/smpi/mc/hostfile_send_deterministic
+++ /dev/null
@@ -1,3 +0,0 @@
-node-1.acme.org
-node-2.acme.org
-node-3.acme.org

diff --git a/examples/smpi/mc/non_deterministic.c b/examples/smpi/mc/non_deterministic.c
deleted file mode 100644 (file)
index 9df64c0..0000000
--- a/examples/smpi/mc/non_deterministic.c
+++ /dev/null
@@ -1,54 +0,0 @@
-/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=model-check:1 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */
-
-/* Copyright (c) 2009-2014. The SimGrid Team.
- * All rights reserved.                                                     */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <stdio.h>
-#include <mpi.h>
-#include <simgrid/modelchecker.h>
-
-
-int main(int argc, char **argv)
-{
-  int recv_buff, err, size, rank, i;
-  MPI_Status status;
-
-  /* Initialize MPI */
-  err = MPI_Init(&argc, &argv);
-  if (err != MPI_SUCCESS) {
-    printf("MPI initialization failed!\n");
-    exit(1);
-  }
-
-  MPI_Comm_size(MPI_COMM_WORLD, &size);   /* Get nr of tasks */
-  MPI_Comm_rank(MPI_COMM_WORLD, &rank);   /* Get id of this process */
-  if (size < 2) {
-    printf("run this program with at least 2 processes \n");
-    MPI_Finalize();
-    exit(0);
-  }
-
-  if (rank == 0) {
-    //printf("MPI_ISend / MPI_IRecv Test \n");
-
-    for(i=0; i < size - 1; i++){
-      MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
-      //printf("Message received from %d\n", recv_buff);
-      MPI_Send(&recv_buff, 1, MPI_INT, status.MPI_SOURCE, 42, MPI_COMM_WORLD);
-      // printf("Sent %d to rank %d\n", status.MPI_SOURCE);
-    }
-
-  }else{
-    MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD);
-    //printf("Sent %d to rank 0\n", rank);
-    MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
-    //printf("Message received from %d\n", recv_buff);
-  }
-
-  MPI_Finalize();
-
-  return 0;
-}

diff --git a/examples/smpi/mc/non_deterministic.tesh b/examples/smpi/mc/non_deterministic.tesh
deleted file mode 100644 (file)
index d32f46a..0000000
--- a/examples/smpi/mc/non_deterministic.tesh
+++ /dev/null
@@ -1,47 +0,0 @@
-#! ./tesh
-
-! timeout 60
-$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_non_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_non_deterministic
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'surf/precision' to '1e-9'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/TCP_gamma' to '4194304'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check' to '1'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/communications_determinism' to '1'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/send_is_detached_thres' to '0'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/running_power' to '1e9'
-> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
-> [0.000000] [mc_global/INFO] Check communication determinism
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
-> [0.000000] [mc_comm_determinism/INFO] The communications pattern of the process 1 is different! (Different communication : 1)
-> [0.000000] [mc_comm_determinism/INFO] ****************************************************
-> [0.000000] [mc_comm_determinism/INFO] ***** Non-deterministic communications pattern *****
-> [0.000000] [mc_comm_determinism/INFO] ****************************************************
-> [0.000000] [mc_comm_determinism/INFO] ** Initial communications pattern (per process): **
-> [0.000000] [mc_comm_determinism/INFO] Communications from the process 1:
-> [0.000000] [mc_comm_determinism/INFO] [(1) node-1.acme.org <- (2) node-2.acme.org] iRecv 
-> [0.000000] [mc_comm_determinism/INFO] [(1) node-1.acme.org -> (2) node-2.acme.org] iSend 
-> [0.000000] [mc_comm_determinism/INFO] [(1) node-1.acme.org <- (3) node-3.acme.org] iRecv 
-> [0.000000] [mc_comm_determinism/INFO] [(1) node-1.acme.org -> (3) node-3.acme.org] iSend 
-> [0.000000] [mc_comm_determinism/INFO] Communications from the process 2:
-> [0.000000] [mc_comm_determinism/INFO] [(2) node-2.acme.org -> (1) node-1.acme.org] iSend 
-> [0.000000] [mc_comm_determinism/INFO] [(2) node-2.acme.org <- (1) node-1.acme.org] iRecv 
-> [0.000000] [mc_comm_determinism/INFO] Communications from the process 3:
-> [0.000000] [mc_comm_determinism/INFO] [(3) node-3.acme.org -> (1) node-1.acme.org] iSend 
-> [0.000000] [mc_comm_determinism/INFO] [(3) node-3.acme.org <- (1) node-1.acme.org] iRecv 
-> [0.000000] [mc_comm_determinism/INFO] ** Communications pattern counter-example (per process): **
-> [0.000000] [mc_comm_determinism/INFO] Communications from the process 1:
-> [0.000000] [mc_comm_determinism/INFO] [(1) node-1.acme.org <- (3) node-3.acme.org] iRecv 
-> [0.000000] [mc_comm_determinism/INFO] [(1) node-1.acme.org -> (3) node-3.acme.org] iSend 
-> [0.000000] [mc_comm_determinism/INFO] [(1) node-1.acme.org <- (2) node-2.acme.org] iRecv 
-> [0.000000] [mc_comm_determinism/INFO] [(1) node-1.acme.org -> (2) node-2.acme.org] iSend 
-> [0.000000] [mc_comm_determinism/INFO] Communications from the process 2:
-> [0.000000] [mc_comm_determinism/INFO] [(2) node-2.acme.org -> (1) node-1.acme.org] iSend 
-> [0.000000] [mc_comm_determinism/INFO] [(2) node-2.acme.org <- (1) node-1.acme.org] iRecv 
-> [0.000000] [mc_comm_determinism/INFO] Communications from the process 3:
-> [0.000000] [mc_comm_determinism/INFO] [(3) node-3.acme.org -> (1) node-1.acme.org] iSend 
-> [0.000000] [mc_comm_determinism/INFO] [(3) node-3.acme.org <- (1) node-1.acme.org] iRecv 
-> [0.000000] [mc_global/INFO] Expanded states = 16037
-> [0.000000] [mc_global/INFO] Visited states = 80801
-> [0.000000] [mc_global/INFO] Executed transitions = 76048
-> [0.000000] [mc_global/INFO] Communication-deterministic : No

diff --git a/examples/smpi/mc/send_deterministic.c b/examples/smpi/mc/only_send_deterministic.c
similarity index 100%
rename from examples/smpi/mc/send_deterministic.c
rename to examples/smpi/mc/only_send_deterministic.c

diff --git a/examples/smpi/mc/send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh
similarity index 53%
rename from examples/smpi/mc/send_deterministic.tesh
rename to examples/smpi/mc/only_send_deterministic.tesh
index 6bafa97..1174e5c 100644 (file)
--- a/examples/smpi/mc/send_deterministic.tesh
+++ b/examples/smpi/mc/only_send_deterministic.tesh
@@ -1,19 +1,26 @@
 #! ./tesh
 
 ! timeout 60
-$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_send_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/send_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_send_deterministic
+$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_only_send_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'surf/precision' to '1e-9'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/TCP_gamma' to '4194304'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check' to '1'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/send_determinism' to '1'
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/communications_determinism' to '1'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/send_is_detached_thres' to '0'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/running_power' to '1e9'
 > [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
 > [0.000000] [mc_global/INFO] Check communication determinism
 > [0.000000] [mc_global/INFO] Get debug information ...
 > [0.000000] [mc_global/INFO] Get debug information done !
-> [0.000000] [mc_global/INFO] Expanded states = 520
-> [0.000000] [mc_global/INFO] Visited states = 1476
-> [0.000000] [mc_global/INFO] Executed transitions = 1312
+> [0.000000] [mc_global/INFO] ******************************************************
+> [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern ****
+> [0.000000] [mc_global/INFO] ******************************************************
+> [0.000000] [mc_global/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2
+> [0.000000] [mc_global/INFO] Expanded states = 2966
+> [0.000000] [mc_global/INFO] Visited states = 13362
+> [0.000000] [mc_global/INFO] Executed transitions = 12576
 > [0.000000] [mc_global/INFO] Send-deterministic : Yes
+> [0.000000] [mc_global/INFO] Recv-deterministic : No
+
+

diff --git a/src/mc/mc_base.c b/src/mc/mc_base.c
index 69e7e02..31dac0c 100644 (file)
--- a/src/mc/mc_base.c
+++ b/src/mc/mc_base.c
@@ -35,10 +35,10 @@ int MC_request_is_enabled(smx_simcall_t req)
 {
   unsigned int index = 0;
   smx_synchro_t act = 0;
+  smx_mutex_t mutex = NULL;
 
   switch (req->call) {
   case SIMCALL_NONE:
-  case SIMCALL_MUTEX_LOCK: /* If MUTEX_LOCK is catched by the MC, it means that the mutex is locked by another process, thus the request shouldn't be enabled (loop until another process is executed) */ 
     return FALSE;
 
   case SIMCALL_COMM_WAIT:
@@ -64,6 +64,13 @@ int MC_request_is_enabled(smx_simcall_t req)
         return TRUE;
     return FALSE;
 
+  case SIMCALL_MUTEX_LOCK:
+    mutex = simcall_mutex_lock__get__mutex(req);
+    if(mutex->owner == NULL)
+      return TRUE;
+    else
+      return (mutex->owner->pid == req->issuer->pid);
+
   default:
     /* The rest of the requests are always enabled */
     return TRUE;
@@ -79,6 +86,8 @@ int MC_request_is_visible(smx_simcall_t req)
       || req->call == SIMCALL_COMM_TEST
       || req->call == SIMCALL_COMM_TESTANY
       || req->call == SIMCALL_MC_RANDOM
+      || req->call == SIMCALL_MUTEX_LOCK
+      || req->call == SIMCALL_MUTEX_UNLOCK
 #ifdef HAVE_MC
       || req->call == SIMCALL_MC_SNAPSHOT
       || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index b700c10..790d1e9 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -395,6 +395,7 @@ void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int valu
         current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t);
       complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking);
     }
+    break;
   default:
     xbt_die("Unexpected call type %i", (int)call_type);
   }

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index af7f1ef..ce77485 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -231,6 +231,7 @@ char *MC_request_to_string(smx_simcall_t req, int value)
 {
   char *type = NULL, *args = NULL, *str = NULL, *p = NULL, *bs = NULL;
   smx_synchro_t act = NULL;
+  smx_mutex_t mutex = NULL;
   size_t size = 0;
 
   switch (req->call) {
@@ -328,6 +329,18 @@ char *MC_request_to_string(smx_simcall_t req, int value)
     }
     break;
 
+  case SIMCALL_MUTEX_LOCK:
+    mutex = simcall_mutex_lock__get__mutex(req);
+    type = xbt_strdup("Mutex LOCK");
+    args = bprintf("locked = %d, owner = %d, sleeping = %d", mutex->locked, mutex->owner != NULL ? (int)mutex->owner->pid : -1, xbt_swag_size(mutex->sleeping));
+    break;
+
+  case SIMCALL_MUTEX_UNLOCK:
+    type = xbt_strdup("Mutex UNLOCK");
+    mutex = simcall_mutex_unlock__get__mutex(req);
+    args = bprintf("locked = %d, owner = %lu, sleeping = %d", mutex->locked, mutex->owner->pid, xbt_swag_size(mutex->sleeping));
+    break;
+
   case SIMCALL_MC_SNAPSHOT:
     type = xbt_strdup("MC_SNAPSHOT");
     args = NULL;