LIVELOCK: Implement progress transition

Makefile.in

@@ -20,7 +20,7 @@ LIBOBJS2=src/misc/cond/MCConditionVariableDefaultPolicy.o src/misc/cond/MCCondit
 
 LIBOBJS3=src/objects/MCThread.o src/objects/MCVisibleObject.o src/objects/MCMutex.o src/objects/MCRWLock.o src/objects/MCRWWLock.o src/objects/MCSemaphore.o src/objects/MCGlobalVariable.o src/objects/MCBarrier.o src/objects/MCConditionVariable.o
 
-LIBOBJS4=src/transitions/barrier/MCBarrierEnqueue.o src/transitions/barrier/MCBarrierInit.o src/transitions/barrier/MCBarrierWait.o src/transitions/cond/MCCondBroadcast.o src/transitions/cond/MCCondEnqueue.o src/transitions/cond/MCCondInit.o src/transitions/cond/MCCondSignal.o src/transitions/cond/MCCondWait.o src/transitions/MCTransitionsShared.o src/transitions/misc/MCAbortTransition.o src/transitions/misc/MCExitTransition.o src/transitions/misc/MCGlobalVariableRead.o src/transitions/misc/MCGlobalVariableWrite.o src/transitions/mutex/MCMutexInit.o src/transitions/mutex/MCMutexLock.o src/transitions/mutex/MCMutexUnlock.o src/transitions/semaphore/MCSemEnqueue.o src/transitions/semaphore/MCSemInit.o src/transitions/semaphore/MCSemPost.o src/transitions/semaphore/MCSemWait.o src/transitions/threads/MCThreadCreate.o src/transitions/threads/MCThreadFinish.o src/transitions/threads/MCThreadJoin.o src/transitions/threads/MCThreadStart.o src/transitions/rwlock/MCRWLockInit.o src/transitions/rwlock/MCRWLockReaderLock.o src/transitions/rwlock/MCRWLockWriterLock.o src/transitions/rwlock/MCRWLockUnlock.o src/transitions/rwlock/MCRWLockWriterEnqueue.o src/transitions/rwlock/MCRWLockReaderEnqueue.o src/transitions/rwwlock/MCRWWLockInit.o src/transitions/rwwlock/MCRWWLockReaderEnqueue.o src/transitions/rwwlock/MCRWWLockReaderLock.o src/transitions/rwwlock/MCRWWLockWriter1Enqueue.o src/transitions/rwwlock/MCRWWLockWriter1Lock.o src/transitions/rwwlock/MCRWWLockWriter2Enqueue.o src/transitions/rwwlock/MCRWWLockWriter2Lock.o src/transitions/rwwlock/MCRWWLockUnlock.o src/transitions/wrappers/MCBarrierWrappers.o src/transitions/wrappers/MCConditionVariableWrappers.o src/transitions/wrappers/MCGlobalVariableWrappers.o src/transitions/wrappers/MCMutexTransitionWrappers.o src/transitions/wrappers/MCSemaphoreTransitionWrappers.o src/transitions/wrappers/MCSharedLibraryWrappers.o src/transitions/wrappers/MCThreadTransitionWrappers.o src/transitions/wrappers/MCRWLockWrappers.o src/transitions/wrappers/MCRWWLockWrappers.o
+LIBOBJS4=src/transitions/barrier/MCBarrierEnqueue.o src/transitions/barrier/MCBarrierInit.o src/transitions/barrier/MCBarrierWait.o src/transitions/cond/MCCondBroadcast.o src/transitions/cond/MCCondEnqueue.o src/transitions/cond/MCCondInit.o src/transitions/cond/MCCondSignal.o src/transitions/cond/MCCondWait.o src/transitions/MCTransitionsShared.o src/transitions/misc/MCAbortTransition.o src/transitions/misc/MCExitTransition.o src/transitions/misc/MCProgressTransition.o src/transitions/misc/MCGlobalVariableRead.o src/transitions/misc/MCGlobalVariableWrite.o src/transitions/mutex/MCMutexInit.o src/transitions/mutex/MCMutexLock.o src/transitions/mutex/MCMutexUnlock.o src/transitions/semaphore/MCSemEnqueue.o src/transitions/semaphore/MCSemInit.o src/transitions/semaphore/MCSemPost.o src/transitions/semaphore/MCSemWait.o src/transitions/threads/MCThreadCreate.o src/transitions/threads/MCThreadFinish.o src/transitions/threads/MCThreadJoin.o src/transitions/threads/MCThreadStart.o src/transitions/rwlock/MCRWLockInit.o src/transitions/rwlock/MCRWLockReaderLock.o src/transitions/rwlock/MCRWLockWriterLock.o src/transitions/rwlock/MCRWLockUnlock.o src/transitions/rwlock/MCRWLockWriterEnqueue.o src/transitions/rwlock/MCRWLockReaderEnqueue.o src/transitions/rwwlock/MCRWWLockInit.o src/transitions/rwwlock/MCRWWLockReaderEnqueue.o src/transitions/rwwlock/MCRWWLockReaderLock.o src/transitions/rwwlock/MCRWWLockWriter1Enqueue.o src/transitions/rwwlock/MCRWWLockWriter1Lock.o src/transitions/rwwlock/MCRWWLockWriter2Enqueue.o src/transitions/rwwlock/MCRWWLockWriter2Lock.o src/transitions/rwwlock/MCRWWLockUnlock.o src/transitions/wrappers/MCBarrierWrappers.o src/transitions/wrappers/MCConditionVariableWrappers.o src/transitions/wrappers/MCGlobalVariableWrappers.o src/transitions/wrappers/MCMutexTransitionWrappers.o src/transitions/wrappers/MCSemaphoreTransitionWrappers.o src/transitions/wrappers/MCSharedLibraryWrappers.o src/transitions/wrappers/MCThreadTransitionWrappers.o src/transitions/wrappers/MCRWLockWrappers.o src/transitions/wrappers/MCRWWLockWrappers.o
 
 LIBOBJS=${LIBOBJS1} ${LIBOBJS2} ${LIBOBJS3} ${LIBOBJS4} \
        	src/mc_shared_sem.o src/MCCommon.o src/main.o

