DeterministicSchedule support for global invariants and auxiliary variables

Summary:
Support for user-defined auxiliary variables and global invariants.
- Add two fields to DSched:
  -- tls_aux: static FOLLY_TLS std::function<void(uint64_t, bool)>*. User-defined auxiliary function with parameters: count of synchronization steps, and boolean indicator of the success of the current step.
  -- step_: uint64_t. Count of shared accesses that correspond to user synchronization steps (atomic accesses for now).
- Add two static functions to DSched:
  -- void setAux(std::function<void(uint64_t, bool)>*).
  -- void callAux(bool success). Calls the aux function with the step count and the bool success argument.
- Add a version of afterSharedAccess(bool) that takes a bool success parameter and calls callAux(success). This version is used in every atomic operation of DeterministicAtomic.
- Add direct load interface to  DeterministicAtomic for use by auxiliary functions.

Note: This the base of a stacked diff with:
- Test the new capabilities in DeterministicScheduleTest.h
Next steps:
- Use the new capabilities to test dynamic MPMCQueue
Other possible additions:
- Change the implementation of DeterministicMutex to allow inspecting its internal state.
- Test the new capabilities for mutexes and semaphores in DeterministicScheduleTest.h
- Performance optimization: e.g., user-space context switching, using regular variables to implements atomics.

Reviewed By: djwatson

Differential Revision: D3648146

fbshipit-source-id: 4f838ff7cfd41ab71cfdf22bb67def3221948311

