sthread:
- Implement pthread_join in MC mode.
+ - Implement semaphore functions in sthread.
XBT:
- simgrid::xbt::cmdline and simgrid::xbt::binary_name are gone.
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-mc-producer-consumer.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/pthread-producer-consumer.c
+include examples/sthread/pthread-producer-consumer.tesh
include examples/sthread/sthread-mutex-simple.c
include examples/sthread/sthread-mutex-simple.tesh
include teshsuite/catch_simgrid.hpp
#########################################################################
foreach(x
- mutex-simple)
+ mutex-simple
+ producer-consumer)
if("${CMAKE_SYSTEM}" MATCHES "Linux")
add_executable (pthread-${x} EXCLUDE_FROM_ALL pthread-${x}.c)
--- /dev/null
+# 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-producer-consumer -q
+> [0.000000] [sthread/INFO] Starting the simulation.
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1819 unique states visited; 108 backtracks (6808 transition replays, 4882 states visited overall)
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2002-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+/* Simple producer/consumer example with pthreads and semaphores */
+
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#define AmountProduced 3 /* Amount of items produced by a producer */
+#define AmountConsumed 3 /* Amount of items consumed by a consumer */
+#define ProducerCount 2 /* Amount of producer threads*/
+#define ConsumerCount 2 /* Amount of consumer threads*/
+#define BufferSize 4 /* Size of the buffer */
+
+sem_t empty;
+sem_t full;
+int in = 0;
+int out = 0;
+int buffer[BufferSize];
+pthread_mutex_t mutex;
+int do_output = 1;
+
+static void* producer(void* id)
+{
+ for (int i = 0; i < AmountProduced; i++) {
+ sem_wait(&empty);
+ pthread_mutex_lock(&mutex);
+ buffer[in] = i;
+ if (do_output)
+ fprintf(stderr, "Producer %d: Insert Item %d at %d\n", *((int*)id), buffer[in], in);
+ in = (in + 1) % BufferSize;
+ pthread_mutex_unlock(&mutex);
+ sem_post(&full);
+ }
+ return NULL;
+}
+static void* consumer(void* id)
+{
+ for (int i = 0; i < AmountConsumed; i++) {
+ sem_wait(&full);
+ pthread_mutex_lock(&mutex);
+ int item = buffer[out];
+ if (do_output)
+ fprintf(stderr, "Consumer %d: Remove Item %d from %d\n", *((int*)id), item, out);
+ out = (out + 1) % BufferSize;
+ pthread_mutex_unlock(&mutex);
+ sem_post(&empty);
+ }
+ return NULL;
+}
+
+int main(int argc, char** argv)
+{
+ if (argc == 2 && strcmp(argv[1], "-q") == 0)
+ do_output = 0;
+ pthread_t pro[2], con[2];
+ pthread_mutex_init(&mutex, NULL);
+ sem_init(&empty, 0, BufferSize);
+ sem_init(&full, 0, 0);
+
+ int ids[10] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}; // The identity of each thread (for debug messages)
+
+ for (int i = 0; i < ProducerCount; i++)
+ pthread_create(&pro[i], NULL, (void*)producer, (void*)&ids[i]);
+ for (int i = 0; i < ConsumerCount; i++)
+ pthread_create(&con[i], NULL, (void*)consumer, (void*)&ids[i]);
+
+ for (int i = 0; i < ProducerCount; i++)
+ pthread_join(pro[i], NULL);
+ for (int i = 0; i < ConsumerCount; i++)
+ pthread_join(con[i], NULL);
+
+ pthread_mutex_destroy(&mutex);
+ sem_destroy(&empty);
+ sem_destroy(&full);
+
+ return 0;
+}
\ No newline at end of file
--- /dev/null
+$ env ASAN_OPTIONS=verify_asan_link_order=0:$ASAN_OPTIONS LD_PRELOAD=${libdir:=.}/libsthread.so ./pthread-producer-consumer
+> [0.000000] [sthread/INFO] Starting the simulation.
+> Producer 1: Insert Item 0 at 0
+> Producer 2: Insert Item 0 at 1
+> Consumer 1: Remove Item 0 from 0
+> Producer 1: Insert Item 1 at 2
+> Consumer 2: Remove Item 0 from 1
+> Producer 2: Insert Item 1 at 3
+> Consumer 1: Remove Item 1 from 2
+> Producer 1: Insert Item 2 at 0
+> Consumer 2: Remove Item 1 from 3
+> Producer 2: Insert Item 2 at 1
+> Consumer 1: Remove Item 2 from 0
+> Consumer 2: Remove Item 2 from 1
+> [0.000000] [sthread/INFO] All threads exited. Terminating the simulation.
+/* Copyright (c) 2002-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
/* SimGrid's pthread interposer. Redefinition of the pthread symbols (see the comment in sthread.h) */
#define _GNU_SOURCE
static int (*raw_sem_init)(sem_t*, int, unsigned int);
static int (*raw_sem_wait)(sem_t*);
static int (*raw_sem_post)(sem_t*);
+static int (*raw_sem_destroy)(sem_t*);
+static int (*raw_sem_trywait)(sem_t*);
+static int (*raw_sem_timedwait)(sem_t*, const struct timespec*);
static void intercepter_init()
{
raw_sem_init = dlsym(RTLD_NEXT, "sem_init");
raw_sem_wait = dlsym(RTLD_NEXT, "sem_wait");
raw_sem_post = dlsym(RTLD_NEXT, "sem_post");
+ raw_sem_destroy = dlsym(RTLD_NEXT, "sem_destroy");
+ raw_sem_trywait = dlsym(RTLD_NEXT, "sem_trywait");
+ raw_sem_timedwait = dlsym(RTLD_NEXT, "sem_timedwait");
}
static int sthread_inside_simgrid = 1;
sthread_enable();
return res;
}
+int sem_init(sem_t* sem, int pshared, unsigned int value)
+{
+ if (raw_sem_init == NULL)
+ intercepter_init();
+
+ if (sthread_inside_simgrid)
+ return raw_sem_init(sem, pshared, value);
+
+ sthread_disable();
+ int res = sthread_sem_init((sthread_sem_t*)sem, pshared, value);
+ sthread_enable();
+ return res;
+}
+int sem_destroy(sem_t* sem)
+{
+ if (raw_sem_destroy == NULL)
+ intercepter_init();
+
+ if (sthread_inside_simgrid)
+ return raw_sem_destroy(sem);
+
+ sthread_disable();
+ int res = sthread_sem_destroy((sthread_sem_t*)sem);
+ sthread_enable();
+ return res;
+}
+int sem_post(sem_t* sem)
+{
+ if (raw_sem_post == NULL)
+ intercepter_init();
+
+ if (sthread_inside_simgrid)
+ return raw_sem_post(sem);
+
+ sthread_disable();
+ int res = sthread_sem_post((sthread_sem_t*)sem);
+ sthread_enable();
+ return res;
+}
+int sem_wait(sem_t* sem)
+{
+ if (raw_sem_wait == NULL)
+ intercepter_init();
+
+ if (sthread_inside_simgrid)
+ return raw_sem_wait(sem);
+
+ sthread_disable();
+ int res = sthread_sem_wait((sthread_sem_t*)sem);
+ sthread_enable();
+ return res;
+}
+int sem_trywait(sem_t* sem)
+{
+ if (raw_sem_trywait == NULL)
+ intercepter_init();
+
+ if (sthread_inside_simgrid)
+ return raw_sem_trywait(sem);
+
+ sthread_disable();
+ int res = sthread_sem_trywait((sthread_sem_t*)sem);
+ sthread_enable();
+ return res;
+}
+int sem_timedwait(sem_t* sem, const struct timespec* abs_timeout)
+{
+ if (raw_sem_timedwait == NULL)
+ intercepter_init();
+
+ if (sthread_inside_simgrid)
+ return raw_sem_timedwait(sem, abs_timeout);
+
+ sthread_disable();
+ int res = sthread_sem_timedwait((sthread_sem_t*)sem, abs_timeout);
+ sthread_enable();
+ return res;
+}
/* Glibc < 2.31 uses type "struct timezone *" for the second parameter of gettimeofday.
Other implementations use "void *" instead. */
}
#if 0
-int sem_init(sem_t *sem, int pshared, unsigned int value) {
- int res;
-
- res=raw_sem_init(sem,pshared,value);
- return res;
-}
-
-int sem_wait(sem_t *sem) {
- int res;
-
- res = raw_sem_wait(sem);
- return res;
-}
-
-int sem_post(sem_t *sem) {
- return raw_sem_post(sem);
-}
-
int pthread_cond_init(pthread_cond_t *cond, pthread_condattr_t *cond_attr) {
*cond = sg_cond_init();
return 0;
+/* Copyright (c) 2002-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
/* SimGrid's pthread interposer. Intercepts most of the pthread and semaphore calls to model-check them.
*
* Intercepting on pthread is somewhat complicated by the fact that pthread is used everywhere in the system headers.
int sthread_mutex_unlock(sthread_mutex_t* mutex);
int sthread_mutex_destroy(sthread_mutex_t* mutex);
+typedef struct {
+ void* sem;
+} sthread_sem_t;
+int sthread_sem_init(sthread_sem_t* sem, int pshared, unsigned int value);
+int sthread_sem_destroy(sthread_sem_t* sem);
+int sthread_sem_post(sthread_sem_t* sem);
+int sthread_sem_wait(sthread_sem_t* sem);
+int sthread_sem_trywait(sthread_sem_t* sem);
+int sthread_sem_timedwait(sthread_sem_t* sem, const struct timespec* abs_timeout);
+
int sthread_gettimeofday(struct timeval* tv);
void sthread_sleep(double seconds);
+/* Copyright (c) 2002-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
/* SimGrid's pthread interposer. Actual implementation of the symbols (see the comment in sthread.h) */
#include "smpi/smpi.h"
#include <simgrid/s4u/Engine.hpp>
#include <simgrid/s4u/Mutex.hpp>
#include <simgrid/s4u/NetZone.hpp>
+#include <simgrid/s4u/Semaphore.hpp>
#include <xbt/base.h>
#include <xbt/sysdep.h>
intrusive_ptr_release(static_cast<sg4::Mutex*>(mutex->mutex));
return 0;
}
+int sthread_sem_init(sthread_sem_t* sem, int pshared, unsigned int value)
+{
+ auto s = sg4::Semaphore::create(value);
+ intrusive_ptr_add_ref(s.get());
+
+ sem->sem = s.get();
+ return 0;
+}
+int sthread_sem_destroy(sthread_sem_t* sem)
+{
+ intrusive_ptr_release(static_cast<sg4::Semaphore*>(sem->sem));
+ return 0;
+}
+int sthread_sem_post(sthread_sem_t* sem)
+{
+ static_cast<sg4::Semaphore*>(sem->sem)->release();
+ return 0;
+}
+int sthread_sem_wait(sthread_sem_t* sem)
+{
+ static_cast<sg4::Semaphore*>(sem->sem)->acquire();
+ return 0;
+}
+int sthread_sem_trywait(sthread_sem_t* sem)
+{
+ auto* s = static_cast<sg4::Semaphore*>(sem->sem);
+ if (s->would_block()) {
+ errno = EAGAIN;
+ return -1;
+ }
+ s->acquire();
+ return 0;
+}
+int sthread_sem_timedwait(sthread_sem_t* sem, const struct timespec* abs_timeout)
+{
+ if (static_cast<sg4::Semaphore*>(sem->sem)->acquire_timeout(abs_timeout->tv_sec +
+ static_cast<double>(abs_timeout->tv_nsec) / 1E9)) {
+ errno = ETIMEDOUT;
+ return -1;
+ }
+ return 0;
+}
int sthread_gettimeofday(struct timeval* tv)
{
}
#if 0
-int sem_init(sem_t *sem, int pshared, unsigned int value) {
- int res;
-
- res=raw_sem_init(sem,pshared,value);
- return res;
-}
-
-int sem_wait(sem_t *sem) {
- int res;
-
- res = raw_sem_wait(sem);
- return res;
-}
-
-int sem_post(sem_t *sem) {
- return raw_sem_post(sem);
-}
-
int pthread_cond_init(pthread_cond_t *cond, pthread_condattr_t *cond_attr) {
*cond = sg_cond_init();
return 0;
