Models for Concurrent Software

Concurrent Software Designs

last updated: 15.December.2005

Concurrent software designs provide a means for people to blueprint and reason about computer programs, targetting systems with multiple instruction execution units (from massively parallel machines to microprocessors with an on-chip DMA controller), or embedded systems that interact with their environment (e.g. a DSP with an on-chip serial port), or multi-tasking operating system kernels that simulate concurrency by interleaving (such as Linux or dvmOS). Note this page requires the symbol font to be correctly viewed or printed.

Definition

A software design is described using an appropriate formal language or model; concurrent software designs are models of software that permit either multiple actions for each unit of time (true concurrency), or interleaving exactly one action for each unit of time (simulated concurrency). Petri-nets were the first substantial model for concurrent software designs, based on graph theory and as an extension to established finite state machines. They generally permit true concurrency (or multiple actions per unit of time). Process algebras, such as CCS or the p-calculus, are the second substantial model, based on set theory and also as an extension to finite-state machines. They generally permit interleaving (or exactly one action per unit of time), but treat communication as a shared atomic action between agents (or processes). Since graph theory is a specialisation of set theory, these models share a common mathematical basis (in set theory). Finite state machines are represented in the simple form by the graph <S,T,®> where S is the set of vertices representing program states, T is the set of edges representing state transitions, and the transition relation ® Í( S ´ S ) is a set of pairs of states for each state transition t Í T. (The simple form omits start and accepting states.)

Abstraction

Of the two styles it is commonly thought easier for people to envisage and thus to model programs using graph-theoretic languages, like Petri-nets. This is because (syntactically) they look more like our understanding of how computer programs run. But like finite-state machines, Petri-nets suffer certain shortcomings in modelling both time and non-determinism (and finiteness). Process algebras, like CCS, evolved both in response to the short-comings of finite-state machines and with the desire to recognise further useful theories of concurrency (see chapter 1 of Milner's Communicating and Mobile Systems: the Pi-Calculus). The principle theory employed with both the CCS and p-calculus models is (behavioural or observational) equivalence: if two designs can in all cases be observed to exhibit the same behaviour (or engage in the same actions) then they are indistinct (and either may be chosen for implementation).

Design method

Design can be described as a theory-based approach for making model refinements to arrive at a smaller set S' from an initial set S, that is S'ÍS, while preserving equivalence (or some property given by a theory) in a relation R, such that (S,S')ÎR. An interesting area of research is to identify and describe theories for concurrent software designs that look to reduce the solution set. Numerous design criteria, such as PRIMFEATCASE (an exam acronym for Portability, Reliability, Implementability, Maintainability, Fairness, Efficiency, Applicability, Testability, Correctness, Accuracy, Security, Economic) might be theorised. A classic design theory is structure, where program designs are constructed from sequence, selection and iteration (or primes) given as a graph theory.

Measurement

It is with the problem of choosing between (syntactically correct and semantically equivalent) designs that measurement provides one way to distinguish between them. And it is this approach that my postgraduate thesis formal measurement of concurrent software designs (1992, this version is a postgraduation re-write) including Measurement WorkBench software begins to address, analysing the structure of concurrent software designs.

Concurrent Software Design Graph (CSDG)

To satisfy a number of motivating principles, and in particular abstraction (or modelling), design (or theory) and measurement (or analysis), I propose a new model for concurrency, the concurrent software design graph, which includes a study of time. This timed-concurrent graph model aims to benefit from the advantages of graphs for representing executable designs and also to draw upon ideas from process algebras for theories of concurrency. In particular a theory of equivalence up to shared actions is interesting (similar to CCS weak bi-simulation in some sense). By way of example:
let P=a.b.c.P'
let Q=d.e.b.Q'
(such that the agents share action b) is modelled in CSDG as the graph

With small variations in the semantics, CSDG permits both interleaving and true concurrency. In CSDG, time is a constraint within which shared actions can transition. CSDG can be used across the software development life-cycle, from abstract designs (with loose time) through to real-time software systems ready for implementation by a multi-tasking operating system or parallel hardware. A sub-goal for CSDG is to focus on, but not be restricted to, implementation using modern kernel-based systems. To this end CSDG is extended to model interrupts and context switching.

Design theories

A main goal for CSDG is to provide definition and analysis for design criteria. As a first step existing design techniques using simple logic, like fairness, can be described over CSDG and it is shown how existing UML designs can be equated or mapped with CSDG. Timed action refinement presents related theories for the decomposition of actions, to provide detail in a system of agents. As a second step and in order to provide formal definition and analysis for design criteria, research is on-going.

"In theory, there is no difference between theory and practice. In practice, there is." (Yogi Berra)