The Stanford Software Research Lunch is a weekly event on Thursday where students and researchers present their latest work to peers. Talks are open to anybody, but regular attendees are expected to give a presentation on their work.

Mailing list: software-research-lunch@lists.stanford.edu (subscribe via mailman)

Calendar: ical

Format: The lunch is held every week during fall, winter and spring quarter. The first week of every quarter is an organizational lunch where people can sign up to give a talk. If you'd like to give a talk, please contact Rohan Yadav.

Past quarters: Fall 2023, Spring 2023, Winter 2023, Fall 2022, Winter 2021, Fall 2020, Winter 2020, Fall 2019, Spring 2019, Winter 2019, Fall 2018, Spring 2018, Winter 2018, Fall 2017, Spring 2017, Winter 2017, Fall 2016.

Ordering Food: For suggestions for those ordering food for the lunch, see here.

10/3: Proving Query Equivalence Using Linear Integer Arithmetic

Time: Thursday, October 3, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Haoran Ding

Abstract: Proving the equivalence between SQL queries is a fundamental problem in database research. Existing provers model queries using algebraic representations and convert such representations into first-order logic formulas so that query equivalence can be verified by solving a satisfiability problem. The main challenge lies in 'unbounded summations', which is used to model common SQL features. Unfortunately, existing provers handle unbounded summations in an ad-hoc manner, which severely limits the verification capability.
SQLSolver is a new SQL equivalence prover, which can handle unbounded summations in a principled way. Our key insight is to use the theory of LIA*, which extends linear integer arithmetic formulas with unbounded sums. We augment the basic LIA* theory to handle several complex scenarios that arise from modeling real-world queries. Evaluated on 400 equivalent query pairs derived from Apache Calcite, Spark SQL, TPC-C, and TPC-H, SQLSolver successfully proves 388 pairs of them, which significantly outperforms existing provers.
https://dl.acm.org/doi/abs/10.1145/3626768

Food:

10/10: Solving the Phase Ordering Problem != Generating the Globally Optimal Code

Time: Thursday, October 10, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Ke Wang

Abstract: Phase ordering problem has been a long-standing challenge in compiler optimizations. Over the past four decades, a significant amount of effort has been devoted, and indeed, substantial progress has been made. However, in this paper, we raise questions about the overall significance of solving the phase ordering problem in the first place, as pursuing a solution to this problem may not align with the fundamental goal of compiler optimizations, i.e., generating the globally optimal code among all programs that compilers deem semantically equivalent to an input program.
Our findings, supported by both theoretical and empirical evidence, show that solving the phase ordering problem is not equivalent to generating such globally optimal code. To achieve this goal, we propose a theoretical approach, called infinitive iterative bi-directional optimizations (IIBO), which is guaranteed to converge to the globally optimal code for any input program. We realize IIBO into a practical algorithm and apply it to optimize real-world programs. Results show that IIBO frequently generates more efficient code than GCC/LLVM, two state-of-the-art industry compilers, as well as exhaustive search, which can be deemed the solution to the phasing ordering problem.
We are currently in active discussions with LLVM engineers on the possible incorporation of our findings into their next release. Given the significance and impact of our results, we expect our work to inspire new design principles for compiler development in the pursuit of generating the globally optimal code.

Food:

10/17: New Algorithms for High-Precision Floating-Point Arithmetic

Time: Thursday, October 17, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: David Zhang

Abstract: Floating-point arithmetic is an indispensable tool for computational modeling and simulation. Modern computing platforms have ubiquitous support for IEEE 754 single (binary32) and double (binary64) precision arithmetic. However, when these precision levels are insufficient, users are forced to turn to software emulation of higher-precision floating-point formats, which can be many thousands of times slower than native machine precision. In this talk, I will present ongoing work to develop new algorithms for high-precision floating-point arithmetic that are simultaneously faster and more accurate than previous work. These algorithms are completely branch-free, making them suitable for data-parallel processors, such as GPUs and SIMD CPUs. I will also present counterexamples to several algorithms in the published literature, highlighting the difficulty of reasoning about floating-point edge cases and roundoff errors. To address this difficulty, I will introduce a novel technique for using SMT solvers to verify floating-point algorithms by coarsely overapproximating the behavior of the FPU. This technique enables previously-infeasible verification problems to be solved in milliseconds.