include/MCConstants.h

@@ -41,6 +41,13 @@ typedef uint64_t trid_t;
 #define MC_STATE_CONFIG_MAX_DEPTH_PER_THREAD_DEFAULT (UINT64_MAX)
 #define MC_STATE_CONFIG_PRINT_AT_TRACE  (UINT64_MAX)
 
+/**
+ * Default maximum number of transitions per thread, that may
+ * occur without making any progress before the system considers
+ * it a no-progress (livelock-like) situation.
+ */
+#define MAX_NO_PROGRESS_DEFAULT (10)
+
 /* The livelock algorithm for pattern detection uses the following constants:
  *   1. LLOCK_MAX_PATTERN_SIZE: Maximum size that a candidate pattern can grow
  *                              before returning no livelock
@@ -54,7 +61,7 @@ typedef uint64_t trid_t;
  */
 #define LLOCK_MAX_PATTERN_SIZE (20)
 #define LLOCK_MIN_PATTERN_REPEATS (3)
-#define LLOCK_MIN_SCAN_DEPTH (50)
+#define LLOCK_MIN_SCAN_DEPTH (10)
 #define LLOCK_INCREASED_MAX_TRANSITIONS_DEPTH (LLOCK_MAX_PATTERN_SIZE * LLOCK_MIN_PATTERN_REPEATS)
 #define LLOCK_MAX_SCAN_DEPTH (LLOCK_INCREASED_MAX_TRANSITIONS_DEPTH)
 

include/MCEnv.h

@@ -3,6 +3,7 @@
 
 #define ENV_MAX_TRANSITIONS_DEPTH_LIMIT   "MCMINI_MAX_TRANSITIONS_DEPTH_LIMIT"
 #define ENV_MAX_DEPTH_PER_THREAD          "MCMINI_MAX_DEPTH_PER_THREAD"
+#define ENV_MAX_NO_PROGRESS               "MCMINI_MAX_NO_PROGRESS"
 #define ENV_DEBUG_AT_TRACE_ID             "MCMINI_DEBUG_AT_TRACE_ID"
 #define ENV_PRINT_AT_TRACE_ID             "MCMINI_PRINT_AT_TRACE_ID"
 #define ENV_PRINT_AT_TRACE_SEQ            "MCMINI_PRINT_AT_TRACE_SEQ"

include/MCProgress.h

@@ -0,0 +1,28 @@
+#ifndef MCMINI_PROGRESS_H
+#define MCMINI_PROGRESS_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/*
+ * Weak declaration.
+ * If McMini is not present, this resolves to NULL.
+ * If McMini is present, libmcmini.so provides the definition.
+ */
+__attribute__((weak))
+void mc_report_progress(void);
+
+#ifdef __cplusplus
+}
+#endif
+
+void MC_PROGRESS(void)
+{
+    if (mc_report_progress) {
+        mc_report_progress();
+    }
+}
+
+#endif /* MCMINI_PROGRESS_H */
+

