Bugs in Code: Understanding, Detecting, and Fixing

Andrzej WÄ…sowski (IT University of Copenhagen).


Course Summary | About the lecturer | Location and schedule | Materials | Assignment

Course summary:

The course will show the ways in which the software engineering research community approaches research on program correctness. I will present a summary of collaboration with open source projects around understanding historical bugs and building tools for detecting new bugs.

In the first part, I will report the state of the union for bugs in two complex software systems : the Linux kernel (which is likely the most popular operating system on the planet) and the ROS operating system (which is not an operating system at all, but likely the most popular robotics middleware on the planet). In both cases, we will look into programming language aspects of problems observed in the very rich histories stored in the source code repositories of this projects. In the Linux kernel case, we will additionally focus on challenges introduced by the highly configurable aspect (bugs hidden well in rare configurations). For ROS, we will emphasize robotics-specific bugs and problems hidden in intensive modularity of the ROS applications architectures. Then, we will ask basic methodological questions: Why a tool builder fighting with bugs might want to search and understand real bugs? What is the cost of studying bugs? How and what kinds of benchmarks can reduce this cost? What can be learnt from real bugs? What are the challenges of studying real bugs, and what methods do we have to reproduce real bugs, in order to use them for experiments later? How can we create benchmarks that will survive a long time, without bit rotting?

In the second part, I will show the EBA tool, specifically designed to uncover resource manipuation bugs in the Linux kernel; in response to some requirements presented in the first part of this lecture. EBA (an effect-based analyzer) creates a program abstraction performing a type inference in a rich type system tracking regions (a memory abstraction), simple shapes (hierarchies of pointers nested in structures) and side-effects of computations. This abstraction is then overlayed on a control-flow graph and fed to a reachability checking algorithm that identifies suspicious sequences of effects: for instance a lock taken twice. I will describe how EBA works, and how we used it to uncover about a dozen sequential double-lock bugs in the Linux kernel.

In the third part, I will attempt to define the problem of program repair, and present several exemplary works by other authors on generating fixes for bugs in software. We will conclude with reflection on challenges in bug finding and bug fixing research.

About the lecturer:

Andrzej WÄ…sowski works with design and use of technologies that improve quality of software, including issues such as correctness and maintainability. He has worked extensively with software product line methods---ways to develop software for similar products at lower cost but with higher quality. He has collaborated with open source projects (Linux kernel and ROS among others) and with industry (for example with Danfoss). Currently, he is investigating quality assurance methods for robotics platforms, in the H2020 project ROSIN.

Andrzej Wasowski is a professor of Software Engineering at IT University in Copenhagen (ITU). He holds an MSc degree from Warsaw University of Technology and a PhD degree from ITU. He has previously held visiting positions at Aalborg University (Denmark), INRIA Rennes (France) and University of Waterloo (Canada).

Location and schedule:

MIMUW building, room 5440

Thursday, June 6
16:00 - 17:15 lecture
Friday, June 7
14:15 - 15:45 lecture
15:45 - 16:00 coffee and cake
16:00 - 17:00 lecture
Saturday, June 8
10:15 - 11:45 lecture
11:45 - 12:00 coffee and cake
12:00 - 13:00 lecture

Materials

Assignment: problem set. Please submit the solutions by email to wasowski at itu.dk by July 21. Also, in case there are any questions concerning the exam, feel free to ask the lecturer.