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: Assorted Lightning Talks

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

Speaker: Rohan Yadav, AJ Root, David Zhang, Matthew Soutoudeh

Abstract: TBD

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: TBD

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

Speaker: Reese Levine

Abstract: TBD

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: Scott Kovach

Abstract: TBD

Food:

12/12: TBD

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

Speaker: Umut Acar

Abstract: TBD

Food: