Parallel and distributed systems are notoriously difficult to build correctly or efficiently. In parallel systems, the manipulation of shared state can cause unintended behavior in the presence of unpredictable task scheduling, while in distributed systems, the manipulation of replicated state can cause unintended behavior in the presence of an unreliable network. Meanwhile, decades of research have not yet produced a general solution to the problem of automatic program parallelization.

In this talk, I’ll discuss how my research addresses these challenges from both theoretical and applied points of view. My work on lattice-based data structures, or LVars, proposes new foundations for expressive deterministic-by-construction parallel and distributed programming models. My work on non-invasive domain-specific languages for parallelism gives programmers language-based tools for safe, deterministic parallelization. The guiding principle and goal of both of these lines of work is to find the right high-level abstractions to express computation in a way that not only does not compromise efficiency, but actually enables it. I’ll conclude by discussing the role that this principle of finding the right efficiency-enabling abstractions can play in my ongoing investigation into SMT-based verification of neural networks.

Presented by: Lindsey Kuper