Stable Multithreading

A New Paradigm for Reliable and Secure Threads

Edición de la obra Stable Multithreading

Multi threaded programs have become pervasive and critical due to the rise of the multi core hardware and the accelerating computational demand. Unfortunately, despite decades of research and engineering effort, these programs remain notoriously difficult to get right, and they are plagued with harmful concurrency bugs that can cause wrong outputs, program crashes, security breaches, and so on. Our research reveals that a root cause of this difficulty is that multithreaded programs have too many possible thread interleavings (or schedules) at runtime. Even given only a single input, a program may run into a great number of schedules, depending on factors such as hardware timing and OS scheduling. Considering all inputs, the number of schedules is even much greater. It is extremely challenging to understand, test, analyze, or verify this huge number of schedules for a multi threaded program and make sure that all these schedules are free of concurrency bugs. Thus, multi threaded programs are extremely difficult to get right. To reduce the number of possible schedules for all inputs, we looked into the relation between inputs and schedules of real-world programs, and made an exciting discovery: many programs need only a small set of schedules to efficiently process a wide range of inputs! Leveraging this discovery, we have proposed a new idea called Stable Multithreading (or StableMT) that reuses each schedule on a wide range of inputs, greatly reducing the number of possible schedules for all inputs. By addressing the root cause that makes multithreading difficult to get right, StableMT makes understanding, testing, analyzing, and verification of multithreaded programs much easier. To realize StableMT, we have built three StableMT systems, TERN, PEREGRINE, and PARROT, with each addressing a distinct research challenge. Evaluation on a wide range of 108 popular multithreaded programs with our latest StableMT system, PARROT, shows that StableMT is simple, fast, and deployable. All PARROT's source code, entire benchmarks, and raw evaluation results are available at http://github.com/columbia/smt-mc. To encourage deployment, we have applied StableMT to improve several reliability techniques, including: (1) making reproducing real world concurrency bugs much easier; (2) greatly improving the precision of static program analysis, leading to the detection of several new harmful data races in heavily tested programs; and (3) greatly increasing the coverage of model checking, a systematic testing technique, by many orders of magnitudes. StableMT has attracted the research community's interests, and some techniques and ideas in our StableMT systems have been leveraged by other researchers to compute a small set of schedules to cover all or most inputs for multi threaded programs.