Do not use MC_process_clock_add() for now, as it makes the exploration infinitely...

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 49622dd..a1217a6 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -158,7 +158,8 @@ void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
       actor_transitions.emplace_back(deserialize_transition(actor.aid, times_considered, stream));
     }
 
-    XBT_DEBUG("Received %zu transitions for actor %ld", actor_transitions.size(), actor.aid);
+    XBT_DEBUG("Received %zu transitions for actor %ld. The first one is %s", actor_transitions.size(), actor.aid,
+              (actor_transitions.size() > 0 ? actor_transitions[0]->to_string().c_str() : "null"));
     whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered, std::move(actor_transitions));
   }
 }

diff --git a/src/s4u/s4u_Actor.cpp b/src/s4u/s4u_Actor.cpp
index 268576e..573d708 100644 (file)
--- a/src/s4u/s4u_Actor.cpp
+++ b/src/s4u/s4u_Actor.cpp
@@ -336,12 +336,12 @@ void sleep_for(double duration)
   kernel::actor::simcall_blocking(
       [issuer, duration]() {
         if (MC_is_active() || MC_record_replay_is_active()) {
-          MC_process_clock_add(issuer, duration);
+          // MC_process_clock_add(issuer, duration); // BUG: Makes the exploration loop
           issuer->simcall_answer();
-          return;
+        } else {
+          kernel::activity::ActivityImplPtr sync = issuer->sleep(duration);
+          sync->register_simcall(&issuer->simcall_);
         }
-        kernel::activity::ActivityImplPtr sync = issuer->sleep(duration);
-        sync->register_simcall(&issuer->simcall_);
       },
       &observer);
 

diff --git a/teshsuite/mc/mcmini/barber_shop_ok.c b/teshsuite/mc/mcmini/barber_shop_ok.c
index b44a934..b0f17ca 100644 (file)
--- a/teshsuite/mc/mcmini/barber_shop_ok.c
+++ b/teshsuite/mc/mcmini/barber_shop_ok.c
@@ -33,6 +33,7 @@ sem_t seatBelt;
 // Flag to stop the barber thread when all customers
 // have been serviced.
 int allDone = 0;
+int DEBUG   = 0;
 
 static void randwait(int secs)
 {
@@ -49,13 +50,16 @@ static void* customer(void* number)
 
   // Leave for the shop and take some random amount of
   // time to arrive.
-  printf("Customer %d leaving for barber shop.\n", num);
+  if (DEBUG)
+    printf("Customer %d leaving for barber shop.\n", num);
   randwait(5);
-  printf("Customer %d arrived at barber shop.\n", num);
+  if (DEBUG)
+    printf("Customer %d arrived at barber shop.\n", num);
 
   // Wait for space to open up in the waiting room...
   sem_wait(&waitingRoom);
-  printf("Customer %d entering waiting room.\n", num);
+  if (DEBUG)
+    printf("Customer %d entering waiting room.\n", num);
 
   // Wait for the barber chair to become free.
   sem_wait(&barberChair);
@@ -65,7 +69,8 @@ static void* customer(void* number)
   sem_post(&waitingRoom);
 
   // Wake up the barber...
-  printf("Customer %d waking the barber.\n", num);
+  if (DEBUG)
+    printf("Customer %d waking the barber.\n", num);
   sem_post(&barberPillow);
 
   // Wait for the barber to finish cutting your hair.
@@ -73,7 +78,8 @@ static void* customer(void* number)
 
   // Give up the chair.
   sem_post(&barberChair);
-  printf("Customer %d leaving barber shop.\n", num);
+  if (DEBUG)
+    printf("Customer %d leaving barber shop.\n", num);
   return NULL;
 }
 
@@ -85,7 +91,8 @@ static void* barber(void* junk)
   while (!allDone) {
 
     // Sleep until someone arrives and wakes you..
-    printf("The barber is sleeping\n");
+    if (DEBUG)
+      printf("The barber is sleeping\n");
     sem_wait(&barberPillow);
 
     // Skip this stuff at the end...
@@ -93,14 +100,17 @@ static void* barber(void* junk)
 
       // Take a random amount of time to cut the
       // customer's hair.
-      printf("The barber is cutting hair\n");
+      if (DEBUG)
+        printf("The barber is cutting hair\n");
       randwait(3);
-      printf("The barber has finished cutting hair.\n");
+      if (DEBUG)
+        printf("The barber has finished cutting hair.\n");
 
       // Release the customer when done cutting...
       sem_post(&seatBelt);
     } else {
-      printf("The barber is going home for the day.\n");
+      if (DEBUG)
+        printf("The barber is going home for the day.\n");
     }
   }
   return NULL;
@@ -116,8 +126,8 @@ int main(int argc, char* argv[])
 
   // Check to make sure there are the right number of
   // command line arguments.
-  if (argc != 4) {
-    printf("Use: SleepBarber <Num Customers> <Num Chairs> <rand seed>\n");
+  if (argc != 5) {
+    printf("Use: SleepBarber <Num Customers> <Num Chairs> <rand seed> <DEBUG>\n");
     exit(-1);
   }
 
@@ -126,6 +136,7 @@ int main(int argc, char* argv[])
   numCustomers = atoi(argv[1]);
   numChairs    = atoi(argv[2]);
   RandSeed     = atol(argv[3]);
+  DEBUG        = atoi(argv[4]);
 
   // Make sure the number of threads is less than the number of
   // customers we can support.

diff --git a/teshsuite/mc/mcmini/barber_shop_ok.tesh b/teshsuite/mc/mcmini/barber_shop_ok.tesh
index 1d8b039..c4b9d14 100644 (file)
--- a/teshsuite/mc/mcmini/barber_shop_ok.tesh
+++ b/teshsuite/mc/mcmini/barber_shop_ok.tesh
@@ -1,4 +1,11 @@
 # We ignore the LD_PRELOAD lines from the expected output because they contain the build path
 ! ignore .*LD_PRELOAD.*
 
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-barber_shop_ok 5 3 0
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-barber_shop_ok 3 2 0 0
+> sthread is intercepting the execution of /home/mquinson/Code/simgrid/build/default/teshsuite/mc/mcmini/mcmini-barber_shop_ok
+> 
+> SleepBarber.c
+> 
+> A solution to the sleeping barber problem using semaphores.
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 5169 unique states visited; 959 backtracks (21531 transition replays, 27659 states visited overall)