FPO

"Modular Control  Plane Verification" 

Zoom link: 
https://princeton.zoom.us/j/95302742818

Naorin Hossain will present her FPO "Navigating Emerging Complexities of Modern Systems: Advancements in Automated Verification and Security Techniques" in CS 302 on January 11, 2024 at 9am in CS 302.

The members of her committee are as follows: 

Margaret Martonosi (advisor, examiner)
Aarti Gupta (reader)
Pradip Bose (reader, IBM)
Amit Levy (examiner)
David August (examiner)

The increasing design complexity at the end of Moore’s Law and Dennard Scaling presents a new challenge for implementing modern systems correctly and securely. This dissertation presents focused efforts for advancing automated verification and security techniques to mitigate incorrect implementations and attackers, respectively. It explores two avenues: 1) correctness verification in virtual memory systems, where shared memory interactions occur across hardware and system-level events, and 2) enhancing security of heterogeneous systems-on-a-chip (SoCs) with anomalous activity detection and localization. In the first thrust, this dissertation develops tools for a systematic, end-to-end formalized approach for verifying and validating virtual memory system implementations using memory transistency model (MTM) specifications. First, I propose a novel formal language for reasoning about MTMs, enabling specification of the software-visible impacts of complex hardware- and system-level interactions that occur in parallel systems with virtual memory. Next, I present empirical MTM testing techniques for verification and validation on real system implementations using specialized stress measures to coax out MTM-specific bugs. The proposed techniques can alleviate complex system verification efforts by automating detection of bugs and vulnerabilities at the hardware-system interface of virtual memory systems. The second thrust of this dissertation develops processes to enhance security of heterogeneous SoC designs. Sophisticated attacks can take down parts of the SoC, resulting in diminished performance gains and failed processes. To design built-in defenses against such attacks, this dissertation proposes the use of network-on-chip (NoC) based hardware counters to monitor ongoing SoC activity in a holistic fashion. With these counters, I develop and demonstrate an anomalous activity detection and localization system to detect and pinpoint availability attacks on SoC components, leveraging machine learning techniques and the inherent interpretability offered by the 3 NoC counters. These techniques enable automated attack and failure detection to be built into the SoC, a particularly valuable feature in the fast-changing heterogeneous SoC design space. Overall, this dissertation advocates for the use of formal and empirical modeling tools to effectively capture complex system behaviors such that vulnerabilities, bugs, and threats can be detected at design time and runtime with automated methods that provide elevated coverage and accuracy.

Udaya Ghai will present his FPO "A Game-theoretic Lens for Robustness in Control" on Monday, December 18, 2023 at 4:00 PM in CS 402.

Location: CS 402

The members of Udaya’s committee are as follows:

Examiners: Elad Hazan (Adviser), Ryan Adams, Naomi Leonard
Readers: Sanjeev Arora, Anirudha Majumdar

A copy of his thesis is available upon request.  Please email gradinfo@cs.princeton.edu if you would like a copy of the thesis.

Everyone is invited to attend his talk.

Abstract follows below:

The control of dynamical systems is a fundamental problem with a vast array of applications, from robotics to biological engineering. Recently, the game-theoretic primitive of regret minimization has been applied to control, yielding novel instance-optimal performance guarantees in more challenging non-stochastic control settings. This thesis further explores the benefits of a multi-agent perspective of control.

Concretely, we begin with a new algorithm for generating disturbances for controller verification, which relies on recasting the players in the nonstochastic control game. Next, we provide a cooperative multi-agent extension of the nonstochastic control setting, involving a reduction from our multi-agent game to single agent regret minimization. Furthermore, we show new notions of robustness to failure can be attained through this perspective, even in a single-agent setting.

While control is a powerful tool, it relies heavily on knowledge of the dynamics. The final chapters provide two very different approaches to robustness without such a model. The first approach extends the nonstochastic control methodology to model-free reinforcement learning. In an alternative approach, we consider unknown systems with dynamics that are \emph{approximately} linear using tools from classical control theory.

