Testing and Analyzing Correctness in Concurrent Systems: From Microprocessors to IoT and Distributed Systems

Abstract

Applications such as the Internet of Things (IoT), multimedia streaming and self driving cars are drivers for explosive data growth. This data growth along with the slowdown of Moore's law presents new challenges for computing and spurs innovation for the next generation of hardware and software. To extract performance at manageable power, systems ranging from microprocessors to IoT devices and distributed systems increasingly leverage parallelism and concurrency. However, the performance and power benefits of parallelism come at the cost of increased complexity in designing, specifying and testing correctness of these systems. This dissertation draws insights across the domains of computer architecture, ΙοΤ and distributed systems, resulting in a set of practical tools and methodologies that allow for rigorous and efficient testing of correctness on multiprocessors, IoT systems and distributed systems. More specifically, this thesis introduces PerpLE, a tool that enables consistency testing for multiprocessors without per-iteration synchronization and relies on property based testing using litmus tests. This dissertation demonstrates how PerpLE speeds up testing performance by orders of magnitude against the state of the art, enabling fast error discovery in commercial microprocessors. Additionally, this dissertation presents Musli Tool, a practical tool for empirical consistency testing of distributed systems that leverages techniques and methodologies based on the computer architecture concept of litmus tests. Musli Tool automates testing by generating property-based tests and increases testing performance and fast portability in open source distributed systems. Finally, this thesis presents a study of rigorous concurrency testing on commercial and open source IoT systems. The study demonstrates correctness deficiencies of IoT systems and identifies the implications of race conditions, lack of atomicity and weak consistency on applications. To mitigate erroneous behavior for IoT applications, the OKAPI tool is introduced. This dissertation presents how to vastly improve the performance and efficiency of consistency testing by leveraging a synchronization free variant of litmus tests and by developing tools to enable analysis and generation of tests based on this new methodology. This thesis also demonstrates how to take lessons learned from testing correctness in microprocessors and adapting to other domains of concurrent systems, particularly distributed systems and IoT.