Open ifndefJOSH opened 2 years ago
I think this has to do with all of the threads using the same next state generator object. This can probably be fixed by creating unique generator objects. However, not quite sure the best way to do this, because:
NextStateGenerator
objects are created in stamina::core::StaminaModelChecker
with access to the PRISM program object and then passed into the StaminaModelBuilder
object. That's currently why it's passed in.storm::generator::NextStateGenerator
objects is implicitly deleted, so attempting to copy-construct new PrismNextStateGenerator
objects causes the compiler to fail.Some ideas:
Commit 0bdaf9e should contribute to fixing this
There is now an issue with the generators
vector. I think it is being allocated in the stack and then being deleted. I can either:
delete
statementshared_ptr
, but you can't cast std::shared_ptr<T>
to T *
without losing the benefits of smart allocation/deallocationThere is now an issue with the
generators
vector. I think it is being allocated in the stack and then being deleted. I can either:* Allocate a pointer if I know that it will exist for the life of the program and/or include a `delete` statement * Allocate a `shared_ptr`, but you can't cast `std::shared_ptr<T>` to `T *` without losing the benefits of smart allocation/deallocation
This is fixed in aa5a3bce218c3347a83141edf1dea93c730a33ca
Now we're back to the old issue--even though there are unique next-state generators
We may need to make a threadsafe NextStateGenerator
class, as Storm's is segfaulting due to a shared "valuator" class. This happens in Storm at <STORM SOURCE DIRECTORY>/src/storm/generator/NextStateGenerator.cpp:111
ETA:
It looks like there may need to be a mutex on the std::unique_ptr<storm::expressions::ExpressionEvaluator<ValueType>> evaluator;
data member in Storm's next state generator. The segmentation fault most likely has to do with that.
Update on the update:
The issue is in STORM--specifically, the STORM datastructures we are using were not designed to be threadsafe. In storm::generator::VariableIteration
in VariableInformation.h:123-133
, there are a series of std::vector
s that are being used to iterate over in the NextStateGenerator
. However, if one thread changes the values of what's in the vectors, all of the other iterators become invalid, which is what may be causing the segfault.
I am not sure how best to fix this without making changes to the STORM codebase, but I have a few ideas:
storm::generator::PrismNextStateGenerator
which locks a mutex on state expansion
We may just need to override void NextStateGenerator<ValueType, StateType>::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const {
That looks to be where the variableInformation is getting changed--and I think this is only happening with new states
Edit, nope. There are two:
storm::storage::sparse::StateValuations NextStateGenerator<ValueType, StateType>::makeObservationValuation() const
void NextStateGenerator<ValueType, StateType>::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const
Current stack trace of segfault:
(As of commit 036d155dca9401c19d2d1449abfa854df1297c1f)