State Exploration Multithreading - Githubissues

fluentverification / stamina-storm

STAMINA - the STochiastic Approximate Model-checker for INfinite-state Analysis, integrated with the Storm model checking engine.

https://staminachecker.org

GNU General Public License v3.0

5 stars 2 forks source link

State Exploration Multithreading #17

Open ifndefJOSH opened 2 years ago

ifndefJOSH commented 2 years ago

Part of the improvements for STAMINA 2.5 involve asynchronous multithreaded exploration of states by multiple threads as requested by the user. Commit c099b02f34c1641ac739596567d4736388ec2c4e creates skeleton for this, but I have a couple of ideas/concerns.

Should the threads be in their own namespace?
Should they be in the same file as the builders?

ifndefJOSH commented 2 years ago

Progress report:

Added lockable queue
Added thread skeleton
Added template for implementation

ifndefJOSH commented 2 years ago

Progress report:

Added -j option. (464a33236bad815c86eea1012bedfce907e8731f)
Debugged templating order issue with *Thread classes
Working on changing StateType to StateAndThreadIndex where necessary
Removed unnecessary remapping method (9ac4e9499bd3c06c43b1699ed558ee220bcde1b3)

ifndefJOSH commented 2 years ago

The thread index is stored in an instantiation of storm::storage::sparse::StateStorage<stamina::builder::threads::ControlThread::StateAndThreadIndex<StateType>> but the builder class requires the StateStorage<> to be templated with just StateType. Not sure how to resolve this. Should I

Use two BitVectorHashmaps?
Try to figure out a way to force the generator to take the state storage

ifndefJOSH commented 2 years ago

An additional idea:

Create two classes:

One which inherits from storm::storage::sparse::StateStorage
One which inherits from storm::storage::BitVectorHashMap

Which will also store the thread values, rather than having a StateAndThreadIndex

ifndefJOSH commented 2 years ago

Other idea to add:

State ownership "expires" based on a LRU cache policy so the owned states hashmap will be a fixed size and thread ownership will be more even. This reduces the need for defragmentation.