Support Happens-Before Constraints in Spec.AllowsConcurrent

[Tomperez98]

Add happens-before constraints to Spec.AllowsConcurrent for linearizability checking

Problem

Spec.AllowsConcurrent validates a group of concurrent operation calls by searching for some sequential ordering that explains the observed responses. This supports sequential consistency, but not full linearizability.

Linearizability additionally requires preserving real-time (wall-clock) precedence: when one operation completes before another begins, the first must appear before the second in the linearization. Today, AllowsConcurrent treats all operations as mutually concurrent and freely reorders them, so it cannot distinguish a valid linearization from one that violates real-time ordering.

Solution

Extend Spec.AllowsConcurrent with an optional happensBefore parameter:

public (bool IsValid, string Message, StateProfile UpdatedStateProfile) AllowsConcurrent(
    StateProfile stateProfile,
    IList<(IOperation operation, object request, object response)> concurrentCalls,
    IEnumerable<(int before, int after)> happensBefore)

Each edge (before, after) constrains the search to orderings where the call at index before appears before the call at index after. Operations without a happens-before relationship are still reordered freely.

Callers derive edges from wall-clock timing: whenever one call completes before another starts, add a happens-before edge. Overlapping calls remain unordered. The resulting partial order (a DAG) models any concurrent history.

This is additive and backward-compatible — the existing two-parameter overload delegates to the new one with an empty edge set.

How it works

ContractStepFunction already participates in Accordant's state-graph exploration. Each step function can be enabled or disabled depending on the current state. This PR adds a predecessor gate: a step function with happens-before predecessors is disabled until all predecessor step IDs appear in the current linearization path.

The path is built by StateGraph.ExploreStateGraph as it traverses orderings. When a step function's ApplyInternal sees that its predecessors haven't all run yet, it returns null (disabled), pruning that branch of the search.

Files changed

File	Change
Accordant/StepFunction/ContractStepFunction.cs	Added _predecessorIds field, SetPredecessorIds(), and applies predecessor gate in ApplyInternal(IState, path)
Accordant.Operations/Operation/Spec.cs	Added three-parameter AllowsConcurrent overload with edge validation and predecessor wiring
Tests/Accordant.Operations.Tests/OperationTests.cs	6 new tests (see below)

Tests

Test	What it covers
PrunesInvalidOrderings	Edge that contradicts the only possible ordering → rejected
RedundantEdgeDoesNotChangeResult	Edge already satisfied by all valid orderings → accepted
TransitiveChain	A→B→C where B is both predecessor and dependent → exercises GUID stability
MultiplePredecessors	A→C and B→C → exercises multi-predecessor accumulation
SelfLoopThrows	Edge (i, i) throws ArgumentException
OutOfRangeIndexThrows	Edge with index outside bounds throws ArgumentException

[Tomperez98]

@microsoft-github-policy-service agree

[imnaseer]

[imnaseer]

Thank you - looks good!