Multithreading for State Building

CMakeLists.txt

@@ -4,49 +4,66 @@
 ## Requires STORM and boost
 ##
 
-cmake_minimum_required(VERSION 3.10)  # CMake version check
-project(sstamina)               # Create project "sstamina"
+cmake_minimum_required(VERSION 3.10)
+
+# Main STAMINA executable
+include_directories("src")
+include_directories("src/stamina")
+
 set(CMAKE_CXX_STANDARD 17)            # Enable c++17 standard
 set(CMAKE_CXX_STANDARD_REQUIRED True)
 set(CMAKE_BUILD_TYPE Debug)
 
-# Add main.cpp file of project root directory as source file
-
+# Source files for the main STAMINA CLI
 set(SOURCE_DIR src)
 set(SOURCE_FILES
-    # Main source files for the `stamina` namespace
+	# Main source files for the `stamina` namespace
 	src/stamina/ANSIColors.h
-    src/stamina/main.cpp
-    src/stamina/Stamina.cpp
-    src/stamina/Stamina.h
-    src/stamina/StaminaArgParse.h
-    src/stamina/StaminaModelChecker.h
-    src/stamina/StaminaModelChecker.cpp
-    src/stamina/StaminaMessages.h
-	src/stamina/StaminaMessages.cpp
-    src/stamina/Options.h
-    src/stamina/Options.cpp
-	src/stamina/StateSpaceInformation.cpp
-	src/stamina/StateSpaceInformation.h
-	# Files for `stamina::builder` namespace
-    src/stamina/builder/StaminaModelBuilder.h
-    src/stamina/builder/StaminaModelBuilder.cpp
-    src/stamina/builder/StaminaIterativeModelBuilder.cpp
-    src/stamina/builder/StaminaIterativeModelBuilder.h
-	# src/stamina/builder/StaminaPriorityModelBuilder.cpp
-    # src/stamina/builder/StaminaPriorityModelBuilder.h
-	src/stamina/builder/StaminaReExploringModelBuilder.cpp
-    src/stamina/builder/StaminaReExploringModelBuilder.h
-	src/stamina/builder/ExplicitTruncatedModelBuilder.h
-	src/stamina/builder/ExplicitTruncatedModelBuilder.cpp
+	src/stamina/main.cpp
+	src/stamina/Stamina.cpp
+	src/stamina/Stamina.h
+	src/stamina/StaminaArgParse.h
+)
+
+# STAMINA library files for linking
+set(LIB_FILES
+	# Files for `stamina::core` namespace
+	src/stamina/core/StaminaModelChecker.h
+	src/stamina/core/StaminaModelChecker.cpp
+	src/stamina/core/StaminaMessages.h
+	src/stamina/core/StaminaMessages.cpp
+	src/stamina/core/Options.h
+	src/stamina/core/Options.cpp
+	src/stamina/core/StateSpaceInformation.cpp
+	src/stamina/core/StateSpaceInformation.h
 	# Files for `stamina::util` namespace
 	src/stamina/util/ModelModify.h
 	src/stamina/util/ModelModify.cpp
 	src/stamina/util/StateIndexArray.h
 	src/stamina/util/StateIndexArray.cpp
 	src/stamina/util/StateMemoryPool.h
 	src/stamina/util/StateMemoryPool.cpp
-
+	# Files for `stamina::builder` namespace
+	src/stamina/builder/StaminaModelBuilder.h
+	src/stamina/builder/StaminaModelBuilder.cpp
+	src/stamina/builder/StaminaIterativeModelBuilder.cpp
+	src/stamina/builder/StaminaIterativeModelBuilder.h
+	src/stamina/builder/StaminaThreadedIterativeModelBuilder.cpp
+	src/stamina/builder/StaminaPriorityModelBuilder.cpp
+	src/stamina/builder/StaminaPriorityModelBuilder.h
+	src/stamina/builder/StaminaReExploringModelBuilder.cpp
+	src/stamina/builder/StaminaReExploringModelBuilder.h
+	src/stamina/builder/ExplicitTruncatedModelBuilder.h
+	src/stamina/builder/ExplicitTruncatedModelBuilder.cpp
+	# Files for `stamina::builder::threads` namespace
+	src/stamina/builder/threads/BaseThread.cpp
+	src/stamina/builder/threads/BaseThread.h
+	src/stamina/builder/threads/ControlThread.cpp
+	src/stamina/builder/threads/ControlThread.h
+	src/stamina/builder/threads/ExplorationThread.cpp
+	src/stamina/builder/threads/ExplorationThread.h
+	src/stamina/builder/threads/IterativeExplorationThread.cpp
+	src/stamina/builder/threads/IterativeExplorationThread.h
 )
 
 message("STORM_PATH is set as " ${STORM_PATH})
