Implement pthread_cond in sthread -- too bad it's TODO in MC

I now have to implement the condition variables in the MC world
(adding the transitions and the dependence theorems), but I first have
to implement the asynchronous version of CV::wait(), as the model
checker can only deal with persistent transitions. That's not a small
assignment, and it will have to wait for tomorrow.

Until then, the pthread_cond support in sthread is somewhat useless.

diff --git a/ChangeLog b/ChangeLog
index e1a85f9..66d4a37 100644 (file)
--- a/ChangeLog
+++ b/ChangeLog
@@ -42,7 +42,7 @@ sthread:
  - Allow to use on valgrind-observed processes
  - Install sthread on user's disk.
  - Implement recursive pthreads.
- - Implement pthread_barrier.
+ - Implement pthread_barrier and pthread_cond.
  - Add some McMini codes to test sthread further (controlled with enable_testsuite_McMini).
 
 Model checking:

diff --git a/src/sthread/sthread.c b/src/sthread/sthread.c
index 6f20733..0bf6c54 100644 (file)
--- a/src/sthread/sthread.c
+++ b/src/sthread/sthread.c
@@ -38,6 +38,12 @@ static int (*raw_pthread_barrier_init)(pthread_barrier_t*, const pthread_barrier
 static int (*raw_pthread_barrier_wait)(pthread_barrier_t*);
 static int (*raw_pthread_barrier_destroy)(pthread_barrier_t*);
 
+static int (*raw_pthread_cond_init)(pthread_cond_t*, const pthread_condattr_t*);
+static int (*raw_pthread_cond_signal)(pthread_cond_t*);
+static int (*raw_pthread_cond_broadcast)(pthread_cond_t*);
+static int (*raw_pthread_cond_wait)(pthread_cond_t*, pthread_mutex_t*);
+static int (*raw_pthread_cond_destroy)(pthread_cond_t*);
+
 static unsigned int (*raw_sleep)(unsigned int);
 static int (*raw_usleep)(useconds_t);
 static int (*raw_gettimeofday)(struct timeval*, void*);
@@ -70,6 +76,12 @@ static void intercepter_init()
   raw_pthread_barrier_wait = dlsym(RTLD_NEXT, "raw_pthread_barrier_wait");
   raw_pthread_barrier_destroy = dlsym(RTLD_NEXT, "raw_pthread_barrier_destroy");
 
+  raw_pthread_cond_init      = dlsym(RTLD_NEXT, "raw_pthread_cond_init");
+  raw_pthread_cond_signal    = dlsym(RTLD_NEXT, "raw_pthread_cond_signal");
+  raw_pthread_cond_broadcast = dlsym(RTLD_NEXT, "raw_pthread_cond_broadcast");
+  raw_pthread_cond_wait      = dlsym(RTLD_NEXT, "raw_pthread_cond_wait");
+  raw_pthread_cond_destroy   = dlsym(RTLD_NEXT, "raw_pthread_cond_destroy");
+
   raw_sleep        = dlsym(RTLD_NEXT, "sleep");
   raw_usleep       = dlsym(RTLD_NEXT, "usleep");
   raw_gettimeofday = dlsym(RTLD_NEXT, "gettimeofday");
@@ -134,6 +146,14 @@ intercepted_pthcall(barrier_init, (pthread_barrier_t * barrier, const pthread_ba
 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));
 
+intercepted_pthcall(cond_init, (pthread_cond_t * cond, const pthread_condattr_t* attr), (cond, attr),
+                    ((sthread_cond_t*)cond, (sthread_condattr_t*)attr));
+intercepted_pthcall(cond_signal, (pthread_cond_t * cond), (cond), ((sthread_cond_t*)cond));
+intercepted_pthcall(cond_broadcast, (pthread_cond_t * cond), (cond), ((sthread_cond_t*)cond));
+intercepted_pthcall(cond_wait, (pthread_cond_t * cond, pthread_mutex_t* mutex), (cond, mutex),
+                    ((sthread_cond_t*)cond, (sthread_mutex_t*)mutex));
+intercepted_pthcall(cond_destroy, (pthread_cond_t * cond), (cond), ((sthread_cond_t*)cond));
+
 #define intercepted_call(rettype, name, raw_params, call_params, sim_params)                                           \
   rettype name raw_params                                                                                              \
   {                                                                                                                    \
@@ -171,33 +191,6 @@ intercepted_call(int, gettimeofday, (struct timeval * tv, XBT_ATTRIB_UNUSED TIME
 intercepted_call(unsigned int, sleep, (unsigned int seconds), (seconds), (seconds));
 intercepted_call(int, usleep, (useconds_t usec), (usec), (((double)usec) / 1000000.));
 
-#if 0
-int pthread_cond_init(pthread_cond_t *cond, pthread_condattr_t *cond_attr) {
-    *cond = sg_cond_init();
-    return 0;
-}
-
-int pthread_cond_signal(pthread_cond_t *cond) {
-       sg_cond_notify_one(*cond);
-    return 0;
-}
-
-int pthread_cond_broadcast(pthread_cond_t *cond) {
-       sg_cond_notify_all(*cond);
-    return 0;
-}
-
-int pthread_cond_wait(pthread_cond_t *cond, pthread_mutex_t *mutex) {
-       sg_cond_wait(*cond, *mutex);
-    return 0;
-}
-
-int pthread_cond_destroy(pthread_cond_t *cond) {
-       sg_cond_destroy(*cond);
-    return 0;
-}
-#endif
-
 /* Trampoline for the real main() */
 static int (*raw_main)(int, char**, char**);
 

diff --git a/src/sthread/sthread.h b/src/sthread/sthread.h
index 6d9c0fa..8447d97 100644 (file)
--- a/src/sthread/sthread.h
+++ b/src/sthread/sthread.h
@@ -63,6 +63,19 @@ int sthread_barrier_init(sthread_barrier_t* barrier, const sthread_barrierattr_t
 int sthread_barrier_wait(sthread_barrier_t* barrier);
 int sthread_barrier_destroy(sthread_barrier_t* barrier);
 
+typedef struct {
+  unsigned unused : 1;
+} sthread_condattr_t;
+
+typedef struct {
+  void* cond;
+} sthread_cond_t;
+int sthread_cond_init(sthread_cond_t* cond, sthread_condattr_t* attr);
+int sthread_cond_signal(sthread_cond_t* cond);
+int sthread_cond_broadcast(sthread_cond_t* cond);
+int sthread_cond_wait(sthread_cond_t* cond, sthread_mutex_t* mutex);
+int sthread_cond_destroy(sthread_cond_t* cond);
+
 typedef struct {
   void* sem;
 } sthread_sem_t;

diff --git a/src/sthread/sthread_impl.cpp b/src/sthread/sthread_impl.cpp
index fda1411..063d265 100644 (file)
--- a/src/sthread/sthread_impl.cpp
+++ b/src/sthread/sthread_impl.cpp
@@ -6,6 +6,7 @@
 /* SimGrid's pthread interposer. Actual implementation of the symbols (see the comment in sthread.h) */
 
 #include "simgrid/s4u/Barrier.hpp"
+#include "simgrid/s4u/ConditionVariable.hpp"
 #include "smpi/smpi.h"
 #include "xbt/asserts.h"
 #include "xbt/ex.h"
@@ -238,6 +239,39 @@ int sthread_barrier_destroy(sthread_barrier_t* barrier){
   return 0;
 }
 
+int sthread_cond_init(sthread_cond_t* cond, sthread_condattr_t* attr)
+{
+  auto cv = sg4::ConditionVariable::create();
+  intrusive_ptr_add_ref(cv.get());
+
+  cond->cond = cv.get();
+  return 0;
+}
+int sthread_cond_signal(sthread_cond_t* cond)
+{
+  XBT_DEBUG("%s(%p)", __func__, cond);
+  static_cast<sg4::ConditionVariable*>(cond->cond)->notify_one();
+  return 0;
+}
+int sthread_cond_broadcast(sthread_cond_t* cond)
+{
+  XBT_DEBUG("%s(%p)", __func__, cond);
+  static_cast<sg4::ConditionVariable*>(cond->cond)->notify_all();
+  return 0;
+}
+int sthread_cond_wait(sthread_cond_t* cond, sthread_mutex_t* mutex)
+{
+  XBT_DEBUG("%s(%p)", __func__, cond);
+  static_cast<sg4::ConditionVariable*>(cond->cond)->wait(static_cast<sg4::Mutex*>(mutex->mutex));
+  return 0;
+}
+int sthread_cond_destroy(sthread_cond_t* cond)
+{
+  XBT_DEBUG("%s(%p)", __func__, cond);
+  intrusive_ptr_release(static_cast<sg4::ConditionVariable*>(cond->cond));
+  return 0;
+}
+
 int sthread_sem_init(sthread_sem_t* sem, int /*pshared*/, unsigned int value)
 {
   auto s = sg4::Semaphore::create(value);

diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt
index 41cad5e..1209bc0 100644 (file)
--- a/teshsuite/mc/CMakeLists.txt
+++ b/teshsuite/mc/CMakeLists.txt
@@ -46,8 +46,17 @@ endif()
 
 
 foreach(x
-#              
-#             simple_cond_broadcast_deadlock   simple_barrier_deadlock  simple_cond_deadlock
+            simple_barrier_ok              simple_barrier_deadlock
+            simple_barrier_with_threads_ok simple_barrier_with_threads_deadlock
+
+#            simple_cond_ok 
+
+#            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_mutex_with_threads_ok simple_mutex_with_threads_deadlock
 
@@ -56,7 +65,6 @@ foreach(x
              simple_semaphores_with_threads_ok simple_semaphores_with_threads_deadlock
 #                   
 #                   philosophers_spurious_deadlock
-#                   simple_cond_broadcast_with_semaphore_deadlock1  simple_cond_broadcast_with_semaphore_deadlock2
             
              barber_shop_ok             barber_shop_deadlock
              philosophers_semaphores_ok philosophers_semaphores_deadlock
@@ -65,12 +73,6 @@ foreach(x
              
              
              # producer_consumer_spurious_nok # infinite no-op loop
-             
-             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
              )
 
   set(teshsuite_src  ${teshsuite_src} ${CMAKE_CURRENT_SOURCE_DIR}/mcmini/${x}.c)