In graph theory, reachability is the notion of being able to get from one vertex in a directed graph to some other vertex. Note that reachability in undirected graphs is trivial–it is sufficient to find the connected components in the graph, which can be done in linear time.

Definition for Reachability: For a directed graph D = (V, A), the reachability relation of D is the transitive closure of its arc set A, which is to say the set of all ordered pairs (s, t) of vertices in V for which there exist vertices v0 = s, v1, …, vd = t such that (vi – 1, vi ) is in A for all 1 ≤ id.

Algorithms for reachability fall into two classes: those that require preprocessing and those that do not. For the latter case, resolving a single reachability query can be done in linear time using algorithms such as breadth first search or iterative deepening depth-first search.

Reachability has many times been modeled using Petri nets.

Producer & Consumer Reachability by Pataricza and Bartha

Because Petri nets can be used for modeling reachability and locks of source code, and the input for it and the symbolic atomistic model (SAM) is the same, too, it is natural to assume, that SAM can be used for modeling reachability and source code locks, too.

In fig above the different slices (parts of the graph) could be symbolic models captured from methods of threads of Java or C++ or other code. Typically some threads are consumers and some producers.

It is straightforward to visualizate logic of threads using the symbolic atomistic model as a base so that crtical resources can be seen as connective nodes between different parts of the threads.

Some links: