Checking the Data Sharing Strategies of Concurrent Systems Level Code
Due to the high degree of control and performance that it affords, programmers use the C language for writing low-level systems software. That it is difficult to write programs in C is not a problem in and of itself. Modern languages deal with its safety issues through innovations in language design, programming interfaces and runtime environments. However, due to the amount and complexity of existing C code, rewriting all of it in modern languages is likely infeasible, and the absence of a modern replacement for C having all of its advantages ensures that it will continue to be used to create new software for the foreseeable future.
The goal of the Ivy compiler is to provide an evolutionary pathway from C to a language with stronger safety guarantees. Because rewriting software all at once is not an option, the design philosophy of Ivy is to provide ways for the programmer to transition software in a modular fashion from C to a language with the desired safety guarantees. Given these requirements, Ivy provides memory- and type-safety to sequential programs with two components, one called Deputy, and the other called Heapsafe. However, Deputy and Heapsafe are unsound when faced with multi-threaded programs.
This dissertation presents SharC, an extension to Ivy that provides for safe concurrent programming, and Shelters, a deadlock-free, pessimistic implementation of atomic sections that avoids software transactional memory and whole-program analysis. SharC allows programmers to declare how objects in multi-threaded programs are shared among threads. SharC uses a combination of static and dynamic analysis to enforce these ``sharing modes.'' Additionally, since objects in programs can go through several phases, SharC allows programmers to declare where the sharing mode of an object changes. SharC checks these sharing mode changes by requiring that there is only one reference to an object when its sharing mode changes. Further, SharC provides features for
applying and changing these sharing modes across complex data structures. Finally, our shelter-based atomic sections are presented as a sharing mode of SharC that can provide the convenience of atomic sections while achieving performance comparable with explicit locking.
We evaluate our implementation of SharC and Shelters on over 1.5 million lines of application and benchmark code, and observe manageable overheads both in terms of performance and programmer effort.