From bdd17c447432a0a638682a1e301b990e401fa5f1 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Thu, 2 Nov 2023 02:53:03 +0100 Subject: [PATCH] Do not use MC_process_clock_add() for now, as it makes the exploration infinitely looping --- src/mc/api/RemoteApp.cpp | 3 ++- src/s4u/s4u_Actor.cpp | 8 +++--- teshsuite/mc/mcmini/barber_shop_ok.c | 33 ++++++++++++++++--------- teshsuite/mc/mcmini/barber_shop_ok.tesh | 9 ++++++- 4 files changed, 36 insertions(+), 17 deletions(-) diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index 49622dd275..a1217a6752 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -158,7 +158,8 @@ void RemoteApp::get_actors_status(std::map& 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 268576eba3..573d708555 100644 --- 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 b44a934f1b..b0f17ca859 100644 --- 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 \n"); + if (argc != 5) { + printf("Use: SleepBarber \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 1d8b039d18..c4b9d14e91 100644 --- 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) -- 2.20.1