# The LVar that was, after all

Last year, I wrote a post about a so-called LVar data structure that, upon closer inspection, turned out not to be an LVar at all. In that post, I proposed a way to fix the problem, but the fix seemed to be at the expense of another desirable property of the data structure. In this post, I return to that example, but this time, I’ll explain how we can have our cake and eat it, too!

## Recap: the lattice that wasn’t

The offending data structure was intended to store the result of a parallel logical “and” operation. It received one write each from two sources, which we could call the “left” and “right” inputs, each of which could be either `True` or `False`.

If it received `True` from both inputs, it would end up in a final state, which we called `TrueTrue`, indicating that the result was true, and if it received `False` from at least one input, it would end up in a final state indicating that the result was false, which we just called `F`.

If it received more writes than it expected, and they conflicted — for instance, a `True` from the left, followed by a `True` from the right, and after that a `False` from the left — it would end up in an error state, called `Top`. And there were also a few intermediate states that it might take on along the way to any of these states, such as a state called `TrueBot` in which `True` had been received from the left and nothing else had been received yet, and `BotTrue`, in which `True` had been received from the right and nothing else had been received.

We wrote down the set of states that the data structure could take on as a partial order. The trouble was that the partial order wasn’t a join-semilattice, since not all pairs of states had a join; the so-called join operation wasn’t associative and therefore wasn’t actually a join. In particular, the join of `BotTrue` and `F` was `F`, which, joined with `TrueBot`, was again `F`. But `TrueBot` joined with `BotTrue` was `TrueTrue`, which, joined with `F`, was `Top`. Since the data structure wasn’t a join-semilattice, all bets were off; it couldn’t be an LVar.

In fact, consider that an execution starting with a write of `True` from the left, then `True` from the right, and finally `False` from the left would end in `Top`, but if the writes happened in a different order — if the execution started with `True` from the right, followed by `False` from the left and then `True` from the left, we’d be in the `F` state, not `Top`. Since LVars are supposed to end up in the same state regardless of the order in which writes occur to them, this was Very Bad.

Fortunately, we could define the data structure’s states and the partial order on them differently, and regain associativity and hence LVar status.

Unfortunately, when we did this, it seemed to be at the price of early answers. The nice thing about the original formulation was that it let us threshold on the states `TrueTrue` and `F`, so that as soon as we reached either one, we could “short circuit” and return a result. In particular, in the original formulation, if we ever got a write of `False` from either the left or the right input, a threshold read could return `F` as soon as that write of `False` happened, by using { `TrueTrue`, `F` } as its threshold set.

But with the lattice-that’s-really-a-lattice, we couldn’t return anything upon reaching the `FalseBot` or `BotFalse` states. Instead, we would have to wait until reaching one of the final states of `FalseTrue`, `TrueFalse`, or `FalseFalse`, even though `FalseBot` and `BotFalse` also amount to false.

Fortunately, it turns out there is a way to get short-circuiting behavior from a lattice like this! It requires a slight change to how threshold reads work. Let’s take a look.

## Threshold reads and activation sets

First, let’s review what a threshold read does. The goal of a threshold read is to make it so that when we read from a data structure, the result will be a deterministic function of the set of all writes to the data structure that occur in the entire execution. The order in which those writes occur, and the order in which the read is interleaved with the writes, shouldn’t matter. It’s kind of a tall order. How do we accomplish this?

One way to do it is to define a threshold set for the read. A threshold set is a set of what we call activation sets, each consisting of what we call activation states. In the case of our parallel “and” computation, one of those activation sets is the set of states that the data structure might be in when at least one `False` has been written:

{ `FalseBot`, `BotFalse`, `FalseTrue`, `TrueFalse`, `FalseFalse` }

When we reach a point in the lattice that’s at or above any of these states, then we know that the result is false. The other activation set is the singleton set

{ `TrueTrue` }

When we reach `TrueTrue`, we know that the result is true. But we have to wait until then, because we don’t know if the result is true unless both the left and right inputs have each contributed `True`. So a state like `TrueBot` doesn’t appear in any of our activation sets.

The threshold set is, again, a set of all the activation sets. So the entire threshold set we’d use for reading from our lattice would be:

{ { `FalseBot`, `BotFalse`, `FalseTrue`, `TrueFalse`, `FalseFalse` }, { `TrueTrue` } }

Using this threshold set, we can do a threshold read. The semantics of a threshold read is as follows: if the data structure’s state reaches (or surpasses) any state or states in a particular activation set, then the threshold read returns that entire activation set, regardless of which of its activation states were reached. If no state in any activation set has yet been reached, the threshold read will block.

In our case, as soon as either input writes `False`, our threshold read will unblock and return the first activation set. Hence we have the short-circuiting behavior that we want; we don’t have to wait for a second input if the first input is `False`. If, on the other hand, both inputs write `True`, the threshold read will unblock and return { `TrueTrue` }.

In a real implementation, of course, the value returned from the threshold read could be more meaningful to the client — for instance, we could just return `False` or `True` instead of returning an activation set. But the translation from { `FalseBot`, `BotFalse`, `FalseTrue`, `TrueFalse`, `FalseFalse` } to `False` could just as easily take place on the client side. In either case, the result returned from the threshold read is the same regardless of which of the activation states caused it to unblock, and it is impossible for the client to tell whether the actual state of the lattice is, say, `TrueFalse` or `FalseFalse` or some other state containing `False`.

