CRPC-TR93390-S

Title:	  A Verified Integration of Imperative Parallel
	  Programming Paradigms in an Object-Oriented
	  Language

Authors:  Paul A. G. Sivilotti (student author)*

Date:	  June 1993

Abstract:

  CC++ is a parallel object-orieted 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.


 * In partial fulfillment of the requirements for the
   degree of Master of Science