Technical Report Number
This paper presents a model of concurrency (Dynamic Synchrony) whose distinctive feature is a novel formal treatment of synchronization. Synchrony is defined as the coordinated execution of two or more actions. The dynamic aspect comes from the fact that the definition of which actions must be executed synchronously can change freely during the execution of the program. This unique modeling capability comes with a UNITY-stype assertional logic that can be applied to program verification and derivation. This paper shows that the proposed proof logic can be used to verify programs expressed using other models of foncurrency without having to translate them to our notation. This capability is illustrated by verifying three versions of a parallel array summation problem, each written using a different model and notation - Swarm, Concurrent Processes, and Input/Output Automata. The new model makes UNITY-stype proofs feasible for a broad range of models of concurrency regardless of the way they handle synchronization and even if they lack an associated proof logic.
Roman, Gruia-Catalin and Plun, Jerome, "Reasoning about Synchrony Illustrated on Three Models of Concurrency" Report Number: WUCS-93-4 (1993). All Computer Science and Engineering Research.