FORMALIZATION OF PROPERTIES OF PARALLEL PROGRAMS

Abstract

Abstract : The paper describes a class of parallel programs and gives a formalization of certain properties of such programs in predicate calculus. Although the programs are syntactically simple, they do exhibit interaction between asynchronous parallel processes, which is the essential feature to be considered. The formalization can easily be extended to more complicated programs. Also presented is a method of simplifying parallel programs, i.e., constructing simpler equivalent programs, based on the 'independence' of statements in them. With these simplifications the formalization gives a practical method for proving properties of such programs. (Author)