Drop-in Concurrent API Replacement
for Exploration, Test, and Debug

My Masters thesis. Describes a system to model concurrent API specifications formally in a way closer to English and then compile that to a form that can be used to ask what-if questions and can be run as a drop-in replacement for the API connected to a C program. A re-write by my faculty advisors later made it into a journal, VMCAI 2012.

Complex concurrent APIs are difficult to reason about annually due to the exponential growth in the number of feasible schedules. Testing against reference solutions of these APIs is equally difficult as reference solutions implement an unknown set of allowed behaviors, and programmers have no way to directly control schedules or API internals to expose or reproduce errors. The work in this paper mechanically generates a drop-in replacement for a concurrent API from a formal specification. The specification is a guarded command system with first-order logic that is compiled into a core calculus. The term rewriting system is connected to actual C programs written against the API through lightweight wrappers in a role-based relationship with the rewriting system. The drop-in replacement supports putative what-if queries over API scenarios for behavior exploration, reproducibility for test and debug, full exhaustive search and other advanced model checking analysis methods for C programs using the API. We provide a Racket instantiation of the rewriting system with a C/Racket implementation of the role-based architecture and validate the process with an API from the Multicore Association.