Constructing correct and efficient concurrent programs

A method is presented for programming correct and efficient cooperation in a set of sequential modules, on the basis of an invariant assertion, by means of formal and static deductions. For each sequential module, the pre- and post-assertions are computed from the invariant. Whereas the pre-assertion gives the synchronizing condition required before execution in order to preserve the invariant, the post-assertion expresses the “contribution” of this execution. Other assertions, called firing conditions, are derived which connect that contribution to the needs of waiting processes as expressed in their synchronizing conditions. A sequential module and its synchronizing and firing conditions are then integrated in a high-level synchronizing construct close to conditional critical regions, but allowing explicit control over the synchronizing conditions to be reevaluated at the exit for process resumption. Three levels of static elimination of useless condition reevaluations are then presented. These eliminations essentially use the information contained in firing conditions; they are shown to preserve partial correctness. The combined use of the notation and of the techniques proposed is illustrated through three examples