Devon Loehr will present his FPO "Lucid: A High-Level, Easy-To-Use Dataplane Programming Language" on Friday, December 1 in CS 302 at 1pm.

Zoom link: https://princeton.zoom.us/j/97653187562?pwd=TmFNVjl1TWJDMkk5bW5Eaitxb05qUT09

The members of his committee are as follows:

Readers: Aarti Gupta and Andrew Appel ; Examiners: David Walker (Adviser), Jennifer Rexford, and Amit Levy 

Abstract: 
The introduction of programmable switches and the P4 language for programming
them has made it possible for network operators to write ever-more sophisticated
network applications, and execute them at high speed. However, possible is not the
same as easy. The de facto standard dataplane programming language, P4, is akin
to an “assembly language” for programmable switches: it provides a powerful but
low-level interface to switch hardware. While this gives the programmer fine-grained
control, it makes it difficult to write and reason about programs with complicated
high-level behavior. Furthermore, modern hardware is heavily specialized for packet
processing. While this specialization allows blazing fast speeds, it also heavily restricts
the sorts of programs a programmable switch can run. Unfortunately, such restrictions
are poorly-represented in modern dataplane languages. Should a program violate one
or more of these restrictions, it will fail to compile, often with an arcane or unhelpful
error message.
This dissertation presents Lucid, a high-level, event-based language for
programmable switches. Lucid raises the level of abstraction for data-plane program-
ming in several ways. Control flow is represented by events, each of which has an
associated handler that is executed when the event is generated. Different threads
of control may be interleaved easily by writing them as handlers for separate events.
Lucid provides high-level representations of switch hardware restrictions, which are
enforced by syntactic checks, including a novel type system for detecting ordering
violations.
Lucid is compiled to P4 for the Intel Tofino, and we find that Lucid programs
typically contain around 10 times fewer lines of code than equivalent P4 programs.
Furthermore, the Lucid interpreter may be used to quickly evaluate different configurations of a Lucid program, in order to automatically optimize a single program for different networking environments.

Edgar Minasyan will present his FPO "Beyond Linear Paradigms in Online Control" on Tuesday, October 17, 2023 at 1:00 PM in CS 201.

Location: CS 201

The members of Edgar’s committee are as follows:
Examiners: Elad Hazan (Adviser), Mark Braverman, Ran Raz
Readers: Bernard Chazelle, Chi Jin

A copy of his thesis is available upon request.  Please email gradinfo@cs.princeton.edu if you would like a copy of the thesis.

Everyone is invited to attend his talk.

Abstract follows below:
In the last century, the problem of controlling a dynamical system has been a core component in numerous applications in autonomous systems, engineering, and sciences. The theoretical foundations built so far include the field of classical control theory as well as recent advances in leveraging regret minimization techniques for guarantees in online control. In either case, however, a linearity assumption is prevalent to enable the derivation of provable guarantees and efficient algorithms. In this thesis, we present several directions to alleviate the linearity assumption in the problem of online control. At the core of all the results lies the regret minimization frame- work: the presented works design new, as well as heavily rely on existing, methods and notions in online convex optimization.

The ultimate goal of this direction is to derive efficient algorithms that perform optimal online control of nonlinear dynamical systems. This goal in full generality is NP-hard hence certain concessions need to be made. We build upon the recent non- stochastic control framework that enables efficient online control of linear dynamical systems: our first advance is to consider time-varying linear dynamical systems which are commonly used to approximate nonlinear dynamics. We argue that the correct performance metric in this setting is the notion of adaptive regret developed for online learning in changing environments and proceed to design an efficient control method for known time-varying linear dynamics. The extension to unknown dynamics proves to be qualitatively harder: our upper/lower bound results show that the system variability of the unknown dynamics is a determining factor on whether meaningful (adaptive) regret guarantees can be achieved. The policies in the described advances enjoy linear/convex parameterizations which can be constraining for complex dynamical systems. Hence, we additionally explore the use of neural network-based policies in online episodic control and derive an efficient regret-minimizing algorithm that in- corporates the interpolation dimension as an expressivity metric for the policy class.

