Zhuo Sun

School of Computing and Information Sciences

Lecture Information:
  • November 5, 2018
  • 10:30 AM
  • ECS 349

Speaker Bio

Zhuo Sun is a Ph.D. candidate in the School of Computing and Information Science at Florida International University. She received her Master’s degree in Software Engineering from Sun Yat-sen University in 2005, and Master’s degree in Telecommunications and Networking from Florida International University in 2011.  While a part-time Ph.D. student, she is working at Motorola Solutions as a software automation engineer to improve software reliability through automated testing. Her research interests lie in the areas of software reliability and program analysis. Her research aims at making concurrent systems more reliable through dynamic and predictive analysis at the code level.


Concurrency bugs are extremely hard to detect due to huge interleaving space. They are happening in the real world more often because of the prevalence of multi-threaded programs taking advantage of multi-core hardware, and microservice based distributed systems moving more and more applications to the cloud. As the most common non-deadlock concurrency bugs, atomicity violations are studied in many recent works, however, those methods are applicable only to single-variable atomicity violation, and don’t take the specific challenge in distributed systems into consideration that have both pessimistic and optimistic concurrency control.

This dissertation presents a tool using model checking to predict atomicity violation concurrency bugs involving two shared variables or shared resources. We developed a unique method inferring correlation between shared variables in multi-threaded programs and shared resources in microservice based distributed systems, that is based on dynamic analysis and is able to detect the correlation that would be missed by static analysis. For multi-threaded programs, we use binary instrumentation tool to capture runtime information about shared variables and synchronization events, and for microservice based distributed systems, we use web proxy to capture Http based traffic about Api calls and the shared resources they access including distributed locks. Based on the detected correlation and runtime trace, the tool is powerful and can explore a vast interleaving space of a multi-threaded program or a microservice based distribute system given a small set of captured test runs. It is applicable to large real-world systems and can predict atomicity violations missed by other related works for multi-threaded programs and a couple of previous unknown atomicity violation in real world open source microservice based systems. A limitation is that redundant model checking may be performed if two recorded interleaved traces yield the same partial order model.