diff --git a/CMakeLists.txt b/CMakeLists.txt index 4efcb6e4f..9fbc351e4 100644 --- a/CMakeLists.txt +++ b/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) ############################################################# diff --git a/src/solver/AbstractNondeterministicLinearEquationSolver.h b/src/solver/AbstractNondeterministicLinearEquationSolver.h index d1cc8bbf2..8d6b41acc 100644 --- a/src/solver/AbstractNondeterministicLinearEquationSolver.h +++ b/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(multTime).count() << "ms" << std::endl; - std::cout << std::chrono::duration_cast(addTime).count() << "ms" << std::endl; - std::cout << std::chrono::duration_cast(reduceTime).count() << "ms" << std::endl; - std::cout << std::chrono::duration_cast(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. diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 608fe92be..398b3d78a 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -696,7 +696,7 @@ namespace storm { tbb::parallel_for(tbb::blocked_range(0, result.size()), TbbMatrixRowVectorScalarProduct(*this, vector, result)); #else const_iterator it = this->begin(); - const_iterator ite = this->begin(); + const_iterator ite; typename std::vector::const_iterator rowIterator = rowIndications.begin(); typename std::vector::const_iterator rowIteratorEnd = rowIndications.end(); typename std::vector::iterator resultIterator = result.begin(); @@ -705,7 +705,7 @@ namespace storm { for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { *resultIterator = storm::utility::constantZero(); - 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 void TbbMatrixRowVectorScalarProduct::operator() (tbb::blocked_range const& range) const { - for (uint_fast64_t row = range.begin(); row < range.end(); ++row) { - ValueType element = storm::utility::constantZero(); - - for (typename SparseMatrix::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::const_iterator it = matrix.begin(startRow); + typename SparseMatrix::const_iterator ite; + typename std::vector::const_iterator rowIterator = matrix.rowIndications.begin() + startRow; + typename std::vector::const_iterator rowIteratorEnd = matrix.rowIndications.begin() + endRow; + typename std::vector::iterator resultIterator = result.begin() + startRow; + typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; + + for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { + *resultIterator = storm::utility::constantZero(); - 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; - #endif } // namespace storage diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 3654dc1b8..9e996366a 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -161,8 +161,8 @@ namespace storm { #ifdef STORM_HAVE_INTELTBB // Declare the helper class for TBB as friend. - template - friend class tbbHelper_MatrixRowVectorScalarProduct; + template + friend class TbbMatrixRowVectorScalarProduct; #endif typedef typename std::vector>::iterator iterator; @@ -657,7 +657,9 @@ namespace storm { TbbMatrixRowVectorScalarProduct(SparseMatrix const& matrix, std::vector const& vector, std::vector& 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 const& range) const; diff --git a/src/utility/vector.h b/src/utility/vector.h index 018e36e88..7f22a52cd 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -131,12 +131,22 @@ namespace storm { */ template void addVectorsInPlace(std::vector& target, std::vector 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(0, target.size(), target.size() / 4), [&](tbb::blocked_range& range) { for (uint_fast64_t current = range.begin(), end = range.end(); current < end; ++current) { target[current] += summand[current]; } }); + tbb::parallel_for(tbb::blocked_range(0, target.size()), + [&](tbb::blocked_range const& range) { + uint_fast64_t firstRow = range.begin(); + uint_fast64_t endRow = range.end(); + + typename std::vector::iterator targetIt = target.begin() + firstRow; + for (typename std::vector::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()); #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 - void reduceVector(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::function filter, std::vector* 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 const& source, std::vector& target, std::vector const& rowGrouping, std::function filter, std::vector* choices) { +#ifdef STORM_HAVE_INTELTBB + tbb::parallel_for(tbb::blocked_range(0, target.size()), + [&](tbb::blocked_range const& range) { + uint_fast64_t startRow = range.begin(); + uint_fast64_t endRow = range.end(); + + typename std::vector::iterator targetIt = target.begin() + startRow; + typename std::vector::iterator targetIte = target.begin() + endRow; + typename std::vector::const_iterator rowGroupingIt = rowGrouping.begin() + startRow; + typename std::vector::const_iterator sourceIt = source.begin() + *rowGroupingIt; + typename std::vector::const_iterator sourceIte; + typename std::vector::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::iterator targetIt = target.begin(); + typename std::vector::iterator targetIte = target.end(); + typename std::vector::const_iterator rowGroupingIt = rowGrouping.begin(); + typename std::vector::const_iterator sourceIt = source.begin(); + typename std::vector::const_iterator sourceIte; + typename std::vector::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 } /*!