sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Temporarily removed the detection of the repository version of TBB from CMakeLists.txt. Corrected TBB sparse matrix-vector multiplication. Added TBB parallel vector addition. 

Former-commit-id: f90ae764c8
tempestpy_adaptions
dehnert 11 years ago
parent
81cf0e2b22
commit
cdc369b96a
9 changed files with 122 additions and 98 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      CMakeLists.txt
  2. 66
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  3. 27
      src/models/Dtmc.h
  4. 7
      src/models/MarkovAutomaton.h
  5. 10
      src/models/Mdp.h
  6. 18
      src/solver/AbstractNondeterministicLinearEquationSolver.h
  7. 34
      src/storage/SparseMatrix.cpp
  8. 36
      src/storage/SparseMatrix.h
  9. 5
      src/utility/vector.h

17
CMakeLists.txt
View File

@ -45,14 +45,14 @@ 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()
#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/")
@ -438,6 +438,7 @@ 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})
include_directories(${TBB_INCLUDE_DIRS})
target_link_libraries(storm tbb tbbmalloc)
target_link_libraries(storm-functional-tests tbb tbbmalloc)

66
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -123,9 +123,9 @@ namespace storm {
for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) {
bool currentChoiceRelevant = false;
for (auto& entry : transitionMatrix.getRow(row)) {
for (auto const& entry : transitionMatrix.getRow(row)) {
// If there is a relevant successor, we need to add the labels of the current choice.
if (relevancyInformation.relevantStates.get(entry.column()) || psiStates.get(entry.column())) {
if (relevancyInformation.relevantStates.get(entry.first) || psiStates.get(entry.first)) {
for (auto const& label : choiceLabeling[row]) {
relevancyInformation.relevantLabels.insert(label);
}
@ -212,21 +212,21 @@ namespace storm {
for (auto const& entry : transitionMatrix.getRow(relevantChoice)) {
// If the successor state is neither the state itself nor an irrelevant state, we need to add a variable for the transition.
if (state != entry.column() && (relevancyInformation.relevantStates.get(entry.column()) || psiStates.get(entry.column()))) {
if (state != entry.first && (relevancyInformation.relevantStates.get(entry.first) || psiStates.get(entry.first))) {
// Make sure that there is not already one variable for the state pair. This may happen because of several nondeterministic choices
// targeting the same state.
if (variableInformation.statePairToIndexMap.find(std::make_pair(state, entry.column())) != variableInformation.statePairToIndexMap.end()) {
if (variableInformation.statePairToIndexMap.find(std::make_pair(state, entry.first)) != variableInformation.statePairToIndexMap.end()) {
continue;
}
// At this point we know that the state-pair does not have an associated variable.
variableInformation.statePairToIndexMap[std::make_pair(state, entry.column())] = variableInformation.statePairVariables.size();
variableInformation.statePairToIndexMap[std::make_pair(state, entry.first)] = variableInformation.statePairVariables.size();
// Clear contents of the stream to construct new expression name.
variableName.clear();
variableName.str("");
variableName << "t" << state << "_" << entry.column();
variableName << "t" << state << "_" << entry.first;
variableInformation.statePairVariables.push_back(context.bool_const(variableName.str().c_str()));
}
@ -316,11 +316,11 @@ namespace storm {
// Iterate over successors and add relevant choices of relevant successors to the following label set.
bool canReachTargetState = false;
for (auto const& entry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(entry.column())) {
for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.column())) {
if (relevancyInformation.relevantStates.get(entry.first)) {
for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.first)) {
followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[currentChoice]);
}
} else if (psiStates.get(entry.column())) {
} else if (psiStates.get(entry.first)) {
canReachTargetState = true;
}
}
@ -335,11 +335,11 @@ namespace storm {
// Iterate over predecessors and add all choices that target the current state to the preceding
// label set of all labels of all relevant choices of the current state.
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (relevancyInformation.relevantStates.get(predecessorEntry.column())) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.column())) {
if (relevancyInformation.relevantStates.get(predecessorEntry.first)) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.first)) {
bool choiceTargetsCurrentState = false;
for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) {
if (successorEntry.column() == currentState) {
if (successorEntry.first == currentState) {
choiceTargetsCurrentState = true;
}
}
@ -581,11 +581,11 @@ namespace storm {
// Iterate over predecessors and add all choices that target the current state to the preceding
// label set of all labels of all relevant choices of the current state.
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (relevancyInformation.relevantStates.get(predecessorEntry.column())) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.column())) {
if (relevancyInformation.relevantStates.get(predecessorEntry.first)) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.first)) {
bool choiceTargetsCurrentState = false;
for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) {
if (successorEntry.column() == currentState) {
if (successorEntry.first == currentState) {
choiceTargetsCurrentState = true;
}
}
@ -913,16 +913,16 @@ namespace storm {
// Assert the constraints (1).
storm::storage::VectorSet<uint_fast64_t> relevantPredecessors;
for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) {
if (relevantState != predecessorEntry.column() && relevancyInformation.relevantStates.get(predecessorEntry.column())) {
relevantPredecessors.insert(predecessorEntry.column());
if (relevantState != predecessorEntry.first && relevancyInformation.relevantStates.get(predecessorEntry.first)) {
relevantPredecessors.insert(predecessorEntry.first);
}
}
storm::storage::VectorSet<uint_fast64_t> relevantSuccessors;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) {
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (relevantState != successorEntry.column() && (relevancyInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column()))) {
relevantSuccessors.insert(successorEntry.column());
if (relevantState != successorEntry.first && (relevancyInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first))) {
relevantSuccessors.insert(successorEntry.first);
}
}
}
@ -941,8 +941,8 @@ namespace storm {
storm::storage::VectorSet<uint_fast64_t> relevantSuccessors;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) {
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (relevantState != successorEntry.column() && (relevancyInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column()))) {
relevantSuccessors.insert(successorEntry.column());
if (relevantState != successorEntry.first && (relevancyInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first))) {
relevantSuccessors.insert(successorEntry.first);
}
}
}
@ -965,7 +965,7 @@ namespace storm {
storm::storage::VectorSet<uint_fast64_t> choicesForStatePair;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) {
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (successorEntry.column() == targetState) {
if (successorEntry.first == targetState) {
choicesForStatePair.insert(relevantChoice);
}
}
@ -1400,13 +1400,13 @@ namespace storm {
bool choiceTargetsRelevantState = false;
for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(successorEntry.column()) && currentState != successorEntry.column()) {
if (relevancyInformation.relevantStates.get(successorEntry.first) && currentState != successorEntry.first) {
choiceTargetsRelevantState = true;
if (!reachableStates.get(successorEntry.column())) {
reachableStates.set(successorEntry.column());
stack.push_back(successorEntry.column());
if (!reachableStates.get(successorEntry.first)) {
reachableStates.set(successorEntry.first);
stack.push_back(successorEntry.first);
}
} else if (psiStates.get(successorEntry.column())) {
} else if (psiStates.get(successorEntry.first)) {
targetStateIsReachable = true;
}
}
@ -1443,7 +1443,7 @@ namespace storm {
// Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states.
for (auto const& successorEntry : originalMdp.getTransitionMatrix().getRow(currentChoice)) {
if (unreachableRelevantStates.get(successorEntry.column())) {
if (unreachableRelevantStates.get(successorEntry.first)) {
isBorderChoice = true;
}
}
@ -1526,13 +1526,13 @@ namespace storm {
bool choiceTargetsRelevantState = false;
for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(successorEntry.column()) && currentState != successorEntry.column()) {
if (relevancyInformation.relevantStates.get(successorEntry.first) && currentState != successorEntry.first) {
choiceTargetsRelevantState = true;
if (!reachableStates.get(successorEntry.column())) {
reachableStates.set(successorEntry.column(), true);
stack.push_back(successorEntry.column());
if (!reachableStates.get(successorEntry.first)) {
reachableStates.set(successorEntry.first, true);
stack.push_back(successorEntry.first);
}
} else if (psiStates.get(successorEntry.column())) {
} else if (psiStates.get(successorEntry.first)) {
targetStateIsReachable = true;
}
}

27
src/models/Dtmc.h
View File

@ -139,7 +139,7 @@ public:
// Is there any state in the subsystem?
if(subSysStates.getNumberOfSetBits() == 0) {
LOG4CPLUS_ERROR(logger, "No states in subsystem!");
return storm::models::Dtmc<T>(storm::storage::SparseMatrix<T>(0),
return storm::models::Dtmc<T>(storm::storage::SparseMatrix<T>(),
storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates),
boost::optional<std::vector<T>>(),
boost::optional<storm::storage::SparseMatrix<T>>(),
@ -189,7 +189,7 @@ public:
// The number of transitions of the new Dtmc is the number of transitions transfered
// from the old one plus one transition for each state to s_b.
storm::storage::SparseMatrix<T> newMat(newStateCount, subSysTransitionCount + newStateCount);
storm::storage::SparseMatrixBuilder<T> newMatBuilder(newStateCount, subSysTransitionCount + newStateCount);
// Now fill the matrix.
newRow = 0;
@ -199,14 +199,14 @@ public:
// Transfer transitions
for(auto& entry : origMat.getRow(row)) {
if(subSysStates.get(entry.first)) {
newMat.addNextValue(newRow, stateMapping[entry.first], entry.second);
newMatBuilder.addNextValue(newRow, stateMapping[entry.first], entry.second);
} else {
rest += entry.second;
}
}
// Insert the transition taking care of the remaining outgoing probability.
newMat.addNextValue(newRow, newStateCount - 1, rest);
newMatBuilder.addNextValue(newRow, newStateCount - 1, rest);
rest = storm::utility::constantZero<T>();
newRow++;
@ -214,9 +214,7 @@ public:
}
// Insert last transition: self loop on s_b
newMat.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::constantOne<T>());
newMat.finalize();
newMatBuilder.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::constantOne<T>());
// 3. Take care of the labeling.
storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates);
@ -245,7 +243,7 @@ public:
boost::optional<storm::storage::SparseMatrix<T>> newTransitionRewards;
if(this->hasTransitionRewards()) {
storm::storage::SparseMatrix<T> newTransRewards(newStateCount, subSysTransitionCount + newStateCount);
storm::storage::SparseMatrixBuilder<T> newTransRewardsBuilder(newStateCount, subSysTransitionCount + newStateCount);
// Copy the rewards for the kept states
newRow = 0;
@ -254,18 +252,18 @@ public:
// Transfer transition rewards
for(auto& entry : this->getTransitionRewardMatrix().getRow(row)) {
if(subSysStates.get(entry.first)) {
newTransRewards.addNextValue(newRow, stateMapping[entry.first], entry.second);
newTransRewardsBuilder.addNextValue(newRow, stateMapping[entry.first], entry.second);
}
}
// Insert the reward (e.g. 0) for the transition taking care of the remaining outgoing probability.
newTransRewards.addNextValue(newRow, newStateCount - 1, storm::utility::constantZero<T>());
newTransRewardsBuilder.addNextValue(newRow, newStateCount - 1, storm::utility::constantZero<T>());
newRow++;
}
}
newTransitionRewards = newTransRewards;
newTransitionRewards = newTransRewardsBuilder.build();
}
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> newChoiceLabels;
@ -283,12 +281,7 @@ public:
}
// 5. Make Dtmc from its parts and return it
return storm::models::Dtmc<T>(newMat,
newLabeling,
newStateRewards,
newTransitionRewards,
newChoiceLabels
);
return storm::models::Dtmc<T>(newMatBuilder.build(), newLabeling, newStateRewards, std::move(newTransitionRewards), newChoiceLabels);
}

