Models for Concurrency

In order to analyze a concurrent system rigorously it is imperative to have a formal description, or model, of the system that is amenable to formal analysis. This basic observation has prompted the development of a variety of different mathematical theories of concurrency over the past two decades, and different schools of thought have arisen on the basis of how to model various kinds of systems and what constitute relevant properties of such systems.

Despite these differences, there is a basic agreement between the different schools of thought: models of concurrent systems cannot be functional. Unlike the traditional, sequential setting, one cannot view a concurrent system as a function from inputs to outputs; it is necessary to take into account the fact that systems do not run in isolation but interact with other systems and hence patterns of stimuli/response relationships vary over time. Instead, models of concurrency typically begin with the basic notion of atomic action, or ``uninterruptible'' system activity. A system executes by performing atomic actions; models differ in terms of how to capture the notion of system execution. Examples of such theories include the following.

Automata-based

theories model systems in terms of states and transitions between states. In process algebras such as ACP, CCS and CSP, transitions are labeled by atomic actions; I/O automata also follow this approach by allowing distinctions between different types of actions. Petri nets extend this paradigm by encoding spatial-distribution information within states.

Action-based

theories model systems via structures consisting of atomic actions. One of the earliest of these described systems in terms of the traces, or sequences of atomic actions, that systems can perform. Elaborations of this model include acceptance trees and refusal sets, both of which decorate basic trace information with information about what stimuli systems may respond to after performing a sequence. Synchronization trees encode system behavior as a trees with edges labeled by actions. Mazurkiewicz traces include an independence relation between actions to capture possible concurrency. In other models, atomic actions are used as labels of partially ordered sets of events (pomsets), possibly enriched with a conflict relation (labeled event structures).

Models of concurrency can be categorized in terms of the decisions each has taken with respect to the following three dichotomies.

• Intensional vs. extensional descriptions
• Interleaving vs. true concurrency
• Branching time vs. linear lime

• Intensional models like labeled transition systems require explicit description of systems states and possible state changes. Extensional models like Mazurkiewicz traces concentrate just on the pattern of possible interactions over time.

• In interleaving models, it is assumed that observations of system behavior are sequential; consequently, the execution of parallel actions is reduced to nondeterministic interleaving (the presence of any concurrent actions is rendered as the choice between their sequential executions). Truly concurrent models instead treat concurrency as fundamental; the behavior of systems is represented in terms of the causal relations among the events performed by the components of distributed states (actions that are not causally related are concurrent) or by describing the locations at which the actions take place.

• The difference between branching time and linear time models lies in the way they deal with the choices that systems might have to face during their execution. In the former case, choice points arising during execution are considered important, while in the latter they are not. Thus, models that do not respect branching time describe concurrent systems in terms of the sets of their possible (partial) runs while in branching time models the points at which different computations diverge from one another is recorded. Hoare's traces and pomsets are linear time models while synchronization trees and labeled event structures are branching time models.

Different decisions about the three dichotomies are appropriate for different purposes. Extensional models provide a useful basis for explaining system behavior, while intensional one are more amenable to automated analysis. An interleaving semantics is useful for specifying extensional behaviors of systems, whereas a truly concurrent semantics might be the basis for describing possible implementations, where for example performance issues are of interest. A branching-time semantics is necessary when safety properties, like deadlock, are of interest while linear time semantics is sufficient to establish liveness properties, like partial termination.

Traditional theories have concerned themselves with modeling choice and concurrency; more recent work has focused on elaborating them with other aspects of system behavior, including real-time and probability (see Section 3.1.