Lindsey Kuper on Abstractions for Correct and Efficient Parallel Computing

My work asks how we build parallel systems that compute quickly and correctly, and distributed systems that remain correct across networks with partitions and unbounded delays. These areas have separate research cultures and vocabularies, so I look for abstractions that help us understand both.

I’ll discuss lattice-based data structures called LVars, a non-invasive language for parallelizing existing code, and verification of neural networks. The common idea is to express programmer intent at a high level in a way that enables efficiency rather than sacrificing it.

We often assume that performance requires getting closer to the hardware. But a high-level representation of intent can give a system information it needs for scheduling and optimization. The same principle can help formal verification of neural networks used in safety-critical settings.

Deterministic programming means that the same inputs yield the same observable outputs. Imagine my shopping cart at an online store represented by a shared map. I add a book and shoes in separate asynchronous threads, then read the cart in another thread.

When I ran a version of this program repeatedly, sometimes it returned both items, sometimes only the book, and sometimes only the shoes. The result depended on scheduling. Replicating the cart across machines would make the problem harder still.

The program is under-synchronized: we could wait for both writes before reading. But rather than fixing each program with ad hoc barriers, we can seek a programming model that guarantees deterministic outcomes for all programs written within it.

One established approach is an IVar: a shared variable written only once, whose reads block until the write arrives. When all communication uses IVars, the combination of a single write and blocking reads ensures determinism.

The cart example suggests a less restrictive option. Adding the book and adding the shoes do not overwrite one another; those updates commute. The nondeterminism appears when a read observes an intermediate state before both writes finish.

LVars permit multiple writes, provided they commute and are inflationary: every write leaves the state unchanged or moves it upward according to an application-specific lattice. Reads are restricted to threshold reads, which block until the state reaches an appropriate threshold.

In the cart lattice, the empty cart is at the bottom and states above it contain different quantities of books and shoes. The two writes can happen in either order and reach the same combined state. A read asking how many books are present blocks until the relevant threshold is crossed.

The read returns the threshold result, not necessarily the complete contents at the instant it unblocks. Shoes may or may not have arrived, but the answer about the two books remains deterministic. Think of a threshold set as a tripwire across the lattice.

Valid threshold sets require a property called pairwise incompatibility. A user of an LVar library need not work through that mathematics for each read: the library exposes only suitable operations. Its implementer must ensure the writes commute and are inflationary and that reads meet the threshold conditions.

Consider parallel graph traversal. Starting at a node, we mark it seen and explore its neighbors, potentially in separate threads. The set of seen nodes grows monotonically until all reachable nodes have been discovered and the set reaches a fixed point.

Set union fits the LVar model, but threshold reads alone cannot express the usual test asking whether a node has not yet been seen. Without a way to decide when to stop, a cycle in the graph could lead to repeated traversal.

We extend the API with events and handlers. A state-changing write produces an event, and a handler can run a callback when a new node arrives. A quiesce operation blocks until callbacks launched by that handler have finished.

We also add freeze, a non-blocking read of the exact contents after which state-changing writes raise an exception. If a program freezes too early, it cannot silently return an incomplete final result followed by successful conflicting writes: it may instead get a write-after-freeze error.

This is quasi-determinism. Two terminating executions produce the same result, or one ends in an error. An error signals a synchronization problem, and the message can identify the write and freeze that raced, helping the programmer debug it.

The proof concerns external outcomes, not identical sequences of execution steps. Its independence property captures the idea that a computation can take a step even if the starting store is larger in the relevant way, because independent effects do not interfere.

I compare this with the frame rule in separation logic. If a command transforms a state satisfying one condition into a state satisfying another, an unrelated disjoint property can remain true throughout. The rule helps us reason about what a program does not change.

Our independence property resembles a frame property, except the pieces of state may overlap while still not interfering. Knowing that effects can safely coexist gives the runtime freedom to schedule work across available parallel resources.

Distributed systems add replicated state and unreliable networks. Ideally every replica of the shopping cart would agree at all times, but that goal conflicts with high availability when network partitions prevent replicas from communicating.

The CAP tradeoff motivates weaker guarantees such as eventual consistency, where replicas may disagree temporarily but eventually converge. We then need an application-appropriate way to reconcile conflicting versions; simply selecting the latest write is not always what users want.

The Dynamo work gives the shopping cart as an example: an application may merge conflicting carts rather than discard one. Conflict-free replicated data types, or CRDTs, formalize related ideas using lattices: replicas can merge differing states using a least upper bound.

