Save memory when doing bounded checking for sparse DTMCs #517
Conversation
SparseDeterministicStepBoundedHorizonHelper takes a matrix with the backwards transitions. By constructing this inside the helper we can deallocate it early, reducing peak memory.
| @@ -101,8 +101,8 @@ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::c | |||
| storm::modelchecker::helper::SparseDeterministicStepBoundedHorizonHelper<ValueType> helper; | |||
| std::vector<ValueType> numericResult = | |||
| helper.compute(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), | |||
| this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), | |||
| pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint()); | |||
| leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound<uint64_t>(), | |||
There was a problem hiding this comment.
@tquatmann is it clear why we referred to the backward transitions previously?
There was a problem hiding this comment.
They're used below the line where they are calculated now, in a call to performProbGreater0:
storm/src/storm/utility/graph.cpp
Line 322 in b26d9af
This function iterates over the rows of the backwards transitions, as it essentially does a reverse flood-fill to find the states which can reach the target state(s). Using the non-transposed matrix would thus require iterating over a column, which is slow and I'm not sure it's even possible with how sparse matrices are implemented.
I don't know off of the top of my head if the same result can be achieved in a forwards manner, but I think it would be much slower since it would probably require maximalSteps iterations over all vertices.
This was the only use of it in the helper, I'm not sure if there are any other potential reasons to refer to the backward transitions but I doubt it.
|
Thanks a lot. To me, this is a clear improvement. A slight alternative could be to have this as an optional argument -- but I think i would dislike the extra code complexity that would add. @tquatmann thoughts? I think we have discussed in other threads that it make sense to create a class/type for submatrices that also would avoid further copies. |
|
Iirc, the original idea was to allow re-using backward transitions for cases where one solves multiple step-bounded reachability queries on the same matrix. However, I don't think that this is currently used somewhere (unless maybe through stormpy?), so I support the suggested changes. |
Ah yeah, that would be a valid alternative. Doing that would probably be pretty easy and just put it as a |
Currently, Storm produces many copies of the transition matrix for the sparse engine. Concretely, there are 2 copies of the original matrix and 2 copies of the P=? submatrix resident at peak RSS.
These are
By deferring the creation of (2), it is freed earlier (its scope is closed earlier), which allows the operating system to reuse its memory for (3) and (4). As such, peak memory usage is determined by
max(m1+m2, m1+m3+m4)instead ofm1+m2+m3+m4.(Addtionally, (4) can be omitted entirely by using the Storm native solver, which is already a setting that can be changed.)
Other sparse model checking functions have the same weakness, but I only did it for this one as a proof-of-concept. Applying this patch and using the native solver nearly halves Storm's memory usage for the factories problem (f=12) from the Rubicon paper, from 1 GB to circa 0.5 GB. Either of these by themselves reduce it to 0.75 GB. This is because for this problem the submatrix has nearly the same size as the original matrix.
An alternative that could be considered is to keep the backwards transitions around in the original model. Currently, I believe that Storm recalculates the transpose over and over. Keeping it around would reduce time usage slightly, whereas dropping it early reduces memory usage.