Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Another easy test from McMini
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 12 Nov 2023 20:38:09 +0000 (21:38 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Mon, 13 Nov 2023 15:05:52 +0000 (16:05 +0100)
MANIFEST.in
teshsuite/mc/CMakeLists.txt
teshsuite/mc/mcmini/simple_threads_ok.c [new file with mode: 0644]
teshsuite/mc/mcmini/simple_threads_ok.tesh [new file with mode: 0644]

index 3a53385..718a59e 100644 (file)
@@ -696,6 +696,8 @@ 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/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
index 1209bc0..5ec629a 100644 (file)
@@ -54,7 +54,6 @@ foreach(x
 #            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
@@ -63,15 +62,15 @@ foreach(x
              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
              )
 
diff --git a/teshsuite/mc/mcmini/simple_threads_ok.c b/teshsuite/mc/mcmini/simple_threads_ok.c
new file mode 100644 (file)
index 0000000..44c716c
--- /dev/null
@@ -0,0 +1,33 @@
+#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;
+}
diff --git a/teshsuite/mc/mcmini/simple_threads_ok.tesh b/teshsuite/mc/mcmini/simple_threads_ok.tesh
new file mode 100644 (file)
index 0000000..b8a82c5
--- /dev/null
@@ -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_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