Support Happens-Before Constraints in Spec.AllowsConcurrent

[Immad (imnaseer)]

Accordant currently provides two related ways to validate observed operation results against a specification:

• Spec.Allows validates an operation sequentially from the current state.
• Spec.AllowsConcurrent validates a group of operation calls by checking whether their observed results can be explained by some valid sequential ordering.

The second capability supports linearizability checking.

Linearizability and sequential consistency are closely related, but they differ in one important respect:

• Sequential consistency requires that the observed results can be explained by some sequential ordering of the operations.
• Linearizability requires such a sequential ordering while also preserving real-time, or wall-clock, precedence. When one operation completes before another begins, the first operation must appear before the second in the linearization.

When every operation in a group is mutually concurrent—meaning that all their execution intervals overlap—there is no real-time ordering to preserve between them. In that case, linearizability and sequential consistency impose the same requirement: any sequential ordering that explains the results is acceptable.

Spec.AllowsConcurrent handles this case well. For example, suppose two clients concurrently attempt to reserve the same available resource. One client will succeed and the other will fail. Accordant considers both possible sequential orderings and determines whether one of them explains the observed responses.

A fully sequential history can also be represented today by validating one operation at a time with Spec.Allows, or by using Spec.AllowsConcurrent with a single operation.

The limitation arises when a history contains both overlapping operations and known real-time ordering constraints.

Consider this execution:

A starts
B starts
A completes
C starts
B completes
C completes

In this history:

• A and B overlap, so either can be linearized first.
• B and C overlap, so either can be linearized first.
• A and C do not overlap. Because A completed before C started, A must be linearized before C.

The operations therefore form a partial order rather than either a simple sequence or a set of fully mutually concurrent calls.

Today, placing A, B, and C in the same Spec.AllowsConcurrent call does not preserve the constraint that A happened before C. The checker can consider an ordering in which C appears before A. Such an ordering can satisfy sequential consistency, but it is not a valid linearization of the observed history because it violates wall-clock precedence.

Proposed change

Extend Spec.AllowsConcurrent so that callers can specify that one operation call happened before another.

For the example above, the caller will provide the relationship:

A → C

Accordant will then consider only sequential orderings that preserve this dependency. Operations without a happens-before relationship will still be reordered freely.

This will allow Spec.AllowsConcurrent to represent a general concurrent history as a DAG:

• nodes represent operation calls and their observed responses;
• edges represent known happens-before relationships;
• valid linearizations are sequential orderings that respect those edges.

The same capability will allow Accordant to validate recorded request-and-response traces together with their wall-clock timing. Accordant can already validate the observed operations and responses; the additional timing information will let it preserve real-time ordering by deriving a happens-before dependency whenever one operation completes before another begins. Operations whose execution intervals overlap will remain unordered.

This will be an additive, backward-compatible change. Existing uses of Spec.AllowsConcurrent without dependencies will continue to behave as they do today, treating all supplied operations as mutually concurrent.

Most of the primitive building blocks for this feature already exist: Accordant can already validate sequential operations and search for a valid ordering of concurrent operations. The requested extension is to constrain that search using caller-provided happens-before relationships.

With this addition, Accordant will support full linearizability checking for general, partially ordered operation histories.

[Tomás Pérez Álvarez (Tomperez98)]

This is what I learned implementing this -> #31

Accordant explores orderings by building a state graph. At each state, any remaining step function can be picked and applied. So to implement this we can add a gate: a step function with predecessors refuses to run until all its predecessors have appeared earlier.

What this enables:

Before this PR, Accordant linearizability checking was limited to fully concurrent groups (all operations overlap) or fully sequential ones. Now dependencies can be expressed A and B overlap, then C starts after A ends

[Immad (imnaseer)]

Thank you for contributing Tomás Pérez Álvarez (@Tomperez98) - genuinely appreciated.

[Immad (imnaseer)]

With this feature checked-in, now we'll have to see how to either update the existing doc pages, or add a new one that talks about this. A sample that's given a set of request response pairs along with wall-clock time, and then analyzes it, and then automatically either calls spec.Allows (if no overlap) or spec.AllowsConcurrent with happens-before (if overlap) can be useful. And if we did that, we would have to build some safeguards around number of concurrent calls as too many at the same time can take a long time to validate. The redeeming factor here is that most bugs can be found with just a few concurrent races (particularly when paired with deterministic simulation testing techniques, or even randomly injected delays/sleeps) in the backend so this isn't a big limitation in practice.

Thank you for the work here!