7
src/models/MarkovAutomaton.h
View File

@ -127,7 +127,7 @@ namespace storm {
uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates;
// Create the matrix for the new transition relation and the corresponding nondeterministic choice vector.
storm::storage::SparseMatrix<T> newTransitionMatrix;
storm::storage::SparseMatrixBuilder<T> newTransitionMatrixBuilder;
std::vector<uint_fast64_t> newNondeterministicChoiceIndices(this->getNumberOfStates() + 1);
// Now copy over all choices that need to be kept.
@ -149,7 +149,7 @@ namespace storm {
for (uint_fast64_t row = this->nondeterministicChoiceIndices[state] + (this->isHybridState(state) ? 1 : 0); row < this->nondeterministicChoiceIndices[state + 1]; ++row) {
for (auto const& entry : this->transitionMatrix.getRow(row)) {
newTransitionMatrix.addNextValue(currentChoice, entry.first, entry.second);
newTransitionMatrixBuilder.addNextValue(currentChoice, entry.first, entry.second);
}
++currentChoice;
}
@ -159,8 +159,7 @@ namespace storm {
newNondeterministicChoiceIndices.back() = currentChoice;
// Finalize the matrix and put the new transition data in place.
newTransitionMatrix.finalize();
this->transitionMatrix = std::move(newTransitionMatrix);
this->transitionMatrix = newTransitionMatrixBuilder.build();
this->nondeterministicChoiceIndices = std::move(newNondeterministicChoiceIndices);
// Mark the automaton as closed.

10
src/models/Mdp.h
View File

@ -143,7 +143,7 @@ public:
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
storm::storage::SparseMatrix<T> transitionMatrix;
storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder;
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
std::vector<storm::storage::VectorSet<uint_fast64_t>> newChoiceLabeling;
@ -161,7 +161,7 @@ public:
}
stateHasValidChoice = true;
for (auto const& entry : this->getTransitionMatrix().getRow(choice)) {
transitionMatrix.addNextValue(currentRow, entry.column(), entry.value());
transitionMatrixBuilder.addNextValue(currentRow, entry.first, entry.second);
}
newChoiceLabeling.emplace_back(choiceLabeling[choice]);
++currentRow;
@ -171,15 +171,15 @@ public:
// If no choice of the current state may be taken, we insert a self-loop to the state instead.
if (!stateHasValidChoice) {
nondeterministicChoiceIndices.push_back(currentRow);
transitionMatrix.addNextValue(currentRow, state, storm::utility::constantOne<T>());
transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::constantOne<T>());
newChoiceLabeling.emplace_back();
++currentRow;
}
}
transitionMatrix.finalize();
nondeterministicChoiceIndices.push_back(currentRow);
Mdp<T> restrictedMdp(std::move(transitionMatrix), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional<std::vector<T>>(this->getStateRewardVector()) : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<T>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<T>>(), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>(newChoiceLabeling));
Mdp<T> restrictedMdp(transitionMatrixBuilder.build(), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional<std::vector<T>>(this->getStateRewardVector()) : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<T>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<T>>(), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>(newChoiceLabeling));
return restrictedMdp;
}

