Lindsey Kuper: Abstractions for Expressive, Efficient Parallel and Distributed Computing

Deterministic Parallel and Distributed Computing via Lattice-Based Structures

• Problem Definition: The speaker addresses two core challenges: building correct and efficient parallel systems and building correct and efficient distributed systems across networks with partitions and unbounded latencies.
• Core Hypothesis: High-level abstractions can enable efficiency by providing the runtime system with enough information to make smart scheduling and optimization choices, contradicting the view that high performance requires low-level coding.
• IVARs vs. LVARs:
  • IVARs (Immutable Variables) guarantee determinism by allowing only a single write to a variable; reads block until that write occurs.
  • IVARs are insufficient for algorithms requiring multiple updates to a shared state (e.g., adding multiple items to a shopping cart).
  • LVARs (Lattice Variables) generalize IVARs to allow multiple writes, provided those writes are commutative (order-independent) and inflationary (state only grows within a lattice).
• Threshold Reads:
  • LVAR reads utilize "threshold reads" where a read blocks until the data lattice reaches a specific threshold set.
  • The read returns the specific threshold element crossed, not necessarily the exact current state, ensuring a deterministic result regardless of timing.
  • Legal threshold sets must satisfy the property of pairwise incompatibility.
• Extensions for Complex Algorithms:
  • Parallel graph traversal, traditionally difficult for deterministic models, is enabled via event handlers (callbacks triggered by state changes) and a freeze operation (a non-blocking read that stops further writes and raises an exception if violated).
  • The system offers quasi-determinism: executions either produce the exact same result or a consistent error (e.g., "write after freeze"), rather than arbitrary incorrect results.
• Distributed Systems Connection:
  • The approach extends to distributed systems using Conflict-Free Replicated Data Types (CRDTs).
  • LVAR-style threshold reads can query CRDTs deterministically even in eventually consistent systems, blocking only until the query's threshold is met on any replica, not all.
  • This reduces synchronization costs while maintaining deterministic query results.
• Proof Technique:
  • Determinism is proven via a property called independence, an inference rule stating that independent effects commute even when memory states overlap, similar to the frame rule in separation logic.

Non-Invasive Domain-Specific Languages for Productivity

• The Two-Language Problem: Researchers and scientists often write code in productive languages (Python, Julia, MATLAB) for prototyping, but must port critical sections to efficiency languages (C++, Fortran) to scale, sacrificing maintainability and productivity.
• Parallel Accelerator:
  • A non-invasive, embedded Domain-Specific Language (DSL) for Julia implemented as a package (parallelaccelerator.jl).
  • It allows parallelization of existing Julia code with minimal changes: importing a library and adding an @acc macro annotation.
  • Supports two implementation modes: a library mode (Julia-based) for debugging and a native high-performance mode for deployment.
• Performance Results:
  • Black-Scholes Benchmark: A 100-million-element array operation achieved over 40x speedup (0.5s vs 22s) on a 36-core machine compared to plain Julia, and outperformed MATLAB's default parallelization.
  • Image Stencil (Blur): Achieved a 600x speedup (1.4s vs ~900s) using the run_stencil construct compared to plain Julia.
  • Comparison to C++: In cases where expert C++ implementations were available, the Parallel Accelerator achieved performance within a factor of two of the expert low-level implementation.
• Adoption and Impact:
  • While the package itself fell out of the top 20 most popular Julia packages, the technology was ported to Python and integrated into the Numba compiler as a major external contribution, enabling multi-threading with a single flag.
  • The technology also served as the basis for a deep neural network DSL (PLDI 2016) and the HPAT distributed analytics toolkit.
• Design Trade-offs:
  • Non-invasive DSLs differ from strict embedded DSLs (like those using monads) by keeping the boundary between host language and DSL porous, allowing interaction with general code but requiring careful handling of error messages which are often in the context of the host language.

Formal Verification of Neural Networks via SMT Solvers

• Motivation: Safety-critical systems (e.g., aircraft collision avoidance) require formal verification, but traditional neural network representations lack certification due to their complexity and "black box" nature.
• Case Study: Replacing a 120-million-entry lookup table (requiring hundreds of gigabytes) with a neural network (~few megabytes) for an aircraft collision avoidance system.
• Verification Strategy:
  • Properties of the neural network are encoded as a Satisfiability Modulo Theories (SMT) formula, specifically using the theory of linear real arithmetic.
  • The Challenge: ReLU activation functions introduce non-linearity, requiring the solver to split them into disjunctions, which causes an exponential explosion in search space (e.g., $2^{300}$ combinations for sub-networks).
  • The Solution: A lazy ReLU splitting technique was developed, introducing a custom domain-specific theory solver within the SMT architecture.
  • This allows the solver to defer splitting ReLUs, pruning the search space significantly (e.g., requiring only 22 splits instead of 300 for the same verification).
• Efficiency Gains:
  • Properties that were impossible to verify previously became tractable, reducing proof times from "the lifetime of the universe" to tens of hours.
  • This demonstrates the principle that high-level domain knowledge (ReLU primitives) integrated into the solver enables efficiency unattainable by eager compilation to pure SAT.

Future Research Agenda

• Domain-Specific Solvers: The speaker proposes developing new SMT solvers with baked-in support for reasoning about lattices and partial orders, tailored for parallel and distributed computing.
• Parallelizing Solvers: A "holy grail" goal is to create a guaranteed deterministic parallel SMT solver where subtasks can safely share state (monotonic growth) without race conditions.
• Democratizing Solver Development:
  • Goal: Create a framework for building high-performance domain-specific solvers that does not require deep expertise in SMT internals.
  • Inspiration: Similar to the Delite framework for high-performance DSLs, this would allow domain experts (e.g., distributed systems researchers) to build custom theory solvers without being SMT experts.
• Verified LVARs: A proposed future project involves using type systems (e.g., Liquid Haskell) to formally verify that LVAR library implementations strictly adhere to commutativity and inflationarity constraints, moving beyond runtime assumptions.
• Scalability Limitations: Current verification techniques handle networks of a few hundred neurons but struggle with modern, large-scale networks; the bottleneck is often the formulation of meaningful properties for low-level inputs (e.g., image pixels).