From: Martin Quinson Date: Sun, 12 Nov 2023 17:38:33 +0000 (+0100) Subject: Add more Mc Mini tests X-Git-Tag: v3.35~74 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/30e0627bbfc12ce4ebeacfda720bc52e95feb22c Add more Mc Mini tests --- diff --git a/MANIFEST.in b/MANIFEST.in index 322f765f6f..21a22fee78 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -670,6 +670,16 @@ include teshsuite/mc/mcmini/producer_consumer_deadlock.c include teshsuite/mc/mcmini/producer_consumer_deadlock.tesh include teshsuite/mc/mcmini/producer_consumer_ok.c include teshsuite/mc/mcmini/producer_consumer_ok.tesh +include teshsuite/mc/mcmini/simple_semaphore_deadlock.c +include teshsuite/mc/mcmini/simple_semaphore_deadlock.tesh +include teshsuite/mc/mcmini/simple_semaphores_deadlock.c +include teshsuite/mc/mcmini/simple_semaphores_deadlock.tesh +include teshsuite/mc/mcmini/simple_semaphores_ok.c +include teshsuite/mc/mcmini/simple_semaphores_ok.tesh +include teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.c +include teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.tesh +include teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.c +include teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.tesh include teshsuite/mc/mutex-handling/mutex-handling.cpp include teshsuite/mc/mutex-handling/mutex-handling.tesh include teshsuite/mc/mutex-handling/without-mutex-handling.tesh diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index dba795fe62..8432916476 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -47,16 +47,17 @@ endif() foreach(x # -# simple_cond_broadcast_deadlock simple_semaphore_deadlock simple_barrier_deadlock simple_cond_deadlock -# simple_semaphores_deadlock -# +# simple_cond_broadcast_deadlock simple_barrier_deadlock simple_cond_deadlock + simple_mutex_ok simple_mutex_deadlock + simple_mutex_with_threads_ok simple_mutex_with_threads_deadlock + + simple_semaphore_deadlock simple_semaphores_deadlock + simple_semaphores_ok + simple_semaphores_with_threads_ok simple_semaphores_with_threads_deadlock # # philosophers_spurious_deadlock # simple_barrier_with_threads_deadlock -# simple_semaphores_with_threads_deadlock # simple_cond_broadcast_with_semaphore_deadlock1 simple_cond_broadcast_with_semaphore_deadlock2 -# simple_mutex_deadlock -# simple_mutex_with_threads_deadlock barber_shop_ok barber_shop_deadlock philosophers_semaphores_ok philosophers_semaphores_deadlock @@ -66,11 +67,9 @@ foreach(x # 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 +# simple_cond_broadcast_with_semaphore_ok simple_cond_ok +# simple_threads_ok ) set(teshsuite_src ${teshsuite_src} ${CMAKE_CURRENT_SOURCE_DIR}/mcmini/${x}.c) diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh b/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh index e25ecc80d3..16b02c8afe 100644 --- a/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh +++ b/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh @@ -1,7 +1,7 @@ # 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_semaphores_ok 4 0 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_semaphores_ok 3 0 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 7470 unique states visited; 324 backtracks (4259 transition replays, 12053 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 209 unique states visited; 10 backtracks (50 transition replays, 269 states visited overall) diff --git a/teshsuite/mc/mcmini/simple_mutex_deadlock.c b/teshsuite/mc/mcmini/simple_mutex_deadlock.c new file mode 100644 index 0000000000..cfdfd735c1 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_mutex_deadlock.c @@ -0,0 +1,18 @@ +#include + +pthread_mutex_t mutex1; +pthread_mutex_t mutex2; + +int main(int argc, char* argv[]) { + pthread_mutex_init(&mutex1, NULL); + pthread_mutex_init(&mutex2, NULL); + + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); + pthread_mutex_unlock(&mutex2); + pthread_mutex_lock(&mutex1); + pthread_mutex_unlock(&mutex1); + + return 0; +} + diff --git a/teshsuite/mc/mcmini/simple_mutex_deadlock.tesh b/teshsuite/mc/mcmini/simple_mutex_deadlock.tesh new file mode 100644 index 0000000000..8f214b2b3d --- /dev/null +++ b/teshsuite/mc/mcmini/simple_mutex_deadlock.tesh @@ -0,0 +1,7 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_mutex_deadlock +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 9 unique states visited; 0 backtracks (0 transition replays, 9 states visited overall) diff --git a/teshsuite/mc/mcmini/simple_mutex_ok.c b/teshsuite/mc/mcmini/simple_mutex_ok.c new file mode 100644 index 0000000000..66189bcc63 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_mutex_ok.c @@ -0,0 +1,26 @@ +#include +#include + +pthread_mutex_t mutex1; +pthread_mutex_t mutex2; + +int main(int argc, char* argv[]) { + + if(argc != 1) { + printf("Expected usage: %s \n", argv[0]); + return -1; + } + + pthread_mutex_init(&mutex1, NULL); + pthread_mutex_init(&mutex2, NULL); + + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + + pthread_mutex_destroy(&mutex1); + pthread_mutex_destroy(&mutex2); + + return 0; +} \ No newline at end of file diff --git a/teshsuite/mc/mcmini/simple_mutex_ok.tesh b/teshsuite/mc/mcmini/simple_mutex_ok.tesh new file mode 100644 index 0000000000..65e6c56db9 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_mutex_ok.tesh @@ -0,0 +1,7 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_mutex_ok +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 7 unique states visited; 0 backtracks (0 transition replays, 7 states visited overall) diff --git a/teshsuite/mc/mcmini/simple_mutex_with_threads_deadlock.c b/teshsuite/mc/mcmini/simple_mutex_with_threads_deadlock.c new file mode 100644 index 0000000000..4cf361dcb8 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_mutex_with_threads_deadlock.c @@ -0,0 +1,35 @@ +#include + +pthread_mutex_t mutex1; +pthread_mutex_t mutex2; +pthread_t thread1, thread2; + +static void * thread_doit1(void *forks_arg) { + pthread_mutex_lock(&mutex2); + pthread_mutex_lock(&mutex1); + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(&mutex2); + return NULL; +} + +static void * thread_doit2(void *forks_arg) { + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(int argc, char* argv[]) { + pthread_mutex_init(&mutex1, NULL); + pthread_mutex_init(&mutex2, NULL); + + pthread_create(&thread1, NULL, &thread_doit1, NULL); + pthread_create(&thread2, NULL, &thread_doit2, NULL); + + pthread_join(thread1, NULL); + pthread_join(thread2, NULL); + + return 0; +} + diff --git a/teshsuite/mc/mcmini/simple_mutex_with_threads_deadlock.tesh b/teshsuite/mc/mcmini/simple_mutex_with_threads_deadlock.tesh new file mode 100644 index 0000000000..5fa24c434a --- /dev/null +++ b/teshsuite/mc/mcmini/simple_mutex_with_threads_deadlock.tesh @@ -0,0 +1,24 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_mutex_with_threads_deadlock +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 3 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:0 owner:3) +> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:2) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 1, owner: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 0, owner: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, 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;3' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 19 unique states visited; 1 backtracks (2 transition replays, 22 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/simple_mutex_with_threads_ok.c b/teshsuite/mc/mcmini/simple_mutex_with_threads_ok.c new file mode 100644 index 0000000000..d460e89830 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_mutex_with_threads_ok.c @@ -0,0 +1,48 @@ +#include +#include +#include + +pthread_mutex_t mutex1; +pthread_mutex_t mutex2; + +static void * thread_doit(void *unused) { + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(int argc, char* argv[]) { + + if(argc < 2) { + printf("Expected usage: %s THREAD_NUM\n", argv[0]); + return -1; + } + + int THREAD_NUM = atoi(argv[1]); + + if(THREAD_NUM < 2) { + printf("At least 2 threads are required\n"); + return -1; + } + + pthread_t *threads = malloc(sizeof(pthread_t) * THREAD_NUM); + + pthread_mutex_init(&mutex1, NULL); + pthread_mutex_init(&mutex2, NULL); + + for(int i = 0; i < THREAD_NUM; i++) { + pthread_create(&threads[i], NULL, &thread_doit, NULL); + } + + for(int i = 0; i < THREAD_NUM; i++) { + pthread_join(threads[i], NULL); + } + + free(threads); + pthread_mutex_destroy(&mutex1); + pthread_mutex_destroy(&mutex2); + + return 0; +} diff --git a/teshsuite/mc/mcmini/simple_mutex_with_threads_ok.tesh b/teshsuite/mc/mcmini/simple_mutex_with_threads_ok.tesh new file mode 100644 index 0000000000..f2f23c16bc --- /dev/null +++ b/teshsuite/mc/mcmini/simple_mutex_with_threads_ok.tesh @@ -0,0 +1,7 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_mutex_with_threads_ok 4 +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 548 unique states visited; 23 backtracks (125 transition replays, 696 states visited overall) diff --git a/teshsuite/mc/mcmini/simple_semaphore_deadlock.c b/teshsuite/mc/mcmini/simple_semaphore_deadlock.c new file mode 100644 index 0000000000..1b7d7b3445 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphore_deadlock.c @@ -0,0 +1,36 @@ +#include +#include + +sem_t sem1; +sem_t sem2; +pthread_t thread1, thread2; + +static void * thread_doit1(void *forks_arg) { + sem_wait(&sem2); + sem_wait(&sem1); + sem_post(&sem1); + sem_post(&sem2); + return NULL; +} + +static void * thread_doit2(void *forks_arg) { + sem_wait(&sem1); + sem_wait(&sem2); + sem_post(&sem2); + sem_post(&sem1); + return NULL; +} + +int main(int argc, char* argv[]) { + sem_init(&sem1, 0, 1); + sem_init(&sem2, 0, 1); + + pthread_create(&thread1, NULL, &thread_doit1, NULL); + pthread_create(&thread2, NULL, &thread_doit2, NULL); + + pthread_join(thread1, NULL); + pthread_join(thread2, NULL); + + return 0; +} + diff --git a/teshsuite/mc/mcmini/simple_semaphore_deadlock.tesh b/teshsuite/mc/mcmini/simple_semaphore_deadlock.tesh new file mode 100644 index 0000000000..ed0cf3d2a0 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphore_deadlock.tesh @@ -0,0 +1,24 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_semaphore_deadlock +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 3 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 SEM_WAIT(sem_id:1 not granted) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 1, capacity: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 1, capacity: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 0, capacity: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 1, capacity: 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;2;3;2;3;3' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 19 unique states visited; 1 backtracks (2 transition replays, 22 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/simple_semaphores_deadlock.c b/teshsuite/mc/mcmini/simple_semaphores_deadlock.c new file mode 100644 index 0000000000..ef8b34a1e2 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphores_deadlock.c @@ -0,0 +1,16 @@ +#include +#include + +sem_t sem; + +int main(int argc, char* argv[]) { + sem_init(&sem, 0, 0); + + sem_post(&sem); + sem_post(&sem); + sem_wait(&sem); + sem_wait(&sem); + sem_wait(&sem); + return 0; +} + diff --git a/teshsuite/mc/mcmini/simple_semaphores_deadlock.tesh b/teshsuite/mc/mcmini/simple_semaphores_deadlock.tesh new file mode 100644 index 0000000000..b023c3f516 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphores_deadlock.tesh @@ -0,0 +1,23 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_semaphores_deadlock +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 1 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 SEM_WAIT(sem_id:0 not granted) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 1 in simcall SEM_UNLOCK(semaphore: 0, capacity: 1) +> [0.000000] [mc_global/INFO] Actor 1 in simcall SEM_UNLOCK(semaphore: 0, capacity: 2) +> [0.000000] [mc_global/INFO] Actor 1 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 1) +> [0.000000] [mc_global/INFO] Actor 1 in simcall SEM_WAIT(semaphore: 0, capacity: 1, granted: yes) +> [0.000000] [mc_global/INFO] Actor 1 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0) +> [0.000000] [mc_global/INFO] Actor 1 in simcall SEM_WAIT(semaphore: 0, capacity: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 1 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 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:'1;1;1;1;1;1;1' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 8 unique states visited; 0 backtracks (0 transition replays, 8 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/simple_semaphores_ok.c b/teshsuite/mc/mcmini/simple_semaphores_ok.c new file mode 100644 index 0000000000..92509cd794 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphores_ok.c @@ -0,0 +1,32 @@ +#define _POSIX_C_SOURCE 200809L + +#include +#include +#include +#include + +sem_t sem; + +int main(int argc, char* argv[]) { + if(argc < 2) { + printf("Expected usage: %s START_NUM\n", argv[0]); + return -1; + } + + int start_num = atoi(argv[1]); + + sem_init(&sem, 0, start_num); + + for(int i = 0; i < start_num; i++) { + sem_wait(&sem); + } + + sem_post(&sem); + sem_post(&sem); + sem_wait(&sem); + sem_wait(&sem); + + sem_destroy(&sem); + + return 0; +} diff --git a/teshsuite/mc/mcmini/simple_semaphores_ok.tesh b/teshsuite/mc/mcmini/simple_semaphores_ok.tesh new file mode 100644 index 0000000000..144d78d27e --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphores_ok.tesh @@ -0,0 +1,7 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_semaphores_ok 5 +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 17 unique states visited; 0 backtracks (0 transition replays, 17 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.c b/teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.c new file mode 100644 index 0000000000..5f783fb35e --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.c @@ -0,0 +1,49 @@ +#include +#include +#include +#include + +int START_NUM; +int DEBUG = 0; + +sem_t sem1, sem2; +pthread_t thread1, thread2; + +static void * thread1_doit(void *forks_arg) { + sem_wait(&sem2); + sem_wait(&sem2); + if(DEBUG) printf("Thread 1: Posted to sem1\n"); + sem_post(&sem1); + return NULL; +} + +static void * thread2_doit(void *forks_arg) { + for( int i = 0; i < START_NUM+1; i++) { + if(DEBUG) printf("Thread 2: Waiting for sem1\n"); + sem_wait(&sem1); + } + if(DEBUG) printf("Thread 2: Posted to sem2\n"); + sem_post(&sem2); + return NULL; +} + +int main(int argc, char* argv[]) { + if(argc != 3){ + printf("Usage: %s START_NUM DEBUG_FLAG\n", argv[0]); + return 1; + } + + START_NUM = atoi(argv[1]); + DEBUG = atoi(argv[2]); + + sem_init(&sem1, 0, START_NUM); + sem_init(&sem2, 0, 1); + + pthread_create(&thread1, NULL, &thread1_doit, NULL); + pthread_create(&thread2, NULL, &thread2_doit, NULL); + + pthread_join(thread1, NULL); + pthread_join(thread2, NULL); + + return 0; +} diff --git a/teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.tesh b/teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.tesh new file mode 100644 index 0000000000..931802ab39 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.tesh @@ -0,0 +1,25 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_semaphores_with_threads_deadlock 1 0 +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 3 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:1 not granted) +> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@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: 1, capacity: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 1, capacity: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 1, capacity: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 0, capacity: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0, capacity: 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;2;2;3;3;3' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 7 unique states visited; 0 backtracks (0 transition replays, 7 states visited overall) + diff --git a/teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.c b/teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.c new file mode 100644 index 0000000000..4e1ff7ad55 --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.c @@ -0,0 +1,46 @@ +#include +#include +#include +#include + +sem_t sem1, sem2; +pthread_t thread1, thread2; + +static void * thread1_doit(void *unused) { + sem_wait(&sem2); + sem_post(&sem1); + sem_wait(&sem2); + return NULL; +} + +static void * thread2_doit(void *sem_count) { + int start_num = *((int*)sem_count); + for(int i = 0; i < start_num + 1; i++) { + sem_wait(&sem1); + } + sem_post(&sem2); + return NULL; +} + +int main(int argc, char* argv[]) { + if(argc < 2) { + printf("Expected usage: %s START_NUM\n", argv[0]); + return -1; + } + + int start_num = atoi(argv[1]); + + sem_init(&sem1, 0, start_num); + sem_init(&sem2, 0, 1); + + pthread_create(&thread1, NULL, &thread1_doit, NULL); + pthread_create(&thread2, NULL, &thread2_doit, &start_num); + + pthread_join(thread1, NULL); + pthread_join(thread2, NULL); + + sem_destroy(&sem1); + sem_destroy(&sem2); + + return 0; +} diff --git a/teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.tesh b/teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.tesh new file mode 100644 index 0000000000..a78278110c --- /dev/null +++ b/teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.tesh @@ -0,0 +1,7 @@ +# 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/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_semaphores_with_threads_ok 3 +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 24 unique states visited; 1 backtracks (1 transition replays, 26 states visited overall)