Food:

10/24: Automated Reasoning About Distributed Systems

Time: Thursday, October 24, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Federico Mora

Abstract: Designing and implementing distributed systems is still an enormous task for software engineers. Much of this challenge stems from the fact that bugs can arise from complex combinations of machine failures and message interleavings that are difficult for humans to reason about manually. As distributed systems become increasingly critical infrastructure, engineers will need more and more computational support to correctly build and deploy them.
In this talk, I will present three automated reasoning techniques that can help software engineers build and deploy correct distributed systems. First, a verification framework for message-passing distributed systems that allows users to write specifications as monitors and execute them alongside deployed systems. Second, a decision procedure for a relevant fragment of logic. Third, a new approach for semi-automatically modelling distributed systems in formal languages.

Food:

10/31: Testing GPU Memory Consistency at Large

Time: Thursday, October 31, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Reese Levine

Abstract: Memory consistency specifications (MCSs) are a difficult, yet critical, part of a concurrent programming framework. Existing MCS testing tools are not immediately accessible, and thus, have only been applied to a limited number of devices. However, in the post-Dennard scaling landscape, there has been an explosion of new architectures and frameworks, exemplified by graphics processing units (GPUs). Studying the shared memory semantics of these new platforms is important for understanding program behavior and ensuring conformance to framework specifications.
In this talk, I will discuss our work on widescale GPU MCS testing. We developed a new methodology, MC Mutants, which utilizes mutation testing to evaluate the effectiveness of MCS testing techniques. MC Mutants is built into an accessible testing tool, GPUHarbor, which we used to collect data from over 100 devices from seven GPU vendors. This massive testing campaign revealed bugs in several GPU compilers and provided insights into weak behavior characteristics across diverse architectures. Furthermore, these results were used to tune testing environments across different devices, allowing us to make testing portable and contribute our tests to the official conformance test suite for WebGPU. Our ongoing work is investigating how to increase the safety and security of GPU programming languages in the face of their weak shared memory guarantees, as well as the challenges and opportunities that come with evolving architectures.

Food:

11/7: Democratizing High-Performance DSL development with BuildIt

Time: Thursday, November 7, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Ajay Brahmakshatriya

Abstract: Today, applications that require high-performance rely on libraries of hand- optimized kernels, with thousands available across various domains and architectures, while Domain-Specific Languages (DSLs) and their accompanying compilers remain relatively rare. A well-designed DSL can describe a much wider variety of programs within a given domain than even the most comprehensive library, while also unlocking powerful cross- function and global domain-specific optimizations that hand-optimized kernels cannot achieve. However, building high-performance DSLs is complex and time-consuming, often requiring compiler experts to devote years to development.
In this talk, I will introduce BuildIt, a C++ framework designed for the rapid prototyping of high-performance DSLs. BuildIt uses a multi-stage programming approach to combine the flexibility of libraries with the performance and specialization of code generation. With BuildIt, domain experts can transform existing libraries into efficient, specialized compilers simply by modifying types of the variables. Moreover, it allows them to implement analyses and transformations without needing to write traditional compiler code. Currently, BuildIt supports code generation for multi-core CPUs and GPUs, with FPGA support coming soon. I will also showcase three DSLs created with BuildIt to highlight its power and ease of use: a reimplementation of the GraphIt graph computing language, the BREeze DSL for regular expressions, and NetBlocks, a DSL for custom network protocol development.

Food:

11/14: TBD

Time: Thursday, November 14, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Anjiang Wei

Abstract: TBD

Food:

12/12: TBD

Time: Thursday, December 12, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Umut Acar

Abstract: TBD

Food: