SPEAKER: Paul Attie

WHEN: Friday, April 27 at 2 PM

WHERE: 149 CN


	An Efficient Method for the Design and Verification of
		      Large Concurrent Systems

We address the design and verification of the synchronization and
communication portion of large concurrent systems. Often, this portion
can be implemented using a fixed, finite amount of synchronization
related data, i.e., it is "finite-state."  Nevertheless, even when
each system component contains only one bit of synchronization related
data, the number of possible global synchronization states for K
components is about 2^K, in general.  Because of this
"state-explosion" phenomenon, the manual verification of large
concurrent systems typically requires lengthy, and therefore
error-prone, proofs. Using a theorem prover increases reliability, but
requires extensive human interaction to axiomatize and solve
verification problems.  Automatic verification methods (e.g., temporal
logic model checking) use state-space exploration to decide if a
system satisfies its specification, and are therefore also subject to
state-explosion.  To date, proposed techniques for ameliorating
state-explosion either require significant manual labor, or work well
only when the system is highly symmetric and regular (e.g., many
functionally similar components connected in similar ways).

Our approach structures the system description so that it is a priori
easy to verify correctness. For every pair of directly interacting
components, we represent their interaction explicitly and separately
from all the other interactions in the system.  We start with a
specification (written in temporal logic) which describes all the
pairwise interactions and we automatically synthesize a "pair-system" for each
such interaction. We then "compose" the pair-systems together to
produce the final large system.  Unlike other temporal logic synthesis
techniques, our method is not subject to state-explosion (even when
all system components are functionally dissimilar), and addresses
non-functional properties such as fault-tolerance, efficiency, and
distribution. We also present possible extensions of our work to
real-time and infinite-state synchronization code.

Readings

Synthesis of large concurrent programs via pairwise composition 
   P.C. Attie
   CONCUR'99: 10th International Conference on Concurrency Theory 

Synthesis of concurrent systems with many similar processes
   P.C. Attie and E.A. Emerson
   ACM Transactions on Programming Languages and Systems, vol. 20, 
   no. 1, pp. 51-115, January 1998 

Note. These papers are available for download