Modeling Systems from Logs of their Behavior

Thesis (Ph.D.)--University of Washington, 2013Billions of people rely on correct and efficient execution of large systems, such as the distributed systems that power Google and Facebook. Yet these systems are complex and challenging to build and understand. Logging of important events is known to be invaluable for debugging and diagnosing problems in such systems. Unfortunately, many execution logs are inscrutable in their raw form. For example, a production Google system may generate a billion-line log file in a single day. This dissertation addresses the challenges that developers and operators face in debugging and reasoning about large systems. Specifically, it presents runtime analysis techniques and corresponding tools to help developers make sense of large systems by leveraging the extensive logs generated by the systems. This dissertation presents three log-analysis tools to infer concise and precise models from execution logs of sequential and distributed systems. Three features distinguish these tools and make them simple to use and applicable to a variety of systems and tasks. (1) These tools process the logs most systems already produce and require developers only to specify a set of regular expressions for parsing the logs. (2) These tools do not depend on source code or other implementation-level details of the systems they model, and they do not constrain the semantics of the events in the log. Finally, (3) these tools are designed to scale to large logs. The first tool, Synoptic, infers a finite state machine model of a sequential system from a log of system behavior. Synoptic has two unique features. First, the model it produces satisfies three kinds of temporal invariants mined from the logs, improving accuracy over related approaches. Second, Synoptic uses both refinement and coarsening to explore the space of models. This dual approach improves model efficiency and precision, compared to an approach that uses just one of these options. The second tool, Dynoptic, infers a communicating finite state machine (CFSM) model of a networked system. This model represents each process independently as a finite state machine, and the process machines are augmented with communication events that allow the processes to coordinate over FIFO queues. Finally, InvariMint generalizes the insights from Synoptic and Dynoptic into an approach for declaratively specifying model inference algorithms. Existing model inference algorithms are difficult to understand, extend, and compare. InvariMint simplifies each of these tasks. The dissertation formally defines the model inference techniques underlying all three tools and proves important properties of each of the approaches. Empirical experiments show that developers find the inferred models useful for identifying bugs, confirming previously known bugs, and increasing their confidence in their implementations. By making these tools publicly available, this dissertation helps to bridge the gap between a systems development culture of logging for debugging with advanced techniques from the formal methods and software engineering research communities