PGo: source to source compiler from PlusCal into Go lang.

PGo compiles PlusCal formal specifications into Go implementations. PGo is designed to reduce the developer burden of implementing a correct distributed system specification, and increases developers' confidence in the correctness of their implementations.

Dinv: distributed system state invariant detector. (Video!)

Distributed systems are difficult to debug and understand. One reasons for this is distributed state, which is not easily accessible and must be pieced together from the states of the individual nodes. Dinv statically analyzes the node source code to identify distributed state variables and then instruments the system to record these variables at runtime. After system execution Dinv uses dynamic analysis to determine consistent distributed state snapshots and infers likely distributed state invariants.

NetSolver: Scalable Virtual Data Center Allocation

NetSolver is an SMT-based VDC allocation tool for multi-path VDC allocation with end-to-end bandwidth guarantees. It scales to data centers with 1,000 or more servers, and can make allocations quickly enough to be applied in practice, while simultaneously improving data center utilization relative to previous work.

TimeSquared: multi-threaded callstack analysis. (Try it)

Helping developers understand complex multi-threaded systems by capturing callstack/event information (with DINAMITE) and supporting exploration of the captured data through visualization.

Callback hell in JavaScript.

Callbacks are a popular language features in JavaScript. However, they are also a source of comprehension and maintainability issues. The example on the left illustrates nested, anonymous callbacks, as well as asynchronous callback scheduling. Not much code, but so much complexity! We carried out a study of callbacks across 138 applications, and are developing tools to help developers manage callback hell in their applications. Our analysis code from the study is online.

ShiViz and TSViz: Visualizing distributed/multi-threaded system logs. (Try ShiViz, Try TSViz)

Concurrent systems generate logs that are complex and unwieldy. ShiViz helps developers understand distributed system logs through visualization. ShiViz visualizes a distributed execution that has been instrumented to record vector clock timestamps (e.g., with distributed clock instrumentation library). The visualizations are simple-to-understand and interactive. The user can understand complex system behavior by exploring the log through the visualization, comparing executions side-by-side, searching for specific behavior (by keyword and topology), and much more. TSViz, builds on ShiViz and visualizes multi-threaded logs with vector clocks and physical timestamps.

Repograms: exploring and juxtaposing software repositories.

Repograms is a tool for visualizing the activity in a software repositories (e.g., git). It uses a simple metaphor of multi-colored blocks of varying sizes to encode different kinds of information about the repository. For example, each unique committer could be assigned to a color and the sequence of blocks can reveal who works when, and how many commits each person makes.

Texada: general LTL specification mining. (video)

Texada is a temporal specification mining tool for extracting linear temporal logic (LTL) specifications of arbitrary length and complexity. Texada takes a user-defined LTL property type template and a log of program traces as input and outputs a set of instantiations of the property type (i.e., LTL formulas) that are true on the traces in the log. Texada is envisioned as a specification mining engine on top of which new software analyses can be developed.

Perfume: Inferring performance models. (Try it, video)

Perfume summarizes a system's logged executions in a performance-aware, behavioral model. Performance metrics present in logs convey vital information about most systems, yet previous model inference work ignores performance data. By leveraging this information, Perfume generates more precise models, which can help developers understand system behavior that depends on metrics like execution time, network traffic, or energy consumption.

NetCheck: Diagnosing networked applications from blackbox traces.

Networked applications can fail for many complex reasons having to do with the network or misbehavior of a remote end-host. NetCheck uses traces of syscalls calls made by the application and any end-hosts that are pertinent to the application logic (e.g., the user's desktop, an SMTP server, and a DHCP server). Using these traces NetCheck reconstructs a plausible partial order of network communication without any clock synchronization. It then uses a set of rules to diagnose network issues that are apparent in the reconstructed network behavior.

ShiVector: Augmenting logs of distributed systems with partial ordering.

A major challenge in debugging distributed systems is analyzing execution logs generated at multiple hosts. ShiVector transparently adds vector timestamps to logs generated by a distributed system. These vector-timestamped logs capture partial ordering information, which can be used for further analysis and log comprehension. ShiVector-augmented logs can be visualized with ShiViz.

Synoptic: Inferring FSM models from logs of sequential executions.

Systems are often difficult to debug and to understand. A typical way of gaining insight into system behavior is by inspecting execution logs. Manual inspection of logs, however, is an arduous process. This project helps this problem by designing Synoptic, a tool to produce summary model of a system log. Two features distinguish Synoptic from other tools. First, Synoptic's models preserve key invariants mined from the log, making them more accurate. Second, Synoptic uses refinement to derive the model, which is more efficient than traditional coarsening algorithms.

CSight: Inferring communicating FSM models of distributed systems.

CSight mines a communicating FSM model to represent the distributed system that generated a set of logs. Like Synoptic, CSight mines models that preserve temporal properties of the system. Engineers can use the inferred models to understand complex behavior, detect anomalies, debug, and increase confidence in the correctness of their implementations.

InvariMint: Declaratively specifying model inference algorithms.

InvariMint is an approach to express FSM model inference algorithms in a common framework. The key idea is to encode properties of an algorithms as finite state machines. These properties can then be instantiated for a specific input log of observations and combined to generate/infer a model that describes the observations. InvariMint (1) leads to new fundamental insights and better understanding of existing algorithms, (2) simplifies creation of new algorithms, including hybrids that extend existing algorithms, and (3) makes it easy to compare and contrast previously published algorithms.