The S# model checker currently preallocates all memory buffers that is uses during model checking. While this allows for an efficient implementation, it has two main drawbacks:
- The allocations are often huge, making them slow for fast analyses (e.g., small models or formula violations that are quickly found).
- The user has to change configuration settings such as state counts, etc., especially for models with large state vectors that easily result in out-of-memory situations.
The model checker should alternatively support dynamic memory allocations, growing its buffers as needed. Naturally, memory should still be allocated in large chunks to avoid any significant performance decreases. In particular, state hashing could become more complicated, as all discovered states might have to be rehashed when the state buffer is grown. Depending on the performance impact of state rehashing, other allocation strategies should be explored.
The S# model checker currently preallocates all memory buffers that is uses during model checking. While this allows for an efficient implementation, it has two main drawbacks:
The model checker should alternatively support dynamic memory allocations, growing its buffers as needed. Naturally, memory should still be allocated in large chunks to avoid any significant performance decreases. In particular, state hashing could become more complicated, as all discovered states might have to be rehashed when the state buffer is grown. Depending on the performance impact of state rehashing, other allocation strategies should be explored.