When a spin lock is detected in the model checking mode, hundreds of events are added to the interleaving, reducing the analysis quality and the resulting interleaving simplicity. It would be better to cut off the sequence of events related to the detected spinlock.
When a spin lock is detected in the model checking mode, hundreds of events are added to the interleaving, reducing the analysis quality and the resulting interleaving simplicity. It would be better to cut off the sequence of events related to the detected spinlock.