Inferring models of systems from observations of their behavior
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
InvariMint Added an option outputCountLabels to output counts on edges; renamed … Jun 22, 2016
bin Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
csight Added an option outputCountLabels to output counts on edges; renamed … Jun 22, 2016
daikonizer Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
embeddedgwt Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
javadoc Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
jvm-dtracing Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
lib Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
output Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
synoptic Add flag to specify k for k-tails entry point May 11, 2018
synopticgwt fix synopticgwt compile May 4, 2015
synopticjung Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
traces Added shopping cart ex args for Perfume Jan 27, 2016
.gitignore Rename .hgignore -> .gitignore Jun 24, 2015
LICENSE.md Update LICENSE.md Jun 24, 2015
README.md fixed links to wiki by making them absolute Dec 20, 2016
RELEASE-README.txt Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
ant-util.xml Partial fix for issue 413 and 418. Apr 18, 2018
build.xml removed synoptigwt from default ant build (it no longer compiles easily) Jun 22, 2016
build_synoptic_distro.py Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
csight-jar.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
csight.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
deterministic.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
doc_usage.sh updated doc_usage script for git repo Jun 22, 2016
eclipse.dict Added an option outputCountLabels to output counts on edges; renamed … Jun 22, 2016
invarimint.bat Merged with changes in default Feb 6, 2015
invarimint.sh Merged with changes in default Feb 6, 2015
invarimint_bigheap.sh Merged with changes in default Feb 6, 2015
java-code_syle-compiler-prefs.epf Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
perfume-jar.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
perfume.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
perfume_bigheap.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
synoptic-jar.bat Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
synoptic-jar.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
synoptic.sh Merged with changes in default Feb 6, 2015
synoptic_bigheap.sh Merged with changes in default Feb 6, 2015
synoptic_dump_heapmap.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
synopticjung-jar.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015
synopticjung.sh Removed unconstrained model checking from Perfume refinement in getSp… Jan 14, 2015

README.md

Overview

This site hosts source code, academic papers, and other resources for three related projects:

  • Synoptic : a tool to infer an FSM model from a sequential log.
  • CSight : a tool to infer a communicating FSM model from a distributed system's logs
  • InvariMint : an approach to declaratively specify model inference algorithms
  • Perfume : a tool to infer performance models from system logs. Try it!

Introduction

Systems are often difficult to debug and to understand. A typical way of gaining insight into system behavior is by inspecting execution logs. However, manual log analysis is often tedious and labor-intensive. Synoptic and CSight are tools that mine a model of the system that generated the log, thereby simplifying log analysis.

  • Synoptic mines a finite state machine (FSM) model representations of a sequential system from its logs. Two features distinguish Synoptic from other tools.

    1. Synoptic's models preserve key event ordering invariants mined from the log, making them more accurate.
    2. Synoptic uses refinement to derive the model, which is more efficient than traditional coarsening algorithms like kTails.
  • 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.

  • 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.

  • Perfume extends Synoptic to account for resource utilization information often available in system logs. Perfume-generated models are FSM models with resource information annotating the event transitions. The algorithm extends trivially to arbitrary integer-valued resources, such as time, memory utilization, network throughput, etc. Perfume mines temporal properties with performance constraints from the log and uses these properties to identify and remove imprecise generalizations in the Synoptic model inference process. See this page to learn more about Perfume.

For users

For academics

  • Synoptic:

  • CSight:

    • ICSE'14 conference paper : describes the approach and evaluates CSight formally and with a user-study.
    • SLAML'11 workshop paper : motivates and defines temporal invariants for partially ordered logs, and gives three algorithms for mining these invariants.
  • InvariMint:

  • Perfume:

    • ASE'14 conference paper : describes the Perfume algorithms and properties in detail; evaluates the tool in a user study and on TCP logs and on logs from related work.
    • ICSE'14 NIER paper : motivates perfume and briefly overviews the approach.

For developers

A synoptic example

1. Lets say you are implementing the two phase commit protocol. You wrote your code, and as part of debugging you included print statements that output a log like the following:

src : 2, dst : 0, timestamp : 16, type : propose, txid : 1
src : 2, dst : 1, timestamp : 17, type : propose, txid : 1
src : 0, dst : 2, timestamp : 18, type : abort, txid : 1
src : 1, dst : 2, timestamp : 19, type : commit, txid : 1
src : 2, dst : 0, timestamp : 20, type : tx_abort, txid : 1
src : 2, dst : 1, timestamp : 21, type : tx_abort, txid : 1
..

2. You then thoroughly tested and debugged the code, and eventually deployed it. After a week of executing thousands of two-phase commit rounds you discover an application-level inconsistency. This leads you to look at the accumulated log:

https://raw.githubusercontent.com/wiki/ModelInference/synoptic/images/main_page/long_2pc_log.png


3. Uh oh. Your first challenge -- to make sense of the thousands of lines in front of you. Your second challenge -- find clues that might lead you to a potential root cause. You fire up Synoptic with:

$ ./synoptic.sh -r '.+ timestamp :(?<DTIME>), type :(?<TYPE>), txid :(?<txId>)' -m '\k<txId>' logfile.txt -o twopc-graph

And you get the following output:

https://raw.githubusercontent.com/wiki/ModelInference/synoptic/images/main_page/2pc_new_graph.png


4. You realize that this graph output differs from the graph that you generated while testing your code:

https://raw.githubusercontent.com/wiki/ModelInference/synoptic/images/main_page/2pc_old_new_graphs.png

You then find exactly where this discrepancy occurs in the log file, and go on from there.

Related projects

  • ShiVector : a tool to augment logs of distributed systems with partial ordering information
  • ShiViz : a tool to visualize partially ordered distributed logs (try it!)

Support

YourKit is kindly supporting the Synoptic project with its full-featured Java Profiler. YourKit, LLC is the creator of innovative and intelligent tools for profiling Java and .NET applications. Take a look at YourKit's leading software products: YourKit Java Profiler and YourKit .NET Profiler.