Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

State Exploration Multithreading #17

Open
ifndefJOSH opened this issue Jul 7, 2022 · 5 comments
Open

State Exploration Multithreading #17

ifndefJOSH opened this issue Jul 7, 2022 · 5 comments
Assignees
@ifndefJOSH
Labels
enhancement New feature or request optimization
Milestone
STAMINA 2.5 - STA...

Comments

@ifndefJOSH
Copy link
Collaborator

Part of the improvements for STAMINA 2.5 involve asynchronous multithreaded exploration of states by multiple threads as requested by the user. Commit c099b02 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 ifndefJOSH added enhancement New feature or request optimization labels Jul 7, 2022
@ifndefJOSH ifndefJOSH self-assigned this Jul 7, 2022
@ifndefJOSH
Copy link
Collaborator Author

Progress report:

  • Added lockable queue
  • Added thread skeleton
  • Added template for implementation

@ifndefJOSH
Copy link
Collaborator Author

Progress report:

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

@ifndefJOSH
Copy link
Collaborator Author

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

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

@ifndefJOSH ifndefJOSH mentioned this issue Jul 13, 2022
Closed
@ifndefJOSH
Copy link
Collaborator Author

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 ifndefJOSH linked a pull request Jul 13, 2022 that will close this issue
Multithreading for State Building #18
Closed
@ifndefJOSH
Copy link
Collaborator Author

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.

@ifndefJOSH ifndefJOSH pinned this issue Sep 21, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ifndefJOSH ifndefJOSH

Labels
enhancement New feature or request optimization
Projects
None yet
Milestone
STAMINA 2.5 - STAMINA 2.0 with dynami...
Development

Successfully merging a pull request may close this issue.

Multithreading for State Building fluentverification/stamina-storm
1 participant
@ifndefJOSH