This suggests applying LVar-style threshold reads to CRDTs. A query asking whether a book is present could wait until a replica observes it, rather than waiting for every replica to agree. Such queries might offer deterministic observations without requiring full consistency everywhere, potentially reducing synchronization.

The next example comes from scientific computing. My friend Laura's group collects radar data from aircraft over Antarctica to study ice and the rock beneath it. She wants to think about geophysics, not manual memory management or scheduling parallel tasks.

A researcher may prototype in MATLAB, Python, R or Julia, then find the code too slow for larger inputs or finer resolution. Porting the slow part to C, C++ or Fortran, often with tools such as OpenMP, can improve speed but creates code that is harder to experiment with and maintain. This is the two-language problem.

High-performance domain-specific languages offer one response. Frameworks such as Delite give up some generality in exchange for both a high-level programming model and performance. Domain information tells a compiler more about the computation and can enable better optimization.

Yet an existing user must learn the DSL and port code, and a language that supports only 95% of the needed functionality can hit a cliff. Even a well-designed DSL cannot anticipate every future use case.

At Intel Labs we built Parallel Accelerator, a non-invasive embedded DSL for Julia. It focuses on speeding up existing numeric array operations rather than requiring users to rewrite their whole program in a separate language. A macro called @acc marks code for acceleration.

For a new construct such as runStencil, the package provides both a Julia library implementation and a high-performance native implementation. Users can turn off the compiler and use library mode for development and debugging, then enable compilation for deployment.

The first example is a Black-Scholes option-pricing benchmark. Its inputs are arrays of numbers and much of the function consists of pointwise arithmetic. The example is meant to show the type of code that can be parallelized, not to explain option pricing.

To accelerate it, we import the package and annotate the function with @acc; the rest remains ordinary Julia. Parallel Accelerator translates array operations to data-parallel maps, avoids some bounds checks when sizes are established, and fuses operations to avoid intermediate arrays.

With arrays of 100 million elements, the original Julia code took about 22 seconds. On a 36-core machine, the accelerated version took just over 13 seconds on one thread, benefiting from optimizations even without parallel execution.

With 36 threads, the run fell to roughly half a second, over 40 times faster than the original. This example was expressly chosen to illustrate the approach's strengths; we do not always see gains that large. The MATLAB comparison used its default parallel settings as well as a single-thread setting.

The results also highlight a Julia convention at the time: explicit loops could be faster than aggregate array operations, and some people worried that the library encouraged a non-idiomatic style. The Julia team supported the approach, but the discussion showed that tooling also influences how people write code.

A second example is a stencil computation. To blur a black-and-white image, update every pixel using a weighted average of its own value and those of its neighbors. The runStencil construct expresses this pattern while remaining close to the original array-style Julia.

On a large image over 100 iterations, plain Julia took almost 900 seconds. The accelerated version took under 40 seconds with one thread and about 1.4 seconds with 36 threads, more than 600 times faster in this example. Unlike Black-Scholes, this required using the domain-specific construct and rewriting a few lines.

Parallel Accelerator itself did not have a lasting major impact on Julia, but its technology influenced other systems. It served as a basis for work on deep neural networks and distributed analytics, and Intel colleagues ported it to Python and integrated it into Numba for multithreaded numerical code.

The final project concerns using SMT solvers to verify neural networks in safety-critical software. In such settings it is prudent, and sometimes legally required, to show rigorously that specific bad outcomes cannot occur. Verification tools have struggled to keep pace as neural networks enter these systems.

Stanford researchers wanted to reduce the storage needed for an aircraft collision-avoidance policy so that it would fit in memory on verified onboard hardware. They trained a neural network to approximate the original policy table, which greatly reduced storage but raised certification concerns.

The system takes sensor measurements once per second and produces one of five advisories: clear of conflict, a weak or strong left turn, or a weak or strong right turn. The original table gives scores for these choices across roughly 120 million possible encounter states and requires hundreds of gigabytes.

The trained network maps an encounter state to advisory scores while using about a thousand times less storage, only a few megabytes. Its outputs do not exactly match the original table, so the relevant question is whether the specific properties we care about still hold.

For example, we might want to establish that when another aircraft is close and approaching from the left, the network always recommends a strong right turn. We encode the network and the desired property as a formula and use an SMT solver to check it.

SAT asks whether a Boolean formula has a satisfying assignment. SMT, satisfiability modulo theories, extends the question to formulas involving expressions from a theory, such as linear real arithmetic. The solver can then reason about constraints on real-valued variables as well as Boolean structure.

