Concurrency without toil: a systematic method for parallel program design

AbstractFormal tools and methods for the design of concurrent programs can be very similar to their sequential counterparts, but nevertheless concurrent programming seems more difficult than sequential programming. Detailed examples in the literature suggest that this particular difficulty originates from interaction problems, when a fine grain of parallelism is required. A systematic technique is proposed to transform a coarse-grained version of a concurrent system into a finer-grained one, through a series of refinements. This technique is illustrated with a classical but still unproved algorithm for mutual exclusion. The incremental development clearly involves two kinds of steps. “Creative” transformations appear mainly at the beginning; these steps are short but rather subtle. “Technical” transformations are routine steps but involve lengthy formal developments. With a careful separation of creative and technical refinements, developments of concurrent programs become longer but no more difficult than developments of sequential programs