A Verified Integration of Parallel Programming Paradigms in CC++

CC++ is an object-oriented parallel programming language that uses parallel composition, atomic functions, and single-assignment variables to express concurrency. We show that this programming paradigm is equivalent to several traditional imperative communication and synchronization models, namely monitors and asynchronous channels. Furthermore, the objectoriented nature of CC++ provides an ideal framework for integrating these paradigms. We specify, implement, and formally verify a collection of libraries that integrates these traditional models with CC++