The construction and validation of reliable multi-threaded programs is extremely difficult. Threads can improve performance on multi-processor machines and multi-core processors by enabling a program to execute more than one routine simultaneously, but unintended interactions between threads are hard to recognize during testing and are a common source of errors in deployed systems.
This research develops hybrid checkers that prevent unintended thread interactions by ensuring that a program's routines are atomic. A routine is atomic if its execution is not affected by and does not interfere with concurrently-executing threads. Previous work on static atomicity checkers (that inspect source code) and dynamic atomicity checkers (that monitor running programs) demonstrate the potential advantages of enforcing atomicity requirements. However, these approaches have precision or coverage limitations that reduce their ability to check large systems effectively. Hybrid checkers synthesize the best aspects of both techniques without suffering from these limitations.
The impacts of hybrid atomicity checkers, and their integration into a broad educational program, include improved software quality and better software engineering practices. Specifically, hybrid checkers provide a cost-effective mechanism for finding errors resistant to testing, are more usable and scalable than existing tools, and support a design methodology that encourages precisely specifying interactions between threads.
Computers now play a central role in virtually all parts of society, and we rely on computing systems to correctly perform many tasks on our behalf. At the same time, however, designing and implementing reliable software systems remains perhaps the greatest challenge facing the computing industry today. Despite great efforts to ensure reliability, software errors still occur, sometimes with costly consequences. Defects may be costly to find and fix, result in loss of data, enable security breaches, and even endanger lives. The problem of ensuring software reliability has been made even more challenging by the widespread adoption of multi-processor computers and multi-core processors. These hardware architectures enable programs to perform multiple tasks at the same time, and designing software to have such multiple threads of control running concurrency is widely believed to be the most promising way to achieve further performance improvements for many computer systems. However, threads may interfere with each other in subtle ways if the programmer does not properly coordinate (or synchronize) their behavior. Errors caused by unanticipated thread interactions are common but particularly difficult to discover during testing since they typically happen only intermittently and are discovered only long after the damaging interference actually occurs. In this grant, we examined automated software validation tools for finding concurrency defects. Programmers can use such tools to identify problems in software during development before they are experienced by users. Automated checking tools have proven quite useful at finding and eliminating other kinds of software defects, but they have traditionally been difficult to use and ineffective for finding synchronization defects in concurrent software. Our basic validation approach is to have programmers place "atomic" specifications on regions of source code that should be free of interference with all other threads. Those specifications, as well as other specifications describing how threads are coordinated, are then verified for correctness by an automated checker. If a code fragment does not exhibit the specified property, a warning is reported to the programmer. We focused on a synthesis of complementary analyses from static checkers (that inspect source code) and dynamic checkers (that monitor running programs) to enforce this type of requirement. This hybrid approach scales better and increases precision over previous work, as shown when we applied our techniques to validate a variety of programs. The intellectual merit and scientific contributions of this work include the development of techniques pushing forward the state of the art on how to check for interference errors in concurrent programs. The techniques studied are able to find concurrency defects ranging from the most-basic type of conflict when two threads access a specific memory location simultaneously without coordination to more subtle atomicity or serializability problems that require enforcing proper thread synchronization across much longer sequences of operations. We have also built and now distribute an open source analysis framework that serves as a test bed for new ideas in concurrency analyses. This framework has already been used extensively by both us and others. This work has contributed to computer science education in several ways. Numerous undergraduate students were trained to perform scientific research as part of this grant. Four of these students are now pursuing graduate degrees in computer science. In addition, we have participated in a number of curricular efforts to improve computer science education, particularly in the area of programming languages and concurrent programming. As part of these efforts, we developed several new models for an undergraduate curriculum in our discipline. Those curricular ideas, as well as results from this research agenda, have been integrated into classes taught at our institution. The greatest broader impact of this research is improving the reliability and robustness of our software infrastructure. The checkers we developed can prevent common and costly categories of synchronization errors that will only become more important to fix as software continues to be developed for multi-processors and multi-core chips. When integrated into a broad educational program, our work may also yield better software engineering practices and design methodologies in which thread interactions are precisely specified and then validated by automated tools.
