Segmentation fault(s): various places in `multithreading` branch

[ifndefJOSH]

Current stack trace of segfault:

#0  0x00007ffff62239f1 in storm::generator::NextStateGenerator<double, unsigned int>::load(storm::storage::BitVector const&) () from /usr/local/lib/libstorm.so
#1  0x00007ffff51275eb in stamina::builder::threads::IterativeExplorationThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::exploreState (this=0x55555580a520, stateProbability=...)
    at /home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/threads/ExplorationThread.cpp:274
#2  0x00007ffff51272a0 in stamina::builder::threads::IterativeExplorationThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::exploreStates (this=0x55555580a520)
    at /home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/threads/ExplorationThread.cpp:231
#3  0x00007ffff5126d3f in stamina::builder::threads::ExplorationThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::mainLoop (this=0x55555580a520)
    at /home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/threads/ExplorationThread.cpp:82
#4  0x00007ffff50f840c in std::__invoke_impl<void, void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> (
    __f=@0x555555872e50: &virtual stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::mainLoop(), __t=@0x555555872e48: 0x55555580a520)
    at /usr/include/c++/10/bits/invoke.h:73
#5  0x00007ffff50f834f in std::__invoke<void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> (
--Type <RET> for more, q to quit, c to continue without paging--
    __fn=@0x555555872e50: &virtual stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::mainLoop()) at /usr/include/c++/10/bits/invoke.h:95
#6  0x00007ffff50f82bf in std::thread::_Invoker<std::tuple<void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> >::_M_invoke<0ul, 1ul> (this=0x555555872e48)
    at /usr/include/c++/10/thread:264
#7  0x00007ffff50f8278 in std::thread::_Invoker<std::tuple<void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> >::operator() (this=0x555555872e48)
    at /usr/include/c++/10/thread:271
#8  0x00007ffff50f825c in std::thread::_State_impl<std::thread::_Invoker<std::tuple<void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> > >::_M_run (
    this=0x555555872e40) at /usr/include/c++/10/thread:215
#9  0x00007ffff4860ed0 in ?? () from /lib/x86_64-linux-gnu/libstdc++.so.6
#10 0x00007ffff2dc5ea7 in start_thread () from /lib/x86_64-linux-gnu/libpthread.so.0
#11 0x00007ffff469faef in clone () from /lib/x86_64-linux-gnu/libc.so.6

(As of commit 036d155)

[ifndefJOSH]

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.
• The copy constructor for the storm::generator::NextStateGenerator objects is implicitly deleted, so attempting to copy-construct new PrismNextStateGenerator objects causes the compiler to fail.

Some ideas:

• Figure out why storm's next state generator has the copy constructor deleted and change that--contribute that to upstream storm.
• OR Create our own copy-safe next-state generator
• OR Create all next state generators in the model builder object and pass them all in IFF we are using threads

[ifndefJOSH]

Commit 0bdaf9e should contribute to fixing this

[ifndefJOSH]

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:

• 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

[ifndefJOSH]

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:

* 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 aa5a3bc

Now we're back to the old issue--even though there are unique next-state generators

[ifndefJOSH]

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.

[ifndefJOSH]

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::vectors 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:

• Create a threadsafe drop-in replacement for storm::generator::PrismNextStateGenerator which locks a mutex on state expansion
  • The problem with this is that if it locks on all expansion, the benefit of multithreading is for nought. However, I think that if a state was previously expanded, it will just return information about that state which it has cached. If this is not implemented in STORM (although I think it is), we can implement it in our extension and contribute changes upstream.
• Find exactly where in the variable information the vector is being modified and mutex on just that. I think it's only modified at the beginning, and if that's the case, we won't really have much of a problem locking just that section
• Ditch programming and research and live in the mountains away from civilization as a hermit with two dogs and no computers

[ifndefJOSH]

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

[ifndefJOSH]

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