Expressing dynamic interaction patterns in concurrent programming
Jerome Y. Plun · 1995
This thesis is concerned with the specification of and reasoning about highly dynamic forms of concurrent computations. The goals are modularity and dependability. The vehicle is a set of new abstract programming constructs and a notation one can use to reason about computations using an assertional-style logic. The principal areas of applicability are mobile computing and dynamically reconfigurable architectures. Synchronization is a very common form of interaction in concurrent systems. Because most models of computing provide only static synchronization, which is unlikely to apply to dynamic systems, I developed a framework in which synchrony among atomic actions is expressed in terms of a predicate specifying whether a group of actions can be executed together in a given state of the computation. The framework includes an assertional proof logic which can be used for dynamic systems as well as for algorithms expressed in another model of computing whose synchronization mechanism is represented by an appropriate predicate. This feature is illustrated on two models which lack an assertional proof logic. Another common form of interaction is data sharing. I define a new paradigm, transient data sharing, which allows changes in which variables share some common data during a computation. The resulting new construct provides a modular approach to specifying and reasoning about dynamic environments, and in particular mobile computing. The notation is a direct extension of that used in the UNITY model, and reasoning about mobile computations relies on that model's proof logic. Several examples are used to explain the notation, demonstrate the modularity of the approach, and illustrate the verification methodology.