18
src/solver/AbstractNondeterministicLinearEquationSolver.h
View File

@ -99,21 +99,34 @@ 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;
@ -121,6 +134,11 @@ 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.

34
src/storage/SparseMatrix.cpp
View File

@ -693,7 +693,7 @@ namespace storm {
template<typename T>
void SparseMatrix<T>::multiplyWithVector(std::vector<T> const& vector, std::vector<T>& result) const {
#ifdef STORM_HAVE_INTELTBB
tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, result.size()), tbbHelper_MatrixRowVectorScalarProduct<storm::storage::SparseMatrix<T>, std::vector<T>, T>(this, &vector, &result));
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();
@ -865,30 +865,26 @@ namespace storm {
template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
#ifdef STORM_HAVE_INTELTBB
template <typename ValueType>
TbbMatrixRowVectorScalarProduct<ValueType>::TbbMatrixRowVectorScalarProduct(SparseMatrix<ValueType> const& matrix, std::vector<ValueType> const& vector, std::vector<ValueType>& result) : result(result), vector(vector), matrix(matrix) {
// Intentionally left empty.
}
template <typename M, typename V, typename T>
tbbHelper_MatrixRowVectorScalarProduct<typename M, typename V, typename T>::tbbHelper_MatrixRowVectorScalarProduct(M const* matrixA, V const* vectorX, V * resultVector) : matrixA(matrixA), vectorX(vectorX), resultVector(resultVector) {}
template <typename M, typename V, typename T>
void tbbHelper_MatrixRowVectorScalarProduct<typename M, typename V, typename T>::operator() (const tbb::blocked_range<uint_fast64_t>& r) const {
for (uint_fast64_t row = r.begin(); row < r.end(); ++row) {
uint_fast64_t index = matrixA->rowIndications.at(row);
uint_fast64_t indexEnd = matrixA->rowIndications.at(row + 1);
// Initialize the result to be 0.
T element = storm::utility::constantZero<T>();
for (; index != indexEnd; ++index) {
element += matrixA->valueStorage.at(index) * vectorX->at(matrixA->columnIndications.at(index));
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];
}
// Write back to the result Vector
resultVector->at(row) = element;
result[row] = element;
}
}
// Explicit instanciations of specializations of this template here.
template class tbbHelper_MatrixRowVectorScalarProduct<storm::storage::SparseMatrix<double>, std::vector<double>, double>;
// Explicitly instantiate the helper class.
template class TbbMatrixRowVectorScalarProduct<double>;
#endif

