From: Martin Quinson Date: Thu, 2 Nov 2023 21:39:19 +0000 (+0100) Subject: Add more tests from McMini X-Git-Tag: v3.35~89^2~22^2~3 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e40065bf1c41a83ae34b6e192abc77f970143006 Add more tests from McMini --- diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index deda1d9559..67fe6ab6ec 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -56,11 +56,11 @@ endif() if("${CMAKE_SYSTEM}" MATCHES "Linux") foreach(x -# barber_shop_deadlock producer_consumer_deadlock +# # simple_cond_broadcast_deadlock simple_semaphore_deadlock simple_barrier_deadlock simple_cond_deadlock # simple_semaphores_deadlock -# philosophers_mutex_deadlock -# philosophers_semaphores_deadlock +# +# # philosophers_spurious_deadlock # simple_barrier_with_threads_deadlock # simple_semaphores_with_threads_deadlock @@ -68,9 +68,16 @@ if("${CMAKE_SYSTEM}" MATCHES "Linux") # simple_mutex_deadlock # simple_mutex_with_threads_deadlock - barber_shop_ok -# philosophers_mutex_ok philosophers_semaphores_ok -# producer_consumer_ok producer_consumer_spurious_nok + barber_shop_ok barber_shop_deadlock + philosophers_semaphores_ok philosophers_semaphores_deadlock + philosophers_mutex_ok philosophers_mutex_deadlock + producer_consumer_ok producer_consumer_deadlock + + + # producer_consumer_spurious_nok # infinite no-op loop + +# +# # simple_barrier_ok simple_barrier_with_threads_ok simple_cond_broadcast_ok # simple_cond_broadcast_with_semaphore_ok simple_cond_ok simple_mutex_ok # simple_mutex_with_threads_ok simple_semaphores_ok simple_semaphores_with_threads_ok simple_threads_ok diff --git a/teshsuite/mc/mcmini/barber_shop_deadlock.c b/teshsuite/mc/mcmini/barber_shop_deadlock.c new file mode 100644 index 0000000000..c10c970bd5 --- /dev/null +++ b/teshsuite/mc/mcmini/barber_shop_deadlock.c @@ -0,0 +1,107 @@ +#define _REENTRANT + +#include +#include +#include +#include +#include + +// The maximum number of customer threads. +#define MAX_CUSTOMERS 10 + +// Define the semaphores. +sem_t waitingRoom; +sem_t barberChair; +sem_t barberPillow; +sem_t seatBelt; + +// Flag to stop the barber thread when all customers have been serviced. +int allDone = 0; +int DEBUG = 0; + +static void *customer(void *number) { + int num = *(int *)number; + + if(DEBUG) printf("Customer %d leaving for barber shop.\n", num); + if(DEBUG) printf("Customer %d arrived at barber shop.\n", num); + + sem_wait(&waitingRoom); + + if(DEBUG) printf("Customer %d entering waiting room.\n", num); + + sem_wait(&barberChair); + + if(DEBUG) printf("Customer %d waking the barber.\n", num); + sem_post(&barberPillow); + + sem_wait(&seatBelt); + + sem_post(&barberChair); + if(DEBUG) printf("Customer %d leaving barber shop.\n", num); + return NULL; +} + +static void *barber(void *junk) { + while (!allDone) { + if(DEBUG) printf("The barber is sleeping\n"); + sem_wait(&barberPillow); + + if (!allDone) { + if(DEBUG) printf("The barber is cutting hair\n"); + if(DEBUG) printf("The barber has finished cutting hair.\n"); + sem_post(&seatBelt); + } + else { + if(DEBUG) printf("The barber is going home for the day.\n"); + } + } + return NULL; +} + +int main(int argc, char *argv[]) { + if(argc != 5){ + printf("Usage: %s numCustomers numChairs RandSeed DEBUG\n", argv[0]); + return 1; + } + + pthread_t btid; + pthread_t tid[MAX_CUSTOMERS]; + int i, numCustomers, numChairs; + long RandSeed; + int Number[MAX_CUSTOMERS]; + + numCustomers = atoi(argv[1]); + numChairs = atoi(argv[2]); + RandSeed = atol(argv[3]); + DEBUG = atoi(argv[4]); + + if (numCustomers > MAX_CUSTOMERS) { + printf("The maximum number of Customers is %d.\n", MAX_CUSTOMERS); + exit(-1); + } + + srand48(RandSeed); + + for (i=0; i [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 4 actors are still running, waiting for something. +> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor (@): " +> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:6) +> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall SEM_WAIT(sem_id:2 not granted) +> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted) +> [0.000000] [ker_engine/INFO] Actor 7 (thread 6@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 1, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_UNLOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 3, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 3, no timeout) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 1, granted: yes) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_UNLOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 3, granted: yes) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 4, no timeout) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 1, granted: yes) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_UNLOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 3, granted: yes) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 5, no timeout) +> [0.000000] [mc_global/INFO] Actor 6 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 7 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;3;3;3;3;3;2;2;2;3;3;3;1;4;4;4;4;4;2;2;2;4;4;4;1;5;5;5;5;5;2;2;2;5;5;5;1;6;7' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 40 unique states visited; 0 backtracks (0 transition replays, 40 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/philosophers_mutex_deadlock.c b/teshsuite/mc/mcmini/philosophers_mutex_deadlock.c new file mode 100644 index 0000000000..4497df76cd --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_mutex_deadlock.c @@ -0,0 +1,59 @@ +// Naive dining philosophers solution, which leads to deadlock. + +#include +#include +#include +#include + +int DEBUG = 0; + +struct forks { + int philosopher; + pthread_mutex_t *left_fork; + pthread_mutex_t *right_fork; +} *forks; + +static void * philosopher_doit(void *forks_arg) { + struct forks *forks = forks_arg; + pthread_mutex_lock(forks->left_fork); + pthread_mutex_lock(forks->right_fork); + + if(DEBUG) printf("Philosopher %d just ate.\n", forks->philosopher); + + pthread_mutex_unlock(forks->left_fork); + pthread_mutex_unlock(forks->right_fork); + return NULL; +} + +int main(int argc, char* argv[]) { + if(argc != 3){ + printf("Usage: %s NUM_PHILOSOPHERS DEBUG\n", argv[0]); + return 1; + } + + int NUM_THREADS = atoi(argv[1]); + DEBUG = atoi(argv[2]); + + pthread_t thread[NUM_THREADS]; + pthread_mutex_t mutex_resource[NUM_THREADS]; + + forks = malloc(NUM_THREADS * sizeof(struct forks)); + + int i; + for (i = 0; i < NUM_THREADS; i++) { + pthread_mutex_init(&mutex_resource[i], NULL); + forks[i] = (struct forks){i, + &mutex_resource[i], &mutex_resource[(i+1) % NUM_THREADS]}; + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]); + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_join(thread[i], NULL); + } + + free(forks); + return 0; +} diff --git a/teshsuite/mc/mcmini/philosophers_mutex_deadlock.tesh b/teshsuite/mc/mcmini/philosophers_mutex_deadlock.tesh new file mode 100644 index 0000000000..6d31afa740 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_mutex_deadlock.tesh @@ -0,0 +1,35 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +! expect return 3 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_mutex_deadlock 5 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 6 actors are still running, waiting for something. +> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor (@): " +> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2) +> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3) +> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:2 owner:4) +> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:3 owner:5) +> [0.000000] [ker_engine/INFO] Actor 5 (thread 4@Lilibeth) simcall MUTEX_WAIT(mutex_id:4 owner:6) +> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_WAIT(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 3, owner: 5) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 3, owner: 5) +> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_WAIT(mutex: 3, owner: 5) +> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 4, owner: 6) +> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 4, owner: 6) +> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_WAIT(mutex: 4, owner: 6) +> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;4;3;4;5;4;5;6;5;6;6' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1298 unique states visited; 199 backtracks (3432 transition replays, 4929 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/philosophers_mutex_ok.c b/teshsuite/mc/mcmini/philosophers_mutex_ok.c new file mode 100644 index 0000000000..8c30821b31 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_mutex_ok.c @@ -0,0 +1,65 @@ +#include +#include +#include +#include + +int DEBUG = 0; + +struct forks { + int philosopher; + pthread_mutex_t *left_fork; + pthread_mutex_t *right_fork; + pthread_mutex_t *dining_fork; +}; + +static void * philosopher_doit(void *forks_arg) { + struct forks *forks = forks_arg; + pthread_mutex_lock(forks->dining_fork); + pthread_mutex_lock(forks->left_fork); + pthread_mutex_lock(forks->right_fork); + pthread_mutex_unlock(forks->dining_fork); + + if(DEBUG) + printf("Philosopher %d is eating.\n", forks->philosopher); + + pthread_mutex_unlock(forks->left_fork); + pthread_mutex_unlock(forks->right_fork); + return NULL; +} + +int main(int argc, char* argv[]) +{ + if(argc != 3){ + printf("Usage: %s NUM_THREADS DEBUG\n", argv[0]); + return 1; + } + + int NUM_THREADS = atoi(argv[1]); + DEBUG = atoi(argv[2]); + + pthread_t thread[NUM_THREADS]; + pthread_mutex_t mutex_resource[NUM_THREADS]; + struct forks forks[NUM_THREADS]; + + pthread_mutex_t dining_fork; + pthread_mutex_init(&dining_fork, NULL); + + int i; + for (i = 0; i < NUM_THREADS; i++) { + pthread_mutex_init(&mutex_resource[i], NULL); + forks[i] = (struct forks){i, + &mutex_resource[i], + &mutex_resource[(i+1) % NUM_THREADS], + &dining_fork}; + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]); + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_join(thread[i], NULL); + } + + return 0; +} diff --git a/teshsuite/mc/mcmini/philosophers_mutex_ok.tesh b/teshsuite/mc/mcmini/philosophers_mutex_ok.tesh new file mode 100644 index 0000000000..d90ff92995 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_mutex_ok.tesh @@ -0,0 +1,6 @@ +# 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-philosophers_mutex_ok 5 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 14170 unique states visited; 2087 backtracks (45202 transition replays, 61459 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.c b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.c new file mode 100644 index 0000000000..92e58b1b59 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.c @@ -0,0 +1,67 @@ +// Dining philosophers solution with semaphores + +#include +#include +#include +#include +#include + +struct forks { + int philosopher; + pthread_mutex_t *left_fork; + pthread_mutex_t *right_fork; + sem_t* sem_dining; + int DEBUG; +} *forks; + +static void * philosopher_doit(void *forks_arg) { + struct forks *forks = forks_arg; + sem_wait(forks->sem_dining); + pthread_mutex_lock(forks->left_fork); + pthread_mutex_lock(forks->right_fork); + + if(forks->DEBUG) printf("Philosopher %d just ate.\n", forks->philosopher); + + pthread_mutex_unlock(forks->left_fork); + pthread_mutex_unlock(forks->right_fork); + sem_post(forks->sem_dining); + return NULL; +} + +int main(int argc, char* argv[]) { + if(argc != 3){ + printf("Usage: %s NUM_PHILOSOPHERS DEBUG\n", argv[0]); + return 1; + } + + int NUM_THREADS = atoi(argv[1]); + int DEBUG = atoi(argv[2]); + + pthread_t thread[NUM_THREADS]; + pthread_mutex_t mutex_resource[NUM_THREADS]; + sem_t sem_dining; + sem_init(&sem_dining, 0, NUM_THREADS); + + forks = malloc(NUM_THREADS * sizeof(struct forks)); + + int i; + for (i = 0; i < NUM_THREADS; i++) { + pthread_mutex_init(&mutex_resource[i], NULL); + forks[i] = (struct forks){i, + &mutex_resource[i], + &mutex_resource[(i+1) % NUM_THREADS], + &sem_dining, + DEBUG}; + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]); + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_join(thread[i], NULL); + } + + free(forks); + return 0; +} diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh new file mode 100644 index 0000000000..66020c9203 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh @@ -0,0 +1,33 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +! expect return 3 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_semaphores_deadlock 3 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 4 actors are still running, waiting for something. +> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor (@): " +> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2) +> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3) +> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:2 owner:4) +> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_WAIT(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;2;2;3;3;3;2;3;4;4;4;3;4;4' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 890 unique states visited; 90 backtracks (1415 transition replays, 2395 states visited overall) diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_ok.c b/teshsuite/mc/mcmini/philosophers_semaphores_ok.c new file mode 100644 index 0000000000..b11e49ffec --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_semaphores_ok.c @@ -0,0 +1,66 @@ +#include +#include +#include +#include +#include + +int DEBUG = 0; + +struct forks { + int philosopher; + pthread_mutex_t *left_fork; + pthread_mutex_t *right_fork; + sem_t* sem_dining; +}; + +static void * philosopher_doit(void *forks_arg) { + struct forks *forks = forks_arg; + sem_wait(forks->sem_dining); + pthread_mutex_lock(forks->left_fork); + pthread_mutex_lock(forks->right_fork); + + if(DEBUG) + printf("Philosopher %d is eating.\n", forks->philosopher); + + pthread_mutex_unlock(forks->left_fork); + pthread_mutex_unlock(forks->right_fork); + sem_post(forks->sem_dining); + return NULL; +} + +int main(int argc, char* argv[]) +{ + if(argc != 3){ + printf("Usage: %s NUM_THREADS DEBUG\n", argv[0]); + return 1; + } + + int NUM_THREADS = atoi(argv[1]); + DEBUG = atoi(argv[2]); + + pthread_t thread[NUM_THREADS]; + pthread_mutex_t mutex_resource[NUM_THREADS]; + struct forks forks[NUM_THREADS]; + + sem_t sem_dining; + sem_init(&sem_dining, 0, NUM_THREADS - 1); + + int i; + for (i = 0; i < NUM_THREADS; i++) { + pthread_mutex_init(&mutex_resource[i], NULL); + forks[i] = (struct forks){i, + &mutex_resource[i], + &mutex_resource[(i+1) % NUM_THREADS], + &sem_dining}; + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]); + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_join(thread[i], NULL); + } + + return 0; +} diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh b/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh new file mode 100644 index 0000000000..1b4113e1e1 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh @@ -0,0 +1,6 @@ +# 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-philosophers_semaphores_ok 3 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 2268 unique states visited; 233 backtracks (3314 transition replays, 5815 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/producer_consumer_deadlock.c b/teshsuite/mc/mcmini/producer_consumer_deadlock.c new file mode 100644 index 0000000000..2cf1ee6a2a --- /dev/null +++ b/teshsuite/mc/mcmini/producer_consumer_deadlock.c @@ -0,0 +1,83 @@ +#include +#include +#include +#include + +int MaxItems; // Maximum items a producer can produce or a consumer can consume +int BufferSize; // Size of the buffer + +sem_t empty; +sem_t full; +int in = 0; +int out = 0; +int *buffer; +pthread_mutex_t mutex; + +int DEBUG = 0; // Debug flag + +static void *producer(void *pno) +{ + int item; + for(int i = 0; i < MaxItems; i++) { + item = rand(); // Produce a random item + pthread_mutex_lock(&mutex); + sem_wait(&empty); + buffer[in] = item; + if(DEBUG) printf("Producer %d: Insert Item %d at %d\n", *((int *)pno),buffer[in],in); + in = (in+1)%BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&full); + } + return NULL; +} + +static void *consumer(void *cno) +{ + for(int i = 0; i < MaxItems; i++) { + pthread_mutex_lock(&mutex); + sem_wait(&full); + int item = buffer[out]; + if(DEBUG) printf("Consumer %d: Remove Item %d from %d\n",*((int *)cno),item, out); + out = (out+1)%BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&empty); + } + return NULL; +} + +int main(int argc, char* argv[]) { + if(argc != 4){ + printf("Usage: %s MAX_ITEMS BUFFER_SIZE DEBUG\n", argv[0]); + return 1; + } + + MaxItems = atoi(argv[1]); + BufferSize = atoi(argv[2]); + DEBUG = atoi(argv[3]); + + buffer = (int*) malloc(BufferSize * sizeof(int)); + + pthread_t pro[5],con[5]; + pthread_mutex_init(&mutex, NULL); + sem_init(&empty,0,BufferSize); + sem_init(&full,0,0); + + int a[5] = {1,2,3,4,5}; //Just used for numbering the producer and consumer + + for(int i = 0; i < 5; i++) { + pthread_create(&pro[i], NULL, producer, (void *)&a[i]); + } + for(int i = 0; i < 5; i++) { + pthread_create(&con[i], NULL, consumer, (void *)&a[i]); + } + + for(int i = 0; i < 5; i++) { + pthread_join(pro[i], NULL); + } + for(int i = 0; i < 5; i++) { + pthread_join(con[i], NULL); + } + + free(buffer); + return 0; +} diff --git a/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh b/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh new file mode 100644 index 0000000000..06b4b2832a --- /dev/null +++ b/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh @@ -0,0 +1,55 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +! expect return 3 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-producer_consumer_deadlock 5 3 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 11 actors are still running, waiting for something. +> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor (@): " +> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2) +> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted) +> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 5 (thread 4@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 7 (thread 6@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 8 (thread 7@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 9 (thread 8@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 10 (thread 9@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 11 (thread 10@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 7 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 8 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 9 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 10 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 11 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;3;4;5;6;7;8;9;10;11' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 31 unique states visited; 0 backtracks (0 transition replays, 31 states visited overall) diff --git a/teshsuite/mc/mcmini/producer_consumer_ok.c b/teshsuite/mc/mcmini/producer_consumer_ok.c new file mode 100644 index 0000000000..9fc1583dd4 --- /dev/null +++ b/teshsuite/mc/mcmini/producer_consumer_ok.c @@ -0,0 +1,93 @@ +#include +#include +#include +#include +#include + +#define MaxBufferSize 5 + +sem_t empty; +sem_t full; +int in = 0; +int out = 0; +int buffer[MaxBufferSize]; +pthread_mutex_t mutex; +int BufferSize; +int ItemCount; +int DEBUG; + +static void *producer(void *pno) +{ + int item; + for(int i = 0; i < ItemCount; i++) { + item = rand(); // Produce an random item + sem_wait(&empty); + pthread_mutex_lock(&mutex); + buffer[in] = item; + if (DEBUG) { + printf("Producer %d: Insert Item %d at %d\n", + *((int *)pno),buffer[in],in); + } + in = (in+1)%BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&full); + } + return NULL; +} + +static void *consumer(void *cno) +{ + for(int i = 0; i < ItemCount; i++) { + sem_wait(&full); + pthread_mutex_lock(&mutex); + int item = buffer[out]; + if (DEBUG) { + printf("Consumer %d: Remove Item %d from %d\n", + *((int *)cno),item, out); + } + out = (out+1)%BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&empty); + } + return NULL; +} + +int main(int argc, char* argv[]) +{ + if (argc < 6) { + printf("Usage: %s \n", argv[0]); + return 1; + } + + int NUM_PRODUCERS = atoi(argv[1]); + int NUM_CONSUMERS = atoi(argv[2]); + ItemCount = atoi(argv[3]); + BufferSize = atoi(argv[4]); + DEBUG = atoi(argv[5]); + + pthread_t pro[NUM_PRODUCERS],con[NUM_CONSUMERS]; + + pthread_mutex_init(&mutex, NULL); + sem_init(&empty,0,BufferSize); + sem_init(&full,0,0); + + int a[NUM_PRODUCERS > NUM_CONSUMERS ? NUM_PRODUCERS : NUM_CONSUMERS]; + + for(int i = 0; i < NUM_PRODUCERS; i++) { + a[i] = i+1; + pthread_create(&pro[i], NULL, producer, (void *)&a[i]); + } + for(int i = 0; i < NUM_CONSUMERS; i++) { + a[i] = i+1; + pthread_create(&con[i], NULL, consumer, (void *)&a[i]); + } + + for(int i = 0; i < NUM_PRODUCERS; i++) { + pthread_join(pro[i], NULL); + } + for(int i = 0; i < NUM_CONSUMERS; i++) { + pthread_join(con[i], NULL); + } + + return 0; +} diff --git a/teshsuite/mc/mcmini/producer_consumer_ok.tesh b/teshsuite/mc/mcmini/producer_consumer_ok.tesh new file mode 100644 index 0000000000..1c201d46a0 --- /dev/null +++ b/teshsuite/mc/mcmini/producer_consumer_ok.tesh @@ -0,0 +1,6 @@ +# 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-producer_consumer_ok 2 2 2 1 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1953 unique states visited; 491 backtracks (12324 transition replays, 14768 states visited overall) \ No newline at end of file