"Tony" Runzhe Yang will present his FPO "From mind to machine: neural circuits, learning algorithms, and beyond." on Tuesday, September 26, 2023 at 12:00 PM in CS 105 and Zoom.

Location: Zoom Link: https://princeton.zoom.us/j/91084214303

The members of Runzhe’s committee are as follows:
Examiners: H. Sebastian Seung (Adviser), Karthik Narasimhan (Adviser), Mala Murthy
Readers: Ryan Adams, Dmitri Chklovskii (Flatiron Institute; NYU)

A copy of his thesis is available upon request.  Please email gradinfo@cs.princeton.edu if you would like a copy of the thesis.
 
Everyone is invited to attend his talk.
 
Abstract follows below:

This thesis explores diverse topics within computational neuroscience and machine learning. The work begins by examining the organization of biological neuronal circuits re- constructed by electron microscopy. First, our study of neural connectivity patterns in the mouse primary visual cortex illustrates the necessity for refined understanding of the non- random features of cortical connections, challenging conventional perspectives. Second, in the larval zebrafish hindbrain, our novel discovery highlights overrepresented three-cycles of neuron, an observation unprecedented in electron microscopy-reconstructed neuronal wiring diagrams. Additionally, I present an exhaustive compilation of motif statistics and network characteristics for the complete adult Drosophila brain. These efforts collectively enrich our understanding of the intricate wiring diagram of neurons, offering new insights into the organizational principles of biological brains.

In the second part of the thesis, I introduce three distinct machine learning algorithms. The first algorithm, a biologically plausible unsupervised learning algorithm, is implemented within artificial neural networks using Hebbian feedforward and anti-Hebbian lateral connections. The theoretical discourse explores the duality and convergence of the learning process, connecting with the generalized concept of the “correlation game” principle. The second algorithm presents a novel multi-objective reinforcement learning approach, adept at managing real-world scenarios where multiple potentially conflicting criteria must be optimized without predefined importance weighting. This innovation allows the trained neural network model to generate policies that align optimally with user- specified preferences across the entire space of preference. The third algorithm employs a cognitive science-inspired learning principle for dialog systems. The designed system engages in negotiation with others, skillfully inferring the intent of the other party and predicting how its responses may influence the opponent’s mental state.

Collectively, these contributions shed light on the complexities of neural circuit organization and offer new methodologies in machine learning. By examining intelligence from both biological and computational perspectives, the thesis presents insights and reference points for future research, contributing to our growing understanding of intelligence.

Xiaoqi (Danny) Chen will present his FPO "Designing Compact Data Structures for Network Measurement and Control" on Wednesday, October 4, 2023 at 2pm in Friend Center 125 (and Zoom).

Zoom link:  https://princeton.zoom.us/j/96617518355

The members of his committee are as follows:

Examiners: Jennifer Rexford (adviser), David Walker, and Maria Apostolaki

Readers: Mark Braverman and Minlan Yu (Harvard University)

Talk abstract follows below.  All are welcome to join.

Abstract:

This dissertation explores the implementation of network measurement and closed-loop control in the data plane of high-speed programmable switches. After discussing the algorithmic constraints imposed by the switch pipeline architecture, primarily stemming from the requirement of high-speed processing, we share our experience in tailoring algorithms for the data plane. Initially, we focus on efficient measurement algorithms, and present two works for detecting heavy hitters and executing multiple distinct-count queries; both require designing novel approximate data structures to meet the tight memory access constraints. Subsequently, we pivot towards using real-time, closed-loop control in the data plane for performance optimization, and present two works for mitigating microbursts and enforcing fair bandwidth limits; both require approximated computation and exploit the sub-millisecond reaction latency unattainable through conventional control planes. We hope by sharing our experience and techniques, which are widely applicable to various algorithms and other data-plane hardware targets, we can lay the foundation for future innovations in the field of network programming for researchers and practitioners alike.

