diff --git a/Makefile.in b/Makefile.in index 88ab4635..09884b8b 100644 --- a/Makefile.in +++ b/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 diff --git a/include/MCConstants.h b/include/MCConstants.h index 0232ca25..b7219228 100644 --- a/include/MCConstants.h +++ b/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) diff --git a/include/MCEnv.h b/include/MCEnv.h index 034d8034..5f4896d7 100644 --- a/include/MCEnv.h +++ b/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" diff --git a/include/MCProgress.h b/include/MCProgress.h new file mode 100644 index 00000000..fd386c2c --- /dev/null +++ b/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 */ + diff --git a/include/MCStack.h b/include/MCStack.h index 93e83068..eccfc81b 100644 --- a/include/MCStack.h +++ b/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; }; diff --git a/include/MCTransition.h b/include/MCTransition.h index a0007112..33dd7bd4 100644 --- a/include/MCTransition.h +++ b/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 diff --git a/include/transitions/misc/MCMiscDefs.h b/include/transitions/misc/MCMiscDefs.h index 1105e6de..3535d4fe 100644 --- a/include/transitions/misc/MCMiscDefs.h +++ b/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 diff --git a/include/transitions/misc/MCProgressTransition.h b/include/transitions/misc/MCProgressTransition.h new file mode 100644 index 00000000..658729dd --- /dev/null +++ b/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 thread) + : MCTransition(thread) + {} + + std::shared_ptr staticCopy() const override; + std::shared_ptr + 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 diff --git a/src/MCStack.cpp b/src/MCStack.cpp index 30245fc6..83a9fa69 100644 --- a/src/MCStack.cpp +++ b/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() { diff --git a/src/launch.c b/src/launch.c index 30b67228..1246d154 100644 --- a/src/launch.c +++ b/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 ]\n" " [--max-transitions-depth-limit|-M ]\n" " (default num = %d)\n" + " [--max-no-progress|-P ]\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); } diff --git a/src/mcmini_private.cpp b/src/mcmini_private.cpp index b52c9fdc..03d7c91a 100644 --- a/src/mcmini_private.cpp +++ b/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,9 +322,15 @@ 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: "); @@ -330,10 +338,12 @@ isInLivelock(uint64_t *increasedDepth) 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())) { diff --git a/src/transitions/misc/MCProgressTransition.cpp b/src/transitions/misc/MCProgressTransition.cpp new file mode 100644 index 00000000..a1c025d1 --- /dev/null +++ b/src/transitions/misc/MCProgressTransition.cpp @@ -0,0 +1,62 @@ +#include "transitions/misc/MCProgressTransition.h" +#include "mcmini_private.h" + +MCTransition* +MCReadProgressTransition(const MCSharedTransition *shm, + void *, MCStack *state) +{ + auto thread = state->getThreadWithId(shm->executor); + return new MCProgressTransition(thread); +} + +std::shared_ptr +MCProgressTransition::staticCopy() const +{ + auto threadCpy = + std::static_pointer_cast( + this->thread->copy()); + return std::make_shared(threadCpy); +} + +std::shared_ptr +MCProgressTransition::dynamicCopyInState(const MCStack *state) const +{ + std::shared_ptr threadInState = + state->getThreadWithId(thread->tid); + return std::make_shared(threadInState); +} + +void +MCProgressTransition::applyToState(MCStack *state) +{ + state->resetNoProgressCount(this->thread->tid); +} + +bool +MCProgressTransition::coenabledWith(const MCTransition *other) const +{ + return true; +} + +bool +MCProgressTransition::dependentWith(const MCTransition *other) const +{ + return false; +} + +MCTransitionUniqueRep +MCProgressTransition::toUniqueRep() const +{ + MCTransitionUniqueRep uniqueRep; + uniqueRep.typeId = MC_PROGRESS_TRANSITION; + uniqueRep.threadId = this->thread->tid; + uniqueRep.param.val[0] = UINT_MAX; + uniqueRep.param.val[1] = UINT_MAX; + return uniqueRep; +} + +void +MCProgressTransition::print() const +{ + mcprintf("thread %lu: PROGRESS\n", thread->tid); +} diff --git a/src/transitions/wrappers/MCThreadTransitionWrappers.cpp b/src/transitions/wrappers/MCThreadTransitionWrappers.cpp index d195a80b..1c84eccc 100644 --- a/src/transitions/wrappers/MCThreadTransitionWrappers.cpp +++ b/src/transitions/wrappers/MCThreadTransitionWrappers.cpp @@ -4,6 +4,7 @@ #include "transitions/MCTransitionsShared.h" #include "transitions/misc/MCAbortTransition.h" #include "transitions/misc/MCExitTransition.h" +#include "transitions/misc/MCProgressTransition.h" #include "transitions/threads/MCThreadCreate.h" #include "transitions/threads/MCThreadFinish.h" #include "transitions/threads/MCThreadJoin.h" @@ -123,3 +124,12 @@ mc_pthread_reach_point() thread_post_visible_operation_hit(typeid(T), &thread); thread_await_scheduler(); } + +extern "C" +__attribute__((visibility("default"))) +void mc_report_progress() +{ + tid_t thread = tid_self; + thread_post_visible_operation_hit(typeid(MCProgressTransition), &thread); + thread_await_scheduler(); +}