diff --git a/folly/test/DeterministicSchedule.cpp b/folly/test/DeterministicSchedule.cpp
index f7668fc587e5bd68d9270683f3b2e0c8007bafc8..e282aaff34ee0b7f6eb8b237dcc655ab2350accd 100644 (file)
--- a/folly/test/DeterministicSchedule.cpp
+++ b/folly/test/DeterministicSchedule.cpp
@@ -33,6 +33,7 @@ namespace test {
 FOLLY_TLS sem_t* DeterministicSchedule::tls_sem;
 FOLLY_TLS DeterministicSchedule* DeterministicSchedule::tls_sched;
 FOLLY_TLS unsigned DeterministicSchedule::tls_threadId;
+FOLLY_TLS std::function<void(uint64_t, bool)>* DeterministicSchedule::tls_aux;
 
 // access is protected by futexLock
 static std::unordered_map<detail::Futex<DeterministicAtomic>*,
@@ -42,9 +43,10 @@ static std::mutex futexLock;
 
 DeterministicSchedule::DeterministicSchedule(
     const std::function<int(int)>& scheduler)
-    : scheduler_(scheduler), nextThreadId_(1) {
+    : scheduler_(scheduler), nextThreadId_(1), step_(0) {
   assert(tls_sem == nullptr);
   assert(tls_sched == nullptr);
+  assert(tls_aux == nullptr);
 
   tls_sem = new sem_t;
   sem_init(tls_sem, 0, 1);
@@ -133,7 +135,15 @@ void DeterministicSchedule::afterSharedAccess() {
   if (!sched) {
     return;
   }
+  sem_post(sched->sems_[sched->scheduler_(sched->sems_.size())]);
+}
 
+void DeterministicSchedule::afterSharedAccess(bool success) {
+  auto sched = tls_sched;
+  if (!sched) {
+    return;
+  }
+  sched->callAux(success);
   sem_post(sched->sems_[sched->scheduler_(sched->sems_.size())]);
 }
 
@@ -161,6 +171,10 @@ int DeterministicSchedule::getcpu(unsigned* cpu,
   return 0;
 }
 
+void DeterministicSchedule::setAux(std::function<void(uint64_t, bool)>& aux) {
+  tls_aux = &aux;
+}
+
 sem_t* DeterministicSchedule::beforeThreadCreate() {
   sem_t* s = new sem_t;
   sem_init(s, 0, 0);
@@ -216,6 +230,16 @@ void DeterministicSchedule::join(std::thread& child) {
   child.join();
 }
 
+void DeterministicSchedule::callAux(bool success) {
+  ++step_;
+  auto aux = tls_aux;
+  if (!aux) {
+    return;
+  }
+  (*aux)(step_, success);
+  tls_aux = nullptr;
+}
+
 void DeterministicSchedule::post(sem_t* sem) {
   beforeSharedAccess();
   sem_post(sem);

diff --git a/folly/test/DeterministicSchedule.h b/folly/test/DeterministicSchedule.h
index 762d337fb0dbf5bcc3117c297d339a71d4f95ec7..c367152d4bccd1695f4e67f82c8042529b73c736 100644 (file)
--- a/folly/test/DeterministicSchedule.h
+++ b/folly/test/DeterministicSchedule.h
@@ -111,6 +111,12 @@ class DeterministicSchedule : boost::noncopyable {
    *  communication. */
   static void afterSharedAccess();
 
+  /** Calls a user-defined auxiliary function if any, and releases
+   *  permission for the current thread to perform inter-thread
+   *  communication. The bool parameter indicates the success of the
+   *  shared access (if conditional, true otherwise). */
+  static void afterSharedAccess(bool success);
+
   /** Launches a thread that will participate in the same deterministic
    *  schedule as the current thread. */
   template <typename Func, typename... Args>
@@ -161,19 +167,37 @@ class DeterministicSchedule : boost::noncopyable {
   /** Deterministic implemencation of getcpu */
   static int getcpu(unsigned* cpu, unsigned* node, void* unused);
 
+  /** Sets up a thread-specific function for call immediately after
+   *  the next shared access for managing auxiliary data and checking
+   *  global invariants. The parameters of the function are: a
+   *  uint64_t that indicates the step number (i.e., the number of
+   *  shared accesses so far), and a bool that indicates the success
+   *  of the shared access (if it is conditional, true otherwise). */
+  static void setAux(std::function<void(uint64_t, bool)>& aux);
+
  private:
   static FOLLY_TLS sem_t* tls_sem;
   static FOLLY_TLS DeterministicSchedule* tls_sched;
   static FOLLY_TLS unsigned tls_threadId;
+  static FOLLY_TLS std::function<void(uint64_t, bool)>* tls_aux;
 
   std::function<int(int)> scheduler_;
   std::vector<sem_t*> sems_;
   std::unordered_set<std::thread::id> active_;
   unsigned nextThreadId_;
+  /* step_ keeps count of shared accesses that correspond to user
+   * synchronization steps (atomic accesses for now).
+   * The reason for keeping track of this here and not just with
+   * auxiliary data is to provide users with warning signs (e.g.,
+   * skipped steps) if they inadvertently forget to set up aux
+   * functions for some shared accesses. */
+  uint64_t step_;
 
   sem_t* beforeThreadCreate();
   void afterThreadCreate(sem_t*);
   void beforeThreadExit();
+  /** Calls user-defined auxiliary function (if any) */
+  void callAux(bool);
 };
 
 /**
@@ -201,7 +225,7 @@ struct DeterministicAtomic {
     FOLLY_TEST_DSCHED_VLOG(this << ".compare_exchange_strong(" << std::hex
                                 << orig << ", " << std::hex << v1 << ") -> "
                                 << rv << "," << std::hex << v0);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(rv);
     return rv;
   }
 
@@ -213,7 +237,7 @@ struct DeterministicAtomic {
     FOLLY_TEST_DSCHED_VLOG(this << ".compare_exchange_weak(" << std::hex << orig
                                 << ", " << std::hex << v1 << ") -> " << rv
                                 << "," << std::hex << v0);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(rv);
     return rv;
   }
 
@@ -222,7 +246,7 @@ struct DeterministicAtomic {
     T rv = data.exchange(v, mo);
     FOLLY_TEST_DSCHED_VLOG(this << ".exchange(" << std::hex << v << ") -> "
                                 << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -230,7 +254,7 @@ struct DeterministicAtomic {
     DeterministicSchedule::beforeSharedAccess();
     T rv = data;
     FOLLY_TEST_DSCHED_VLOG(this << "() -> " << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -238,7 +262,7 @@ struct DeterministicAtomic {
     DeterministicSchedule::beforeSharedAccess();
     T rv = data.load(mo);
     FOLLY_TEST_DSCHED_VLOG(this << ".load() -> " << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -246,7 +270,7 @@ struct DeterministicAtomic {
     DeterministicSchedule::beforeSharedAccess();
     T rv = (data = v);
     FOLLY_TEST_DSCHED_VLOG(this << " = " << std::hex << v);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -254,14 +278,14 @@ struct DeterministicAtomic {
     DeterministicSchedule::beforeSharedAccess();
     data.store(v, mo);
     FOLLY_TEST_DSCHED_VLOG(this << ".store(" << std::hex << v << ")");
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
   }
 
   T operator++() noexcept {
     DeterministicSchedule::beforeSharedAccess();
     T rv = ++data;
     FOLLY_TEST_DSCHED_VLOG(this << " pre++ -> " << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -269,7 +293,7 @@ struct DeterministicAtomic {
     DeterministicSchedule::beforeSharedAccess();
     T rv = data++;
     FOLLY_TEST_DSCHED_VLOG(this << " post++ -> " << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -277,7 +301,7 @@ struct DeterministicAtomic {
     DeterministicSchedule::beforeSharedAccess();
     T rv = --data;
     FOLLY_TEST_DSCHED_VLOG(this << " pre-- -> " << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -285,7 +309,7 @@ struct DeterministicAtomic {
     DeterministicSchedule::beforeSharedAccess();
     T rv = data--;
     FOLLY_TEST_DSCHED_VLOG(this << " post-- -> " << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -294,7 +318,7 @@ struct DeterministicAtomic {
     T rv = (data += v);
     FOLLY_TEST_DSCHED_VLOG(this << " += " << std::hex << v << " -> " << std::hex
                                 << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -305,7 +329,7 @@ struct DeterministicAtomic {
     data += v;
     FOLLY_TEST_DSCHED_VLOG(this << ".fetch_add(" << std::hex << v << ") -> "
                                 << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -314,7 +338,7 @@ struct DeterministicAtomic {
     T rv = (data -= v);
     FOLLY_TEST_DSCHED_VLOG(this << " -= " << std::hex << v << " -> " << std::hex
                                 << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -325,7 +349,7 @@ struct DeterministicAtomic {
     data -= v;
     FOLLY_TEST_DSCHED_VLOG(this << ".fetch_sub(" << std::hex << v << ") -> "
                                 << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -334,7 +358,7 @@ struct DeterministicAtomic {
     T rv = (data &= v);
     FOLLY_TEST_DSCHED_VLOG(this << " &= " << std::hex << v << " -> " << std::hex
                                 << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -345,7 +369,7 @@ struct DeterministicAtomic {
     data &= v;
     FOLLY_TEST_DSCHED_VLOG(this << ".fetch_and(" << std::hex << v << ") -> "
                                 << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -354,7 +378,7 @@ struct DeterministicAtomic {
     T rv = (data |= v);
     FOLLY_TEST_DSCHED_VLOG(this << " |= " << std::hex << v << " -> " << std::hex
                                 << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -365,7 +389,7 @@ struct DeterministicAtomic {
     data |= v;
     FOLLY_TEST_DSCHED_VLOG(this << ".fetch_or(" << std::hex << v << ") -> "
                                 << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -374,7 +398,7 @@ struct DeterministicAtomic {
     T rv = (data ^= v);
     FOLLY_TEST_DSCHED_VLOG(this << " ^= " << std::hex << v << " -> " << std::hex
                                 << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
 
@@ -385,9 +409,14 @@ struct DeterministicAtomic {
     data ^= v;
     FOLLY_TEST_DSCHED_VLOG(this << ".fetch_xor(" << std::hex << v << ") -> "
                                 << std::hex << rv);
-    DeterministicSchedule::afterSharedAccess();
+    DeterministicSchedule::afterSharedAccess(true);
     return rv;
   }
+
+  /** Read the value of the atomic variable without context switching */
+  T load_direct() const noexcept {
+    return data.load(std::memory_order_relaxed);
+  }
 };
 
 /**