Refinement Checking

In order to check if a process Impl refines (in a particular semantic model) a process Spec, FDR firstly converts Impl and Spec into labelled transition systems, as described in Compilation. FDR then normalises the specification machine, as described in normal. FDR then explores the states of these processes in breadth-first order, checking that the states are related according to the semantic model. As soon as FDR finds a counterexample it immediately reports it. Thus, thanks to the breadth-first order, any counterexample that FDR returns will be minimal in the length of the trace (including taus).

In order to understand exactly how FDR visits state pairs during a refinement check, consider the following script:

channel a, b, c

P1 = a -> P2
P2 = P3 |~| P4
P3 = b -> P2
P4 = a -> P1

Q1 = a -> Q2
Q2 = b -> Q1

assert Q1 [T= P1

FDR initialises the search by looking at the state pair (Q1, P1) (nb. state pairs consist of a specification state and an implementation state). In the traces model, FDR only has to check that the events (excluding tau) offered by P1 are a subset of those offered by Q1, which is clearly the cases here. Hence, FDR now adds the successor state pairs for each event offered by P1 to the search. In this case, there is only one successor state pair after a, (Q2, P2).

When considering the state pair (Q2, P2) note that P2 does not offer any visible events, and therefore the event check is trivially true. FDR now needs to add any new state pairs to the search. In this case, the two state pairs (Q2, P3) and (Q2, P4) are added to the search. Note that the specification part of the state pair is kept the same because the implementation performs a tau. FDR will now consider the new state pairs. In particular, when it considers (Q2, P4) FDR will find a counterexample since the events offered by P4 are not a subset of those offered by Q2.

In order to reconstruct the trace that the invalid state pair was reached by, FDR stores a parent state pair of each state pair that it finds during the search. Thus, in the above example, FDR will set the parent of (Q2, P4) as (Q2, P2) and the parent of (Q2, P2) to (Q1, P1). Thus, FDR can reconstruct the counterexample trace by finding events that transition between (Q1, P1) and (Q2, P2), and (Q2, P2) and (Q2, P4). This will yield the trace <a, tau>, in this case.

Counterexamples

A counterexample to a refinement assertion consists of a trace leading to a particular state pair that are not related according the to semantic model in use. Thus, if the traces model is in use, then this must mean that the implementation can perform an event that the specification cannot. If the failures model is in use, then either the above case applies, or the implementation can refuse a set of events that the specification cannot. If the failures-divergences model is in use, then this must mean that either one of the above cases applies, or the implementation is divergent but the specification is not.

Uniqueness

If FDR is asked to generate multiple counterexamples then this motivates the question of what FDR considers distinct counterexamples to be. In all cases, only a single counterexample will be generated from a single state pair. Thus, if a state pair is reachable via two different traces then only one counterexample will be generated, regardless of the number requested. Further, once FDR has found a counterexample for a given state pair, it does not look at successors of the state pair to see if they are counterexamples. Thus, for FDR to report two distinct counterexamples the counterexamples must be distinct state pairs, and the second state pair must be reachable via a path that does not include the first state pair. For example, the following has two counterexamples since the two STOP states are reachable via distinct paths:

P1 = STOP |~| P2
P2 = STOP

assert P1 :[deadlock free [F]]

However, the following only has one counterexample, since the second invalid state pair is only reachable via the first invalid state pair:

P1 = a -> P2 [] b -> STOP
P2 = a -> P1

Spec = a -> Spec

assert Spec [T= P1

Note that both P1 and` P2 violate the property, but P2 is only reachable via P1 and thus is not considered.

Non-Determinism

As noted above, thanks to the breadth-first ordering that FDR visits the state pairs in, FDR will always pick the counterexample that is reachable in the fewest events (either tau or a visible event). Whilst this might imply that the counterexample returned is chosen deterministically, this is not the case when FDR is being used in parallel mode (i.e. refinement.bfs.workers is greater than 1) for two reasons:

  1. The predecessor state pair of each state pair is chosen by a race between the different processor cores on each ply. For example, if two different cores both discover the same state pair on the same ply, then the state pair that is marked as the new state pair’s predecessor is chosen non-deterministically. This can result in a different trace being returned. The following script should exhibit this behaviour:

    channel a, b, c
    
    P = a -> b -> Q [] b -> a -> Q
    Q = c -> STOP
    
    R = a -> R [] b -> R [] c -> R
    
    assert R [F= P
    

    Note that there is precisely one state that violates the refinement, Q, but there are two different routes to Q, via either <a, b> or <b, a>. Hence, since the states b -> Q and a -> Q are discovered on the same ply of the breadth-first search the winner will be chosen non-deterministically (assuming that they are visited by different cores). This should result in FDR non-deterministically returning either the counterexample trace <a, b, c> or <b, a, c>.

  2. On each ply of the search, there is essentially a race between the processor cores to find a counterexample: the first core that finds a counterexample wins. For example, consider the following refinement check:

    channel a, b
    
    P = a -> STOP |~| b -> STOP
    
    assert STOP [T= P
    

    There are two different counterexamples to this assertion: either the event a can be performed, or the event b. Since these counterexamples are both found on the second ply of the search (the first ply simply explores the tau transitions available from the starting state), FDR will pick the counterexample non-deterministically, providing the two different states are picked by different cores.

In general use, the fact that different counterexamples are produced should hopefully not be an issue. Unfortunately, there is no efficient way to make a parallel version of FDR deterministically return the same counterexample. If it is important that the same counterexample is returned each time then refinement.bfs.workers should be set to 1, thus disabling the parallel refinement checker. This will obviously result in a decrease in performance, but it does mean that the same counterexample will always be returned.

Implementation

Todo

Write

BTrees

Log-Space Merge Trees