Skill v1.0.0

Trusted Publisher100/100

microsoft/accordant/concurrency

──Details

PublishedOctober 1, 2026 at 05:01 AM

Content Hashsha256:9a40784048ef2370...

Git SHA

──Files

Files (1 file, 7.3 KB)

SKILL.md7.3 KBactive

SKILL.md · 271 lines · 7.3 KB

version: "1.0.0" name: accordant-concurrency description: How to test for race conditions using concurrent tests and linearizability - use this skill when testing concurrent operations or finding race condition bugs

Concurrency Testing in Accordant

Accordant can test concurrent operations to find race conditions. It runs operations simultaneously and validates that results are linearizable — explainable by some sequential ordering.

The Problem: Race Conditions

Consider a booking system where each slot can only be booked once:

Slot "9am" is available.
 
Concurrent requests:
  - Alice: BookSlot("9am")
  - Bob: BookSlot("9am")
 
Valid outcomes (one must fail):
  ✓ Alice succeeds, Bob gets Conflict
  ✓ Bob succeeds, Alice gets Conflict
 
Invalid outcome (BUG!):
  ✗ Both succeed — double booking!

Linearizability

The correctness criterion for concurrent operations:

Results must be explainable by some sequential ordering of the operations.

If Alice got 200 and Bob got 409 → Valid (as if Alice went first) If both got 200 → Invalid (no sequential order explains this)

Defining the Spec

csharp

[State]
public partial class BookingState
{
    public Dictionary<string, string?> Slots { get; set; } = new();  // null = available
}
 
var spec = new Spec<BookingState>();
 
spec.Operation<string, ApiResult<Slot>>("CreateSlot", (slotId, state) =>
{
    if (state.Slots.ContainsKey(slotId))
        return Expect.That<ApiResult<Slot>>(r => r.IsConflict).SameState();
 
    return Expect.That<ApiResult<Slot>>(r => r.IsSuccess && r.Data.IsAvailable)
           .ThenState<BookingState>(s => s.Slots[slotId] = null);
});
 
spec.Operation<(string SlotId, string Customer), ApiResult<Slot>>("BookSlot", (request, state) =>
{
    var (slotId, customer) = request;
 
    if (!state.Slots.TryGetValue(slotId, out var bookedBy))
        return Expect.That<ApiResult<Slot>>(r => r.IsNotFound).SameState();
 
    if (bookedBy != null)
        return Expect.That<ApiResult<Slot>>(r => r.IsConflict, $"Already booked by {bookedBy}").SameState();
 
    return Expect.That<ApiResult<Slot>>(r => r.IsSuccess && r.Data.BookedBy == customer)
           .ThenState<BookingState>(s => s.Slots[slotId] = customer);
});

Running Concurrent Tests

csharp

[Test]
public async Task ConcurrentTests_FindsRaceConditions()
{
    var spec = CreateSpec();
 
    spec.ExecuteWith<BookingApiClient>()
        .Bind<string, ApiResult<Slot>>("CreateSlot", (c, id) => c.CreateSlot(id).Result)
        .Bind<(string, string), ApiResult<Slot>>("BookSlot", (c, r) => c.BookSlot(r.Item1, r.Item2).Result);
 
    var inputs = new InputSet
    {
        spec.GetOperation<string, ApiResult<Slot>>("CreateSlot").With("9am", "Create slot"),
        spec.GetOperation<(string, string), ApiResult<Slot>>("BookSlot").With(("9am", "Alice"), "Alice books"),
        spec.GetOperation<(string, string), ApiResult<Slot>>("BookSlot").With(("9am", "Bob"), "Bob books"),
    };
 
    var testCases = spec.GenerateConcurrentTests(
        new BookingState(),
        inputs,
        new TestGenerationOptions { MaxDepth = 4 });
 
    var context = spec.CreateTestingContext();
    context.Register(new BookingApiClient(CreateHttpClient()));
 
    var results = await spec.RunTests(
        context,
        new BookingState(),
        testCases,
        new TestExecutionOptions
        {
            BeforeEachAsync = async _ => await ResetDatabase()
        });
 
    var failures = results.Where(r => !r.Success).ToList();
    Assert.IsEmpty(failures, $"Failed: {failures.FirstOrDefault()?.LastFailureMessage}");
}

