-
I'm on version 1.5.3 And I noticed the tasks that I spawn in my unit test become serialized after rewiring.
This will always print "AAAAABBBBB" or "BBBBBAAAAA". Why does rewiring have this result? Shouldn't it properly explore all these interleavings? |
Beta Was this translation helpful? Give feedback.
Replies: 9 comments
-
@jhwj9617 this is not a bug, but a feature: to tame state-space explosion, coyote does not explore an interleaving at every single instruction; instead, it explores interleavings in what we call "scheduling points". The most common scheduling points are calls to concurrent task APIs (e.g. If you try the following it should do what you expected:
There is also a quite new coyote API called |
Beta Was this translation helpful? Give feedback.
-
@jhwj9617 If you anticipate that your code can have low-level data races, i.e., there are shared objects (like |
Beta Was this translation helpful? Give feedback.
-
Btw, to elaborate a bit more why you got these interleavings when not doing binary rewriting, that is because these tasks (and underlying task scheduler) are not controlled by Coyote in that case (it requires binary rewriting to take control) and thus are in the scheduling mercy of the default uncontrolled TPL scheduler and can interleave arbitrarily :) |
Beta Was this translation helpful? Give feedback.
-
Thanks for the explanation @akashlal @pdeligia |
Beta Was this translation helpful? Give feedback.
-
@jhwj9617 unfortunately the Basically, using Systematic fuzzing is more flexible and does not have this issue as it simply fuzzes the schedule (without trying to control it). Imagine 2 tasks running in your test, the systematic fuzzing mode can choose to delay one of the tasks at specific points in the execution (these are pretty much the same as the scheduling points that we discussed earlier). By introducing such delays, Coyote tries to trigger a race condition that might break the test. Similar to default testing mode, Coyote can run as many such fuzzing test iterations as you want, in each iteration delaying (or not) tasks in different ways and points in the execution. Now the cool thing is that instead of doing it naively with fully randomized delays (that might overlap each other, canceling their effects, or delaying for too long slowing down the program), it has the ability to perform fuzzing in a more systematic + contextualized way (e.g., it knows that currently another task is being delayed, or was delayed in a previous iteration, so takes that into account to do more "clever" fuzzing decisions). But this contextualization is still WIP, so we don't actively advertise this feature, but you can still use it. Now saying all this, the benefit of using this fuzzing mode is that it can typically just work on most codebases without having us to explicitly support every single task API or synchronization primitive (e.g., |
Beta Was this translation helpful? Give feedback.
-
(Btw, if |
Beta Was this translation helpful? Give feedback.
-
Thanks for the clear answer @pdeligia Also, is this forum better to ask questions? https://gitter.im/Microsoft/coyote?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge |
Beta Was this translation helpful? Give feedback.
-
Thanks @jhwj9617, and absolutely agree with what you say about documenting these things. We are a small team so it has been a matter of prioritization, but we plan to enhance the documentation and add this things soon (open an issue to track this #335) -- thanks for the really useful feedback! It's totally fine -- and preferred -- to ask questions here on GitHub as issues (like you have been doing) or even discussions to have them in a centralized place. The gitter channel is also fine, but it has not been very active, and I personally do not monitor it often for that reason (we might actually remove it from the readme to keep things more streamlined). |
Beta Was this translation helpful? Give feedback.
-
Moving discussion here: #100 |
Beta Was this translation helpful? Give feedback.
@jhwj9617 this is not a bug, but a feature: to tame state-space explosion, coyote does not explore an interleaving at every single instruction; instead, it explores interleavings in what we call "scheduling points". The most common scheduling points are calls to concurrent task APIs (e.g.
Task.Run
,Task.Wait
,Task.WhenAll
,Task.Delay(...)
, etc), or calls toawait
, interleavings aroundlock
(and others). We have been adding more over time -- we do not currently have a list of all these in the docs (its a TODO).If you try the following it should do what you expected: