[Colloquium] Leesatapornwongsa/MS Presentation/Dec 2, 2014

[Margaret Jaffey]

This is an announcement of Tanakorn Leesatapornwongsa's MS
Presentation.

------------------------------------------------------------------------------
Date:  Tuesday, December 2, 2014

Time:  1:30 PM

Place:  Ryerson 251

M.S. Candidate:  Tanakorn Leesatapornwongsa

M.S. Paper Title: SAMC: Semantic-Aware Model Checking for Fast
Discovery of Deep Bugs in Cloud Systems

Abstract:
In the last five years, we have seen a rise of implementation- level
distributed system model checkers (dmck) for verifying the reliability
of real distributed systems. Existing dmcks however rarely exercise
multiple failures due to the state-space explosion problem, and thus
do not address present reliability challenges of cloud systems in
dealing with complex failures. To scale dmck, we introduce
semantic-aware model checking (SAMC), a white-box principle that takes
simple semantic information of the target system and incorporates that
knowledge into state-space reduction policies. We present four novel
reduction policies: local-message independence (LMI), crash-message
independence (CMI), crash recovery symmetry (CRS), and reboot
synchronization symmetry (RSS), which collectively alleviate redundant
re- orderings of messages, crashes, and reboots. SAMC is systematic;
it does not use randomness or bug-specific knowledge. SAMC is simple;
users write protocol- specific rules in few lines of code. SAMC is
powerful; it can find deep bugs one to two orders of magnitude faster
compared to state-of-the-art techniques.

Tanakorn's advisor is Prof. Andrew Chien

Login to the Computer Science Department website for details:
 https://cs.uchicago.edu/phd/ms_announcements#tanakorn

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Margaret P. Jaffey            margaret at cs.uchicago.edu
Department of Computer Science
Student Support Rep (Ry 156)               (773) 702-6011
The University of Chicago      http://cs.uchicago.edu
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=