Projects

Optimized

JavaScript

JavaScript has emerged as the de facto language of the web and is gaining traction for programming apps, wearables, and even embedded microcontrollers. But executing JavaScript quickly with just-in-time compilation is memory-intensive, while interpreters are memory-efficient but slow.

The SJSx project aggressively reduces the memory footprint of JavaScript execution via type-directed ahead-of-time compilation while achieving performance competitive to modern just-in-time compilers. Along the way, we developed a novel type inference algorithm for a type system with objects, structural subtyping, prototype inheritance, and first-class methods.

People. Satish Chandra, Colin Goron, Jean-Baptiste Jeannin, Manu Sridharan, Frank Tip, Youngil Choi.

Papers. OOPSLA 2016.

Error

Explanation

Many modern languages have support for automatic type inference. But when inference fails, the error messages reported can be opaque, highlighting a code location far from the source of the problem.

The Hobbes project provides a framework for extending existing type inference algorithms to produce error reports based on correcting sets, which contain a minimal set of type constraints that, if fixed, allow the program to type check. By leveraging the existing type inference algorithm, Hobbes gains a substantial performance boost compared to other error reporting engines, and adoption is much simpler.

People. Satish Chandra, Calvin Loncaric, Manu Sridharan.

Papers. OOPSLA 2016.

Verified SDN

Controllers

Software-defined networking promises rapid innovation and efficient deployment by shifting intelligence from switching hardware to software on a logically-centralized server. But software development is notoriously error-prone, and bugs in SDN controller software can cause network vulnerabilities.

The Cocoon project provides a simple, declarative specification language for packet-forwarding properties embedded in a richer language for network design. Cocoon translates controller programs to Boogie and automatically checks whether a program satisifies its specification.

People. Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Nina Narodytska, Cole Schlesinger, Douglas B. Terry, and George Varghese.

Papers. NetPL 2016.

Theory of reprogrammable

packet-processing pipelines

In a Software-Defined Network (SDN), a central, computationally powerful controller manages a set of distributed, computationally simple switches. The controller computes a policy describing how each switch should route packets, and it then populates packet-processing tables on each switch with rules to enact the routing policy. As network conditions change, the controller continues to add and remove rules from switches to adjust the policy as needed.

The CNC project develops a language for targeting reconfigurable packet-processing hardware and a proved-correct compiler for compiling a virtual pipeline to heterogeneous back-end hardware. It builds on the NetKAT language to provide a sound equational theory for program transformations.

People. Carolyn Anderson, Nate Foster, Arjun Guha, Michael Greenberg, Jean-Baptiste Jeannin, Dexter Kozen, David Walker.

Papers. POPL 2014, ICFP 2014, Dissertation.