[Colloquium] [defense] Lukman/Dissertation Defense/Jul 10, 2020

[Margaret Jaffey]

This is an announcement about Jeffrey Lukman's dissertation defense.

Here is the Zoom link to participate:


https://uchicagostudents.zoom.us/j/97285118853?pwd=OW43NkVxM3dWZVVVK3NYWmFzOFBkdz09

Meeting ID: 972 8511 8853 Password: dcbugs One tap mobile
+13126266799,,97285118853#,,,,0#,,664061# US (Chicago)
+19294362866,,97285118853#,,,,0#,,664061# US (New York) Dial by your
location +1 312 626 6799 US (Chicago) +1 929 436 2866 US (New York) +1
301 715 8592 US (Germantown) +1 253 215 8782 US (Tacoma) +1 346 248
7799 US (Houston) +1 669 900 6833 US (San Jose)

Meeting ID: 972 8511 8853 Password: 664061 Find your local number:
https://uchicagostudents.zoom.us/u/acVUUyZNF6

       Department of Computer Science/The University of Chicago

                     *** Dissertation Defense ***


Candidate:  Jeffrey Lukman

Date:  Friday, July 10, 2020

Time:  2:00 PM

Place:  remotely via Zoom

Title: Algorithmic, Heuristic, and Systemic Approaches for Software
Model Checking of Distributed Systems

Abstract:
Today, distributed software infrastructures have become a dominant
backbone for cloud computing and modern applications. Large-scale
distributed systems such as scalable frameworks, storage systems,
synchronization, and cluster management services have emerged as the
data center operating system. Unfortunately, the reliability of
distributed systems is threatened by non-deterministic concurrency
bugs as it executes many complicated distributed protocols on
thousands of machines with no common clocks and it must face a variety
of random hardware failures. Facing the challenge of concurrency bugs,
this thesis proposes efficient approaches to empower software model
checking to quickly unearth concurrency bugs based on a comprehensive
characteristics study of real-world concurrency bugs in distributed
systems.

This thesis makes three main contributions. First, we present TaxDC,
the largest and most comprehensive taxonomy of distributed concurrency
(DC) bugs. We study the characteristics of 104 real-world distributed
concurrency (DC) bugs along several axes of analysis, such as the
triggering timing condition and input preconditions, error and failure
symptoms, and fix strategies from four widely-deployed cloud-scale
distributed systems: Cassandra, Hadoop MapReduce, HBase, and
ZooKeeper. This characteristics study provides many motivation and
guidelines for DC-bug detection, testing, and tools design.

Second, we present FLYMC, a fast, scalable, and systematic software
model checker for testing distributed systems implementations. To
overcome the path/state-space explosion problem in testing complex
interleavings of messages and faults, FLYMC introduces three powerful
algorithms: state symmetry, event independence, and parallel flips. As
a result, collectively, these algorithms make our approach on average
16×(up to 78×) faster than other state-of-the-art solutions. FLYMC is
integrated with eight distributed systems, successfully reproduced
twelve known DC bugs, and found ten new DC bugs which all have been
confirmed by developers.

Third, we present HMC, a heuristic software model checker to unearth
DC bugs faster. By exploiting the properties of distributed systems
and software model checking, HMC introduces four novel algorithms:
blocking state-event, last state-event, miss-prediction step, and
prioritized node crash, to prioritize more-likely test scenarios that
will reach new corner cases. With HMC, we reproduced five DC bugs in
Cassandra on average 6× (up to 15×) faster than FLYMC which we
consider as the state-of-the-art of systematic software model checker.

Jeffrey's advisor is Prof. Haryadi Gunawi

Login to the Computer Science Department website for details,
including a draft copy of the dissertation:

 https://newtraell.cs.uchicago.edu/phd/phd_announcements#lukman

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