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