@@ -59,18 +76,33 @@ set(CUDD_PATH ${STORM_PATH}/storm/resources/3rdparty/cudd-3.0.0/cplusplus)
 find_package(Boost)
 if (Boost_FOUND)
 	message("BOOST found!")
-    include_directories(${Boost_INCLUDE_DIRS})
-    include_directories(${Boost_INCLUDES})
+	include_directories(${Boost_INCLUDE_DIRS})
+	include_directories(${Boost_INCLUDES})
 endif (Boost_FOUND)
 
 find_package(storm REQUIRED PATHS ${STORM_PATH})
-# if (storm_FOUND)
-#	message("STORM found!")
-#else
-#	message("STORM not found! STORM required to build STAMINA!")
-#endif
+if (storm_FOUND)
+	message("STORM found!")
+else()
+	message("STORM not found! STORM required to build STAMINA!")
+endif()
+
+# STAMINA shared-object libraries project
+project(stamina VERSION 2.5.0 DESCRIPTION "Shared objects for STAMINA usage")
+include_directories("src")
+include_directories("src/stamina")
+
+add_library(stamina SHARED ${LIB_FILES})
+set_target_properties(stamina PROPERTIES VERSION ${PROJECT_VERSION})
+target_include_directories(${PROJECT_NAME} PUBLIC ${SOURCE_DIR} ${storm_INCLUDE_DIR} ${storm-parsers_INCLUDE_DIR} ${STORM_PATH} ${LIB_PATH})
+target_link_libraries(${PROJECT_NAME} PUBLIC storm storm-parsers)
+
+# TODO: Continue cmake for lib: https://stackoverflow.com/questions/17511496/how-to-create-a-shared-library-with-cmake
 
 # Add executable target with source files listed in SOURCE_FILES variable
+project(sstamina VERSION 2.5.0 DESCRIPTION "Main STAMINA/STORM executable")
 add_executable(sstamina ${SOURCE_FILES})
 target_include_directories(${PROJECT_NAME} PUBLIC ${SOURCE_DIR} ${storm_INCLUDE_DIR} ${storm-parsers_INCLUDE_DIR} ${STORM_PATH} ${LIB_PATH})
-target_link_libraries(${PROJECT_NAME} PUBLIC storm storm-parsers)
+target_link_libraries(${PROJECT_NAME} PUBLIC storm storm-parsers stamina)
+
+

doc/algorithms/multithreading.md

