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_barrier_deadlock.c
+include teshsuite/mc/mcmini/simple_barrier_deadlock.tesh
+include teshsuite/mc/mcmini/simple_barrier_ok.c
+include teshsuite/mc/mcmini/simple_barrier_ok.tesh
+include teshsuite/mc/mcmini/simple_barrier_with_threads_deadlock.c
+include teshsuite/mc/mcmini/simple_barrier_with_threads_deadlock.tesh
+include teshsuite/mc/mcmini/simple_barrier_with_threads_ok.c
+include teshsuite/mc/mcmini/simple_barrier_with_threads_ok.tesh
+include teshsuite/mc/mcmini/simple_mutex_deadlock.c
+include teshsuite/mc/mcmini/simple_mutex_deadlock.tesh
+include teshsuite/mc/mcmini/simple_mutex_ok.c
+include teshsuite/mc/mcmini/simple_mutex_ok.tesh
+include teshsuite/mc/mcmini/simple_mutex_with_threads_deadlock.c
+include teshsuite/mc/mcmini/simple_mutex_with_threads_deadlock.tesh
+include teshsuite/mc/mcmini/simple_mutex_with_threads_ok.c
+include teshsuite/mc/mcmini/simple_mutex_with_threads_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
static int (*raw_pthread_mutexattr_getrobust)(const pthread_mutexattr_t*, int*);
static int (*raw_pthread_mutexattr_setrobust)(pthread_mutexattr_t*, int);
+static int (*raw_pthread_barrier_init)(pthread_barrier_t*, const pthread_barrierattr_t*, unsigned int count);
+static int (*raw_pthread_barrier_wait)(pthread_barrier_t*);
+static int (*raw_pthread_barrier_destroy)(pthread_barrier_t*);
+
static unsigned int (*raw_sleep)(unsigned int);
static int (*raw_usleep)(useconds_t);
static int (*raw_gettimeofday)(struct timeval*, void*);
raw_pthread_mutexattr_getrobust = dlsym(RTLD_NEXT, "pthread_mutexattr_getrobust");
raw_pthread_mutexattr_setrobust = dlsym(RTLD_NEXT, "pthread_mutexattr_setrobust");
+ raw_pthread_barrier_init = dlsym(RTLD_NEXT, "raw_pthread_barrier_init");
+ raw_pthread_barrier_wait = dlsym(RTLD_NEXT, "raw_pthread_barrier_wait");
+ raw_pthread_barrier_destroy = dlsym(RTLD_NEXT, "raw_pthread_barrier_destroy");
+
raw_sleep = dlsym(RTLD_NEXT, "sleep");
raw_usleep = dlsym(RTLD_NEXT, "usleep");
raw_gettimeofday = dlsym(RTLD_NEXT, "gettimeofday");
intercepted_pthcall(mutex_unlock, (pthread_mutex_t * mutex), (mutex), ((sthread_mutex_t*)mutex));
intercepted_pthcall(mutex_destroy, (pthread_mutex_t * mutex), (mutex), ((sthread_mutex_t*)mutex));
+intercepted_pthcall(barrier_init, (pthread_barrier_t * barrier, const pthread_barrierattr_t* attr, unsigned count),
+ (barrier, attr, count), ((sthread_barrier_t*)barrier, (const sthread_barrierattr_t*)attr, count));
+intercepted_pthcall(barrier_wait, (pthread_barrier_t* barrier),( barrier),((sthread_barrier_t*) barrier));
+intercepted_pthcall(barrier_destroy, (pthread_barrier_t* barrier),( barrier),((sthread_barrier_t*) barrier));
+
#define intercepted_call(rettype, name, raw_params, call_params, sim_params) \
rettype name raw_params \
{ \
int sthread_mutex_unlock(sthread_mutex_t* mutex);
int sthread_mutex_destroy(sthread_mutex_t* mutex);
+typedef struct {
+ unsigned unused : 1;
+} sthread_barrierattr_t;
+
+typedef struct {
+ void* barrier;
+} sthread_barrier_t;
+int sthread_barrier_init(sthread_barrier_t* barrier, const sthread_barrierattr_t* attr, unsigned count);
+int sthread_barrier_wait(sthread_barrier_t* barrier);
+int sthread_barrier_destroy(sthread_barrier_t* barrier);
+
typedef struct {
void* sem;
} sthread_sem_t;
/* SimGrid's pthread interposer. Actual implementation of the symbols (see the comment in sthread.h) */
+#include "simgrid/s4u/Barrier.hpp"
#include "smpi/smpi.h"
#include "xbt/asserts.h"
#include "xbt/ex.h"
}
/* Do not intercept valgrind step 1 */
- if (not strcmp(argv[0], "/usr/bin/valgrind.bin") || not strcmp(argv[0], "/bin/sh")) {
+ if (not strcmp(argv[0], "/usr/bin/valgrind.bin") || not strcmp(argv[0], "/bin/sh")|| not strcmp(argv[0], "/bin/bash")|| not strcmp(argv[0], "gdb")) {
printf("sthread refuses to intercept the execution of %s. Running the application unmodified.\n", argv[0]);
fflush(stdout);
return raw_main(argc, argv, envp);
intrusive_ptr_release(static_cast<sg4::Mutex*>(mutex->mutex));
return 0;
}
+
+int sthread_barrier_init(sthread_barrier_t* barrier, const sthread_barrierattr_t* attr, unsigned count){
+ auto b = sg4::Barrier::create(count);
+ intrusive_ptr_add_ref(b.get());
+
+ barrier->barrier = b.get();
+ return 0;
+}
+int sthread_barrier_wait(sthread_barrier_t* barrier){
+ XBT_DEBUG("%s(%p)", __func__, barrier);
+ static_cast<sg4::Barrier*>(barrier->barrier)->wait();
+ return 0;
+}
+int sthread_barrier_destroy(sthread_barrier_t* barrier){
+ XBT_DEBUG("%s(%p)", __func__, barrier);
+ intrusive_ptr_release(static_cast<sg4::Barrier*>(barrier->barrier));
+ return 0;
+}
+
int sthread_sem_init(sthread_sem_t* sem, int /*pshared*/, unsigned int value)
{
auto s = sg4::Semaphore::create(value);
simple_semaphores_with_threads_ok simple_semaphores_with_threads_deadlock
#
# philosophers_spurious_deadlock
-# simple_barrier_with_threads_deadlock
# simple_cond_broadcast_with_semaphore_deadlock1 simple_cond_broadcast_with_semaphore_deadlock2
barber_shop_ok barber_shop_deadlock
# producer_consumer_spurious_nok # infinite no-op loop
-# simple_barrier_ok simple_barrier_with_threads_ok simple_cond_broadcast_ok
+ simple_barrier_ok simple_barrier_deadlock
+ simple_barrier_with_threads_ok simple_barrier_with_threads_deadlock
+# simple_cond_broadcast_ok
# simple_cond_broadcast_with_semaphore_ok simple_cond_ok
# simple_threads_ok
)
--- /dev/null
+#include <pthread.h>
+
+pthread_barrier_t barrier;
+
+int main(int argc, char* argv[]) {
+ pthread_barrier_init(&barrier, NULL, 2);
+ pthread_barrier_wait(&barrier);
+ 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:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_barrier_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 BARRIER_WAIT(barrier_id:0)
+> [0.000000] [mc_global/INFO] Counter-example execution trace:
+> [0.000000] [mc_global/INFO] Actor 1 in simcall BARRIER_ASYNC_LOCK(barrier: 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'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 2 unique states visited; 0 backtracks (0 transition replays, 2 states visited overall)
--- /dev/null
+#include <pthread.h>
+
+pthread_barrier_t barrier;
+
+int main(int argc, char* argv[])
+{
+ pthread_barrier_init(&barrier, NULL, 1);
+ pthread_barrier_wait(&barrier);
+ 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:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_barrier_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. 3 unique states visited; 0 backtracks (0 transition replays, 3 states visited overall)
--- /dev/null
+#include <pthread.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+int THREAD_NUM;
+int DEBUG = 0;
+
+pthread_barrier_t barrier;
+pthread_t *thread;
+
+static void * thread_doit(void *unused)
+{
+ if(DEBUG) printf("Thread %lu: Waiting at barrier\n", (unsigned long)pthread_self());
+ pthread_barrier_wait(&barrier);
+ if(DEBUG) printf("Thread %lu: Passed the barrier\n", (unsigned long)pthread_self());
+ return NULL;
+}
+
+int main(int argc, char* argv[]) {
+ if(argc != 3){
+ printf("Usage: %s THREAD_NUM DEBUG_FLAG\n", argv[0]);
+ return 1;
+ }
+
+ THREAD_NUM = atoi(argv[1]);
+ DEBUG = atoi(argv[2]);
+
+ thread = (pthread_t*) malloc(THREAD_NUM * sizeof(pthread_t));
+
+ pthread_barrier_init(&barrier, NULL, THREAD_NUM);
+ for(int i = 0; i < THREAD_NUM; i++) {
+ pthread_create(&thread[i], NULL, &thread_doit, NULL);
+ }
+
+ pthread_barrier_wait(&barrier);
+
+ for(int i = 0; i < THREAD_NUM; i++) {
+ pthread_join(thread[i], NULL);
+ }
+
+ free(thread);
+ 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:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_barrier_with_threads_deadlock 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_global/INFO] **************************
+> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [ker_engine/INFO] 2 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:4)
+> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall BARRIER_WAIT(barrier_id:0)
+> [0.000000] [mc_global/INFO] Counter-example execution trace:
+> [0.000000] [mc_global/INFO] Actor 1 in simcall BARRIER_ASYNC_LOCK(barrier: 0)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall BARRIER_ASYNC_LOCK(barrier: 0)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall BARRIER_ASYNC_LOCK(barrier: 0)
+> [0.000000] [mc_global/INFO] Actor 1 in simcall BARRIER_WAIT(barrier: 0)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall BARRIER_WAIT(barrier: 0)
+> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 2, no timeout)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall BARRIER_WAIT(barrier: 0)
+> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 3, no timeout)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall BARRIER_ASYNC_LOCK(barrier: 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;2;3;1;2;1;3;1;4'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 10 unique states visited; 0 backtracks (0 transition replays, 10 states visited overall)
--- /dev/null
+#define _POSIX_C_SOURCE 200809L
+
+#include <pthread.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+int DEBUG;
+
+pthread_barrier_t barrier;
+
+static void * thread_doit(void *t)
+{
+ int *tid = (int*)t;
+ if(DEBUG) {
+ printf("Thread %d: Waiting at barrier\n", *tid);
+ }
+ pthread_barrier_wait(&barrier);
+ if(DEBUG) {
+ printf("Thread %d: Crossed barrier\n", *tid);
+ }
+ return NULL;
+}
+
+int main(int argc, char* argv[])
+{
+ if(argc < 3) {
+ printf("Expected usage: %s THREAD_NUM DEBUG_FLAG\n", argv[0]);
+ printf("DEBUG_FLAG: 0 - Don't display debug information, 1 - Display debug information\n");
+ return -1;
+ }
+
+ int THREAD_NUM = atoi(argv[1]);
+ DEBUG = atoi(argv[2]);
+
+ pthread_t *threads = malloc(sizeof(pthread_t) * THREAD_NUM);
+
+ pthread_barrier_init(&barrier, NULL, THREAD_NUM);
+
+ int *tids = malloc(sizeof(int) * THREAD_NUM);
+ for(int i = 0; i < THREAD_NUM; i++) {
+ tids[i] = i;
+ pthread_create(&threads[i], NULL, &thread_doit, &tids[i]);
+ }
+
+ for(int i = 0; i < THREAD_NUM; i++) {
+ pthread_join(threads[i], NULL);
+ }
+
+ free(threads);
+ free(tids);
+ pthread_barrier_destroy(&barrier);
+
+ 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:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_barrier_with_threads_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. 10 unique states visited; 0 backtracks (0 transition replays, 10 states visited overall)
