Integrate DMCTP into McMini

.clang-tidy

@@ -1,20 +1,32 @@
-Checks: '-*,clang-diagnostic-*,llvm-*,misc-*,-misc-unused-parameters-misc-non-private-member-variables-in-classes,readability-identifier-naming'
+---
+Checks:          'clang-diagnostic-*,clang-analyzer-*'
+WarningsAsErrors: ''
+HeaderFileExtensions:
+  - ''
+  - h
+  - hh
+  - hpp
+  - hxx
+ImplementationFileExtensions:
+  - c
+  - cc
+  - cpp
+  - cxx
+HeaderFilterRegex: ''
+AnalyzeTemporaryDtors: false
+FormatStyle:     none
 CheckOptions:
-  - key:             readability-identifier-naming.ClassCase
-    value:           CamelCase
-  - key:             readability-identifier-naming.EnumCase
-    value:           CamelCase
-  - key:             readability-identifier-naming.FunctionCase
-    value:           camelBack
-  - key:             readability-identifier-naming.MemberCase
-    value:           camelBack
-  - key:             readability-identifier-naming.ParameterCase
-    value:           camelBack
-  - key:             readability-identifier-naming.UnionCase
-    value:           CamelCase
-  - key:             readability-identifier-naming.VariableCase
-    value:           camelBack
-  - key:             readability-identifier-naming.NamespaceCase
-    value:           lower_case
-  - key:             readability-identifier-naming.InlineNamespaceCase
-    value:           lower_case
+  cert-dcl16-c.NewSuffixes: 'L;LL;LU;LLU'
+  google-readability-namespace-comments.ShortNamespaceLines: '10'
+  cert-err33-c.CheckedFunctions: '::aligned_alloc;::asctime_s;::at_quick_exit;::atexit;::bsearch;::bsearch_s;::btowc;::c16rtomb;::c32rtomb;::calloc;::clock;::cnd_broadcast;::cnd_init;::cnd_signal;::cnd_timedwait;::cnd_wait;::ctime_s;::fclose;::fflush;::fgetc;::fgetpos;::fgets;::fgetwc;::fopen;::fopen_s;::fprintf;::fprintf_s;::fputc;::fputs;::fputwc;::fputws;::fread;::freopen;::freopen_s;::fscanf;::fscanf_s;::fseek;::fsetpos;::ftell;::fwprintf;::fwprintf_s;::fwrite;::fwscanf;::fwscanf_s;::getc;::getchar;::getenv;::getenv_s;::gets_s;::getwc;::getwchar;::gmtime;::gmtime_s;::localtime;::localtime_s;::malloc;::mbrtoc16;::mbrtoc32;::mbsrtowcs;::mbsrtowcs_s;::mbstowcs;::mbstowcs_s;::memchr;::mktime;::mtx_init;::mtx_lock;::mtx_timedlock;::mtx_trylock;::mtx_unlock;::printf_s;::putc;::putwc;::raise;::realloc;::remove;::rename;::scanf;::scanf_s;::setlocale;::setvbuf;::signal;::snprintf;::snprintf_s;::sprintf;::sprintf_s;::sscanf;::sscanf_s;::strchr;::strerror_s;::strftime;::strpbrk;::strrchr;::strstr;::strtod;::strtof;::strtoimax;::strtok;::strtok_s;::strtol;::strtold;::strtoll;::strtoul;::strtoull;::strtoumax;::strxfrm;::swprintf;::swprintf_s;::swscanf;::swscanf_s;::thrd_create;::thrd_detach;::thrd_join;::thrd_sleep;::time;::timespec_get;::tmpfile;::tmpfile_s;::tmpnam;::tmpnam_s;::tss_create;::tss_get;::tss_set;::ungetc;::ungetwc;::vfprintf;::vfprintf_s;::vfscanf;::vfscanf_s;::vfwprintf;::vfwprintf_s;::vfwscanf;::vfwscanf_s;::vprintf_s;::vscanf;::vscanf_s;::vsnprintf;::vsnprintf_s;::vsprintf;::vsprintf_s;::vsscanf;::vsscanf_s;::vswprintf;::vswprintf_s;::vswscanf;::vswscanf_s;::vwprintf_s;::vwscanf;::vwscanf_s;::wcrtomb;::wcschr;::wcsftime;::wcspbrk;::wcsrchr;::wcsrtombs;::wcsrtombs_s;::wcsstr;::wcstod;::wcstof;::wcstoimax;::wcstok;::wcstok_s;::wcstol;::wcstold;::wcstoll;::wcstombs;::wcstombs_s;::wcstoul;::wcstoull;::wcstoumax;::wcsxfrm;::wctob;::wctrans;::wctype;::wmemchr;::wprintf_s;::wscanf;::wscanf_s;'
+  llvm-else-after-return.WarnOnUnfixable: 'false'
+  cert-str34-c.DiagnoseSignedUnsignedCharComparisons: 'false'
+  google-readability-namespace-comments.SpacesBeforeComments: '2'
+  cppcoreguidelines-non-private-member-variables-in-classes.IgnoreClassesWithAllMemberVariablesBeingPublic: 'true'
+  google-readability-braces-around-statements.ShortStatementLines: '1'
+  google-readability-function-size.StatementThreshold: '800'
+  llvm-qualified-auto.AddConstToQualified: 'false'
+  llvm-else-after-return.WarnOnConditionVariables: 'false'
+  cert-oop54-cpp.WarnOnlyIfThisHasSuspiciousField: 'false'
+SystemHeaders:   false
+...

