Why does coyote find no bugs in this code?

[MaximTkachenko]

Hi,
I use this sample to play with coyote:

[Microsoft.Coyote.SystematicTesting.Test]
public static async Task ParallelIncrement()
{
    CheckRewritten();
    
    var incrementer = new Incrementer();
    await incrementer.ExecuteAsync(1000);

    Assert.Equal(1000, incrementer.Number);
}

private static void CheckRewritten()
{
    if (!Microsoft.Coyote.Rewriting.RewritingEngine.IsAssemblyRewritten(typeof(Incrementer).Assembly))
    {
        throw new Exception(string.Format("Error: please rewrite this assembly using coyote rewrite {0}",
            typeof(Incrementer).Assembly.Location));
    }
}

public class Incrementer
{
    public int Number { get; private set; }

    public async Task ExecuteAsync(int iterations)
    {
        var tasks = new Task[iterations];

        for (int i = 0; i < iterations; i++)
        {
            tasks[i] = Task.Run(() => Number++);
        }

        await Task.WhenAll(tasks);
    }
}

And I expect that coyote will find a bug since Incrementer increments Number in parallel using Task.Run. I use this script to run this test:

dotnet build -c Release
coyote rewrite bin\Release\net6.0\CoyoteTests.dll
coyote test bin\Release\net6.0\CoyoteTests.dll -m ParallelIncrement -i 50

Why does coyote find no bugs here? Are there some limitations?

[akashlal]

Coyote is not designed to explore low-level data races. For the bug to manifest in your code, there needs to be a context switch after Number has been read but before the incremented value is stored back to it. Coyote will not explore such context switches on its own. You can force it as follows:

var t = Number + 1;
SchedulingPoint.Interleave();
Number = t;

I would expect that coyote will find the bug then.

By default, coyote only explores context switches at synchronization points (acquire/release a lock) or at Task APIs.