Wednesday, July 20, 2011
10:00 AM
CSB Room 703
Zijiang James Yang
Western Michigan University
SMT Based Symbolic Analysis for Concurrent Systems
In the first part, I will present an approach to generate data race witnesses by an SMT-based analysis. Data race is one of the most dangerous errors in concurrent programming, and despite intensive studies, it remains a notorious cause of failures. Detecting data races, statically or dynamically, is already a hard problem, and yet it is even harder for a programmer to decide whether or how a reported data race can appear in the actual program execution. In this talk I will introduce algorithms for generating debugging aid information called witnesses, which are concrete thread schedules that can deterministically trigger the data races.

Unfortunately due to the complexity of concurrent systems, subtle bugs remains even under the most rigorous testing and verification. Thus ability to replay a program's execution on a multi-processor system can significantly help concurrent programming. To replay a shared-memory concurrent program, existing solutions record its program input and the shared-memory dependencies between threads. In the second part of this talk, I will present a processor-based record-and-replay solution that does not require detecting and logging shared-memory dependencies to enable multi-processor execution replay. Shared-memory dependencies between threads are reconstructed offline, during replay, using an algorithm based on an SMT solver. In addition to saving log space, the proposed solution significantly reduces the complexity of hardware support required for enabling replay. The proposed approach can support replay of not only sequentially consistent executions but also executions under relaxed memory models.

Bio: Zijiang James Yang is an Associate Professor of Computer Science at Western Michigan University. Before joining WMU he was a researcher at NEC Labs America, Inc. He received his Ph.D. from the University of Pennsylvania in 2003. Dr. Yang was the recipient of the 2008 ACM TODAES best paper award, 2008 WMU CEAS Outstanding Young Researcher Award, and the 2010 PADTAD best paper award. He holds 9 U.S. patents. Dr. Yang has been a visiting professor at the University of Michigan since 2009.