## Incompatibility

In order for the behavior of a threshold read to be deterministic, it must be unblocked by a unique activation set in the threshold set. We ensure this by requiring that elements in an activation set must be pairwise incompatible with elements in every other activation set. That is, for all distinct activation sets Q and R in a given threshold set: for all q in Q and for all r in R, the join of q and r is the greatest element of the lattice, in this case, `Top`. In our running example, we have two distinct activation sets, so if we let Q be { `TrueTrue` } and let R be { `FalseBot`, `BotFalse`, `FalseTrue`, `TrueFalse`, `FalseFalse` }, the join of `TrueTrue` and r must be `Top`, where r is any element of R. We can easily verify that this is the case. Furthermore, since the lattice of states that our data structure can take on is finite, we can quickly verify that our join function actually computes a least upper bound, as we’ve seen before.

Why is incompatibility necessary? Consider the following (illegal) “threshold set” that does not meet the incompatibility criterion:

{ { `FalseBot`, `BotFalse` }, { `TrueBot`, `BotTrue` } }

A threshold read corresponding to this so-called “threshold set” will unblock and return { `FalseBot`, `BotFalse` } as soon as a state containing `False` is reached, and it will unblock and return { `TrueBot`, `BotTrue` } as soon as a state containing `True` is reached. The trouble with such a threshold read is that there exist states, such as `FalseTrue` and `TrueFalse`, that could unblock either activation set. If the left input writes `False` and the right input writes `True`, and these writes occur in arbitrary order, then the threshold read will return a nondeterministic result, depending on the order in which the two writes arrive. With the incompatible threshold set we showed, the threshold read would deterministically return `False` — although, if the `True` arrived first, the read would have to block until the `False` arrived, whereas if the `False` arrived first, it could unblock immediately.

## How is this different? How is it better?

In the formulation of threshold reads I’ve just described, a threshold set is a set of sets of states. In the old way of doing things, though, a threshold set was merely a set of states.

For instance, under the old system, if we wanted to do a (non-short-circuiting!) threshold read from our LVar, we could just use the threshold set

{`TrueTrue`, `FalseTrue`, `TrueFalse`, `FalseFalse`}

and the threshold read would unblock and return a particular element, such as `TrueFalse`, whenever that element was reached or surpassed.

Incompatibility played an important role in the old formulation of threshold sets, too: all the elements in a threshold set had to be pairwise incompatible. In the new formulation, the elements of each activation set have to be incompatible with elements of every other activation set, but the activation sets themselves don’t have to be pairwise incompatible. Indeed, in our example, `FalseBot` and `FalseTrue` are quite compatible with each other, even though they’re in the same activation set. The important thing is that they, and all the other elements of that activation set, are incompatible with `TrueTrue`.

Since elements of each activation set have to be incompatible with elements of every other activation set, we have a way to mechanically turn old-style threshold sets into new-style threshold sets and retain the old semantics: just have every member of the old-style threshold set become a singleton activation set. So, instead of the old-style threshold set

{ `TrueTrue`, `FalseTrue`, `TrueFalse`, `FalseFalse` }

we’d have

{ { `TrueTrue` } , { `FalseTrue` } , { `TrueFalse` } , { `FalseFalse`} }

which is perfectly legal under the new formulation. It retains the non-short-circuiting semantics of the old formulation, though. To fix that, we can combine the latter three activation sets into one activation set, and throw in `FalseBot` and `BotFalse` to boot, giving us

{ { `TrueTrue` }, { `FalseBot`, `BotFalse`, `FalseTrue`, `TrueFalse`, `FalseFalse` } }

which is in fact exactly the new-style threshold set proposed above.

In retrospect, I think that the `F` state in the so-called “lattice” of the original, flawed formulation was reaching for something like activation sets. It tried to collapse different states containing `False` into one state, just like the activation set of all the states containing `False` does. The difference is that, with the new formulation, this collapse happens just a bit later, at reading time, rather than at writing time.

I don’t know if there is a way to mechanically translate from old-style threshold sets to those that allow short-circuiting. I also don’t know how to find out if a given program is “as short-circuiting as it can be”. (I think the idea of “short-circuiting” generalizes beyond this parallel-and example, and that there is in general a tension between determinism and short-circuiting.) I also don’t know if there is a lattice-theoretical or category-theoretical interpretation of what is going on with our activation sets. If you know of one and can explain it to me, I’d really appreciate that!

## Where to read more

My collaborators and I have been mulling over this new formulation of threshold sets for a while, and we mentioned it in passing in a recent paper. The first place that it’s been spelled out in detail, though, is in a new draft paper that we just submitted.

The new paper is mostly about what it means to do LVar-style threshold queries of distributed data structures, which I haven’t discussed at all here, but we decided to describe this new, more general form of threshold read while we were at it. Parts of this post are from section 2 of that paper, so if you’ve read this far, you already have a head start on the paper.

Comments welcome!