You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There's been some research in the past demonstrating it's feasible to speed up model checking with SIMD instructions by processing several states at once. In practice, doing this is quite challenging, but a recent post gives clues of how to do this better using some AVX-512 tricks. I'm still not convinced we can feasibly implement general optimisation but we should at least evaluate this.
Taking this one step further, we may even be able to "vectorise" a model that e.g. uses a value_t of uint8_t by packing eight of these into a uint64_t. We may be missing support to do some of the conditional enabling, but I think the only way to know for sure is to try and build it.
There's been some research in the past demonstrating it's feasible to speed up model checking with SIMD instructions by processing several states at once. In practice, doing this is quite challenging, but a recent post gives clues of how to do this better using some AVX-512 tricks. I'm still not convinced we can feasibly implement general optimisation but we should at least evaluate this.
Taking this one step further, we may even be able to "vectorise" a model that e.g. uses a
value_t
ofuint8_t
by packing eight of these into auint64_t
. We may be missing support to do some of the conditional enabling, but I think the only way to know for sure is to try and build it.Also of relevance: http://cppcast.com/2018/11/jeff-amstutz/
The text was updated successfully, but these errors were encountered: