Because computations in a concurrent system can interact with each other while being executed, the number of possible execution paths in the system can be extremely large, and the resulting outcome can be
indeterminate. Concurrent use of shared
resources can be a source of indeterminacy, leading to issues such as
deadlocks, and
resource starvation. Design of concurrent systems often entails finding reliable techniques for coordinating their execution, data exchange,
memory allocation, and execution scheduling to minimize
response time and maximize
throughput. == Theory == Concurrency theory has been an active field of research in
theoretical computer science. One of the first proposals was
Carl Adam Petri's seminal work on
Petri nets in the early 1960s. In the years since, a wide variety of formalisms have been developed for modeling and reasoning about concurrency.
Models A number of formalisms for modeling and understanding concurrent systems have been developed, including: • The
parallel random-access machine • The
actor model • Computational bridging models such as the
bulk synchronous parallel (BSP) model •
Petri nets •
Process calculi •
Calculus of communicating systems (CCS) •
Communicating sequential processes (CSP) model •
π-calculus •
Tuple spaces, e.g.,
Linda •
Simple Concurrent Object-Oriented Programming (SCOOP) •
Reo Coordination Language •
Trace monoids Some of these models of concurrency are primarily intended to support reasoning and specification, while others can be used through the entire development cycle, including design, implementation, proof, testing, and simulation of concurrent systems. Some of these are based on
message passing, while others have different mechanisms for concurrency. The proliferation of different models of concurrency has motivated some researchers to develop ways to unify these different theoretical models. For example, Lee and Sangiovanni-Vincentelli have demonstrated that a so-called "tagged-signal" model can be used to provide a common framework for defining the
denotational semantics of a variety of different models of concurrency, while Nielsen, Sassone, and Winskel have demonstrated that
category theory can be used to provide a similar unified understanding of different models. The Concurrency Representation Theorem in the actor model provides a fairly general way to represent concurrent systems that are closed in the sense that they do not receive communications from outside. (Other concurrency systems, e.g.,
process calculi can be modeled in the actor model using a
two-phase commit protocol.) The mathematical denotation denoted by a closed system is constructed increasingly better approximations from an initial behavior called using a behavior approximating function to construct a denotation (meaning) for as follows: :: In this way, can be mathematically characterized in terms of all its possible behaviors.
Logics Various types of
temporal logic can be used to help reason about concurrent systems. Some of these logics, such as
linear temporal logic and
computation tree logic, allow assertions to be made about the sequences of states that a concurrent system can pass through. Others, such as
action computational tree logic,
Hennessy–Milner logic, and
Lamport's temporal logic of actions, build their assertions from sequences of
actions (changes in state). The principal application of these logics is in writing specifications for concurrent systems. == Practice ==