Potential bug with race condition

[Ulimo]

Hi, this might be a user error, but I got the examples working and got correct bug reports.

But the following code:

[Fact]
public async Task Test()
{
    long counter = 17;

    var task1 = Task.Run(() =>
    {
        var val = counter;
        counter -= val;
    });
    var task2 = Task.Run(() =>
    {
        var val = counter;
        counter -= val;
    });

    await Task.WhenAll(task1, task2);

    Assert.Equal(0, counter);
}

[Fact]
[Microsoft.Coyote.SystematicTesting.Test]
public void CoyoteTest()
{
    var configuration = Configuration.Create().WithTestingIterations(10);
    var engine = TestingEngine.Create(configuration, Test);
    engine.Run();
}

Does not produce any bugs. in some cases this can return -17 instead of 0, but I cant get coyote to produce that result.

Changing to this:

[Fact]
public async Task Test()
{
    long counter = 17;

    var task1 = Task.Run(async () =>
    {
        var val = counter;
        await Task.Delay(1);
        counter -= val;
    });
    var task2 = Task.Run(async () =>
    {
        var val = counter;
        await Task.Delay(1);
        counter -= val;
    });

    await Task.WhenAll(task1, task2);

    Assert.Equal(0, counter);
}

produces the bug report correctly, is this expected behaviour or should the first example also produce a bug?

[akashlal]

This is expected behavior. By default, Coyote does not interrupt tasks at memory accesses. It only interrupts them at certain Task APIs (such as the await that you inserted in the second program). You can try the flag --rewrite-memory-locations. It is experimental, but it would add scheduling points at memory accesses.

[Ulimo]

Thank you for the quick response, rewrite memory locations was already default set to true, but then I know!

[Ulimo]

I changed my code to this and it seems to produce the correct results

[Fact]
public async Task Test()
{
    long counter = 17;

    var task1 = Task.Run(() =>
    {
        var val = counter;
        SchedulingPoint.Interleave();
        counter -= val;
    });
    var task2 = Task.Run(() =>
    {
        var val = counter;
        SchedulingPoint.Interleave();
        counter -= val;
    });

    await Task.WhenAll(task1, task2);

    Assert.Equal(0, counter);
}

So for now I guess I just have to add interleave to places where I want it to check.

[pdeligia]

Thanks @Ulimo and @akashlal, you also need to enable: Configuration.WithMemoryAccessRaceCheckingEnabled (or if you run from command line: --enable-memory-access-races). The --rewrite-memory-locations flag is for enabling/disabling the rewriting itself (which is indeed on by default), but you also have to enable the feature during testing (off by default to avoid exploding the schedule-space).

@Ulimo can you try this and let us know? (But the automated memory-access interleaving feature is indeed experimental and might not work for every single scenario as Akash said.)