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 spring 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 |
|---|---|---|
| April 7 | Tomas Petricek | Programming Systems Deserve a Theory Too! |
| April 14 | Kyle Miller | Informalizing formalized mathematics using the Lean theorem prover |
| April 21 | Yanwen Xu | Using all the processors in your heterogeneous system: a case study for tree-based applications |
| April 28 | Tim Goodwin | What goes wrong in serverless runtimes? |
| May 5 | Yuka Ikarashi | Exocompilation for productive programming of hardware accelerators |
| May 12 | Graydon Hoare | Vectorized Interpreters: MRT for PL |
| May 19 | Thomas Dickerson | Fangorn: Making Immutable Trees Mutable and Wait-Free |
| May 26 | cancelled | |
| June 2 | Lovro Lugović | Real-World Choreographic Programming |
| June 9 | Priyanka Mondal | Asynchrony and Choreographies |
April 7
Speaker: Tomas Petricek
Title: Programming Systems Deserve a Theory Too!
Abstract: What do Commodore 64 BASIC, Jupyter Notebooks and Flash have in common? They all include an uninteresting programming language, but are interesting when we view them as programming systems and think about how programmers interact with them to construct programs. We know very well how to study the theory of programming languages, but what can we say about programming systems?
Bio: Tomas Petricek is an assistant professor Charles University. He is interested in stateful, interactive and graphical programming systems, new ways of thinking about programming that make it easier and more accessible, as well as history and philosophy of computing. Previously, he developed novel tools for data exploration and visualization, contributed to the F# language and type providers at Microsoft Research and obtained PhD from University of Cambridge for his work on coeffects, a theory of context-aware programming languages.
April 14
Speaker: Kyle Miller
Title: Informalizing formalized mathematics using the Lean theorem prover
Abstract: One of the applications of interactive theorem provers in pure mathematics is being able to produce machine-verified formal proofs. I will talk about a less-obvious application, which is using formalized mathematics to author interactive informal expositions. I will demonstrate a prototype of an “auto-informalization” system written in Lean that presents the reader with an interface to view proofs at a desired level of detail. I will also discuss thoughts on the impact of such tools in mathematics. This is joint work with Patrick Massot.
Bio: Kyle Miller is a postdoc in the mathematics department at UCSC. His primary research interests are in knot theory and graph theory, and he is currently on leave to work with Patrick Massot at Université Paris-Saclay in Orsay, France to pursue research in computer-formalized mathematics. Kyle is a contributor and maintainer for mathlib, the mathematical library for the Lean interactive theorem prover. In his spare time, he enjoys dreaming about PL designs and tinkering with compilers.
April 21
Speaker: Yanwen Xu
Title: Using all the processors in your heterogeneous system: a case study for tree-based applications
Abstract: Specialized processing units such as GPU/FPGA are widely adopted in heterogenous systems, e.g., in data centers and supercomputers. However, another type of heterogeneous system - shared memory heterogeneous systems - often found in mobile SoCs, has received less attention, despite more and more die area consists of accelerators on these devices. In this talk, I will present a framework for accelerating tree-based applications in shared memory heterogeneous systems, such as those used in computer graphics and statistical learning.
Bio: Yanwen Xu is a third-year Ph.D. student in the computer science & engineering department at UCSC, advised by Professor Tyler Sorensen. His primary research interest is in heterogenous computing in edge devices, particularly developing novel compiler techinques to optimize the use of computing resources in these systems. Yanwen has collaborated with Princeton’s team on a DARPA-funded project, where he explored mapping heterogeneous workloads to emerging architectures.
April 28
Speaker: Tim Goodwin
Title: What goes wrong in serverless runtimes?
Abstract: Serverless computing promises to drastically simplify the process of deploying and manging applications in the cloud. The paradigm involves dynamic autoscaling and “scale-to-zero” functionality, ensuring that applications consume only the compute resources they need to complete their work. Supporting these features reliably, however, requires a high level of complexity at the runtime level. In this talk, I will discuss some of the essential challenges in serverless platform design through a presentation of a recent bug study conducted on Knative, a popular, industrial-strength open-source serverless platform.
Bio: Tim Goodwin is a first-year Ph.D. student in the CSE department at UCSC, advised by Lindsey Kuper and Andrew Quinn. His research interests are in distributed systems and the abstractions used to build them. Recently, he has been exploring the programming challenges associated with emerging cloud-native technologies like serverless programming and Kubernetes.
May 5
Speaker: Yuka Ikarashi
Title: Exocompilation for productive programming of hardware accelerators
Abstract: High-performance kernel libraries are critical to exploiting accelerators and specialized instructions in many applications. Because compilers are difficult to extend to support diverse and rapidly-evolving hardware targets, and automatic optimization is often insufficient to guarantee state-of-the-art performance, these libraries are commonly still coded and optimized by hand, at great expense, in low-level C and assembly. To better support development of high-performance libraries for specialized hardware, we propose a new programming language, Exo, based on the principle of exocompilation: externalizing target-specific code generation support and optimization policies to user-level code. Exo allows custom hardware instructions, specialized memories, and accelerator configuration state to be defined in user libraries. It builds on the idea of user scheduling to externalize hardware mapping and optimization decisions. Schedules are defined as composable rewrites within the language, and we develop a set of effect analyses which guarantee program equivalence and memory safety through these transformations. We show that Exo enables rapid development of state-of-the-art matrix-matrix multiply and convolutional neural network kernels, for both an embedded neural accelerator and x86 with AVX-512 extensions, in a few dozen lines of code each.
Bio: Yuka Ikarashi is a PhD candidate at MIT CSAIL, advised by Jonathan Ragan-Kelley. She is interested in creating compiler systems and programming languages for real-world applications. She is a co-creator of the Exo programming language and has been a developer for other compiler frameworks such as Clang/LLVM and ROOT. She previously worked at Apple, Amazon, and CERN. She received Masason Foundation Fellowship and Funai Foundation Fellowship awards.
May 12
Speaker: Graydon Hoare
Title: Vectorized Interpreters: MRT for PL
Abstract: Conventional interpreters and compilers are two different techniques for implementing programming languages. They each make specific sets of compromises on various key pragmatic concerns. A third, often-overlooked implementation technique exists called a “vectorized interpreter” with a different and compelling set of compromises. This talk will examine the technique in some depth, making an “MRT” analogy that is hopefully illuminating (or at least an amusing surprise).
Bio: Graydon Hoare is a systems programmer with a focus on programming language design and implementation. He was the initial developer of Rust, and has worked on numerous language toolchains, runtimes, debuggers, profilers and other development tools over 25 years of industrial work including Red Hat, Mozilla and Apple.
May 19
Speaker: Thomas Dickerson
Title: Fangorn: Making Immutable Trees Mutable and Wait-Free
Abstract: We show how to implement a large class of wait-free operations on mutable trees by applying type-level rewrite rules to specifications for immutable versions of the same ADT. Among the supported operations are efficient, linearizable, copy-on-write snapshots; thereby supporting consistent iteration and speculative updates.
The transformation is achieved by executing each recursive step using the LLX and SCX primitives of Brown et al. (2013) and suspending each tail call into the structure of the tree itself (rather than relying on the mechanisms of the host programming language). We bootstrap our operations on the root of the tree using a wait-free universal construction based on LLX/SCX.
We also show how to extend the LLX/SCX primitives to allow control-flow operations to propagate correctly across thread boundaries.
Bio: Thomas Dickerson is the Chief Science Officer (and a co-founder) at Geopipe, in Burlington, Vermont. Geopipe is a deep-tech startup using ML to parse the planet’s geospatial data and create simulation-ready environments from real-world locations. Previously, he did his PhD at Brown University where he was advised by Maurice Herlihy. His research interests are, broadly, applying a computational lens to interdisciplinary problems.
May 26
cancelled
June 2
Speaker: Lovro Lugović
Title: Real-World Choreographic Programming
Abstract: Choreographic programming is a recent programming paradigm where the overall behaviour of a distributed system is programmed from a global viewpoint—as a choreography between different participants (roles). The choreography can then be automatically compiled (projected) to a correct implementation for each role. This relieves the programmer from manually writing the separate send and receive actions performed by the roles, which simplifies development and avoids communication mismatches.
However, the applicability of choreographic programming in the real world is still largely unexplored. We carry out the first development of a widespread real-world protocol using choreographic programming, the Internet Relay Chat (IRC). We show how we have dealt with IRC’s complex interaction patterns and the issue of interoperability with third-party software. The development is based on Choral, an object-oriented higher-order choreographic programming language.
Bio: Lovro Lugović is a computer science PhD student in the IMADA department at the University of Southern Denmark (SDU), advised by Fabrizio Montesi. His research interests are in distributed systems, concurrency theory, choreographic programming and programming languages.
June 9
Speaker: Priyanka Mondal
Title: Asynchrony and Choreographies
Abstract: Choreographic programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. It enables the programmers to write a centralized program (choreography) and compile it via endpoint projection into programs for each participating node in a distributed system. However, choreographic languages are typically synchronous, whereas most real-world systems have asynchronous communications. In this talk we will discuss how we can make a choreographic programming language support asynchronous communication by adding extra semantics to it.
Bio: Priyanka Mondal is a PhD student in the Department of Computer Science & Engineering at UCSC. She is advised by Owen Arden and Ioannis Demertzis. Her research interests include language-based security, cryptography, and distributed systems.