microsoft/coyote

Documentation describing different exploration strategies?

jhwj9617 opened this issue · 2 comments

jhwj9617 commented

I'm trying to learn about the different strategies, but the docs don't have a clear description of each one.
I'm referring to random, prioritization, fair-prioritization, probabilistic, rl, dfs, portfolio.

An perhaps a sample of when would use each one.

akashlal commented

So far we've been developing these strategies in the research world (through published papers) and that a user of coyote need not have to understand them. With that objective, the recommendation is to always use the 'portfolio' strategy. Portfolio runs several strategies in parallel and stops as soon as a bug is hit. It is not easy to describe precisely which one to use and when.

pdeligia commented

Thanks @jhwj9617 and @akashlal. One note to avoid confusion: we currently do not support portfolio strategy thru the TestingEngine API. I have been wanting to add it for a while now (and there is a PR for that), will try to do that for the next release.

Now as Akash mentioned, this can be an advanced topic, and honestly for most bugs we have seen so far in production services using different strategies (other than the default random) does not matter, even random will find them. Usually more advanced strategies are useful for very deep bugs, e.g. ones that require very complex interleavings and execution paths to be found. Adding documentation and some bug examples to educate users on the different strategies is a good idea on the long term, but our current thinking is to keep this as transparent and lightweight as possible for most users. Portfolio is a great option for this since all the handpicked schedulers will be used in turn as Akash said and we can tune it over time.

With the above in mind, my recommendation right now is to not try switch to another strategy (unless you have discussed directly with us first about your scenario, and we have a good reason to do that), and only switch to portfolio once that is available, since it will make things transparent. Need to experiment with this, but we will actually most likely make portfolio the default (instead of current random) so you won't even need to think that at all.