Lindsey Kuper

In a couple of days, I’m headed to the WoDet workshop, which is co-located with ASPLOS in Salt Lake City this year. WoDet is a workshop devoted to determinism and correctness in parallel programming, and there’s some good stuff on this year’s schedule.

At WoDet I’ll be presenting our new paper, “Joining Forces: Toward a Unified Account of LVars and Convergent Replicated Data Types”, that describes our first steps toward bringing together LVars and CRDTs. In one direction, we discuss extending CvRDTs to support threshold reads; in the other direction, we discuss extending LVars to support general inflationary updates, rather than just the least-upper-bound updates that they support now.

In practice, we already use general inflationary updates, which we call “bump” operations, in a couple of the applications that we’ve implemented with LVish – for example, they’re handy for implementing monotonic counters, which play a crucial role in the HashRF algorithm that PhyBin uses. But we haven’t added general inflationary updates to the LVars formalism yet, nor have we shown that they don’t interfere with determinism. So, that’s one of the things I want to do next. I’m starting by adding support for “bump” operations to the lambdaLVish Redex model1 – if it doesn’t look like anything’s happened there in a while, nudge me to work faster!

In the adding-threshold-reads-to-CvRDTs direction, the paper sketches out the basic idea, but we have yet to do any work implementing it. Although we’ve gotten some interest, we don’t know yet if threshold reads of CvRDTs will be useful in practice. If nothing else, though, I think it would be nice to be able to use lattices to reason about both eventually consistent and strongly consistent reads within the same system. Since real systems allow one to make consistency choices at the level of individual queries, it would be nice if our formalisms could handle per-query consistency choices, too.

Finally, also appearing at WoDet will be my colleague Praveen Narayanan’s paper on implementing graph algorithms in LVish using a bulk-retry mechanism. This is a milestone of sorts: the first publication on LVars or LVish that I’m not an author of! I hope to be the non-author of many more LVars papers one day.

  1. “lambdaLVish” is the new name for the LVish calculus from our POPL ‘14 paper. I renamed it to minimize confusion with the LVish Haskell library. ↩

Comments