Themis Melissaris will present his Pre FPO "Towards Testing and Analyzing Correctness in Concurrent Systems: From Microprocessors to IoT and Distributed Systems" on Monday, January 18, 2021 via Zoom

https://princeton.zoom.us/j/92110015157

Committee:
Margaret Martonosi: advisor
Kelly Shaw:  co-advisor, reader, Williams College
Kyle Jamieson: reader
David August: non-reader
Wyatt Lloyd: non-reader

Abstract follows below.  All are invited to attend.

Abstract:
The explosive data growth and the slowdown of Moore’s law presents new challenges for the next generation of hardware and software. To extract performance, systems ranging from microprocessors to internet of things (IoT) devices and distributed systems, increasingly leverage parallelism and concurrency. However, the performance benefits come at the cost of increased complexity in designing, specifying and testing correctness of these systems.

This dissertation draws insights across the different domains of computer architecture, IoT 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 synchronization-free consistency testing for multiprocessors and relies on property based testing using Litmus tests. This dissertation demonstrates PerpLE’s ability to speed up testing performance by orders of magnitude against the existing state of the art, enabling fast error discovery in commercial microprocessors. In addition, this thesis presents a study for rigorous concurrency testing of commercial and opensource 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. Finally, 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 provides automated testing by generating property-based tests and allows for increased testing performance and fast portability in open source distributed systems.