From Code to Cables: Rethinking Reliability in Modern Systems

​Talk 1: Merging at Scale: From Broken Builds to Green Mainline

​In monorepos, “green” pull requests don’t always guarantee a green mainline. At Uber’s scale, with thousands of engineers and daily commits, independent changes pass builds but fail after merging, leading to integration failures, lost productivity, and slower development. This talk explains how Uber addressed this by rethinking the merge process. We introduce SubmitQueue, a predictive merge system that validates future mainline states before changes merge. It combines speculative execution, building only the components affected by a change, and probabilistic prioritization to focus builds on changes most likely to succeed, keeping the mainline green. We’ll cover:

• ​Why passing builds don’t guarantee safe merges

• ​How speculative merge queues detect integration failures early

• ​Techniques to scale merging (target-based builds, pruning, probabilistic speculation)

• ​Optimizations like bypassing large diffs to reduce wait times

• ​Lessons from operating at Uber scale

​This session shares practical approaches to keeping the mainline green while maintaining development velocity.

​About Speakers:
Preetam Dwivedi is a Staff Engineer on Uber’s Developer Platform team, leading systems for code hosting, review, merge queues, and artifacts. He specializes in distributed systems and scaling developer infrastructure, with a focus on modernizing workflows and cloud migrations.

​Manjari Akella is a Senior Software Engineer on the same team, focused on improving developer productivity. She has contributed to Uber’s Go monorepo, enhanced Go libraries, and worked on artifact management and merge queues.

​
Talk 2: Security Is Not a Runtime Concern: Eliminating the Kernel Trap with Formal Proof-Carrying IPC

​Modern operating systems are built on a performance bug: the "Security Tax." We’ve accepted that Ring 3 isolation requires expensive syscall traps, context switches, and redundant runtime bounds checks. But these overheads aren't a law of nature; they are simply evidence of unfinished work at compile-time.

​In this talk, we explore Salt, a systems language that embeds a Z3 theorem prover directly into the codegen loop to prove memory safety and layout before a single byte of machine code is emitted. By using Weakest Precondition (WP) generation, the Salt compiler physically elides runtime safety branches, allowing the KeuOS microkernel to move performance-critical drivers and networking to userspace with unikernel-level latency (~150 cycles per packet). We will deep-dive into the "12-Cycle Mic Drop": Proof-Carrying IPC. We'll show how the compiler seals structural proofs into a 64-bit SipHash "hint" that the kernel verifies in a dozen instructions, eliminating the need for traditional MMU-guarded isolation between microkernel services.

​Key Takeaways:

• ​The End of the Syscall: Why traditional read/write conventions are a legacy mistake and how SPSC (Single-Producer, Single-Consumer) rings provide a "zero-trap" data plane.

• ​Contract Elision: How to use SMT solvers to prove safety once at compile-time so you can delete defensive code from your production binaries.

• ​Vertical Integration: Why building a language specifically to host an OS allows for optimizations (like polyhedral loop tiling in MLIR) that beat clang -O3 and Rust in 18 of 22 industry benchmarks.

• ​Practical Sovereignty: A look at LETTUCE (a verified, Redis-compatible store) and Basalt (LLM inference) running on a kernel with no "Security Tax."

​About Speaker:
Kevin O'Connor is a Software Engineer at Google, where he currently works on posing algorithms in Google Maps, and teaches the "AI-Augmented Engineering 101" internal course at Google. Other experience is as TL at Snapchat, SWE experience at Twitter, Braintree Payments, and Wolfram Research.

​Dont forget to RSVP and join us at the event location to learn more about the topics in depth along with your free pizza!.

​Thanks Uber for sponsoring the event.

​-------

​Instructions to get in
- Parking: available in the building (quite a bit pricey), better to use spothero to find closeby.
- Access: Enter into building: 1191 2nd Ave (Second & Seneca), Seattle, WA, 98101, press #7 (7th floor) in the elevator to access and security will do the checkin and guide folks to the meetup area.

​-------