.pre-commit-config.yaml

@@ -1,6 +1,8 @@
 repos:
   - repo: https://github.com/pre-commit/pre-commit-hooks
-    rev: v4.3.0
+    rev: v4.6.0
     hooks:
       - id: trailing-whitespace
-      - id: check-added-large-files
+      - id: check-added-large-files
+      - id: check-case-conflict
+      - id: end-of-file-fixer

dmtcp/BUG.README

@@ -0,0 +1,7 @@
+Sept. 21, 2024
+
+export LD_LIBRARY_PATH=/home/gene/dmtcp.git/lib/dmtcp
+
+~/dmtcp.git/bin/dmtcp_launch -i3 --disable-alloc-plugin --with-plugin ~/mcmini-pirtle/dmtcp/build/libmcmini.so ./src/examples/hello-world &
+
+dmtcp_commnd -c

dmtcp/CMakeLists.txt

@@ -0,0 +1,122 @@
+cmake_minimum_required(VERSION 3.10)
+project(McMini-Revamp
+    VERSION 1.0.0
+    DESCRIPTION "A bite-sized model checker"
+    LANGUAGES C CXX)
+
+# Require C11 and C++11
+set(CMAKE_C_STANDARD 11)
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
+set(CMAKE_C_STANDARD_REQUIRED TRUE)
+set(CMAKE_CXX_STANDARD_REQUIRED TRUE)
+
+# Project configuration
+option(BUILD_TESTS OFF)
+option(VERBOSE_TESTING OFF)
+set(MCMINI_DIR "${CMAKE_SOURCE_DIR}")
+set(MCMINI_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/include")
+set(MCMINI_CMAKE_MODULE_DIR "${CMAKE_SOURCE_DIR}/cmake")
+set(MCMINI_WITH_DMTCP OFF)
+
+# Project source files
+set(MCMINI_C_SRC
+  src/common/exit.c
+  src/common/mem.c
+  src/common/runner_mailbox.c
+  src/common/shm_config.c
+)
+set(MCMINI_CPP_SRC
+  src/mcmini/mcmini.cpp
+  src/mcmini/constants.cpp
+  src/mcmini/signal.cpp
+  src/mcmini/visible_object.cpp
+  src/mcmini/coordinator/coordinator.cpp
+  src/mcmini/log/filter.cpp
+  src/mcmini/log/logger.cpp
+  src/mcmini/model/detached_state.cpp
+  src/mcmini/model/diff_state.cpp
+  src/mcmini/model/program.cpp
+  src/mcmini/model/cond_var_arbitrary_policy.cpp
+  src/mcmini/model/cond_var_default_policy.cpp
+  src/mcmini/model/cond_var_single_grp_policy.cpp
+  src/mcmini/model/cond_var_wakegroup.cpp
+  src/mcmini/model/state_sequence.cpp
+  src/mcmini/model/transition_registry.cpp
+  src/mcmini/model/transition_sequence.cpp
+  src/mcmini/model/transitions/condition_variables.cpp
+  src/mcmini/model/transitions/mutex.cpp
+  src/mcmini/model/transitions/process.cpp
+  src/mcmini/model/transitions/thread.cpp
+  src/mcmini/model/transitions/semaphore.cpp
+  src/mcmini/model_checking/algorithms/classic_dpor.cpp
+  src/mcmini/model_checking/algorithms/clock_vector.cpp
+  src/mcmini/real_world/dmtcp_process_source.cpp
+  src/mcmini/real_world/fifo.cpp
+  src/mcmini/real_world/fork_process_source.cpp
+  src/mcmini/real_world/local_linux_process.cpp
+  src/mcmini/real_world/resources.cpp
+  src/mcmini/real_world/shm.cpp
+  src/mcmini/real_world/target.cpp
+)
+set(LIBMCMINI_C_SRC
+  src/common/exit.c
+  src/common/mem.c
+  src/common/multithreaded_fork.c
+  src/common/runner_mailbox.c
+  src/common/shm_config.c
+  src/lib/dmtcp-callback.c
+  src/lib/entry.c
+  src/lib/interception.c
+  src/lib/log.c
+  src/lib/main.c
+  src/lib/record.c
+  src/lib/sem-wrappers.c
+  src/lib/template/loop.c
+  src/lib/template/sig.c
+  src/lib/wrappers.c
+  src/mcmini/Thread_queue.c
+)
+
+set(MCMINI_EXTRA_COMPILER_FLAGS -Wall -Werror)
+set(MCMINI_EXTRA_COMPILER_DEFINITIONS "")
+set(MCMINI_EXTRA_LINK_FLAGS -lrt -pthread)
+
+set(LIBMCMINI_EXTRA_COMPILER_FLAGS -Wall -Werror -fPIC)
+set(LIBMCMINI_EXTRA_COMPILER_DEFINITIONS MC_SHARED_LIBRARY=1 DMTCP=1 LOGGING_ROOT="${CMAKE_SOURCE_PATH}")
+
+# -lrt -> shared memory
+# -pthread -> libpthread.so
+# -lm -> math library
+# -ldl -> dlsym etc.
+set(LIBMCMINI_EXTRA_LINK_FLAGS -lrt -pthread -lm -ldl)
+
+# libmcmini.so -> the dylib which is loaded
+add_library(libmcmini SHARED "${LIBMCMINI_C_SRC}")
+set_target_properties(libmcmini PROPERTIES OUTPUT_NAME "mcmini")
+
+target_include_directories(libmcmini PUBLIC "${MCMINI_INCLUDE_DIR}")
+target_compile_definitions(libmcmini
+  PUBLIC
+    "${LIBMCMINI_EXTRA_COMPILER_DEFINITIONS}")
+target_compile_options(libmcmini
+  PRIVATE
+    "${LIBMCMINI_EXTRA_COMPILER_FLAGS}")
+target_link_libraries(libmcmini
+  PUBLIC
+    "${LIBMCMINI_EXTRA_LINK_FLAGS}")
+
+add_executable(mcmini "${MCMINI_CPP_SRC}" "${MCMINI_C_SRC}")
+target_include_directories(mcmini PUBLIC "${MCMINI_INCLUDE_DIR}")
+target_compile_definitions(mcmini
+  PUBLIC
+    "${MCMINI_EXTRA_COMPILER_DEFINITIONS}")
+target_compile_options(mcmini
+  PRIVATE
+    "${MCMINI_EXTRA_COMPILER_FLAGS}")
+target_link_libraries(mcmini
+  PUBLIC
+    "${MCMINI_EXTRA_LINK_FLAGS}")
+
+add_subdirectory(src/examples)
+add_subdirectory(test)

dmtcp/Cond_Var_Readme.md

@@ -0,0 +1,118 @@
+This document provides a detailed explanation of the algorithm used to manage condition variables 
+to support checkpoint and replay and model checking at restart time.
+
+## Thread State Tracking in Condition Variables
+Each condition variable maintains a waiting_threads queue. The queue contains thread_queue_node entries that store:
+- The thread's ID (runner_id_t)
+- The thread's condition variable state (thread_cv_state)
+## Recording Phase
+Track condition variable states and thread queus to enable replay at restart time.
+Each state in condition_variable_state corresponds to a phase in the lifescycle
+  of a condition variable. The status of a condition variable can be one of the following:
+  - CV_UNINITIALIZED: The condition variable has not been initialized yet via mc_pthread_cond_init.
+  - CV_INITIALIZED: The condition variable has been initialized and ready for use (post mc_pthread_cond_init).
+  - CV_PREWAITING: A thread is releasing the mutex but hasn't fully entered the wait state yet
+  (mc_pthread_cond_wait in progress), hence entered outer waiting room. This prevents checkpointing during the 
+  unsafe gap between mutex unlock and wait.
+  - CV_WAITING: The thread has successfully entered the wait state i.e, consumed the signal or successfully returned
+  from libpthread_cond_timed_wait. (mc_pthread_cond_wait).
+  - CV_SIGNALED: A signal/broadcast has been sent; the condition variable resumes operation (mc_pthread_cond_signal/broadcast).
+  - CV_DESTROYED: The condition variable has been destroyed (post mc_pthread_cond_destroy).
+  Note that the status of a condition variable can be CV_SIGNALED even when there are no threads waiting on it.
+  This is because a thread can signal a condition variable even when no threads are waiting on it (spurious wakeup).
+
+## Thread State Transitions
+
+When a thread calls pthread_cond_wait():
+- It's added to the waiting queue with state CV_PREWAITING. 
+- After successfully entering wait, its state changes to CV_WAITING. 
+
+When signaled:
+- Its state changes to CV_SIGNALED
+- The thread eventually dequeues and processes the signal
+
+## Lost Wakeup Tracking
+
+- The system tracks lost wakeups when signals are sent to condition variables with no waiting threads.
+- These are recorded to ensure correct reconstruction during restart. 
+
+## Serializing Thread-Condition Relationships
+The system uses a two-level approach to serialize thread relationships:
+
+### CV_WAITERS_QUEUE Entries
+
+- For each thread in a condition variable's waiting queue, a specialized entry is created. 
+- Contains: condition variable location, thread ID, and thread's CV state
+- This preserves the complete thread queue state including waiting order
+
+### State Preservation
+
+- During serialization, the system traverses each condition variable's waiting queue. 
+- For each thread, it records its specific relationship with the condition variable.
+- This enables accurate reconstruction during deserialization. 
+
+## Post-Restart Thread State Reconstruction
+During restart, the system reconstructs condition variable states and thread relationships:
+
+### Creating State Map
+
+- CV_WAITERS_QUEUE entries are processed to build a cv_waiting_threads map
+- Maps each condition variable address to an ordered list of (thread_id, cv_state) pairs
+
+### Policy-Based Management
+- Each condition variable has a policy object (ConditionVariableArbitraryPolicy) that:
+    - Maintains thread waiting queue order
+    - Preserves thread-specific state for each queued thread
+    - Manages signaling and state transitions
+
+### Thread State Re-establishment
+- During model object creation, waiting threads are added with their correct states
+- The add_waiter_with_state() method ensures each thread's state is preserved
+
+## Post-Restart Handling By Condition Variable State
+
+### Case 1: CV_UNINITIALIZED
+- Thread behavior: No special handling required
+- System action: Condition variable will be initialized when first accessed
+
+### Case 2: CV_INITIALIZED
+- Thread behavior: Thread sends COND_INIT_TYPE message via mailbox
+- System action:
+    - Scheduler initializes condition variable using libpthread_cond_init()
+    - No thread state tracking needed as no threads are waiting
+
+### Case 3: CV_PREWAITING
+- Thread behavior:
+    - Thread sends COND_ENQUEUE_TYPE message to re-enter waiting queue
+    - Thread waits for scheduler acknowledgment
+    - Thread sends COND_WAIT_TYPE to block until signaled
+- System action:
+    - Scheduler adds thread to condition variable's waiting queue with CV_PREWAITING state
+    - Scheduler ensures mutex is released (critical for preventing deadlocks)
+    - Maintains pre-checkpoint thread state to ensure correct handling
+
+### Case 4: CV_WAITING
+- Thread behavior:
+    - Thread sends COND_ENQUEUE_TYPE message to re-register in waiting queue
+    - Thread sends COND_WAIT_TYPE to re-enter wait state
+- System action:
+    - Scheduler adds thread to waiting queue with CV_WAITING state
+    - Reconstructs exact pre-checkpoint waiting order
+    - Thread properly blocks waiting for signal
+
+### Case 5: CV_SIGNALED
+- Thread behavior:
+    - If thread was signaled pre-checkpoint, it resumes execution
+    - If thread was waiting, it follows CV_WAITING behavior
+- System action:
+    - Scheduler identifies which threads were signaled pre-checkpoint
+    - These threads are added to "wake groups" in the policy
+    - Ensures signaled threads receive priority for resumption
+    - Maintains proper FIFO ordering for signal processing
+
+### Case 6: CV_DESTROYED
+- Thread behavior: Thread sends COND_DESTROY_TYPE message
+- System action:
+    - Scheduler verifies no threads are waiting (or handles error)
+    - Resources associated with condition variable are properly released
+    - No further operations allowed on the condition variable