Title: Adding Simplicity and Order in Today's Complex Software


Abstract:
Real-world software becomes increasingly complex and hard to get right due to two trends. First, driven by the rise of the multi-core hardware, software is moving from single-threaded to multi-threaded, and the concurrently running threads can interleave in too many different ways. These messy thread interleavings aggravate understanding, testing, and analyzing of software, and can easily lead to wrong outputs and security breaches. Second, driven by the diverse computational demands, software is getting larger and larger, leading to exponential growth of program paths. It is extremely hard for existing techniques to check critical programming rules (e.g., allocated memory must be freed, and assertions must always succeed) on these exponentially many program paths, thus software is prone to harmful bugs (e.g., resource leaks and crashes).

In this talk, I will present two new techniques that can make software much easier to get right by removing unnecessary software complexity. First, I will present Stable Multi-Threading (StableMT), a reliable and secure parallelism paradigm that can greatly reduce the amount of thread interleavings, and a practical StableMT runtime system that is fast and scalable with a wide range of popular software. Second, I will introduce rule-directed pruning, a new algorithm that can soundly prune program paths irrelevant to a checked rule, leading to exponential speedup of a state-of-the-art verification tool, and eight new rule violations confirmed or fixed in widely used software. These two new techniques have broad applications, and they have been leveraged by researchers to greatly improve several existing reliability and security techniques.


Bio:
Heming Cui is a PhD candidate at Computer Science of Columbia University. His thesis research is focused on improving software reliability and security with runtime and program analysis techniques. His general interests are in operating systems, programming languages, and distributed systems. Before joining Columbia, he obtained his master and bachelor degrees from Tsinghua University, Beijing, China.