include/MCStack.h

@@ -138,6 +138,12 @@ class MCStack {
    */
   MCSortedStack irreversibleStatesStack;
 
+  /**
+   * @brief Counts number of consecutive transitions per thread,
+   * which did not make any progress reports.
+   */
+  int noProgressCount[MAX_TOTAL_THREADS_IN_PROGRAM];
+
 private:
 
   /**
@@ -608,9 +614,12 @@ class MCStack {
   // TODO: De-couple priting from the state stack + transitions
   void printThreadSchedule() const;
   void copyCurrentTraceToArray(MCTransitionUniqueRep* trace_arr, int& trace_len) const;
+  void updateNoProgressCount(tid_t tid);
+  void resetNoProgressCount(tid_t tid);
   void printDebugProgramState();
   void printTransitionStack() const;
   void printNextTransitions() const;
+  void printThreadsWithoutProgress() const;
   void printLivelockResults(int firstCycleIndex, int pattern_len) const;
   void printRepeatingTransitions(int pattern_len) const;
 };

include/MCTransition.h

@@ -48,7 +48,8 @@ enum MCTransitionType {
   MC_GLOBAL_VARIABLE_WRITE,
   MC_GLOBAL_VARIABLE_READ,
   MC_ABORT_TRANSITION,
-  MC_EXIT_TRANSITION
+  MC_EXIT_TRANSITION,
+  MC_PROGRESS_TRANSITION
 };
 
 /* A structure used to store the unique representation

include/transitions/misc/MCMiscDefs.h

@@ -5,5 +5,6 @@
 #include "transitions/misc/MCExitTransition.h"
 #include "transitions/misc/MCGlobalVariableRead.h"
 #include "transitions/misc/MCGlobalVariableWrite.h"
+#include "transitions/misc/MCProgressTransition.h"
 
 #endif // GMAL_GMALMISCDEFS_H

include/transitions/misc/MCProgressTransition.h

@@ -0,0 +1,35 @@
+#ifndef MC_PROGRESS_TRANSITION_H
+#define MC_PROGRESS_TRANSITION_H
+
+#include "MCTransition.h"
+
+/**
+ * Emitted when the target program calls MC_PROGRESS() to explicitly
+ * report progress. Helps detect long per-thread execution without
+ * progress, a prerequisite for livelock.
+ *
+ * NOTE: This is purely a bookkeeping transition that
+ *       should not affect thread interleavings.
+ */
+MCTransition *MCReadProgressTransition(const MCSharedTransition *, void *, MCStack *);
+
+struct MCProgressTransition : public MCTransition {
+public:
+
+  MCProgressTransition(std::shared_ptr<MCThread> thread)
+    : MCTransition(thread)
+  {}
+
+  std::shared_ptr<MCTransition> staticCopy() const override;
+  std::shared_ptr<MCTransition>
+  dynamicCopyInState(const MCStack *) const override;
+
+  void
+  applyToState(MCStack *) override;
+  bool dependentWith(const MCTransition *) const override;
+  bool coenabledWith(const MCTransition *) const override;
+  MCTransitionUniqueRep toUniqueRep() const override;
+  void print() const override;
+};
+
+#endif

src/MCStack.cpp

@@ -637,19 +637,18 @@ MCStack::hasRepetition(const MCTransitionUniqueRep* trace, int trace_len,
 bool
 MCStack::isProgress(const MCTransitionUniqueRep* trace, int trace_len)
 {
-  for (int i = trace_len; i > trace_len - LLOCK_MAX_SCAN_DEPTH; i--) {
-    switch (trace[i].typeId) {
-      case MC_GLOBAL_VARIABLE_WRITE:
-      case MC_THREAD_JOIN:
-      case MC_THREAD_FINISH:
-      case MC_ABORT_TRANSITION:
-      case MC_EXIT_TRANSITION:
-      case MC_THREAD_CREATE:
-        return true;
-      default: continue;
+  int numThreads = programState->getNumProgramThreads();
+  int noProgressThreshold = MAX_NO_PROGRESS_DEFAULT;
+  if (getenv(ENV_MAX_NO_PROGRESS)) {
+    noProgressThreshold = strtoul(getenv(ENV_MAX_NO_PROGRESS), nullptr, 10); 
+  }
+  for (int tid = 0; tid < numThreads; tid++) {
+    if (this->noProgressCount[tid] >= noProgressThreshold) {
+      return false;
     }
   }
-  return false;
+
+  return true;
 }
 
 bool
@@ -1249,6 +1248,24 @@ MCStack::printThreadSchedule() const
   mcprintf("\n");
 }
 
+void
+MCStack::printThreadsWithoutProgress() const
+{
+  int numThreads = programState->getNumProgramThreads();
+  int noProgressThreshold = MAX_NO_PROGRESS_DEFAULT;
+  if (getenv(ENV_MAX_NO_PROGRESS)) {
+    noProgressThreshold = strtoul(getenv(ENV_MAX_NO_PROGRESS), nullptr, 10);
+  }
+
+  mcprintf("\nNO PROGRESS DETECTED IN THREAD(S): ");
+  for (int tid = 0; tid < numThreads; tid++) {
+    if (this->noProgressCount[tid] >= noProgressThreshold) {
+      mcprintf("%lu ", tid);
+    }
+  }
+  mcprintf("\n\n");
+}
+
 void
 MCStack::printLivelockResults(int firstCycleIndex, int pattern_len) const
 {
@@ -1265,6 +1282,7 @@ MCStack::printLivelockResults(int firstCycleIndex, int pattern_len) const
     this->getTransitionAtIndex(i).print();
     i++;
   }
+  this->printThreadsWithoutProgress();
 
   mcprintf("END\n");
   mcflush();
@@ -1296,6 +1314,19 @@ MCStack::copyCurrentTraceToArray(MCTransitionUniqueRep* trace_arr,
   trace_len = i;
 }
 
+void
+MCStack::updateNoProgressCount(tid_t tid)
+{
+    this->noProgressCount[tid]++;
+}
+
+void
+MCStack::resetNoProgressCount(tid_t tid)
+{
+ // mcprintf("thread %lu: PROGRESS\n", tid);
+  this->noProgressCount[tid] = -1;
+}
+
 void
 MCStack::printDebugProgramState()
 {

src/launch.c

@@ -54,6 +54,20 @@ main(int argc, char *argv[])
       setenv(ENV_MAX_TRANSITIONS_DEPTH_LIMIT, cur_arg[0] + 2, 1);
       cur_arg++;
     }
+    else if (strcmp(cur_arg[0], "--max-no-progress") == 0 ||
+        strcmp(cur_arg[0], "-P") == 0) {
+      setenv(ENV_MAX_NO_PROGRESS, cur_arg[1], 1);
+      char *endptr;
+      if (strtol(cur_arg[1], &endptr, 10) == 0 && endptr[0] != '\0') {
+        fprintf(stderr, "%s: illegal value\n", "--max-no-progress");
+        exit(1);
+      }
+      cur_arg += 2;
+    }
+    else if (cur_arg[0][1] == 'P' && isdigit(cur_arg[0][2])) {
+      setenv(ENV_MAX_NO_PROGRESS, cur_arg[0] + 2, 1);
+      cur_arg++;
+    }
     else if (strcmp(cur_arg[0], "--max-depth-per-thread") == 0 ||
         strcmp(cur_arg[0], "-m") == 0) {
       setenv(ENV_MAX_DEPTH_PER_THREAD, cur_arg[1], 1);
@@ -163,10 +177,12 @@ main(int argc, char *argv[])
       fprintf(stderr, "Usage: mcmini [--max-depth-per-thread|-m <num>]\n"
                       "              [--max-transitions-depth-limit|-M <num>]\n"
                       "                               (default num = %d)\n"
+                      "              [--max-no-progress|-P <num>]\n"
+                      "                               (default num = %d)\n"
                       "              [--first-deadlock|--first|-f] (default)\n"
                       "              [--all-deadlocks|--all|-a]\n"
                       "              [--check-for-livelock|-l] (livelock"
-		                       " using round-robin sched.)\n"
+                                     " using round-robin sched.)\n"
                       "                               (experimental)\n"
                       "              [--weak-livelock|--wl|-w]"
                                          " (busy waiting with 1 thread)\n"
@@ -182,7 +198,8 @@ main(int argc, char *argv[])
                       "       (To check data races in target, compile target as in\n" 
                       "        Makefile_llvm in the top level of the McMini source code.)\n",
               MC_STATE_CONFIG_MAX_TRANSITIONS_DEPTH_LIMIT_DEFAULT,
-	      LLOCK_INCREASED_MAX_TRANSITIONS_DEPTH
+              MAX_NO_PROGRESS_DEFAULT,
+              LLOCK_INCREASED_MAX_TRANSITIONS_DEPTH
              );
       exit(1);
     }

src/mcmini_private.cpp

@@ -237,6 +237,8 @@ mc_create_global_state_object()
     typeid(MCGlobalVariableRead), &MCReadGlobalRead);
   programState->registerVisibleOperationType(
     typeid(MCGlobalVariableWrite), &MCReadGlobalWrite);
+  programState->registerVisibleOperationType(typeid(MCProgressTransition),
+                                             &MCReadProgressTransition);
   programState->start();
 }
 
@@ -320,20 +322,28 @@ isInLivelock(uint64_t *increasedDepth)
 
   while (nextTransition != nullptr && transitionId <
          MC_STATE_CONFIG_MAX_TRANSITIONS_DEPTH_LIMIT_DEFAULT) {
+    const int typeId = nextTransition->toUniqueRep().typeId;
     tid_t tid = nextTransition->getThreadId();
+
     mc_run_thread_to_next_visible_operation(tid);
 
+    programState->simulateRunningTransition(
+      *nextTransition, shmTransitionTypeInfo, shmTransitionData);
+
+    programState->updateNoProgressCount(tid);
 
     #ifdef DEBUG
       mcprintf("Program State: ");
       programState->printDebugProgramState();
       nextTransition->print();
     #endif
 
-    programState->simulateRunningTransition(
-      *nextTransition, shmTransitionTypeInfo, shmTransitionData);
-
-    if (checkForWeakLivelock) {
+    if (typeId == MC_PROGRESS_TRANSITION) {
+      // Transition exists only to record progress; reschedule the same
+      // thread to execute its next actual visible operation.
+      nextTransition = &(programState->getNextTransitionForThread(tid));
+    }
+    else if (checkForWeakLivelock) {
       nextTransition = programState->getFirstEnabledTransition();
     }
     else {
@@ -345,22 +355,10 @@ isInLivelock(uint64_t *increasedDepth)
   if (nextTransition == nullptr && !programState->isInDeadlock()) {
     programState->copyCurrentTraceToArray(traceArr, traceLen);
     // FUTURE EXTENSION: User declares progress; no livelock 
-    // hasLivelock = !programState->isProgress(traceArr, traceLen);
-    hasLivelock = programState->hasRepetition(traceArr, traceLen, increasedDepth);
-  }
-  else if (transitionId >= MAX_TOTAL_TRANSITIONS_IN_PROGRAM) {
-    printResults();
-    mcprintf(
-      "*** IsInLivelock:  Execution Limit Reached! ***\n\n"
-      "McMini ran a trace with %lu transitions.  To increase this limit,\n"
-      "modify MAX_TOTAL_TRANSITIONS_IN_PROGRAM in MCConstants.h and"
-      " re-compile.\n"
-      "But first, try running mcmini with the \"--max-depth-per-thread\""
-      " flag (\"-m\")\n"
-      "to limit how far into a trace a McMini thread can go.\n",
-      transitionId);
-    mc_stop_model_checking(EXIT_FAILURE);
+    hasLivelock = !programState->isProgress(traceArr, traceLen) &&
+      programState->hasRepetition(traceArr, traceLen, increasedDepth);
   }
+
   programState->resetMaxTransitionsDepthLimit();
   return hasLivelock;
 }
@@ -666,7 +664,7 @@ mc_search_dpor_branch_with_thread(const tid_t backtrackThread)
 
     depth++;
     transitionId++;
-
+    const int typeId = nextTransition->toUniqueRep().typeId;
     const tid_t tid = nextTransition->getThreadId();
     // Execute in target application
     mc_run_thread_to_next_visible_operation(tid);
@@ -696,7 +694,12 @@ mc_search_dpor_branch_with_thread(const tid_t backtrackThread)
       }
     }
 
-    nextTransition = programState->getFirstEnabledTransition();
+    if (typeId == MC_PROGRESS_TRANSITION) {
+      nextTransition = &(programState->getNextTransitionForThread(tid));
+    }
+    else {
+      nextTransition = programState->getFirstEnabledTransition();
+    }
 
     if (nextTransition == nullptr ||
         (traceSeqLength() > 0 && programState->isInDeadlock())) {