Skip to content
This repository has been archived by the owner on Aug 26, 2022. It is now read-only.

Commit

Permalink
Fixed race condition in periodic timers (#438)
Browse files Browse the repository at this point in the history
  • Loading branch information
pdeligia authored Jun 17, 2019
1 parent 8517d39 commit 2b56ad2
Show file tree
Hide file tree
Showing 3 changed files with 135 additions and 1 deletion.
8 changes: 7 additions & 1 deletion Source/Core/Runtime/Timers/MachineTimer.cs
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,13 @@ public MachineTimer(TimerInfo info, Machine owner)
this.Owner = owner;

this.TimeoutEvent = new TimerElapsedEvent(this.Info);
this.InternalTimer = new Timer(this.HandleTimeout, null, this.Info.DueTime, Timeout.InfiniteTimeSpan);

// To avoid a race condition between assigning the field of the timer
// and HandleTimeout accessing the field before the assignment happens,
// we first create a timer that cannot get triggered, then assign it to
// the field, and finally we start the timer.
this.InternalTimer = new Timer(this.HandleTimeout, null, Timeout.InfiniteTimeSpan, Timeout.InfiniteTimeSpan);
this.InternalTimer.Change(this.Info.DueTime, Timeout.InfiniteTimeSpan);
}

/// <summary>
Expand Down
128 changes: 128 additions & 0 deletions Tests/Core.Tests/Machines/Timers/TimerStressTest.cs
Original file line number Diff line number Diff line change
@@ -0,0 +1,128 @@
// ------------------------------------------------------------------------------------------------
// Copyright (c) Microsoft Corporation. All rights reserved.
// Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
// ------------------------------------------------------------------------------------------------

using System;
using System.Collections.Generic;
using System.Threading.Tasks;
using Microsoft.PSharp.Timers;
using Xunit;
using Xunit.Abstractions;

namespace Microsoft.PSharp.Core.Tests
{
public class TimerStressTest : BaseTest
{
public TimerStressTest(ITestOutputHelper output)
: base(output)
{
}

private class SetupEvent : Event
{
public TaskCompletionSource<bool> Tcs;

public SetupEvent(TaskCompletionSource<bool> tcs)
{
this.Tcs = tcs;
}
}

private class T1 : Machine
{
private TaskCompletionSource<bool> Tcs;

[Start]
[OnEntry(nameof(InitOnEntry))]
[OnEventDoAction(typeof(TimerElapsedEvent), nameof(HandleTimeout))]
private class Init : MachineState
{
}

private void InitOnEntry()
{
this.Tcs = (this.ReceivedEvent as SetupEvent).Tcs;

// Start a regular timer.
this.StartTimer(TimeSpan.FromTicks(1));
}

private void HandleTimeout()
{
this.Tcs.SetResult(true);
this.Raise(new Halt());
}
}

[Fact(Timeout= 6000)]
public async Task TestTimerLifetime()
{
await this.RunAsync(async r =>
{
int numTimers = 1000;
var awaiters = new Task[numTimers];
for (int i = 0; i < numTimers; i++)
{
var tcs = new TaskCompletionSource<bool>();
r.CreateMachine(typeof(T1), new SetupEvent(tcs));
awaiters[i] = tcs.Task;
}

Task task = Task.WhenAll(awaiters);
await WaitAsync(task);
});
}

private class T2 : Machine
{
private TaskCompletionSource<bool> Tcs;
private int Counter;

[Start]
[OnEntry(nameof(InitOnEntry))]
[OnEventDoAction(typeof(TimerElapsedEvent), nameof(HandleTimeout))]
private class Init : MachineState
{
}

private void InitOnEntry()
{
this.Tcs = (this.ReceivedEvent as SetupEvent).Tcs;
this.Counter = 0;

// Start a periodic timer.
this.StartPeriodicTimer(TimeSpan.FromTicks(1), TimeSpan.FromTicks(1));
}

private void HandleTimeout()
{
this.Counter++;
if (this.Counter == 10)
{
this.Tcs.SetResult(true);
this.Raise(new Halt());
}
}
}

[Fact(Timeout = 6000)]
public async Task TestPeriodicTimerLifetime()
{
await this.RunAsync(async r =>
{
int numTimers = 1000;
var awaiters = new Task[numTimers];
for (int i = 0; i < numTimers; i++)
{
var tcs = new TaskCompletionSource<bool>();
r.CreateMachine(typeof(T2), new SetupEvent(tcs));
awaiters[i] = tcs.Task;
}

Task task = Task.WhenAll(awaiters);
await WaitAsync(task);
});
}
}
}

0 comments on commit 2b56ad2

Please sign in to comment.