Modality’s core technology is one that can reconstruct a partial order of happenings in a system that’s been instrumented with it. We call this a causal order, or, to put it another way, the binary relation upon which this order is predicated is a “causes” relation. The notation we use when we want to say that causes is .

Additionally, another way to think about a partial order is as a graph, more precisely, a directed acyclic graph (DAG). Modality builds a DAG from the events and the snapshots that it records, produces, and merges and we call that graph a trace. This post talks about a way we can have a dialog with a trace—a way to ask it questions, and a way to find a common language with which to do so.

The Logic of DAGs

Let’s begin this section by defining a straw-graph. We’ll call it G.

If we had such a trace that took the shape of G, what kind of questions might we want to ask it? Here’s some examples:

1. Did occur?
2. Is there a path from to ?
3. Is there a path from to that passes through ?
4. Is there a case where or occur, but are not causally connected to one another?

One way that we can state each of these questions is with a logical expression. Here’s a translation of each of these questions into their logic syntax.

Let’s break these down.

The appearance of a vertex or node in an expression refers to its presence in the graph^[1]. As we stated in the front matter of this post, the right-pointing arrow denotes a “causes” relation. The last expression may have an unfamiliar cast of characters—∧, ¬, and ∨ —these mean, respectively, “and”, “or”, and “not”. All together, that last expression is saying more precisely that either A or C are present in the graph, and there is not a path from B to C or a path from C to B.

To ask a question of the graph is to hand it one of these expressions and ask if that expression is true of itself. With our small straw-graph G, we can, fairly trivially I might add, look at the graph and know that yes, for each of these questions, the graph would answer back in the affirmative.

However, when the graph is much larger, the expressions more complex, and a computer the medium through which we have this conversation, we need a way to systematize the evaluation of expressions like this—which brings us to the next section.

A Small Step in the Right Direction

A common way to evaluate a logical expression is to first normalize it until it reaches the point that it can be normalized no further. This is what’s called its normal form. For this case, we want to normalize our expressions until they reach that point that they are a series of disjunctions^[2]—logical “or”s. This is called disjunctive normal form (DNF). Here’s an example of the steps towards a DNF for our last expression from the previous section:

We begin with

The first step we’d need to take is to distribute that negation (¬) to the two sides of its nested disjunction. That would give use something like

From here, we need to break up that nested ∨ so that each side of it has its own expression alongside the following conjunctions (logical “and”s).

This expression is now in DNF, as it’s been normalized to the point that it’s a series of (just one in this case) of disjunctions.

Translating DNF to a Graph’s Native Tongue

It turns out there’s a way to take the DNF of an expression and turn it back into a graph. These DNFs-as-graphs are called binary decision diagrams (BDDs). Put coarsely, a BDD illustrates an expression’s evaluation as a DAG, kind of like the control flow graph we get from the SSA/IR of a programming language. The BDD of our normalized expression from the previous section would look like this:

A BDD works by unifying variables in an expression’s DNF. The B and C on either side of the DNF expression are of course the same B and C, so we unify them in our BDD. After we’ve unified, we now need to verify. Each arrow in this graph is labeled either t or f—they denote the path to take if an expression is either true or false, respectively. For the first vertex, if it evaluates to false, that’s okay—we’re not done yet. The disjunction gives us another option, we can pick back up with C, and then verify that each of the negations are also true, if they are, then this expression evaluates to true. Any other path leads us to false.

What Good is a BDD Anyway?

By representing an assertion against a trace as a graph, we can actually present to a user, graphically, what part of the assertion which they provided actually failed by giving them the BDD overlayed with the path that evaluation took in that diagram. It’s not just a semi-formal way to think about the evaluation of an assertion, it’s an actual, concrete, useful part of providing a better experience to a Modality user when they’re needle-searching in their own haystacks consisting of many, many straws.

---

1. In a more verbose syntax we may write A true, but for the sake of legibility, we’ll state the assumption here, that if a vertex is in an expression, that means we expect its presence. This is of course dualized by the absence of a vertex in a trace, where the vertex at hand is negated: . ↩︎

2. More precisely, both sides of each disjunction need to be flat, that is, they ought not contain any nested , as those should be lifted into each distinct expression for any conjunction they may be adjacent to. ↩︎