Grant: Discovery Launch Supplement

This proposal does not involve Indigenous communities, societies or individuals. Concurrent systems are ubiquitous, and concurrency is inescapable when designing complex computing systems. Indeed, it is a means of structuring complex systems as combinations of simpler programs, and it lets us harness the benefits of parallel and distributed computing architectures. However, concurrent systems are hard to get right, impacting both human safety and the economy. For example, concurrency-related defects caused patients to receive fatal doses of radiation from the Therac-25 radiation therapy machine, and they were partly responsible for the Northeast blackout of 2003. My Discovery research program enhances the safety and reliability of concurrent systems, with a focus on message-passing and shared-memory concurrency. Each of these concurrency paradigm is challenging to use on its own, and many systems combine both. Their complex interactions are rarely considered by existing work, but they are an important source of defects. My program's vision is to produce tractable theoretical foundations and tools for specifying, implementing, and reasoning about concurrent systems. My students and I will pursue three long-term goals that support my vision: 1. Increase the expressiveness and static safety guarantees of programming languages for specifying and implementing message-passing concurrent systems. 2. Similarly increase the expressiveness and safety guarantees of languages for shared-memory concurrency. Additional challenges compared to the message-passing setting include capturing phenomena like circularity that are used by data structures like doubly linked lists. 3. Investigate foundational logical techniques for combining concurrency paradigms in languages while still providing robust, language-level safety guarantees. Methodology. We will leverage the proven track record of the proofs-as-programs methodology to guide language design. This logical foundation also lets us deduce desirable program safety properties from known logical results, and it helps ensure that our theoretical results are broadly applicable. My students and I will mechanize our languages in a proof assistant and then extract verified compilers. To evaluate expressiveness, we will use our languages to implement and verify reusable libraries of concurrent algorithms. Impact. My Discovery program lays the foundation for lightweight static verification of concurrent systems, thereby reducing the costs incurred by concurrency defects. My program clarifies the interactions between language features and different concurrency paradigms, and it provides logically informed language design principles. These results will inform the development of industrial programming languages, leading to safer concurrent systems. Thus, this program will bolster the reliability of Canada's computing infrastructure, benefiting both public and private sectors.