Functional Programming & Process Algebra

Objects Considered Harmful 

Copyright 2011 Chris  Kohlhepp

  • The next frontier is about managing the complexities emerging from massive parallelism – of thousands of interacting entities cooperating. Doing this effectively in an off-the-cuff manner will be challenging r without a process calculus because parallelism is essentially orthogonal to Object Orientation.

ooharmful

Peter Welch (p.h.welch@kent.ac.uk)

Computing Laboratory, University of Kent at Canterbury

  • Software development to date, emergence of object orientation, etc. has been about managing complexity between components and transformations between domain model and implementation model.

ooharmful2

Peter Welch (p.h.welch@kent.ac.uk)

Computing Laboratory, University of Kent at Canterbury

Communicating Sequential Processes

  • Invented 1978 by Sir Charles Anthony Richard Hoare, Oxford University   (also inventor of Quicksort)
  • Reference: Communicating Sequential Processes. (2004) Prentice Hall International.

Hoare CAR & Jim Davies, Oxford University Computing Laboratory

Available from www.usingcsp.com

  • Communicating Scala Objects, Bernard Sufrin, Oxford University Computing Laboratory

Why ? Wherefore art thou ? What Google’s GO has to say about CSP…

“A way to formally describe concurrent computations in a compositional manner – compositionality being something  that other paradigms for concurrency have problems with !”

go

 

CSP Syntax

cspsyntax

Algebraic system of laws, step, distributive & associative that allow simplification and rewriting in different terms, e.g.  For example, we have :

P || (Q u R) = (P || Q) u (P || R)

(P u Q) || R = (P || R) u (Q || R)

This means we can rewrite parallel constructs in equivalent sequential constructs and vice versa.

CSP A Trivial Example

csptrivial1

csptrivial2

CSP Deadlock Example

cspdeadlock1

cspdeadlock2

CSP Refinement

A process Q is a traces refinement of another, P, if all the possible sequences of communications which Q can do are also possible for P.

csprefinement1

Also, a finer distinction between processes can be made by constraining the events which an implementation is permitted to block as well as those which it performs.

csprefinement2

  • Why is this important ?
  • Because we can use this concept to verify properties of a system !
  • Questions we can answer : is a specific process behaviour a subtype of generic process?

 

The level crossing example:

channel car, train : LOC
channel gate : POS
channel crash
-- ... define safe system
SAFE_SYSTEM = describe conditions that cannot lead to a crash
-- ... proposed spec of software implementation
assert PROPOSED [T= SAFE_SYSTEM
-- ... assert refinement
-- ... generally speaking if our proposed system is a refinement
-- ... both in terms of events which can occur (traces refinement) and
-- ... in terms of events which cannot occur (failures refinement), then
-- ... and only then can we assert that software implementing PROPOSED
-- ... cannot lead to the event 'crash'

In summary, we can use CSP to define the desired behaviour of a system, and subsequently verify compliance of a proposed specification with the desired traits.

Prominent real life example :

Lowe, G. (1996). “Breaking and fixing the Needham-Schroeder public-key protocol using FDR”. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag. pp. 147–166.. http://citeseer.ist.psu.edu/lowe96breaking.html.

One useful application of CSPs algebraic laws is to rewrite parallel solution in sequential terms or vice versa to arrive at desired levels of parallel composition, then use refinement checks to verify that both solutions are logically identical.

Further Reading

In as much as it is concerned with concurrent processes that exchange messages, the Actor model is broadly similar to CSP. However, the two models make some fundamentally different choices with regard to the primitives they provide:

  • CSP processes are anonymous, while actors have identities.
  • CSP message-passing fundamentally involves a rendezvous between the processes involved in sending and receiving the message, i.e. the sender cannot transmit a message until the receiver is ready to accept it. In contrast, message-passing in actor systems is fundamentally asynchronous, i.e. message transmission and reception do not have to happen at same time, and senders may transmit messages before receivers are ready to accept them. These approaches may be considered duals of each other, in the sense that rendezvous-based systems can be used to construct buffered communications that behave as asynchronous messaging systems, while asynchronous systems can be used to construct rendezvous-style communications by using a message/acknowledgement protocol to synchronize senders and receivers.

The Process Analysis Toolkit (PAT) [20][21] is a CSP analysis tool developed in the School of Computing at the National University of Singapore. PAT is able to perform refinement checking, LTL model-checking, and simulation of CSP and Timed CSP processes. The PAT process language extends CSP with support for mutable shared variables, asynchronous message passing, and a variety of fairness and quantitative time related process constructs such as deadline and waituntil.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s