Sven Dorkenwald will present his FPO "Analysis of neuronal wiring diagrams" on Friday, August 18, 2023 at 1:00 PM in Neuroscience Institute A32 and Zoom.

Location: Zoom link:https://princeton.zoom.us/j/97076372854

The members of Sven’s committee are as follows:
Examiners: H. Sebastian Seung (Adviser), Michael Freedman, Mala Murthy
Readers: Felix Heid, Viren Jain (Google)

A copy of his thesis is available upon request.  Please email gradinfo (@cs.princeton.edu) if you would like a copy of the thesis.
 
Everyone is invited to attend his talk.

Abstract follows below:
To understand how the brain works, one must know its neurons and their connections. Maps of synaptic connections between neurons can be created by acquiring and analyzing electron microscopic (EM) brain images, but until recently, even the largest datasets were insufficient to map full neuronal circuits in most organisms or even small brains. Advances in automated EM image acquisition and analysis have now given rise to neuronal reconstructions of mammalian brain circuits and entire insect brains. Errors in these automated reconstructions must still be corrected through proofreading. This thesis introduces new methods to bridge the gap between automated neuron reconstructions and the analysis of neuronal wiring diagrams. First, it presents a proofreading infrastructure that facilitates correction of whole neurons in up to petascale (∼ 1mm3 brain tissue) datasets by communities of scientists and proofreaders. Second, it embeds this proofreading system into an analysis infrastructure to enable queries of the connectome data while it is actively being edited. Third, it presents a self-supervised learning technique for efficient inference of semantic information which is crucial for circuit analyses. These methods have already been used by hundreds of users and enabled numerous neuroscientific analyses. Additionally, this thesis presents the analysis of the largest connectivity map to date between cortical neurons of a defined type (L2/3 pyramidal neurons in mouse visual cortex) which identified constraints on the learning algorithms employed by the cortex. Finally, this thesis reports on the completion of the wiring diagram of the Drosophila melanogaster brain containing ∼130,000 neurons and describes how this work enabled it. The Drosophila connectome was created through a years-long community-based effort and is an incredible resource for the science community and a milestone for connectomics on the way to large mammalian brains. The methods presented in this thesis will be useful for the analysis of larger brain samples as we aim for connectomes of whole mammalian brains.

Mingzhe Wang will present his FPO "Deep Learning for Automated Theorem Proving" on Monday, August 21, 2023 at 3:00 PM in CS 301 and Zoom.

Location: Zoom link: https://princeton.zoom.us/j/3294749300

The members of Mingzhe’s committee are as follows:
Examiners: Jia Deng (Adviser), Danqi Chen, Karthik Narasimhan
Readers: Andrew Appel, Sanjeev Arora

A copy of his thesis is available upon request.  Please email gradinfo@cs.princeton.edu if you would like a copy of the thesis. 

Everyone is invited to attend his talk. 

Abstract follows below:
Automated theorem proving is a fundamental AI task with broad applications to the formalization of mathematics, software and hardware verification, and program synthesis. Deep learning has emerged as a promising approach for guiding theorem provers. In this dissertation, we present our work on developing deep learning approaches for automated theorem proving.

First, we propose FormulaNet, a deep learning-based approach to the problem of premise selection. FormulaNet represents a logical formula as a graph that is invariant to variable renaming and then embeds the graph into a vector via a novel graph embedding method that preserves the information of edge ordering. Our approach achieves state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.

Next, we propose MetaGen, a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover.  On real-world tasks, we demonstrate that synthetic data from our approach improves the theorem prover and advances the state of the art of automated theorem proving in Metamath.

Finally, we extend our theorem generator to the interactive theorem prover Lean. We propose TermGen, a neural generator that automatically synthesizes theorems and proofs in Lean by directly constructing proof terms. We also propose a method of expert iteration for training TermGen to synthesize short theorems. At last, we present a case study of generating formal specifications of while-loop programs through a rule-based theorem generator.

Adviser: Appel

Readers: David Walker, Nate Foster (Cornell)

Examiners: Appel, Rexford,  Kincaid