Dissertation Talk: Modular and Safe Event-Driven Programming
Seminar | May 3 | 2:30-3:30 p.m. | 531 Cory Hall
Ankush Pankaj Desai, University Of California, Berkeley
Asynchronous event-driven systems can be found in myriad domains including cloud computing systems, device drivers, and robotics.
These systems are notoriously hard to get right as the programmer needs to reason about numerous control paths resulting from the complex interleaving of events (messages) and failures.
Unsurprisingly, it is easy to introduce subtle errors while attempting to fill in gaps between high-level system specifications and their concrete implementations.
In the first half of this talk, I will present P, a domain specific language for modular and safe event-driven programming.
P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events.
P also supports a module system that enables compositional (assume-guarantee) reasoning of event-driven programs.
A P program can not only be compiled into executable code, but it can also be validated using state-of-the-art model checking and systematic testing approaches (e.g., using search prioritization and symbolic execution).
P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. More recently, it is being used for the design and implementation of fault-tolerant distributed systems and robotics systems with assurances of safety and liveness.
In the second half of this talk, I will present Drona, a programming framework for safe robotics.
Drona combines ideas from programming languages, formal verification, and runtime-assurance to enable building safe robotics systems,
especially in the presence of untrusted components including third-party libraries and data-driven machine learning components.
Our experiments both in simulation and on actual drones show that the robotics software stack built using Drona guarantees safety, including when untrusted components have bugs or deviate from the desired behavior.