microsoft/coyote

Rewiring serializes task runs?

jhwj9617 opened this issue ยท 9 comments

I'm on version 1.5.3

And I noticed the tasks that I spawn in my unit test become serialized after rewiring.

            var tasks = new List<Task>()
            {
                Task.Run(() =>
                {
                    for (int i = 0; i<5; i++)
                    {
                        Console.WriteLine("A");
                    }
                }),
                Task.Run(() =>
                {
                    for (int i = 0; i<5; i++)
                    {
                        Console.WriteLine("B");
                    }
                }),
            };

            Task.WaitAll(tasks.ToArray());

This will always print "AAAAABBBBB" or "BBBBBAAAAA".
But if I don't rewire and I get Assembly is not rewritten for testing, see https://aka.ms/coyote-rewrite.
I will get expected interleavings, e.g. "AAABABBABB"

Why does rewiring have this result? Shouldn't it properly explore all these interleavings?

@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 to await, interleavings around lock (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:

            var tasks = new List<Task>()
            {
                Task.Run(async () =>
                {
                    for (int i = 0; i<5; i++)
                    {
                        Console.WriteLine("A");
                        await Task.Yield();
                    }
                }),
                Task.Run(async () =>
                {
                    for (int i = 0; i<5; i++)
                    {
                        Console.WriteLine("B");
                        await Task.Yield();
                    }
                }),
            };

            Task.WaitAll(tasks.ToArray());

There is also a quite new coyote API called SchedulingPoint for explicitly introducing your own interleavings e.g. in mocks (no-op in production; outside of coyote test engine), see here. You can try this in your original non-async example by replacing my await Task.Yield() with e.g. SchedulingPoint.Interleave().

@jhwj9617 If you anticipate that your code can have low-level data races, i.e., there are shared objects (like Console.WriteLine) that will be accessed by multiple threads without synchronization, then you should add a SchedulingPoint just before (or just after) such access.

@jhwj9617
But if I don't rewire and I get Assembly is not rewritten for testing, see https://aka.ms/coyote-rewrite.
I will get expected interleavings, e.g. "AAABABBABB"

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 :)

Thanks for the explanation @akashlal @pdeligia
I noticed these interleaves do occur when I introduce some async keywords, like lock (myObject){}, then Coyote understands where this scheduling point is.
However, I haven't yet observed this with ReaderWriterLockSlim from System.Threading library - which is what I'm testing with. The test will run into an actual deadlock. But I also found that WithSystematicFuzzingEnabled can detect these types of deadlocks/exceptions. The docs don't really explain what exactly this does.

@jhwj9617 unfortunately the WithSystematicFuzzingEnabled enables a new feature that we are in the process of tweaking and evaluating, so it's not documented yet (but we still expose it for folks who are interested in using it). But I am glad you discovered it as it can indeed get you around the ReaderWriterLockSlim, which we do not currently support in the default testing mode of Coyote (more on this below).

Basically, using WithSystematicFuzzingEnabled enables an alternative testing mode that injects (contextualized) delays to fuzz the concurrent schedule. This is a different (and more relaxed) approach to fully controlling and sequentializing the schedule that Coyote does by default (where it pauses all running tasks, and allows only one to proceed at a time, and at each scheduling point decides which task to go next, based on the underlying exploration strategy). As you can imagine, if Coyote does not understand the semantics of a synchronization primitive and does not intercept it (as it happens with ReaderWriterLockSlim in your case) it can easily result into a deadlock if it keeps scheduling something that gets blocked trying to acquire a lock.

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., ReaderWriterLockSlim in your case), which takes effort / time. The disadvantage is that systematic fuzzing is still quite early days so might not give as deep coverage as regular controlled testing yet, but you can still get good value out of it.

(Btw, if ReaderWriterLockSlim is very important for you, we can look into adding support for this so you can continue using the default systematic testing mode of coyote instead of fuzzing, but we need some time to schedule this. Let us know.)

Thanks for the clear answer @pdeligia
It is not hugely important, since systematic fuzzing is available for this purpose.
I would say some documentation describing supported/unsupported Task APIs and synchronization primitives (at least within the native .NET libraries) would be extremely helpful.

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

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).

Moving discussion here: #100