Languages, Systems, and Data Seminar (Winter 2023)

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 Albert Schimpf Set-Theoretic Types for Erlang (postponed)
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 TBD
Feb. 17 Rishabh Iyer TBD
Feb. 24 Dominik Winterer TBD
March 3 Andrew Osterhout TBD
March 10 José Renau TBD
March 17 TBD TBD

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

(This talk is postponed)

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.

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

Abstract: TBD

Bio: TBD

Feb. 17

Speaker: Rishabh Iyer

Title: TBD

Abstract: TBD

Bio: TBD

Feb. 24

Speaker: Dominik Winterer

Title: TBD

Abstract: TBD

Bio: TBD

March 3

Speaker: Andrew Osterhout

Title: TBD

Abstract: TBD

Bio: TBD

March 10

Speaker: José Renau

Title: TBD

Abstract: TBD

Bio: TBD

March 17

Speaker: TBD

Title: TBD

Abstract: TBD

Bio: TBD


Archive