@@ -0,0 +1,153 @@
+# Multithreading STAMINA Algorithm
+
+In order to properly create multithreading in STAMINA, we must add mutual exclusions to the state space at some level, however there is a tradeoff in memory impact and CPU time:
+	+ If we place a Mutex on every single state, we see a massive memory impact. The `std::mutex` and the C equivalent `pthread_mutex_t` are both 40 bytes.
+	+ If we place one mutex on the entire state space then we see no benefit to multithreading, since every state that is modified must first lock the entire state space for all other threads.
+Therefore, 
+
+**Exploration Thread Object**
+
+```
+OBJECT ExplorationThread
+	DATA MEMBERS
+		PUBLIC CONST i -> INT // (written on construction)
+		PUBLIC numberStatesOwned := INT
+		PUBLIC finished -> bool // (many read, one write)
+		PUBLIC X -> queue() (mutex)
+		PRIVATE S -> queue()
+	END DATA MEMBERS
+
+	METHODS
+		PUBLIC PROCEDURE doExploration() -> VOID
+			WHILE shouldNotDie DO
+				// Weak priority on cross exploration
+				IF NOT X.empty() AND NOT X.locked() THEN
+					s := dequeue(X)
+					Add to s reachability probability
+					explore(s)
+				ELSE IF NOT S.empty() THEN
+					s := dequeue(S)
+					explore(s)
+				ELSE
+					finished := true
+				END IF
+			END DO
+		END PROCEDURE
+
+		PUBLIC PROCEDURE explore(s -> state) -> VOID
+			FOR EACH s' in next(s)
+				IF owner(s') == null THEN
+					o := requestOwnership(s')
+					IF o == i THEN
+						exploreSuccessor(s')
+					END IF
+				ELSE IF owner(s') != i THEN
+					threads[owner(s')].X.enqueue(s')
+				ELSE
+					exploreSuccessor(s')
+				END IF
+			END FOR
+		END PROCEDURE
+
+		PUBLIC PROCEDURE exploreSuccessor(s' -> state) -> VOID
+			(STAMINA 2.0 block)
+			TODO: Add STAMINA 2.0 block
+		END PROCEDURE
+	END METHODS
+END OBJECT
+```
+
+**Control Thread Object**
+
+```
+OBJECT ControlThread
+	DATA MEMBERS
+		PRIVATE ownedThreads -> HashMap<state, INT>()
+		PRIVATE ownershipMutex -> SharedMutex() (Mutex that allows multiple reads but only one write)
+		PUBLIC transitionMatrixQueues -> list<LockableQueue<INT, INT, double>>() (One queue for each of the threads to prevent the need for sharing mutual exclusion)
+	END DATA MEMBERS
+
+	METHODS
+		PUBLIC PROCEDURE requestOwnership(state, threadIndex) -> INT
+			IF state in ownedThreads THEN
+				RETURN ownedThreads.get(state)
+			ELSE
+				TRY LOCK ownershipMutex
+				WHEN LOCK achieved THEN
+					(Checks to see of some other state beat us to the lock)
+					IF state IN ownedThreads THEN
+						RETURN ownedThreads.get(state)
+					ELSE
+						CLAIM OWNERSHIP OF STATE
+						ownedThreads.insert(state, threadIndex)
+						RETURN threadIndex
+					END IF
+				END WHEN
+			END IF
+		END PROCEDURE
+
+		PUBLIC PROCEDURE whoOwns(state) -> INT
+			(DOES NOT LOCK MUTEX)
+			IF state IN ownedThreads THEN
+				RETURN ownedThreads.get(state)
+			ELSE
+				RETURN null
+			END IF
+		END PROCEDURE
+
+		PUBLIC PROCEDURE mainLoop() -> VOID
+			INT numberFinishedThreads := 0
+			DO WHILE numberFinishedThreads < numberThreads
+				FOR EACH queue IN transitionMatrixQueues DO
+					WHILE NOT queue.empty() DO
+						fromState, toState, rate := queue.dequeue()
+						transitionMatrixEntries.insert(fromState, toState, rate)
+					END WHILE
+					IF THE CORRESPONDING THREAD IS FINISHED
+						numberFinishedThreads := numberFinxploredThreads + 1
+						(At some point we should add some defragmentation to transfer thread ownership)
+					END IF
+				DONE
+			END DO
+		END PROCEDURE
+	END METHODS
+END OBJECT
+```
+
+**Model Builder Object**
+
+```
+OBJECT ModelBuilder
+	DATA MEMBERS
+		threads -> list()
+		transitionMatrixEntries -> TransitionMatrixEntries() (Asynchronous helper for transition matrix creation)
+	END DATA MEMBERS
+	BEGIN METHODS
+		PUBLIC PROCEDURE exploreStates() -> VOID
+			initQueue := queue()
+			si := initialState()
+			numberPerimeterStates := 0
+			initQueue.enqueue(si)
+			DO WHILE numberPerimeterStates < numberThreads
+				s := dequeue(initQueue)
+
+				ENQUEUE ALL successor states and update PI/EXPLOREDMAPS/PERIMETERSTATES
+				numberPerimeterStates := numberPerimeterStates - 1
+			END WHILE
+			index := 1
+			FOR EACH s IN PERIMETER STATES DO
+				threads[index].X.enqueue(s)
+				index := index + 1
+			END FOR
+			WHILE anyThreadWorking() DO
+				IDLE
+			END WHILE
+		END PROCEDURE
+	END METHODS
+END OBJECT
+```
+
+
+## METHODS TODO TO IMPLEMENT
+
++ `StaminaModelBuilder::getStateMap`

src/stamina/ANSIColors.h

@@ -4,8 +4,8 @@
  * Modified from https://stackoverflow.com/questions/2616906/how-do-i-output-coloured-text-to-a-linux-terminal
  * */
 
-#ifndef ANSI_COLORS_H
-#define ANSI_COLORS_H
+#ifndef STAMINA_ANSI_COLORS_H
+#define STAMINA_ANSI_COLORS_H
 
 /* FOREGROUND */
 #define RST  "\x1B[0m"
@@ -28,4 +28,4 @@
 #define BOLD(x) "\x1B[1m" x RST
 #define UNDL(x) "\x1B[4m" x RST
 
-#endif // ANSI_COLORS_H
+#endif // STAMINA_ANSI_COLORS_H