Verified Integration of Imperative Parallel Programming Paradigms in an Object-Oriented Language.

摘要

CC++ is a parallel object-oriented 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; semaphores, monitors, and asynchronous channels. A collection of libraries which integrates these traditional models with CC++ is specified, implemented, and formally verified.