Conference Presentation, Keynote
Lindsey Kuper: Abstractions for Expressive, Efficient Parallel and Distributed Computing
Jane StreetLindsey Kuper, Ron, Laura, Kunle Olokutun, Asante Toney, Neil Conway, Peter Alvaro, Carl, Nikki Vazou
- The researcher anticipates making progress in parallel and distributed computing by developing unifying abstractions and high-level representations of programmer intent to enable smart scheduling and optimizations.
- A research agenda will connect SMT solvers for neural network verification with language-based approaches for parallel and distributed systems, including the development of new domain-specific solvers with built-in support for reasoning about lattices and partial orders over the next five years to life.
- Plans involve extending the LVAR API to use events and event handlers for parallel graph traversal and parallelizing solvers themselves to achieve guaranteed deterministic parallel SMT solving, a goal that is hypothesized but currently untested.
- The speaker expects to create a framework for quickly building high-performance domain-specific solvers to democratize solver hacking, allowing domain experts to create custom solvers without SMT internal expertise, though the current process for regular users remains difficult.
- Predictions indicate that using higher-level ReLU primitives and constraints will make the verification of large neural networks tractable and efficient, avoiding the exponential runtimes associated with eager splitting, though current state-of-the-art tools still lag behind the requirements for modern reasonably sized networks.
- Performance expectations for the Parallel Accelerator tool include running Black-Scholes code on 36 threads in half a second (over 40 times faster than original code) and stencil computation in 1.4 seconds (more than 600 times faster than Julia code), with a fallback to sequential execution if specific operations cannot be parallelized.
- The quasi-determinism result guarantees that if two executions end, their configurations are identical or one is an error configuration; hitting the error case implies a synchronization bug, with error messages potentially identifying the exact races.
- Verification of determinism in LVARs relies on programmer assumptions regarding library properties like commutativity, and future work intends to call an SMT solver to verify type classes such as
Ordto ensure data structures are true lattices, as no type system currently proves this within the Elvar library. - The "freeze" operation is expected to allow retrieval of exact LVAR contents while raising exceptions for any subsequent state-changing rights, and the speaker notes uncertainty regarding the completeness claims made by domain experts for verified properties in systems like the aircraft collision avoidance system.
- Risks identified include the "Parallel Accelerator" providing poor error messages typical of research-quality code, the difficulty of extending APIs for certain algorithms, and the limitation that verifying properties for low-level inputs like camera pixels remains a harder problem than for high-level inputs.