Added proper TBB multi-threading to all operation relevant to model checking MDPs.

Former-commit-id: dcb4bde1d3

CMakeLists.txt

@@ -28,7 +28,7 @@ include_directories(${GMMXX_INCLUDE_DIR})
 option(DEBUG "Sets whether the DEBUG mode is used" ON)
 option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
 option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON)
-option(USE_INTELTBB "Sets whether the Intel TBB Extensions should be used." OFF)
+option(ENABLE_INTELTBB "Sets whether the Intel TBB is available." OFF)
 option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precompiled headers)." OFF)
 option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF)
 option(USE_LIBCXX "Sets whether the standard library is libc++." OFF)
@@ -45,15 +45,6 @@ set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory
 ##
 #############################################################
 
-#set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb41_20130314_merged-win-lin-mac/")
-#if(MSVC)
-#	set(ENV{TBB_ARCH_PLATFORM} "intel64/vc11")
-#elseif(CMAKE_COMPILER_IS_GNUCC)
-#	set(ENV{TBB_ARCH_PLATFORM} "intel64/gcc4.4")
-#else(CLANG)
-#	set(ENV{TBB_ARCH_PLATFORM} "intel64/clang3.2")
-#endif()
-
 # Add the resources/cmake folder to Module Search Path for FindTBB.cmake
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmake/")
 
@@ -200,7 +191,7 @@ else()
 endif()
 
 # Intel TBB Defines
-if (TBB_FOUND AND USE_INTELTBB)
+if (TBB_FOUND AND ENABLE_INTELTBB)
 	set(STORM_CPP_INTELTBB_DEF "define")
 else()
 	set(STORM_CPP_INTELTBB_DEF "undef")
@@ -299,7 +290,7 @@ if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL ""))
 	set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib")
 endif ()
 link_directories(${Boost_LIBRARY_DIRS})
-if (TBB_FOUND AND USE_INTELTBB)
+if (TBB_FOUND AND ENABLE_INTELTBB)
 	link_directories(${TBB_LIBRARY_DIRS})
 endif()
 
@@ -435,15 +426,14 @@ endif(UNIX AND NOT APPLE)
 ##
 #############################################################
 if (TBB_FOUND)
-	message(STATUS "StoRM - Found Intel TBB with Interface Version ${TBB_INTERFACE_VERSION}")
-	if (USE_INTELTBB)
-		message(STATUS "StoRM - Linking with Intel TBB for activated Matrix/Vector MT")
-        message(${TBB_LIBRARY_DIRS})
+	message(STATUS "StoRM - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.")
+	if (ENABLE_INTELTBB)
+		message(STATUS "StoRM - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.")
 		include_directories(${TBB_INCLUDE_DIRS})
 		target_link_libraries(storm tbb tbbmalloc)
 		target_link_libraries(storm-functional-tests tbb tbbmalloc)
 		target_link_libraries(storm-performance-tests tbb tbbmalloc)
-	endif(USE_INTELTBB)
+	endif(ENABLE_INTELTBB)
 endif(TBB_FOUND)
 
 #############################################################

src/solver/AbstractNondeterministicLinearEquationSolver.h

@@ -99,34 +99,21 @@ namespace storm {
 
                 // Proceed with the iterations as long as the method did not converge or reach the
                 // user-specified maximum number of iterations.
-                std::chrono::nanoseconds multTime(0);
-                std::chrono::nanoseconds addTime(0);
-                std::chrono::nanoseconds reduceTime(0);
-                std::chrono::nanoseconds convergedTime(0);
-                auto clock = std::chrono::high_resolution_clock::now();
                 while (!converged && iterations < maxIterations) {
                     // Compute x' = A*x + b.
-                    clock = std::chrono::high_resolution_clock::now();
                     A.multiplyWithVector(*currentX, *multiplyResult);
-                    multTime += std::chrono::high_resolution_clock::now() - clock;
-                    clock = std::chrono::high_resolution_clock::now();
                     storm::utility::vector::addVectorsInPlace(*multiplyResult, b);
-                    addTime += std::chrono::high_resolution_clock::now() - clock;
                     
                     // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
                     // element of the min/max operator stack.
-                    clock = std::chrono::high_resolution_clock::now();
                     if (minimize) {
                         storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, nondeterministicChoiceIndices);
                     } else {
                         storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, nondeterministicChoiceIndices);
                     }
-                    reduceTime += std::chrono::high_resolution_clock::now() - clock;
                     
                     // Determine whether the method converged.
-                    clock = std::chrono::high_resolution_clock::now();
                     converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative);
-                    convergedTime += std::chrono::high_resolution_clock::now() - clock;
                     
                     // Update environment variables.
                     swap = currentX;
@@ -134,11 +121,6 @@ namespace storm {
                     newX = swap;
                     ++iterations;
                 }
