Time: Fridays, noon - 1:05pm (PT)
Location: The Internet / The LSD Lab (Engineering 2, Room 398)
Organizers: Lindsey Kuper and Tyler Sorensen
The Languages, Systems, and Data Seminar meets weekly to discuss interesting topics in the areas of programming languages, systems, databases, formal methods, security, software engineering, verification, architecture, and beyond. Our goal is to encourage interactions and discussions between students, researchers, and faculty with interests in these areas. The seminar is open to everyone interested. Participating UCSC students should register for the 2-credit course CSE 280O (let the organizers know if you’re an undergrad and need a permission code).
For winter 2023, we will continue to host the LSD Seminar in a hybrid fashion. Anyone can attend on Zoom, and local folks can gather in person in the lab. Speakers can join either in person or on Zoom, whichever is convenient.
Talks will be advertised on the ucsc-lsd-seminar-announce (for anyone) and lsd-group (for UCSC-affiliated people) mailing lists.
| Date | Speaker | Title |
|---|---|---|
| Jan. 6 | Milijana Surbatovich | Designing Formally Correct Intermittent Systems |
| Jan. 13 | POPL SRC lightning talks (Jonathan Castello, Nathan Liittschwager, Gan Shen) | |
| Jan. 20 | cancelled | |
| Jan. 27 | Richard Lin | Usable Programming for Building Things (with a focus on electronics) |
| Feb. 3 | Ike Nassi | The Practical Advantages of Distributed Virtual Machines and How They Work |
| Feb. 10 | Dustin Richmond | bPentimento: Data Remanence in Cloud FPGAs |
| Feb. 17 | Rishabh Iyer | Performance interfaces for Network Functions and beyond |
| Feb. 24 | Dominik Winterer | Finding 1,700+ Bugs in the SMT Solvers Z3 and CVC5 in Three Years |
| March 3 | Andrew Osterhout | ROMP: A Random-walk Based Parallel Explicit-State Stateless Model Checker |
| March 10 | José Renau | Live Hardware Development at UCSC |
| March 17 | Albert Schimpf | Set-Theoretic Types for Erlang |
Jan. 6
Speaker: Milijana Surbatovich
Title: Designing Formally Correct Intermittent Systems
Abstract:
Batteryless, energy-harvesting devices (EHDs) are an emerging platform that enables computing in remote, inaccessible environments. Instead of using a battery, an EHD harvests energy from its environment into a buffer and operates intermittently, only as energy is available. This operational cycle causes the device to experience frequent, arbitrary power failures that make correct programming difficult. To make progress, an intermittent system typically saves execution state before power failure and restores it after the device reboots. Incorrectly determining which state must be saved and where a save point should be made causes software to exhibit memory and timing bugs that would not occur on continuously powered program executions. As EHDs are envisioned to be remotely-deployed, low-maintenance devices, programs must execute reliably, without memory consistency or timing violations. Unfortunately, existing systems rely on informal, undefined correctness notions, providing few correctness guarantees.
In this talk, I present my work in designing formally correct intermittent systems. I show how existing correctness notions are insufficient, leading to unaddressed bugs. I then define formal correctness conditions for memory consistency and timing properties on intermittent systems, using these definitions to design enforcement mechanisms and abstractions programmers can use to specify their desired properties. This work allows the development of intermittent systems that meet specified guarantees of time and memory consistency, improving reliability.
Bio:
Milijana Surbatovich is a final year PhD Candidate in the Electrical and Computer Engineering Department at Carnegie Mellon University, co-advised by Professors Brandon Lucia and Limin Jia. Her research interests are in applied formal methods, programming languages, and systems for intermittent computing. She is excited by research problems that require reasoning about correctness and security across the architecture, system, and language stack. Previously, she received an MS in ECE from CMU in 2020 while doing her PhD and a BS in Computer Science from University of Rochester in 2017.
Jan. 13
POPL SRC lightning talks (Jonathan Castello, Nathan Liittschwager, Gan Shen)
Jan. 20
cancelled
Jan. 27
Speaker: Richard Lin
Title: Usable Programming for Building Things (with a focus on electronics)
Abstract: While modern programming languages and development practices have made programming powerful yet still accessible to novices, the underlying mechanisms - high level of abstraction, encapsulation and re-use of expert knowledge, and automated correctness checks - can also be hugely beneficial to fields beyond software. For example, structuring board-level electronic circuit designs as code enables designers to write and re-use subcircuits that automate common calculations, while the expert knowledge that these encapsulate helps make design accessible to those with less in-depth knowledge.
Yet, it’s not as simple as “boards… but in code”: new tools must also be useful to, and usable by, existing designers. In this talk, I present my work on developing a hardware description language (HDL) system for electronics that simultaneously aims to be powerful for experts yet usable by all. I’ll go over the entire process, from understanding user needs through initial interview studies, to designing the core language and its abstractions, to building supporting tools that bridge this powerful textual design interface with the familiar graphical tools that are used by today’s engineers.
Bio: I’m currently a postdoc at UC Los Angeles, and before that I received my PhD from UC Berkeley. My research interests focus on building open-source tools that bring the power of software engineering to electronics design, ultimately making custom device design possible for more people. In the past, I’ve worked on the Chisel HDL project, which brings modern software engineering practices to chip-level digital design and similarly focuses on open-source, usability, and practical adoption.
Feb. 3
Speaker: Ike Nassi
Title: The Practical Advantages of Distributed Virtual Machines and How They Work
Abstract: In this talk, I’ll describe a distributed virtual machine architecture. The virtual machine aggregates multiple physical servers and runs them as if they were a single physical server running a single unmodified standard operating system which manages all the resources as if it were a single machine. No changes to applications are required.
The talk explains why creating this was difficult, but also why it’s not as difficult as many might perceive. It explains the concept of non-disruptive automatic dynamic adaptive computing using machine learning and introspection. Particular emphasis is given to auto-scaling, automatic optimization, simplicity of adoption, and hardware evolution. Along the way, some elegant solutions to new problems we hadn’t anticipated were addressed.
Bio: Ike was the founder of TidalScale. The team and the IP is now part of HPE. Ike Nassi is an Adjunct Professor of Computer Science at UC Santa Cruz, and a Founding Trustee at the Computer History Museum. Previously, he was an Executive Vice President and Chief Scientist at SAP. Before TidalScale, Ike helped start three companies: Encore Computer Corporation building hierarchical strongly coherent shared memory symmetric multiprocessors (1984); InfoGear Technology, which developed both Internet appliances (including the first iPhone) and associated backend services (1996); and Firetide, an early wireless mesh networking company (2000).
He worked at Apple Computer where he was SVP for all software and a Corporate Officer, Visual Technology, and Digital Equipment Corporation. Dr. Nassi has been a Visiting Scholar at Stanford University, twice a Research Scientist at MIT, and a Visiting Scholar at University of California, Berkeley. He has served on the board of the Anita Borg Institute for Women and Technology, and the IEEE Computer Society Industry Advisory Board. He holds a PhD in Computer Science from Stony Brook University.
He was awarded two certificates for Distinguished Service from the Department of Defense, one for his work on the design of the programming language Ada and one for his work on DARPA ISAT. He is a Life Fellow of IEEE and a Life member of ACM. He is named on 35 patents.
Feb. 10
Speaker: Dustin Richmond
Title: bPentimento: Data Remanence in Cloud FPGAs
Abstract: Cloud FPGAs strike an alluring balance between computational efficiency, energy efficiency, and cost. It is the flexibility of the FPGA architecture that enables these benefits, but that very same flexibility that exposes new security vulnerabilities. We show that a remote attacker can recover “FPGA pentimenti” – long-removed secret data belonging to a prior user of a cloud FPGA. The sensitive data constituting an FPGA pentimento is an analog imprint from bias temperature instability (BTI) effects on the underlying transistors. We demonstrate how this slight degradation can be measured using a time-to-digital (TDC) converter when an adversary programs one into the target cloud FPGA. This technique allows an attacker to ascertain previously safe information on cloud FPGAs, even after it is no longer explicitly present. Notably, it can allow an attacker to (1) extract proprietary details from an encrypted FPGA design image available on the cloud marketplace and (2) recover information from a previous user of a cloud FPGA. We demonstrate the ability to extract design details and recover previous cloud FPGA user information on the cloud platform. Our experiments show that BTI degradation (burn-in) and recovery are measurable and constitute a security threat to commercial cloud FPGAs.
Bio: Dustin Richmond is an Assistant Professor of Computer Science and Engineering in the Baskin School of Engineering at UC Santa Cruz. Dustin completed his postdoc in the Bespoke Silicon Group at the Paul Allen School of Computer Science at the University of Washington, and earned his Ph.D. from the University of California, San Diego. His research interests are in the design of flexible and secure architectures that can generalize across applications, evolve with software, and dynamically adapt to changes in data. His prior work includes HammerBlade, a flexible supercomputer funded by DARPA; RIFFA: A Reconfigurable Interface for FPGA Accelerators, which won a Community Best Paper Award at the 2013 International Conference on Field-Programmable Logic; and contributions to the PYNQ project at Xilinx. He is an NSF Graduate Research Fellow and an ARCS Fellow. He won the Outstanding Community Leader Award from the UC San Diego Graduate Student Association, and the Excellence in Service and Leadership Award from the UC San Diego Computer Science and Engineering Department. Last, but not least, he also won the Best Social Hour Theme Award for teaching other students the basics of lock picking by locking all the Friday afternoon event food in metal boxes.
Feb. 17
Speaker: Rishabh Iyer
Title: Performance interfaces for Network Functions and beyond
Abstract: Modern programmers routinely use third-party code, and infrastructure operators deploy software they did not write. This would not be possible without semantic interfaces—documentation, header files, specifications—that succinctly describe what that third-party code does.
In this talk, I will propose performance interfaces as a way to describe a system’s performance, akin to how a semantic interface describes its functionality. I will concretize this idea in the domain of network functions (NFs) and describe a tool (PIX) that automatically extracts simple, yet precise performance interfaces from NF implementations. Finally, I will show how developers and operators can use PIX-extracted interfaces to identify performance regressions, diagnose and fix performance bugs and identify the latency impact of NIC offloads.
Bio: Rishabh Iyer is a sixth year PhD student at EPFL working with George Candea and Katerina Argyraki. His research interests are centred around computer systems and networking although he can often be found dabbling with formal verification tools. Prior to joining EPFL, he received his bachelor’s degree from IIT Bombay in 2017.
Feb. 24
Speaker: Dominik Winterer
Title: Finding 1,700+ Bugs in the SMT Solvers Z3 and CVC5 in Three Years
Abstract: Satisfiability Modulo Theory (SMT) solvers are important tools for many advances in programming languages, e.g., symbolic execution engines, software model checkers, and program verifiers. SMT solvers’ robustness is crucial—Incorrect results from SMT solvers can invalidate client applications’ results and lead to disasters in safety-critical domains. Hence, the SMT community has undertaken great efforts to make SMT solvers reliable. Despite this, SMT solvers are complex software and still have latent bugs. Although various fuzzing campaigns have targeted SMT solvers, most known critical bugs were exposed by client applications of the solvers and not by fuzzers.
We devised several general methods for stress-testing SMT solvers [1, 2]. We have been extensively stress-testing the two state-of-the-art SMT solvers Z3 and CVC4. So far, we have found 1,700+ unique bugs in Z3 and CVC4—1,200+ have already been fixed by the developers and 500+ are critical soundness bugs. Our detected bugs are diverse, distributing over almost every SMT-LIB logic and theory: Perhaps surprisingly, our tools detected soundness bugs in linear arithmetic, bit vectors, and uninterpreted functions, decidable logics widely believed to be stable. The developers appreciated our effort by comments such as “great find”, “excellent find” and “nice catch”.
Bio:
Dominik Winterer is a fifth-year Ph.D. student advised by Prof. Zhendong Su at ETH Zurich and a member of the AST lab. He is interested in formal methods problems in Programming Languages and Software Engineering. Dominik’s vision is to robustify modern formal methods software through devising novel testing approaches. Dominik has been awarded the PLDI distinguished paper award.
March 3
Speaker: Andrew Osterhout
Title: ROMP: A Random-walk Based Parallel Explicit-State Stateless Model Checker
Abstract: Model checking via parallelized random walks is a way to get fast way to find bugs in models with huge statespaces. This is largely due to not having to use a global has to monitor the progress of a normal BFS or DFS traversal of a statespace. There however other ways to improve this performance even further with the use of heuristics statespace reductions, and figuring out when to cut your losses on a poor performing walks. We take the first few steps into refining such methodologies by utilizing the Murphi model checking language and a simple multithreaded random walking generated model checker.
Bio: Hello, I am Andrew Osterhout, I am a graduate of the University of Utah, currently working as a research assistant / research programmer under Ganesh Gopalakrishnan, where I primarily work on verification systems for data race detection in GPUs and Model Checking based verification projects. I currently live in Santa Cruz with my partner and work remotely. I am currently working on a LLNL contract via the University of Utah for GPU race detection on AMD unified memory architectures, as well as shepherding the romp project form the side lines while I juggle grad school applications.
March 10
Speaker: José Renau
Title: Live Hardware Development at UCSC
Abstract: Prof. Renau will present the research effort by his team at UCSC. The talk focuses on open-source Live CHIP design flows to improve hardware design productivity. With a focus on 2 main areas: LiveHD and Pyrope.
LiveHD (https://github.com/masc-ucsc/livehd) is hardware compiler with Verilog, Chisel, and Pyrope front-ends. The latest effort is compiler speed around fast structures and parallelization.
Pyrope (https://masc-ucsc.github.io/docs/pyrope/00-hwdesign/) is a new hardware description language. It has a modern syntax designed to be efficient and more approachable to non-hardware designers.
Bio: Jose Renau (http://www.soe.ucsc.edu/~renau) is a CSE department professor at University of California, Santa Cruz. His area of research is computer architecture, focusing on productive hardware design flows (Live Hardware Design Flow or LiveHD, architectural simulators like ESESC, new hardware description language like Pyrope, new design methodologies like Fluid Pipelines), out-of-order cores, and RISC-V verification. Past projects with Thread Level Speculation, infrared thermal measurements, power modeling, and design effort metrics/models. Prof. Renau has a Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign. He is currently the IEEE TCMM Chair.
March 17
Speaker: Albert Schimpf
Title: Set-Theoretic Types for Erlang
Abstract:
Erlang is a functional programming language with dynamic typing. The language offers great flexibility for destructing values through pattern matching and dynamic type tests. Erlang also comes with a type language supporting parametric polymorphism, equi-recursive types, as well as union and a limited form of intersection types. However, type signatures only serve as documentation, there is no check that a function body conforms to its signature.
Set-theoretic types and semantic subtyping fit Erlang’s feature set very well. They allow expressing nearly all constructs of its type language and provide means for statically checking type signatures. This talk will give a brief overview of the history and capabilities of set-theoretic types and how to apply it to an existing dynamically typed language without or with only minor modifications to the code and the challenges involved.
Bio:
I’m a PhD student at the Department of Computer Science of the University of Kaiserslautern, in the AG Softwaretechnik.
My current research topic is applying Set-Theoretic Type Theory to a currently dynamically-typed language called Erlang, which includes defining an operational semantics for that language and designing and implementing an efficient type checker.
My previous work includes building efficient tools for verification, mainly propositional satisfiablility and regular language inclusion solvers, working on replicated distributed data stores and language design for workflows.