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/mcmini/simple_threads_ok.c
+include teshsuite/mc/mcmini/simple_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
# simple_cond_broadcast_ok simple_cond_broadcast_deadlock
# simple_cond_broadcast_with_semaphore_ok
# simple_cond_broadcast_with_semaphore_deadlock1 simple_cond_broadcast_with_semaphore_deadlock2
-# simple_threads_ok
# simple_cond_deadlock
simple_mutex_ok simple_mutex_deadlock
simple_semaphore_deadlock simple_semaphores_deadlock
simple_semaphores_ok
simple_semaphores_with_threads_ok simple_semaphores_with_threads_deadlock
-#
-# philosophers_spurious_deadlock
+ simple_threads_ok
+
barber_shop_ok barber_shop_deadlock
philosophers_semaphores_ok philosophers_semaphores_deadlock
philosophers_mutex_ok philosophers_mutex_deadlock
producer_consumer_ok producer_consumer_deadlock
-
+ # philosophers_spurious_deadlock # infinite no-op loop
# producer_consumer_spurious_nok # infinite no-op loop
)
--- /dev/null
+#include <pthread.h>
+#include <stdlib.h>
+#include <unistd.h>
+#include <stdio.h>
+
+static void * thread_doit(void *unused) {
+ int len = (int) ((drand48() * 5) + 1);
+ sleep(len);
+ 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]);
+
+ pthread_t *threads = malloc(sizeof(pthread_t) * thread_num);
+
+ 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);
+
+ 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_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. 7 unique states visited; 0 backtracks (0 transition replays, 7 states visited overall)
\ No newline at end of file