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
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
# 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)
# 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)
--- /dev/null
+#include <pthread.h>
+
+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;
+}
+
--- /dev/null
+# 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)
--- /dev/null
+#include <pthread.h>
+#include <stdio.h>
+
+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
--- /dev/null
+# 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)
--- /dev/null
+#include <pthread.h>
+
+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;
+}
+
--- /dev/null
+# 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 <pid> (<name>@<host>): <status>"
+> [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
--- /dev/null
+#include <pthread.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+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;
+}
--- /dev/null
+# 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)
--- /dev/null
+#include <pthread.h>
+#include <semaphore.h>
+
+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;
+}
+
--- /dev/null
+# 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 <pid> (<name>@<host>): <status>"
+> [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
--- /dev/null
+#include <pthread.h>
+#include <semaphore.h>
+
+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;
+}
+
--- /dev/null
+# 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 <pid> (<name>@<host>): <status>"
+> [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
--- /dev/null
+#define _POSIX_C_SOURCE 200809L
+
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+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;
+}
--- /dev/null
+# 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
--- /dev/null
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+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;
+}
--- /dev/null
+# 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 <pid> (<name>@<host>): <status>"
+> [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)
+
--- /dev/null
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+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;
+}
--- /dev/null
+# 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)