How Concurrent Tests Work

Sequential prefix sets up a known state
N operations execute simultaneously
All N! orderings are checked for linearizability
If any ordering explains the results → Valid
If no ordering works → Race condition found!

Example Test Case

Sequential: CreateSlot("9am")
Concurrent: [BookSlot(Alice)] || [BookSlot(Bob)]

Validation

Accordant tries both orderings:

Try Alice → Bob:

BookSlot(Alice) from available → expects Success
BookSlot(Bob) from booked → expects Conflict

Try Bob → Alice:

BookSlot(Bob) from available → expects Success
BookSlot(Alice) from booked → expects Conflict

If actual results match either ordering → Valid

MaxConcurrencyLevel

Control how many operations run concurrently:

csharp

var options = new TestGenerationOptions
{
    MaxConcurrencyLevel = 3  // Up to 3 concurrent operations
};

Higher concurrency finds more bugs but increases test count (N! orderings to check).

Finding the Bug

When a race condition exists, Accordant reports:

FAILURE in concurrent test case:
  Sequential prefix: CreateSlot("9am")
  Concurrent: BookSlot(Alice) || BookSlot(Bob)
  
  Observed results:
    BookSlot(Alice) → 200 OK, slot booked by Alice
    BookSlot(Bob) → 200 OK, slot booked by Bob
  
  ERROR: No linearization found!
    - If Alice first: Bob should get 409 Conflict
    - If Bob first: Alice should get 409 Conflict
    - Both succeeded → RACE CONDITION BUG

Fixing Race Conditions

Common approaches:

Database-Level Locking

csharp

using var transaction = await _db.Database.BeginTransactionAsync(
    IsolationLevel.Serializable);

Optimistic Concurrency (ETags)

csharp

var slot = await _db.Slots.FindAsync(slotId);
if (slot.ConcurrencyToken != expectedToken)
    throw new ConcurrencyException();

Application-Level Lock

csharp

private static readonly SemaphoreSlim _lock = new(1, 1);
 
await _lock.WaitAsync();
try { /* booking logic */ }
finally { _lock.Release(); }

Common Race Condition Patterns

Double-Booking

Two users book the same resource simultaneously:

csharp

// Both execute this check at the same time, both see "available"
if (slot.IsAvailable)
{
    slot.BookedBy = customer;  // Both write!
    await _db.SaveChangesAsync();
}

Lost Updates

Two concurrent updates, one overwrites the other:

csharp

// Thread A reads balance = 100
// Thread B reads balance = 100
// Thread A: balance = 100 + 50 = 150, saves
// Thread B: balance = 100 + 30 = 130, saves (overwrites A!)

Counter Races

Increment operations that don't use atomic operations:

csharp

// Wrong - not atomic
var count = await GetCount();
await SetCount(count + 1);
 
// Right - use atomic increment
await _db.ExecuteSqlRawAsync("UPDATE counters SET value = value + 1 WHERE id = @id");

Test Case Structure

Concurrent test cases have:

Sequential prefix: Operations to reach a specific state
Concurrent operations: 2+ operations that fire simultaneously
Optional sequential suffix: Verify final state

csharp

// Generated test case structure:
// Prefix: CreateSlot("9am") → Slot available
// Concurrent: [BookSlot(Alice), BookSlot(Bob)]  
// Suffix: GetSlot("9am") → Verify winner

Best Practices

Test write-write conflicts: Focus on operations that modify the same data
Include read-after-write: Add GET operations to verify final state
Keep concurrency level reasonable: 2-3 concurrent ops usually sufficient
Reset state properly: Concurrent tests are sensitive to leftover state
Run multiple times: Race conditions are timing-dependent

Next Steps

Async Operations: Model background work that completes over time
Troubleshooting: Debug failing concurrent tests

All versions v1.0.1 →