include examples/smpi/trace_call_location/trace_call_location.tesh
include examples/smpi/trace_simple/trace_simple.c
include examples/smpi/trace_simple/trace_simple.tesh
+include examples/sthread/pthread-mc-mutex-simple.tesh
+include examples/sthread/pthread-mc-mutex-simpledeadlock.tesh
include examples/sthread/pthread-mutex-simple.c
include examples/sthread/pthread-mutex-simple.tesh
+include examples/sthread/pthread-mutex-simpledeadlock.c
include examples/sthread/sthread-mutex-simple.c
include examples/sthread/sthread-mutex-simple.tesh
include src/include/catch_simgrid.hpp
include src/mc/sosp/Snapshot_test.cpp
include src/mc/transition/Transition.cpp
include src/mc/transition/Transition.hpp
+include src/mc/transition/TransitionActorJoin.cpp
+include src/mc/transition/TransitionActorJoin.hpp
include src/mc/transition/TransitionAny.cpp
include src/mc/transition/TransitionAny.hpp
include src/mc/transition/TransitionComm.cpp
endforeach()
+# Regular pthread examples that may deadlock: test sthread + MC in that case
+############################################################################
+
+foreach(x
+ mutex-simpledeadlock)
+
+ if(SIMGRID_HAVE_MC AND ("${CMAKE_SYSTEM}" MATCHES "Linux")) # sthread is linux-only
+
+ add_executable (pthread-${x} EXCLUDE_FROM_ALL pthread-${x}.c)
+ set_target_properties(pthread-${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
+ target_link_libraries(pthread-${x} PRIVATE Threads::Threads)
+ target_link_libraries(pthread-${x} PUBLIC "-Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once cmake is >3.13
+
+ add_dependencies(tests-mc pthread-${x})
+ ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh)
+ endif()
+
+ set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh)
+ set(examples_src ${examples_src} ${CMAKE_CURRENT_SOURCE_DIR}/pthread-${x}.c)
+
+endforeach()
+
# Regular sthread examples: test the internal interface for debugging purpose
#############################################################################
--- /dev/null
+
+# This test raises a deadlock, thus the return code of 3
+! expect return 3
+
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+$ ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-mutex-simpledeadlock
+> [0.000000] [sthread/INFO] Starting the simulation.
+> All threads are started.
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> The thread 0 is terminating.
+> The thread 1 is terminating.
+> User's main is terminating.
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [mc_global/INFO] Counter-example execution trace:
+> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 0, owner:2)
+> [0.000000] [mc_global/INFO] 2: MUTEX_WAIT(mutex: 0, owner:2)
+> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 1, owner:3)
+> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 1, owner:3)
+> [0.000000] [mc_global/INFO] 3: MUTEX_WAIT(mutex: 1, owner:3)
+> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 0, owner:2)
+> [0.000000] [mc_global/INFO] Path = 2;2;3;2;3;3
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 19 unique states visited; 2 backtracks (22 transition replays, 2 states visited overall)
--- /dev/null
+/* Simple test code that may deadlock:
+
+ Thread 1 locks mutex1 then mutex2 while thread 2 locks in reverse order.
+ Deadlock occures when each thread get one mutex and then ask for the other one.
+ */
+
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t mutex1;
+pthread_mutex_t mutex2;
+
+static void* thread_fun1(void* val)
+{
+ pthread_mutex_lock(&mutex1);
+ pthread_mutex_lock(&mutex2);
+ pthread_mutex_unlock(&mutex1);
+ pthread_mutex_unlock(&mutex2);
+
+ fprintf(stderr, "The thread %d is terminating.\n", *(int*)val);
+ return NULL;
+}
+static void* thread_fun2(void* val)
+{
+ pthread_mutex_lock(&mutex2);
+ pthread_mutex_lock(&mutex1);
+ pthread_mutex_unlock(&mutex1);
+ pthread_mutex_unlock(&mutex2);
+
+ fprintf(stderr, "The thread %d is terminating.\n", *(int*)val);
+ return NULL;
+}
+
+int main(int argc, char* argv[])
+{
+ pthread_mutex_init(&mutex1, NULL);
+ pthread_mutex_init(&mutex2, NULL);
+
+ int id[2] = {0, 1};
+ pthread_t thread1;
+ pthread_t thread2;
+ pthread_create(&thread1, NULL, thread_fun1, (void*)&id[0]);
+ pthread_create(&thread2, NULL, thread_fun2, (void*)&id[1]);
+ fprintf(stderr, "All threads are started.\n");
+ pthread_join(thread1, NULL);
+ pthread_join(thread2, NULL);
+
+ pthread_mutex_destroy(&mutex1);
+ pthread_mutex_destroy(&mutex2);
+
+ fprintf(stderr, "User's main is terminating.\n");
+ return 0;
+}
