accordant-concurrency

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

[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

[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, );
}

How Concurrent Tests Work

1. Sequential prefix sets up a known state
2. N operations execute simultaneously
3. All N! orderings are checked for linearizability
4. If any ordering explains the results → Valid
5. 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:

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

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

Optimistic Concurrency (ETags)

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

Application-Level Lock

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:

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

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

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

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

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

Best Practices

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

Next Steps

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