-                
-                std::cout << std::chrono::duration_cast<std::chrono::milliseconds>(multTime).count() << "ms" << std::endl;
-                std::cout << std::chrono::duration_cast<std::chrono::milliseconds>(addTime).count() << "ms" << std::endl;
-                std::cout << std::chrono::duration_cast<std::chrono::milliseconds>(reduceTime).count() << "ms" << std::endl;
-                std::cout << std::chrono::duration_cast<std::chrono::milliseconds>(convergedTime).count() << "ms" << std::endl;
 
                 // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
                 // is currently stored in currentX, but x is the output vector.

src/storage/SparseMatrix.cpp

@@ -696,7 +696,7 @@ namespace storm {
             tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, result.size()), TbbMatrixRowVectorScalarProduct<T>(*this, vector, result));
 #else
             const_iterator it = this->begin();
-            const_iterator ite = this->begin();
+            const_iterator ite;
             typename std::vector<uint_fast64_t>::const_iterator rowIterator = rowIndications.begin();
             typename std::vector<uint_fast64_t>::const_iterator rowIteratorEnd = rowIndications.end();
             typename std::vector<T>::iterator resultIterator = result.begin();
@@ -705,7 +705,7 @@ namespace storm {
             for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) {
                 *resultIterator = storm::utility::constantZero<T>();
                 
-                for (ite = it + (*(rowIterator + 1) - *rowIterator); it != ite; ++it) {
+                for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) {
                     *resultIterator += it->second * vector[it->first];
                 }
             }
@@ -872,20 +872,26 @@ namespace storm {
         
         template <typename ValueType>
         void TbbMatrixRowVectorScalarProduct<ValueType>::operator() (tbb::blocked_range<uint_fast64_t> const& range) const {
-            for (uint_fast64_t row = range.begin(); row < range.end(); ++row) {
-                ValueType element = storm::utility::constantZero<ValueType>();
-
-                for (typename SparseMatrix<ValueType>::const_iterator it = matrix.begin(row), ite = matrix.end(row); it != ite; ++it) {
-                    element += it->second * vector[it->first];
-                }
+            uint_fast64_t startRow = range.begin();
+            uint_fast64_t endRow = range.end();
+            typename SparseMatrix<ValueType>::const_iterator it = matrix.begin(startRow);
+            typename SparseMatrix<ValueType>::const_iterator ite;
+            typename std::vector<uint_fast64_t>::const_iterator rowIterator = matrix.rowIndications.begin() + startRow;
+            typename std::vector<uint_fast64_t>::const_iterator rowIteratorEnd = matrix.rowIndications.begin() + endRow;
+            typename std::vector<ValueType>::iterator resultIterator = result.begin() + startRow;
+            typename std::vector<ValueType>::iterator resultIteratorEnd = result.begin() + endRow;
+            
+            for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) {
+                *resultIterator = storm::utility::constantZero<ValueType>();
                 
-                result[row] = element;
+                for (ite = matrix.begin() + *(rowIterator + 1); it != ite; ++it) {
+                    *resultIterator += it->second * vector[it->first];
+                }
             }
         }
         
         // Explicitly instantiate the helper class.
         template class TbbMatrixRowVectorScalarProduct<double>;
-        
 #endif
         
     } // namespace storage

src/storage/SparseMatrix.h

@@ -161,8 +161,8 @@ namespace storm {
             
 #ifdef STORM_HAVE_INTELTBB
             // Declare the helper class for TBB as friend.
-            template <typename M, typename V, typename TPrime>
-            friend class tbbHelper_MatrixRowVectorScalarProduct;
+            template <typename ValueType>
+            friend class TbbMatrixRowVectorScalarProduct;
 #endif
             
             typedef typename std::vector<std::pair<uint_fast64_t, T>>::iterator iterator;
@@ -657,7 +657,9 @@ namespace storm {
             TbbMatrixRowVectorScalarProduct(SparseMatrix<ValueType> const& matrix, std::vector<ValueType> const& vector, std::vector<ValueType>& result);
             
             /*!
-             * Performs the actual multiplication of a row with the vector.
+             * Performs the actual multiplication of a range of rows with the given vector.
+             *
+             * @param range The range of rows to multiply with the given vector.
              */
             void operator() (tbb::blocked_range<uint_fast64_t> const& range) const;
             

src/utility/vector.h

@@ -131,12 +131,22 @@ namespace storm {
              */
             template<class T>
             void addVectorsInPlace(std::vector<T>& target, std::vector<T> const& summand) {
+#ifdef DEBUG
                 if (target.size() != summand.size()) {
-                    LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes operation impossible.");
-                    throw storm::exceptions::InvalidArgumentException() << "Length of vectors do not match, which makes operation impossible.";
+                    throw storm::exceptions::InvalidArgumentException() << "Invalid call to storm::utility::vector::addVectorsInPlace: operand lengths mismatch.";
                 }
+#endif
 #ifdef STORM_HAVE_INTELTBB
-                tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, target.size(), target.size() / 4), [&](tbb::blocked_range<uint_fast64_t>& range) { for (uint_fast64_t current = range.begin(), end = range.end(); current < end; ++current) { target[current] += summand[current]; } });
+                tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, target.size()),
+                                  [&](tbb::blocked_range<uint_fast64_t> const& range) {
+                                        uint_fast64_t firstRow = range.begin();
+                                        uint_fast64_t endRow = range.end();
+                                      
+                                        typename std::vector<T>::iterator targetIt = target.begin() + firstRow;
+                                        for (typename std::vector<T>::const_iterator summandIt = summand.begin() + firstRow, summandIte = summand.begin() + endRow; summandIt != summandIte; ++summandIt, ++targetIt) {
+                                                *targetIt += *summandIt;
+                                        }
+                                  });
 #else
                 std::transform(target.begin(), target.end(), summand.begin(), target.begin(), std::plus<T>());
 #endif