Even for decidable theories, solving can be very slow. An eager SMT architecture reduces the entire problem to a Boolean SAT formula, but that can lose high-level structure. For example, reasoning directly about addition makes its commutativity easier to exploit than reasoning only over low-level Boolean expressions.

A lazy SMT architecture keeps a SAT solver and combines it with specialized theory solvers for domains such as arithmetic, arrays and bit vectors. Preserving domain structure lets the system apply knowledge at a higher level before reducing everything to Boolean cases.

For a neural network, even linear arithmetic is not enough by itself: nonlinear activation functions complicate the formula. A ReLU activation can be encoded as a disjunction, but eagerly passing every such choice to the SAT solver can make verification prohibitively slow.

My Stanford collaborators made the linear-programming theory solver aware of ReLU constraints. It can leave a ReLU unsplit while solving the rest of the problem and split only when necessary. That higher-level primitive made the aircraft-network verification tractable for the properties studied.

Each subnetwork in the example has 300 ReLU activations, giving 2^300 possible on-or-off combinations. The solver did not need to split all of them: one listed property had a maximum split depth of 22. The resulting checks could still take tens of hours, but that was far more practical than exploring every combination.

In a workshop paper, we also proposed using piecewise-linear approximations to extend this approach to other activations, such as sigmoid functions. At the time of the talk, that extension had not been implemented.

Looking forward, I want domain-specific solvers that understand structures relevant to parallel and distributed computing, including lattices and partial orders. I also want to parallelize solvers while safely sharing the information their subtasks discover as they process a formula.

My untested hypothesis is that deterministic techniques developed for other settings could help parallel SMT solving. The longer-term goal is to make it easier for domain experts to build high-performance theory solvers without becoming experts in every internal detail of an SMT solver.

Asked whether existing SMT solvers could serve as a starting point, I say yes in principle: systems such as Z3 and CVC4 already have solver cores and theory components. In practice, their open source code can still be difficult to modify, whether because of technical barriers, documentation or culture.

An audience member asks for comparison with low-level code. Our paper included expert parallel C++ implementations for three workloads. We considered it a success to get within about a factor of two of those implementations, although the slide did not show that comparison.

A non-invasive DSL is a kind of embedded DSL. The distinction is not rigid, but the aim is to make the boundary with the host language more porous. An LVar library such as Elvish is another embedded DSL, with operations organized in a monad and a clearer boundary with other code.

Parallel Accelerator cannot parallelize all Julia code: it targets a subset of aggregate numerical array operations and falls back to sequential execution when it cannot handle something. I recommend annotating small functions rather than huge blocks, so accelerated code can interact with the rest.

Error messages are another usability issue for embedded DSLs. They can appear in terms of the host language rather than the DSL, and making them useful takes significant effort. Parallel Accelerator's messages are not as good as they should be, which is a limitation of the research implementation.

Asked about Bloom and BloomL, I note the close connection. BloomL extends distributed programming over arbitrary lattices and aims for eventual consistency, but eventual convergence differs from determinism: a reader may still observe different intermediate states before replicas converge.

BloomL restricts non-monotonic operations throughout its model. With the Haskell LVar library, one can instead have a phase where a structure grows monotonically, freeze it, and then use it as an ordinary data structure. The projects developed concurrently and reveal useful connections between research communities.

A question compares Parallel Accelerator with auto-vectorization. It can only accelerate operations it knows; otherwise the sequential fallback preserves correctness but may be slow. Warnings or optimization advice about unsupported operations would be useful, though I do not have a complete answer for how to provide it.

Asked about the size of networks that can be verified, I say the state of the art is still inadequate. Reluplex handled networks larger than earlier SMT-based work, but the example split a larger system into subnetworks of about 300 neurons, still small compared with many modern networks.

Subsequent work using abstract interpretation has explored ways to prune or group parts of the search space more efficiently. But an even bigger challenge may be stating the property to verify. Aircraft position and speed provide relatively high-level inputs; a camera image represented by pixels makes a property such as avoiding pedestrians much harder to formulate.

Another question asks how we know the chosen collision-avoidance properties cover the important dangers. We do not claim a proof of complete functional correctness: we proved particular properties that could be written down. As with security, the value of a safety claim depends on what failures or threats are considered.

Finally, someone asks about statically verifying the LVar assumptions. Type systems such as Deterministic Parallel Java can express and check some commutativity properties. Our LVar library instead relies on its implementers to ensure that writes and threshold reads obey the required laws.

Verified LVars are on my research list. Work using Liquid Haskell to verify ordering laws suggests that an SMT-backed approach could also help establish the properties required of a lattice. The aim would be to check assumptions that the present library leaves to its implementer.