36
src/storage/SparseMatrix.h
View File

@ -36,8 +36,8 @@ namespace storm {
#ifdef STORM_HAVE_INTELTBB
// Forward declaration of the TBB Helper class.
template <typename M, typename V, typename T>
class tbbHelper_MatrixRowVectorScalarProduct;
template <typename ValueType>
class TbbMatrixRowVectorScalarProduct;
#endif
// Forward declare matrix class.
@ -642,20 +642,34 @@ namespace storm {
#ifdef STORM_HAVE_INTELTBB
/*!
* This function is a helper for the parallel execution of the multipliyWithVector method.
* It uses Intel's TBB parallel_for paradigm to split up the row/vector multiplication and summation.
* This class is a helper class for parallel matrix-vector multiplication using Intel TBB.
*/
template <typename M, typename V, typename T>
class tbbHelper_MatrixRowVectorScalarProduct {
template <typename ValueType>
class TbbMatrixRowVectorScalarProduct {
public:
tbbHelper_MatrixRowVectorScalarProduct(M const* matrixA, V const* vectorX, V * resultVector);
/*!
* Constructs a helper object with which TBB can perform parallel matrix-vector multiplication.
*
* @param matrix The matrix to use for the multiplication.
* @param vector The vector with which to multiply the matrix.
* @param result The vector that is supposed to hold the result after performing the multiplication.
*/
TbbMatrixRowVectorScalarProduct(SparseMatrix<ValueType> const& matrix, std::vector<ValueType> const& vector, std::vector<ValueType>& result);
void operator() (const tbb::blocked_range<uint_fast64_t>& r) const;
/*!
* Performs the actual multiplication of a row with the vector.
*/
void operator() (tbb::blocked_range<uint_fast64_t> const& range) const;
private:
V * resultVector;
V const* vectorX;
M const* matrixA;
// The vector that is supposed to hold the result after performing the multiplication.
std::vector<ValueType>& result;
// The vector with which to multiply the matrix.
std::vector<ValueType> const& vector;
// The matrix to use for the multiplication.
SparseMatrix<ValueType> const& matrix;
};
#endif

5
src/utility/vector.h
View File

@ -135,8 +135,11 @@ namespace storm {
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.";
}
#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]; } });
#else
std::transform(target.begin(), target.end(), summand.begin(), target.begin(), std::plus<T>());
#endif
}
/*!

Write Preview
Loading…
Cancel
Save