@@ -153,30 +163,78 @@ namespace storm {
              * @param choices If non-null, this vector is used to store the choices made during the selection.
              */
             template<class T>
-            void reduceVector(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::function<bool (T const&, T const&)> filter, std::vector<uint_fast64_t>* choices = nullptr) {
-                uint_fast64_t currentSourceRow = 0;
-                uint_fast64_t currentTargetRow = -1;
-                uint_fast64_t currentLocalRow = 0;
-                for (auto it = source.cbegin(), ite = source.cend(); it != ite; ++it, ++currentSourceRow, ++currentLocalRow) {
-                    // Check whether we have considered all source rows for the current target row.
-                    if (rowGrouping[currentTargetRow + 1] <= currentSourceRow || currentSourceRow == 0) {
-                        currentLocalRow = 0;
-                        ++currentTargetRow;
-                        target[currentTargetRow] = source[currentSourceRow];
-                        if (choices != nullptr) {
-                            (*choices)[currentTargetRow] = 0;
-                        }
-                        continue;
+            void reduceVector(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::function<bool (T const&, T const&)> filter, std::vector<uint_fast64_t>* choices) {
+#ifdef STORM_HAVE_INTELTBB
+                tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, target.size()),
+                                  [&](tbb::blocked_range<uint_fast64_t> const& range) {
+                                      uint_fast64_t startRow = range.begin();
+                                      uint_fast64_t endRow = range.end();
+                                      
+                                      typename std::vector<T>::iterator targetIt = target.begin() + startRow;
+                                      typename std::vector<T>::iterator targetIte = target.begin() + endRow;
+                                      typename std::vector<uint_fast64_t>::const_iterator rowGroupingIt = rowGrouping.begin() + startRow;
+                                      typename std::vector<T>::const_iterator sourceIt = source.begin() + *rowGroupingIt;
+                                      typename std::vector<T>::const_iterator sourceIte;
+                                      typename std::vector<uint_fast64_t>::iterator choiceIt;
+                                      uint_fast64_t localChoice;
+                                      if (choices != nullptr) {
+                                          choiceIt = choices->begin();
+                                      }
+
+                                      for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt) {
+                                          *targetIt = *sourceIt;
+                                          ++sourceIt;
+                                          localChoice = 0;
+                                          if (choices != nullptr) {
+                                              *choiceIt = 0;
+                                          }
+                                          
+                                          for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) {
+                                              if (filter(*sourceIt, *targetIt)) {
+                                                  *targetIt = *sourceIt;
+                                                  if (choices != nullptr) {
+                                                      *choiceIt = localChoice;
+                                                  }
+                                              }
+                                          }
+                                          
+                                          if (choices != nullptr) {
+                                              ++choiceIt;
+                                          }
+                                      }
+                                  });
+#else
+                typename std::vector<T>::iterator targetIt = target.begin();
+                typename std::vector<T>::iterator targetIte = target.end();
+                typename std::vector<uint_fast64_t>::const_iterator rowGroupingIt = rowGrouping.begin();
+                typename std::vector<T>::const_iterator sourceIt = source.begin();
+                typename std::vector<T>::const_iterator sourceIte;
+                typename std::vector<uint_fast64_t>::iterator choiceIt;
+                uint_fast64_t localChoice;
+                if (choices != nullptr) {
+                    choiceIt = choices->begin();
+                }
+                
+                for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt) {
+                    *targetIt = *sourceIt;
+                    ++sourceIt;
+                    localChoice = 0;
+                    if (choices != nullptr) {
+                        *choiceIt = 0;
                     }
-                    
-                    // We have to upate the value, so only overwrite the current value if the value passes the filter.
-                    if (filter(*it, target[currentTargetRow])) {
-                        target[currentTargetRow] = *it;
-                        if (choices != nullptr) {
-                            (*choices)[currentTargetRow] = currentLocalRow;
+                    for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) {
+                        if (filter(*sourceIt, *targetIt)) {
+                            *targetIt = *sourceIt;
+                            if (choices != nullptr) {
+                                *choiceIt = localChoice;
+                            }
                         }
                     }
+                    if (choices != nullptr) {
+                        ++choiceIt;
+                    }
                 }
+#endif
             }
             
             /*!