Missing tutorial on optimizing the number of interleavings / analysis speed
essen opened this issue · 3 comments
I'm currently using default Concuerror options, other than things related to file locations or test names.
I've ran into a test that would have taken up close to an hour to finish. The test isn't too complex, it basically starts and stops a Ranch listener twice. But this involves a large number of processes and ets operations. The same test with only one start and stop takes 1404 interleavings and finishes in a matter of seconds.
I've found while looking at the tests that finishing the test function with receive after infinity -> ok end is a good way to ensure that the other processes did everything they could before the test function returns. I'm assuming there's some special handling in Concuerror because receive after infinity -> ok end in the middle of a test function leads to errors. Nevertheless this allowed me to get rid of a monitor and reduced the number of interleavings by a few hundreds on the single start/stop test.
There's probably other tips you may share. I haven't found them but perhaps I didn't look long enough.
Finally, there are options to limit the depth or the total number of interleaving explored and so on, but it is unclear what this means in terms of evaluating the correctness of the program, and it is also not clear how Concuerror decides which interleavings will not be explored.
I feel Kostis may have discussed this in a conference talk but it would be good to have around in text form.
Sorry for leaving this unaddressed for so long... I have now revised a post I wrote back in April about it and will merge/publish it as soon as tests for the new related option pass.
Post is live at https://concuerror.com/tips.html !
Wow thanks! I'll review it during the coming weeks.