Towards a taxonomy(?) of CSP-based systems

Contents

New: 12Oct2016. Last updated 25Aug2021
This page is in group Technology. This note started with an attempt to look at how channels are modelled (in code, really) but then ended up with trying to systemise what I found. The note was even called Channel structures at the start.

Fold handling with Collapse-O-Matic plugin

I am using Collape-O-Matic (here) on many pages.

Expand All (for searching)
Collapse All

Typical fold

This text 123456789 will only be found with browser search when the fold is expanded

Towards a classification of CSP-based systems?

This might be the final title. See below.

Towards a taxonomy of CSP-based systems?

I wonder if it’s possible, by inspecting these channel tops of the icebergs, to discover an informal taxonomy of CSP-based systems? We would at least start by inspecting only the top, but of course there would be matters uncovered. We might want to inspect also below the obvious.

Already done: Chalmers

Update Aug2017: Kevin Chalmers presented an important paper at CPA 2017 at Malta. What are Communicating Process Architectures? Towards a Framework for Evaluating Message-passing Concurrency Languages by Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK, see [5]. Chalmers evaluates Go, Rust, Erlang, and occam-pi.

Update 20Mar2017: I had forgotten. At CPA 2015 at Kent (I was there), Kevin Chalmers (beside me in the picture) did a workshop entitled Message Passing Concurrency Shootout [4].

Since I started this blog note after it, and the fact that I now do remember it was happening, I must have taken a clue. My initial idea here was to see how much about the rest of the system one might possibly infer from the structure of the channel description. Of course that angle falls. But then, the below is how far I did come (or have come).. (and I have included XC):

Taxonomy

For me this is plain hair-pulling..

Taxonomy means hierarchical classification, and any species would be placed at any one leave of the classification tree(?) Maybe it’s only flat classification I’m after, since I’m certain that I would end up with a table to pick from. Any one classified system would have several traits. But «Flynn’s taxonomy» (see Wiki-refs below) is taxonomy..

I attended a lecture on the taxonomy of computer languages at Simula-67’s 25 years anniversary (in 1992) where Peter Wegner listed up a taxonomy of  object-based language design. It still sits as an aha experience for me. He had in 1987 published a seminal article on this  that I still find quite intriguing [1]. On page 178 I take these excerpts:

sequential process: A process that has just one thread of control.
quasi-concurrent process: A process that has at most one active thread of control.
concurrent process: A process that may have multiple active threads of control.

Sequential processes (Ada and Nil) generally have a body with an interface of entry points at which messages to perform operations may be queued. An invoking operation (incoming message) must wait until the already executing process is ready to accept it by means of a “rendezvous” which joins the incoming and active threads of control for purposes of synchronization and argument communication and then separates the threads so that invoking and invoked processes may again proceed in parallel.

The concurrent languages CSP [HOI], Ada, and Nil [SY] have sequential processes.

Note that all three language classes are fully concurrent. They differ in their restriction on concurrency within processes but are similar in placing no restriction on concurrency between processes.

Sure CSP stands for Communicating Sequential Processes, so Wegner didn’t fight Hoare’s decision on that. However, CSP allows compositional processes, but for occam’s case there’s always implicit fork and join, so sequential would still stand. The base process won’t run on.

I think that when he says that «Note that all three language classes are fully concurrent» he breaks or contradicts the thing that taxonomy is hierarchical classification – but this seems to be ok. So maybe I too may use the taxonomy word?

This chapter could have been named Towards a taxonomy of process-oriented programming, but then, no. There already is a good taxonomy in the process-oriented programming  Wikipedia page. And besides, I want to try it explicitly for CSP-based (not CSP-oriented?) methodologies.

I am not certain whether a classification here would include type of realtime systems, hard, firm or soft. To some extent I guess it would be rather orthogonal. Except for the queuing problem that I will have to treat a lot. This might at least rule out some parts here for safety critical (search for «Ravenscar»).

How to attack the problem

As this note develops I see that observing how I add, remove and move around the chapters will at least help some. I have started to add «Tax:: at some places.

List of taxonomic elements

..the list

Tax:: Extracted from below chapters:

  1. Channels synchronousity (synchronous, buffered asynchronous)
    1. Full (buffered) channel
      1. Blocking (waiting)
      2. Busy-poll?
  2. Channels access rights (point-to-point or multi-parties)
    1. Point-to-point
      1. Arrays of point-to-point
    2. One-many, many-one or many-many
    3. Parallel usage rules and checks
    4. Scoping of channel ends (see one end or all ends)
  3. Channel direction (one direction or sessions that include processing with replies)
  4. Channel movability (static or movable)
  5. Channel over channels
  6. Channel deadlock freeness (like my own XCHAN)
    1. Or patterns like client/server sessions with remote procedure calls
  7. Two-phase synchronisation available
    1. Synch and commit
      1. Like occam-pi !! or ??
  8. «Rejectable» channel
  9. Channel error handling
  10. Channel may be closed
  11. Channel contents
    1. Typed
      1. Tagged (synchronisation points per data segment)
      2. All in one batch (like a single struct)
    2. Untyped
  12. Selective choice (select, alt) fairness control
    1. Prioritised (application decides «fairness»)
    2. Random (run-time decides)
  13. Uncontrolled (bad) nondeterminsim
    1. None as no queueing for selective wait access
    2. Nondeterminstic timing of queues
    3. Safe subset (like Ada Ravenscar profile)
  14. Flora of timers in selective choice
    1. Selective choice’s timeout
    2. Application timers
      1. EGGTIMER
      2. REPTIMER
  15. Selective choice direction set (only inputs or also outputs)
  16. Individual control of guards in selective choice
    1. Boolean conditions (occam)
    2. nul-channel (Go)
    3. None
  17. Multi-core (distributed or shared memory)
    1. Copy semantics (sends by memcpy or the like)
    2. Move semantics (sends by passing pointer around)
      1. Scoping of this pointer when not valid
      2. Avoiding busy-poll?
  18. CSP by
    1. Programming language
    2. Library
      1. Mechanism (thread, generator, future etc.)
  19. System
    1. Naked (no other than «CSP» run-time)
    2. Running on top of OS
      1. Blocking OS system calls
    3. Web-type
      1. Server, client, any side
  20. Process context
    1. In stack
      1. One stack per process
      2. Common stack
    2. In heap
    3. Static
  21. Process scheduling
    1. As communicating sequential processes (cooperative scheduling driven by events or timeouts on channels)
      1. Rescheduling to synchronisation points by auto-generated jump table
      2. Piggy-backing on open source, like Pthreads
      3. Some other way to store/restore program/instruction pointer and process context
    2. Preemptive
  22. Scheduler’s restore of process context
    This is closely related to the above point, but it still would need a separate point

    1. Restoring a context pointer
    2. Move of context
  23. Process composition
    1. Flat only
    2. Composite
      1. Rescheduling a process where it is
      2. Flattening out the process hierarchy
  24. Process type
    1. Built-in
    2. Coroutine
  25. Process creation
    1. PAR-block with built-in start/stop synchronisation
    2. Fork and yield by process creator
  26. Targeting type of system
    1. Hard real-time system
    2. Firm real-time system
    3. Soft real-time system
    4. None
  27. Degree of CSP’ability
    1. Formal semantics
    2. Need to busy-poll in application

Go channel

Go channel some code

type hchan struct {
        qcount   uint           // total data in the queue
        dataqsiz uint           // size of the circular queue
        buf      unsafe.Pointer // points to an array of dataqsiz elements
        elemsize uint16
        closed   uint32
        elemtype *_type // element type
        sendx    uint   // send index
        recvx    uint   // receive index
        recvq    waitq  // list of recv waiters
        sendq    waitq  // list of send waiters

        // lock protects all fields in hchan, as well as several
        // fields in sudogs blocked on this channel.
        //
        // Do not change another G's status while holding this lock
        // (in particular, do not ready a G), as this can deadlock
        // with stack shrinking.
        lock mutex
}

Tax:: Channels may be bidrectional. Both synchronous & fifo buffered. Both channel ends available from a goroutine by any number of goroutines. Code may run on multi-core but mainly up to underlying OS. Channel runtime passes pointers to shared memory around. Run-time spawns a new goroutine if blocking system call lasts too long. Selective choice «fair» but that fairness is not under application code control. Select on inputs and outputs. Boolean conditions on selective choice guards simulated by setting the channel to nil. A nil channel is never ready. A channel may be closed. Channel variables are references, meaning that an opaque pointer to the channel «object» can be passed around in shared memory only. Slogan «Do not communicate by sharing memory; instead, share memory by communicating» (here). No parallel usage checks by compiler (perhaps not possible). Run-time Data Race Detector available: https://golang.org/doc/articles/race_detector.html. Semantics in language specs (https://golang.org/ref/spec) is here: https://golang.org/ref/spec#Channel_types

Python

PyCSP channel

A Python library.

PyCSP channel some code

Channel selfs
    self.channel
    self.ispoisoned
    self.isretired
    self.msg
    self._op
    self.poison
    self.process
    self.readers
    self.readqueue
    self.result
    self.s = Scheduler()
    self.writers
    self.writequeue
class ChannelReq(object):
    def __init__(self, process, msg=None):
    def poison(self):
    def retire(self):
    def offer(self, recipient):
class Channel(object):
    def __new__(cls, *args, **kargs):
    def __init__(self, name=None, buffer=0):
    def check_termination(self):
    def _read(self):
    def _write(self, msg):
    def _post_read(self, req):
    def _remove_read(self, req):
    def _post_write(self, req):
    def _remove_write(self, req):
    def match(self):
    def poison(self):
    def __pos__(self):
    def __neg__(self):
    def __mul__(self, multiplier):
    def __rmul__(self, multiplier):
    def reader(self):
    def writer(self):
    def join_reader(self):
    def join_writer(self):
    def leave_reader(self):
    def leave_writer(self):
    // "For basic class:
    self.__call__

Python Standard Library

Example:

import multiprocessing as mp
mp.Process
mp.Pipe

I don’t know if anybody has built CSP on top of this.

JavaScript

node-csp channels library on Node.js

JavaScript

node-csp channel some code

Chan has put and take. From the github source:

// Channels are object that have two methods, take and put, 
// both of these methods return operations that have type 
// chan and functions that return whether they should continue
// executing or block.

Chan.prototype.put = function (msg)
Chan.prototype.take = function () 

// Channel variables:
this.size
this.buffer
this.drain

// Channel return states:
return { state: "continue" };
return { state: "sleep" };

This is actually all of it. From the API doc:

(yield) spawn(*gen, arg1 ... argN)
new Chan(size = 0)
yield Chan.prototype.put(val)
yield Chan.prototype.take() = val
yield wait(ms)
yield select(chan1 ... chanN) = chan
yield quit()
wrap(fn(arg1 ... argN, cb(err, val)))
// Make a function take a channel instead of a callback:
chanify(fn(arg1 ... argN, cb(err, val)), chan)

 js-csp

JavaScript

The above link states that «This is a very close port of Clojurescript’s core.async. The most significant difference is that the IOC logic is encapsulated using generators (yield) instead of macros. Therefore resources on core.async or Go channels are also helpful.»

js-csp channel some code

// Channel operations
yield put(ch, value)
yield take(ch)
  csp.CLOSED: Returned when taking from a closed channel. 
  Cannot be put on a channel. 
  Equal null for now.
offer(ch, value)
poll(ch)
  csp.NO_VALUE: Returned when using poll on a channel that is either closed 
  or has no values to take right away.
yield alts(operations, options?)
  options.default
  options.priority
  csp.DEFAULT: If an alts returns immediately when no operation is ready, 
  the key channel of the result holds this value instead of a channel.
yield sleep(msecs)
ch.close()

Here’s most of the rest of it:

chan(bufferOrN?, transducer?, exHandler?)
buffers.fixed(n)
buffers.dropping(n)
buffers.sliding(n)
Transducers
timeout(msecs)

var ch = csp.chan();
csp.takeAsync(ch,..)
csp.putAsync(ch,..);

Goroutines: go(f*, args?)
var ch = csp.go(function*(x)

spawn(generator)
var ch = csp.spawn(id(42))

Communicating Generators in JavaScript

Micallef, K. and Vella, K. (2016). Communicating Generators in JavaScript. In Communicating Process Architectures 2016. Also see it mentioned here.

C++

Channels, an alternative to callbacks and futures

A suggestion by John Bandela at CppCom 2016. See Channels – An Alternative to Callbacks and Futures – John Bandela – CppCon 2016.pdf

C++ by Bandela channel some code

CHANNEL
template  structchannel {
  usingnode_t            = detail::node_t;
  node_base  *read_head  = nullptr;
  node_base  *read_tail  = nullptr;
  node_base  *write_head = nullptr;
  node_base  *write_tail = nullptr;
  std::atomic closed{false};
  std::mutexmut;
  usinglock_t = std::unique_lock
}

Development and Evaluation of a Modern C++CSP Library

Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK. CPA 2016. See http://www.wotug.org/cpa2016/programme.shtml#paper12. (Its list has been blended into this note as well. Thanks!)

Java

CTJ – Communication Threads Java

Broenink, J. F., Bakkers, A. W. P., and Hilderink, G. H. (1999).
Communicating Threads for Java.
In Cook, B. M., editor, Proceedings of WoTUG-22: Architectures, Languages and Techniques for
Concurrent Systems, pages 243–262.

JVMCSP

Shrestha, C. and Pedersen, J. B. (2016).
JVMCSP – Approaching Billions of Processes on a Single-Core jvm.
In Communicating Process Architectures 2016.

JCSP – Communicating Sequential Processes for Java

This is «An implementation of CSP concepts (processes, channels, barriers, etc) in Java» (CSProjects).

This library was built by giants. I think they put everything in there that the Java language made possible. A side effect of this is that when data is sent by reference that reference can’t (like in occam-pi) be unscoped by the language. I think that the authors had to accept that in this way its channels weren’t as «safe» as occam channels. But they were still highly useful.

Base class Channel docs

The public class Channel in Channel.java by P.H. Welch seems to be the base class.

  • This class provides static factory methods for constructing all the different types of channel.
  • Channels carry either Objects or integers.
  • Basic channels are zero-buffered: the writer and reader processes must synchronise. Buffered channels can be made with various buffering policies: e.g. fixed size blocking FIFO ({@link org.jcsp.util.Buffer here}), fixed size overwrite-oldest-when-full ({@link org.jcsp.util.OverWriteOldestBuffer here}), fixed size discard-when-full ({@link org.jcsp.util.OverFlowingBuffer here}), infinite sized FIFO ({@link org.jcsp.util.InfiniteBuffer here}).
  • Channels can be made {@link Poisonable} with user-chosen immunity (for the simple and safe shutdown of networks or sub-networks).
  • Channels are either one-one (connecting a single writer process with a single reader), one-any (connecting a single writer process with any number of readers), any-one (connecting any number of writer processes with a single reader) or any-any (connecting any number of writer processes with any number of readers). Do not misuse them (e.g. use a one-one to connect more than one writer process to more than one reader).
  • Channels are used to construct process networks. Channel ends, obtained from a channel via its in() and out() methods, should be plugged into the processes that need them. An input-end is used for reading from the channel; an output-end is used for writing to the channel. A process should not be given a whole channel – only the end that it needs.
  • Channel input-ends of one-one and any-one channels may be used as {@link Guard guards} in a {@link Alternative choice}. Channel input-ends of one-any or any-any channels may not be so used.
  • Channel output-ends of one-one {@link One2OneChannelSymmetric symmetric} channels may also be used as {@link Guard guards} in a {@link Alternative choice}. Channel output-ends of all other kinds of channel may not. Symmetric channels are currently an experiment: buffering and poisoning are not yet supported.
  • For convenience, there are also methods for constructing arrays of channels (and for extracting arrays of channel-ends from arrays of channels).

The JCSPCHANNEL has been formally verified [3]. The work on the Ada Ravenscar channels (later and [2]) also refers to this work.

JCSP channel some code

Here are all the java source files, not only for the Channel classes.
svn – Revision 376: /jcsp/trunk/src/org/jcsp/lang:

AbstractConnectionImpl.java
Alternative.java
AlternativeError.java
AltingBarrier.java
AltingBarrierBase.java
AltingBarrierCoordinate.java
AltingBarrierError.java
AltingChannelAccept.java
AltingChannelInput.java
AltingChannelInputImpl.java
AltingChannelInputInt.java
AltingChannelInputIntImpl.java
AltingChannelInputIntSymmetricImpl.java
AltingChannelInputSymmetricImpl.java
AltingChannelInputWrapper.java
AltingChannelOutput.java
AltingChannelOutputInt.java
AltingChannelOutputIntSymmetricImpl.java
AltingChannelOutputSymmetricImpl.java
AltingConnectionClient.java
AltingConnectionClientImpl.java
AltingConnectionServer.java
AltingConnectionServerImpl.java
Any2AnyCallChannel.java
Any2AnyChannel.java
Any2AnyChannelImpl.java
Any2AnyChannelInt.java
Any2AnyChannelIntImpl.java
Any2AnyConnection.java
Any2AnyConnectionImpl.java
Any2AnyImpl.java
Any2AnyIntImpl.java
Any2OneCallChannel.java
Any2OneChannel.java
Any2OneChannelImpl.java
Any2OneChannelInt.java
Any2OneChannelIntImpl.java
Any2OneConnection.java
Any2OneConnectionImpl.java
Any2OneImpl.java
Any2OneIntImpl.java
Barrier.java
BarrierError.java
BasicOne2OneChannelSymmetric.java
BasicOne2OneChannelSymmetricInt.java
BlackHoleChannel.java
BlackHoleChannelInt.java
Bucket.java
BufferedAny2AnyChannel.java
BufferedAny2AnyChannelIntImpl.java
BufferedAny2OneChannel.java
BufferedAny2OneChannelIntImpl.java
BufferedChannelArrayFactory.java
BufferedChannelFactory.java
BufferedChannelIntArrayFactory.java
BufferedChannelIntFactory.java
BufferedOne2AnyChannel.java
BufferedOne2AnyChannelIntImpl.java
BufferedOne2OneChannel.java
BufferedOne2OneChannelIntImpl.java
CSProcess.java
CSTimer.java
Channel.java
ChannelAccept.java
ChannelArrayFactory.java
ChannelDataRejectedException.java
ChannelFactory.java
ChannelInput.java
ChannelInputImpl.java
ChannelInputInt.java
ChannelInputIntImpl.java
ChannelInputWrapper.java
ChannelInt.java
ChannelIntArrayFactory.java
ChannelIntFactory.java
ChannelInternals.java
ChannelInternalsInt.java
ChannelOutput.java
ChannelOutputImpl.java
ChannelOutputInt.java
ChannelOutputIntImpl.java
ChannelOutputWrapper.java
Connection.java
ConnectionArrayFactory.java
ConnectionClient.java
ConnectionClientMessage.java
ConnectionClientOpenMessage.java
ConnectionFactory.java

ConnectionMessage.java
ConnectionServer.java
ConnectionServerMessage.java
ConnectionWithSharedAltingClient.java
ConnectionWithSharedAltingServer.java
Crew.java
CrewServer.java
Guard.java
InlineAlternative.java
JCSP_InternalError.java
MultiwaySynchronisation.java
Mutex.java
One2AnyCallChannel.java
One2AnyChannel.java
One2AnyChannelImpl.java
One2AnyChannelInt.java
One2AnyChannelIntImpl.java
One2AnyConnection.java
One2AnyConnectionImpl.java
One2AnyImpl.java
One2AnyIntImpl.java
One2OneCallChannel.java
One2OneChannel.java
One2OneChannelImpl.java
One2OneChannelInt.java
One2OneChannelIntImpl.java
One2OneChannelSymmetric.java
One2OneChannelSymmetricInt.java
One2OneConnection.java
One2OneConnectionImpl.java
ParThread.java
Parallel.java
PoisonException.java
Poisonable.java
PoisonableAny2AnyChannelImpl.java
PoisonableAny2AnyChannelIntImpl.java
PoisonableAny2OneChannelImpl.java
PoisonableAny2OneChannelIntImpl.java
PoisonableBufferedAny2AnyChannel.java
PoisonableBufferedAny2AnyChannelInt.java
PoisonableBufferedAny2OneChannel.java
PoisonableBufferedAny2OneChannelInt.java
PoisonableBufferedOne2AnyChannel.java
PoisonableBufferedOne2AnyChannelInt.java
PoisonableBufferedOne2OneChannel.java
PoisonableBufferedOne2OneChannelInt.java
PoisonableOne2AnyChannelImpl.java
PoisonableOne2AnyChannelIntImpl.java
PoisonableOne2OneChannelImpl.java
PoisonableOne2OneChannelIntImpl.java
PriParallel.java
ProcessInterruptedException.java
ProcessManager.java
RejectableAltingChannelInput.java
RejectableAltingChannelInputImpl.java
RejectableBufferedOne2AnyChannel.java
RejectableBufferedOne2OneChannel.java
RejectableChannel.java
RejectableChannelInput.java
RejectableChannelInputImpl.java
RejectableChannelOutput.java
RejectableChannelOutputImpl.java
RejectableOne2AnyChannel.java
RejectableOne2OneChannel.java
Sequence.java
SharedAltingConnectionClient.java
SharedChannelInput.java
SharedChannelInputImpl.java
SharedChannelInputInt.java
SharedChannelInputIntImpl.java
SharedChannelOutput.java
SharedChannelOutputImpl.java
SharedChannelOutputInt.java
SharedChannelOutputIntImpl.java
SharedConnectionClient.java
SharedConnectionServer.java
SharedConnectionServerImpl.java
Skip.java
Spurious.java
SpuriousLog.java
StandardChannelFactory.java
StandardChannelIntFactory.java
StandardConnectionFactory.java
Stop.java
TaggedProtocol.java
doc-files/
package.html

Tax:: JCSP channels are about as many-flavoured as possible. But they are always uni-directional and may be buffered. Full channel recovery included.

(Aside: I may have had a hand with the fact that this library was conceived as early as 1996. See http://oyvteig.blogspot.com/2010/12/021-problems-with-threads.html, search for JCSP)

occam without HW

1983 Proto occam 1988 occam 2 TM INMOS Limited

I think only SPoC in this group is interesting in the context of this blog note. Not CCSP, KRoC or Tranterpreter, which I think are too close to the transputer (byte code).

SPoC – Southampton Portable occam Compiler

Southampton Portable occam Compiler. Dowload from http://www.wotug.org/parallel/occam/compilers/spoc/ or http://folk.ntnu.no/sverrehe/occam/download.html

SPoC channel some code

From file occam2c.h. This, with occam2c.c are used by the C code generated from occam sources:

typedef const void * (*tFuncPtr)();

typedef struct Task tTask;
#define NoTask (tTask *)0

typedef struct { tTask *Task; void *Data; } CHAN;

typedef enum
{
  HighPriority=0,
  LowPriority=1
} tTaskPri;

typedef enum
{
  OUT_p=1,
  IN_p=2,
  EXEC_p=3,
  WAIT_p=4,
  ALTING_p=5,
  TALTING_p=6,
  TWAIT_p=7,
  TSOCK_p=8
} tTaskMode;
typedef enum
{
  NotAlting_p = -1,
  Enabling_p  = -2,
  Waiting_p   = -3,
  Ready_p     = -4,
  TReady_p    = -5
} tAltMode;

typedef enum
{
  TimeNotSet_p = -2,
  TimeSet_p = -3
} tTimerMode;

struct Task
{
  tTask *Next;      /* Linked List of Active Tasks */
  tTask *Parent;    /* Parent Task */

  tFuncPtr Func;    /* Current Function being executed by this task */
  void *FP;         /* Frame Pointer for this task */

  tTaskMode state;
  int Children;     /* Active Children Count */

  char *name;       /* Task Name */

  union
  {
    struct
    {
      long len;         /* Comms */
      void *data;       /* Comms */
      char buff[4];     /* Comms */
    } io;
    struct
    {
      tTimerMode TimerMode;  /* Timer Alternation */
      tTimer time;
    } timer;
  } comms;

  tAltMode AltMode;      /* Alternation */
  int TaskId;       /* Number identifying task, for debugging */
  int TaskPriority;
};

extern tTask *QFP[NUM_PRIORITY_LEVELS],*QBP[NUM_PRIORITY_LEVELS],*QTM,*CURTASK;
extern tTimer TIMER;

#define INPUT(c,m,s,l) {FP->_Header.IP = l;  if (ChanIn  (c,m,s)) return;}
#define INPUT1(c,m,l){FP->_Header.IP = l;  if (ChanIn1 (c,m)) return;}
#define INPUT2(c,m,l){FP->_Header.IP = l;  if (ChanIn2 (c,m)) return;}
#define INPUT4(c,m,l){FP->_Header.IP = l;  if (ChanIn4 (c,m)) return;}
#define INPUT8(c,m,l)INPUT(c,m,8,l)

#define OUTPUT(c,m,s,l){FP->_Header.IP = l;  if (ChanOut (c,m,s)) return;}
#define OUTPUT1(c,m,l){FP->_Header.IP = l;  if (ChanOut1(c,m)) return;}
#define OUTPUT2(c,m,l){FP->_Header.IP = l;  if (ChanOut2(c,m)) return;}
#define OUTPUT4(c,m,l){FP->_Header.IP = l;  if (ChanOut4(c,m)) return;}
#define OUTPUT8(c,m,l)OUTPUT(c,m,8,l)

#define ALT()       { AltStart(); }
#define ENBC(f,c)   { if (f) EnableChannel(c); }
#define ENBS(f)     { if (f) EnableSkip(); }
#define ENBT(f,t)   { if (f) EnableTimer(t); }
#define ALTWT(l)    { FP->_Header.IP = l; if (AltWait()) return; }
#define DISC(l,f,c) ( (f) ? DisableChannel(l,c) : (false) )
#define DISS(l,f)   ( (f) ? DisableSkip(l)      : (false) )
#define DIST(l,f,t) ( (f) ? DisableTimer(l,t)   : (false) )
#define ALTEND()    { FP->_Header.IP = AltFinish(); break; }
#define DELAY(t,l)  { FP->_Header.IP = l; WaitOnTimer(t); return; }

#define ENDP(){End_Process(); return; }
#define WAITP(l){FP->_Header.IP = l; DeSchedule(WAIT_p); return; }
#define INITCH(c){(c)->Task = NoTask; (c)->Data = NULL; }

CCSP – transputer byte code for other machines

The occam community didn’t have the resources to build a portable occam compiler, so there became a heavy reliance on the old occam compiler that produced byte code for the transputer. Personally I used this for many years – but we had transputers. That compiler was more or less «magic», and only the «high priests» were able to modify in it – like for adding movable semantics of channels. So, to try to port occam to other architectures it was somewhat extended transputer byte code that was the starting point. When it should have been put away since the transputer was already dead. Money could have changed the fate of all this. Disclaimer: this is how I read the situation at the conferences I attended those years. I may be wrong.

  • CCSP – a Portable CSP-based Run-time System Supporting C and occam, by J.Moores. In B.M.Cook, editor, Architectures, Languages and Techniques for Concurrent Systems, volume 57 of Concurrent Systems Engineering series, pages 147–168, Amsterdam, the Netherlands, April 1999. WoTUG, IOS Press.
  • CCSP – A Portable CSP-Based Run-Time System supporting C and occam, by, J.Moores, in WoTUG-22 Keele University, UK, Easter 1999. Architectures, Languages and Techniques for concurrent systems, p.19-36. Edited by B.M.Cook. ISBN 90 5199 480 X, 4 274 90285 4 C3000, ISSN 1383-7575.
  • The code is at https://github.com/concurrency/kroc/tree/master/runtime/ccsp
    • I think this is an extremely elegant solution, but also extremely complex

Here’s the WoTUG-22 Abstract (http://www.wotug.org/wotug22/p5ab.shtml):

Abstract. CCSP is a highly portable run-time system that conforms to the ideas of CSP and supports both the C and occam programming languages. Its aim is to further the use of the CSP mind-set in both industrial and academic applications. The run-time system implements a useful and efficient subset of the basic CSP constructs. It allows occam-style designs to be programmed in C, thereby allowing full use of the optimisation phases of standard C compilers. It supports the KRoC occam system for Linux/PC platforms. In addition, a number of features have emerged from industrial collaboration as essential for soft real-time systems in the real world. These include: prioritised scheduling with 32 priority levels, integration of communications hardware to provide support for distributed processing, and access to a highly accurate real-time clock. This paper discusses the high level structure and functionality of the features provided.

This should be verey interesting for the blog note.

KRoC – Kent Retargetable occam Compiler

This is the «Kent occam-pi system» (CSProjects). This probably is the closest to a reference platform for rather «pure» occam. It has occam-pi (occam-π) on top. It generates transputer byte code and need CCSP to run on Intel X86. See [4 transterpreter].

See https://www.cs.kent.ac.uk/projects/ofa/kroc/

I guess that it is not so interesting in the context of this blog note.

occam – Transterpreter for other machines

  1. http://www.transterpreter.org
  2. https://en.wikipedia.org/wiki/Transterpreter
  3. http://projects.cs.kent.ac.uk/projects/transterpreter/trac/
  4. http://www.transterpreter.org/publications/pdfs/the-transterpreter-a-transputer-interpreter.pdf (contains chapter «Limitations of SPoC and KRoC»)

«An open-source and highly portable virtual machine designed to exploit concurrency on embedded systems, for running process-oriented programs written in the occam-pi programming language.» (From top ref)

It seems rather abandoned now, but of course it’s still interesting. However, since it’s a virtual machine for occam-pi it’s the transputer channel instructions that would be of interest. How they are translated to Intel 86-format isn’t in scope here.

I guess that it is not so interesting in the context of this blog note.

C

ProXC concurrency library

This is a student paper by Edvard Severin Pettersen at NTNU (Norwegian University of Science and Technology), Trondheim, in December 2016. It’s entitled «ProXC – A CSP-Inspired Concurrency Library for the C Programming Language».

See http://www.teigfam.net/oyvind/work/studentprosjekt.html – where you may also download and read the paper.

The code is at Github: https://github.com/edvardsp/libproxc/releases/tag/v1.0 named libproxc pre-diploma with the comment that «This is the first feature-complete version of libproxc, which was the result of my project thesis in autumn 2016.»

ProXC concurrency library some code

// From chan.h
struct ChanEnd {
    enum {
        CHAN_WRITER,
        CHAN_READER,
        CHAN_ALTER,
    } type;

    void  *data;

    struct Chan  *chan;

    struct Proc   *proc;
    struct Guard  *guard;

    TAILQ_ENTRY(ChanEnd)  node;
};

struct Chan {
    uint64_t  id;

    size_t  data_size;

    struct ChanEndQ  endQ;
    struct ChanEndQ  altQ;
};

Embedded (C)

On top of asynch FSM runtime

Private. See my From message queue to ready queue

Top of asynch FSM runtime channel some code

typedef struct
{
    FsmProcessIds_a       sender;         // Optional for runtime verification
    FsmProcessIds_a       receiver;       // Optional for runtime verification
    FsmProcessIds_a       first;          // MB_ID type of first arriver 
                                          // (to be rescheduled by second arriver)
    size_t                dataLenB;       // Number of bytes to be copied
    void                 *dataPtr;        // Data to be copied
    SystemMessageNames_a  alt_in_S_EVENT; // For ALTing
    StateALT_a           *StateALTPtr;    // For ALTing
    size_t               *CntArrTxLenPtr; // If not NULL, then dataLen of TX is placed
                                          // in &CntArrTxLenPtr after memcpy
} Chan_a;

Naked (ChanSched)

Private. See our New ALT for Application Timers and Synchronisation Point Scheduling. And the reason for it: A scheduler is not as transparent as I thought.

Naked channel some code

typedef struct Tag_Chan_a
{
    bool_a                        ChanFirst;
    My_ProcessIds_a               ChanFirst_ProcessId; // uint_t
    ChanAltSetChannelIds_XBits_a *ChanAltSetChannelIds_XBits_Ptr; // Some boolean array
    ChanType_a                    ChanType; // One of these:
    union
    {                                          // CHAN_SIGNAL_A: no such struct needed
        struct { Chan_Synch_a* Ptr; } s_Synch; // CHAN_SYNCH_A.
                                               // Contains DataPtr and DataSize
        struct { Chan_Timer_a* Ptr; } s_Timer; // CHAN_ALTTIMER_A, CHAN_EGGREPTIMER_A.
                                               // Contains some state, future timeout 
                                               // and repeat time
    } u_Type;
    bool_a IsVarLen; // Only used for tighter check of memcpy
} Chan_a;

We introduced application timer in the ALT: EGGTIMER, REPTIMER.

Language with HW

occam on transputer

Inmos. The transuter is an «occam machine». Occam’s concurrency part implements a subset of CSP. See Transputer instruction set. A compiler writer’s guide. Inmos 1988. ISBN 0-13-929100-8. Scanned by transputer.net by Michael Bruestle, see http://www.transputer.net/iset/pdf/tis-acwg.pdf (I have made a 122 MB searchable version that’s here. Bruestle has on 19Oct2016 allowed me to keep it here; he may of course upload it to transputer.net. However, the bookmarks of the index of the original file are gone!)

occam on transputer channel some code

Of course this doesn’t make any more sense than perhaps triggering your curiousness:

6.8.1 Initialising channels (page 44)

CHAN OF PROTOCOL    c:       mint; stlc

[n]CHAN OF PROTOCOL c:       ldc 0; stl i; ldc n; stl i+1;
                          L: mint; ldl c; ldl i;
                             wsub; stnl 0;
                             ldlp i; ldc (END-L); lend;
                        END:

I never did assembler on transputer, except for some inline asm. But it’s fun just to get the feeling. The transputer.net site has a separate Transputer instruction set page at http://www.transputer.net/iset/iset.asp

Tax:: Occam channels are always non-buffered synchronised unidirectional point-to-point. A server may listen to an array of these channels in the ALT or PRI ALT construct.

XC on XMOS processor

None of the material seem to mention CSP. My guess is that they are somewhat burnt by the Inmos / Transputer experience and don’t want to be framed by it. Fair enough; also because they have gone quite a way since then. And XMOS isn’t the new Inmos; the XCORE isn’t a new transputer. The transputer was in some respects many years ahead of its time. In my opinion the XCORE also shines in that respect; but also in a tradition. (Standard disclaimer about no money, no ads, no gifts etc.). Personally I do XC programming (for Tiobe) at home in my aquarium project. I have a XMOS page here.

The newest document is [4]:

  1. The XMOS XS1 Architecture by David May, XMOS 2009, see http://www.xmos.com/download/private/The-XMOS-XS1-Architecture(1.0).pdf
  2. XC Reference Manual by Douglas WATT Richard OSBORNE David MAY, see http://www.xmos.com/published/xc-reference-manual
  3. XC Specification, see https://www.xmos.com/support/tools/libraries?subcategory=&component=14805
  4. XMOS Programming Guide, see https://www.xmos.com/published/xmos-programming-guide

From [4]:

The xCORE architecture delivers, in hardware, many of the elements that you would normally see in a real-time operating system (RTOS). This includes the task scheduler, timers, and channel communication as well as providing separate logical processor cores for the real-time tasks.

xC provides three methods of inter-task communication: interfaces, channels and streaming channels.
Channels provide a the simplest method of communication between tasks; they allow synchronous passing of untyped data between tasks. Streaming channels allow asynchronous communication between tasks; they exploit any buffering in the communication fabric (SIC) of the hardware to provide a simple short-length FIFO between tasks. The amount of buffering is hardware dependent but is typically one or two words of data. Channels (both streaming and normal) are the lowest level of abstraction to the communication hardware available in xC and can be used to implement quite efficient inter-core communication but have no type-checking and cannot be used between tasks on the same core.
Interfaces provide a method to perform typed transactions between tasks. This allows the program to have multiple transaction functions (like remote function calls) between the tasks. Interfaces do allow communication between tasks running on the same logical core. In addition, interfaces also allow notifications to asynchronously signal between tasks during otherwise synchronous communications.

I have programmed quite a lot with this (see here) and I enjoy every hour. Having channels only between cores and interfaces only on cores feels like no mismatch at all, even when coming from the channel-everywhere world that started with occam. It feels like a correct next step. And after all, they are both joined in the select statement. This example is also from [4], showing only channel:

XC channel some code

chan c;
par { 
    task1(c);
    task2(c);
}

void task1(chanend c) {
    c <: 5; 
}

void task2(chanend c) {
    select {
    case c :> int i:
        printintln(i); 
        break;
    } 
}

Tax:: XC channels are always non-buffered synchronised unidirectional point-to-point. A server may listen to an array of these channels in the select statement. Interfaces have the same property: they are point-to-point, but a select handles an array of them.

Ada

Ada with rendezvous

Ada has a concurrency concept based on CSP, but it also has protected objects. For the CSP part, instead of channels it uses rendezvous. After all, in CSPm (below), a synchronised, zero-buffered channel is just «syntactic sugar» for shared state.

Ada has entry calls for the active part (I don’t know if active is the correct term here, maybe client is better?). The other part (server, then?) in a loop uses select, when and accept. This is great.

However, the Ada Ravenscar profile solves the implementation issue that this language mechanism has been done with nondeterministic queue handling (as is Go). I have described some about this Channels and rendezvous vs. safety-critical systems (Note 035), where some interesting comments are attached. So, the select mechanism and the rendezvous are based on queuing – not good for some safety critical systems. The solution is to disallow rendezvous and use protected objects instead. If I had based my life on safety critical systems in Ada then I’d been in shock if I really weren’t able to talk an assessor out of it. However, this probably is an important classification when working with some taxonomy.

Tax:: Rendezvous with entry-calls. Ravenscar profile for safety-critical, hard real-time systems (no queues with more than one entry, schedulability)

Ada with CSP «Ravenscar channels»

However, the Ravenscar profile has been extended with CSP channels. See [2]. This is extremely interesting and I will study it more. This was shown to me in Comment #2 by Peter Morris in Note 035 referenced above. They also formally model their channel, and link that to Martin & Welch’s (Welsh (SIC)) formal verification of the JCSP channel (where JCSPCHANNEL, mentioned above and SimpleRavenChannel are equal), see [3].

They are showing the code of protected object Data and Sync in the code, but the Channel code isn’t there. However, the formal model of channel is.

Related languages

Erlang

I have not placed Erlang in top heading level here because, even if they seem to say it’s based on CSP, it’s probably rather lightheartedly, since basic communication is asynchronous. That already breaks the very basics of CSP. But the community seems to embrace CSP, so I guess it’s me who needs to read myself up on this. As a first, I’ll listen to José Valim describing Elixir and the underlying Erlang VM at Trondheim developer Conference 2016 (TDC2016). To me the paradigm reminds me more of SDL (Specification and Description Language, I have a blog about it). And Scala (below)

From Wikipedia (30Oct2016) I quote (emphasised by me):

Erlang’s main strength is support for concurrency. It has a small but powerful set of primitives to create processes and communicate among them. Erlang is conceptually similar to the occam programming language, though it recasts the ideas of communicating sequential processes (CSP) in a functional framework and uses asynchronous message passing.
…
Though all concurrency is explicit in Erlang, processes communicate using message passing instead of shared variables, which removes the need for explicit locks (a locking scheme is still used internally by the VM)
..
Inter-process communication works via a shared-nothing asynchronous message passing system: every process has a «mailbox», a queue of messages that have been sent by other processes and not yet consumed. A process uses the receive primitive to retrieve messages that match desired patterns. A message-handling routine tests messages in turn against each pattern, until one of them matches. When the message is consumed and removed from the mailbox the process resumes execution. A message may comprise any Erlang structure, including primitives (integers, floats, characters, atoms), tuples, lists, and functions.
…
Ports are used to communicate with the external world. Ports are created with the built-in function open_port. Messages can be sent to and received from ports, but these messages must obey the so-called «port protocol.»

Update 5Feb2020: «I år skal Kodemaker prøve Elixir og Erlang» (translated: «This year, Kodemaker will try Elixir and Erlang«) at Kode24 by editor Ole Petter Baugerød Stokke. Three paragraphs, starting with «Elixir er et språk flere i Kodemaker har hatt lyst til å ta i bruk en stund nå. » (Norwegian) spells out like this (Google translate improved):

Elixir is a language many people in Kodemaker have wanted to use for a while now. The language is very suitable if you want to write code with a high degree of asynchronousity and concurrency. It runs on the Erlang VM – a platform designed for distributed systems with fast response time and good error handling.

We have worked with actor frameworks like Akka on JVM in the past – which is inspired by Erlang, but it is extra fun to work with the «original».

We believe the reason why Elixir and Erlang are not used anymore is due to lack of experience in the Norwegian market. We intend to do this, so stay tuned for our reports

I also add the «Synchronous message passing in Erlang» article in case any of the Kode24 readers reads this. Since one has to built synchronousity on top of async, not the other way around (the first which some would state, is «better»).

Elixir #phoenix

Update 7Jan2021: This pas published on Slack, Elixir-lang (here) on 6Jan2021, but it was suggested that I take it to Elixir forum instead. I might do that. But I now have in internal conversation with a guy at Slack, he will probably resolve this for me. Here is the question:

Hi, this is my first encounter here. I joined because I have a theoretical question that I did not resolve by reading [e01]. I am not planning to code or use this, but I plan to use the info for comparison. I work with the embedded concurrent language XC on XCore by XMOS (and blog about it (disclaimer: no income, gifts, ads there, just fun and expenses)). In XC we can define interfaces that the compiler would know about. Roles have to be defined: client and server. The client always initiates a session (with params). The server listens for it in a select. The server handles it and does processing. When it’s done it sends a message back to the client that it’s ready. This has to be parameterless. The client then has to ask for the result. A server can this way handle multiple clients, and the architecture ensures that this is deadlock free.

I read in a student paper about the phoenix system. Then in a blog note [e02] where I got the impression that in phoenix servers may initiate a comm with a client any time. The XC scheme prohibits this, to avoid deadlocks. Is it true that in phoenix both clients and servers may initiate a session? In case, what’s under the hood to make it happen? I did design a scheme once, that I called XCHAN (there is a paper about it, ref from my blog: [e05]), where both sides could start a session without getting any deadlock, but it did require some state below the channel motor that drives most of this. It also had a clear role assignment. (Also in XC most of this stuff is handled by channels, where so called chanends are HW resources. (Since the scheduler on that multi-core architecture is also in HW)).

TODO: Added: The Promela channel some code shows an example where two parties are equal with respect to both being servers and both being clients (is this role model then correct to use?) and they won’t deadlock. It’s because Promela (along with Go and others) has selective choice also including outputs.

TODO: Links to investigate:

  1. Phoenix.Channel behaviour
  2. Elixir And Phoenix So Far, Channels by Chedy Missaoui (2017)
  3. BUILDING A REAL-TIME APP WITH PHOENIX by Sophie DeBenedetto (channels, long polling)
  4. My Case for Erlang: Connecting Human, Reality and Computer by Kevin E
  5. XCHANs: Notes on a New Channel Type (2012)

Scala

Intended to be run as Java bytecode by JVM (Java Virtual Machine).

This language (with Erlang) is also under «Related languages». Even if it’s interesting I probably should not handle it in this context. There is no channel and the communication is asynchronous. However, concurrent actors do communicate.

From Wikipedia (30Oct2016) I quote (emphasised by me):

For example, Erlang’s special syntax for sending a message to an actor, i.e. actor ! message can be (and is) implemented in a Scala library without needing language extensions.
…
Scala standard library includes support for the actor model, in addition to the standard Java concurrency APIs. Lightbend Inc., provides a platform that includes Akka, a separate open source framework that provides actor-based concurrency. Akka actors may be distributed or combined with software transactional memory (transactors). Alternative communicating sequential processes (CSP) implementations for channel-based message passing are Communicating Scala Objects, or simply via JCSP.
…
An Actor is like a thread instance with a mailbox.
…
Scala also comes with built-in support for data-parallel programming in the form of Parallel Collections integrated into its Standard Library since version 2.9.0.
…
Besides actor support and data-parallelism, Scala also supports asynchronous programming with Futures and Promises, software transactional memory, and event streams.

Futures and promises, although interesting: not here. (But I have quoted a case with them in this blog note (above)).

C#

CoCoL: Concurrent Communications Library

Skovhede, K. and Vinter, B. (2015).
CoCoL: Concurrent Communications Library.
In Communicating Process Architectures 2015

Other

PLAS Wiki

This is a data base from the University of Kent at Canterbury (UK) loaded with important ideas. PLAS stands for Programming Languages and Systems Research Group Wiki. It was last updated in 2013. It is extremely important that UofKent keeps this Wiki up and running the next 20 years (but the Internet Archive’s Wayback Engine has (parts of?) it, like here).

CSProjects

I discovered this when I looked at the JCSP files. There seems to be a lot of CSP-based projects there. I have listened to lots  of lectures on them at CPA conferences over the years.

CHP (Haskell)

Brown, N. C. (2008).
Communicating Haskell Processes: Composable Explicit Concurrency Using Monads.
In Welch, P. H., Stepney, S., Polack, F., Barnes, F. R. M., McEwan, A. A., Stiles, G. S., Broenink, J. F.,
and Sampson, A. T., editors, Communicating Process Architectures 2008, pages 67–83.

Communicating Scala Objects

Sufrin, B. (2008). Communicating Scala Objects. In Welch, P. H., Stepney, S., Polack, F., Barnes, F. R. M., McEwan, A. A., Stiles, G. S., Broenink, J. F., and Sampson, A. T., editors, Communicating Process Architectures 2008, pages 35–54.

Kotlin

Aug2018: I was made aware of Kotlin by reading PROGRAMMING LANGUAGES MAY FINALLY BE REACHING A STATUS QUO in WIRED. It pointed to  The RedMonk Programming Language Rankings: June 2018 where they made quite some fuzz about Kotlin. So I went to Kotlin (programming language). On none of this I could find a single word about concurrency! A new language from 2011, endorsed by Google in 2017 and it doesn’t have any built-in view on concurrency!

However, it outputs Java virtual machine (JVM) bytecode and JavaScript source code. For both JavaScript (that has no concurrency of its own, see here) and Kotlin, JVM helps a lot. It is possible to build concurrency on top of JVM, done by many of the other Java libraries mentioned here.

The Wikipedia article points to an article by the people behind Kotlin, JetBrains: [6]. (I make a [ref] of this and not the others to make it visible in the References list). Here is a quote:

Coroutines

Coroutines in Kotlin make non-blocking asynchronous code as straightforward as plain synchronous code.

Asynchronous programming is taking over the world, and the only thing that is holding us back is that non-blocking code adds considerable complexity to our systems. Kotlin now offers means to tame this complexity by making coroutines first-class citizens in the language through the single primitive: suspending functions. Such a function (or lambda) represents a computation that can be suspended (without blocking any threads) and resumed later.

Technically, coroutines are light-weight means of cooperative multi-tasking (very similar to fibers). In other words, they are just much better threads: almost free to start and keep around, extremely cheap to suspend (suspension is for coroutines what blocking is for threads), very easy to compose and customize.

We designed coroutines for maximum flexibility: very little is fixed in the language, and very much can be done as a library. The kotlinx.coroutines project features libraries on top of Rx, CompletableFuture, NIO, JavaFx and Swing. Similar libraries can be written for Android and JavaScript. Even many built-in constructs available in other languages can now be expressed as Kotlin libraries. This includes generators/yield from Python, channels/select from Go and async/await from C#: (code dropped here)

These people relate to «blocking» as dangerous, and like «suspension» better: «suspension is for coroutines what blocking is for threads«. I have discussed the use of words and the semantics of «blocking» here.

Then, on GitHub I found this about Coroutines for Kotlin (Revision 3.2) that’s quite versatile, and with a chapter on Channels (here). «Go-style type-safe channels can be implemented in Kotlin as a library. …  It allows us to copy Go-style code into Kotlin almost verbatim. The fibonacci function that sends n fibonacci numbers in to a channel from the 4th concurrency example of a tour of Go would look like this in Kotlin:»

suspend fun fibonacci(n: <Int>, c: SendChannel<Int>) {
    var x = 0
    var y = 1
    for (i in 0..n - 1) {
        c.send(x)
        val next = x + y
        x = y
        y = next
    }
    c.close()
}

«The suspend modifier indicates that this is a function that can suspend execution of a coroutine.»

The also show an example of a select: «Go-style select control block that suspends until one of the actions becomes available on one of the channels can be implemented as a Kotlin DSL, so that the 5th concurrency example of a tour of Go would look like this in Kotlin.» Of course I like what I see:

suspend fun fibonacci(c: SendChannel<Int>, quit: ReceiveChannel<Int>) {
    var x = 0
    var y = 1
    whileSelect {
        c.onSend(x) {
            val next = x + y
            x = y
            y = next
            true // continue while loop
        }
        quit.onReceive {
            println("quit")
            false // break while loop
        }
    }
}

I see a modern language where this is even discussed! I saw it discussed many years ago with CSP and Modula-2, then concurrency was everyone’s own library. Now it’s discussed by the language designers!

Modeling tools

Modeling and formal verification tools.

channel in CSPm

The CSPm tool is very much alive. I saw it presented by Formal Systems in the nineties. Now it may be downloaded and used for research for free. I have used it myself and like it quite a lot, even if the learning curve is quite steep.

It does refinement checking. I start with a a model of the specification with quite many «don’t cares», and then model the implementation with no «don’t cares». From https://www.cs.ox.ac.uk/projects/fdr/manual/cspm/definitions.html#channels

CSPM channels are used to create events and are declared in a very similar way to datatypes. For example:

channel done
channel x, y : {0..1}.Bool

declares three channels, one that takes no parameters (and hence done is of type Event), and two that have two components: a value from {0.1} and a boolean. Thus, the set of events defined by the above is {done, x.0.false, x.1.false, x.0.true, x.1.true, y.0.false, y.1.false, y.0.true, y.1.true}. These events can then by used by Prefix to declare processes such as P = x?a?b -> STOP.

In general, channels are declared using the following syntax:

channel n1, ..., nM : te

where te is a Type Expressions and the ni are unqualified names. As a result of this, n1, nM are bound to event constructors that when dotted with appropriate values (according to te), yield an event«. In particular, if te is of type {t1.(…).tN}, then each ni is of type t1 => … => tN => Event.

chan in Promela

This tool is still alive, after all these years. I have also used this, and as CSPm also like it quite a lot. But it’s basically a Process Modeling Language (hence the name) and not refinement. (Even if Wikipedia states that it may).

From Wikipedia: » In PROMELA models, communication via message channels can be defined to be synchronous (i.e., rendezvous), or asynchronous (i.e., buffered).». This example (from Wikipedia) is very interesting. It has two processes with selective choice between both inputs and outputs, and it won’t deadlock. ? is input and ! is output on channels (as in occam):

Promela channel some code

mtype = {M_UP, M_DW};
chan Chan_data_down = [0] of {mtype};
chan Chan_data_up   = [0] of {mtype};
proctype P1 (chan Chan_data_in, Chan_data_out)
{
    do
    ::  Chan_data_in ? M_UP -> skip;
    ::  Chan_data_out ! M_DW -> skip;
    od;
};
proctype P2 (chan Chan_data_in, Chan_data_out)
{
    do
    ::  Chan_data_in ?  M_DW -> skip;
    ::  Chan_data_out !  M_UP -> skip;
    od;
};
init
{
    atomic
    {
        run P1 (Chan_data_up,   Chan_data_down);
        run P2 (Chan_data_down, Chan_data_up);
    }
}

When I used it I saw that I don’t get rid of deadlock by buffering. Of course I don’t, but it feels good to have it mentioned. Buffering is something else.

I would have been able to do the same thing with tho XCHANs, one in each direction (see XCHANs: Notes on a New Channel Type (2012))

channel in PAT

PAT = Process Analysis Toolkit.

See http://pat.comp.nus.edu.sg/ and https://en.wikipedia.org/wiki/PAT_(model_checker)

This seems, unlike the two tools above, to not have been updated for some years. More later.

CSP-Prover

Is «an interactive theorem prover on the process algebra CSP based on the theorem prover Isabelle». It’s been last updated in May 2016 (CSP-Prover-5-1-2016). It’s been developed by Information Technology Research Institute, National Institute of Advanced Industrial Science and Technology (AIST) in Japan and Department of Computer Science College of Science Swansea University in the UK. It looks like the two persons Yoshinao Isobel and Markus Roggenbach are central people. The download consists of .thy files. The systems seems to run on all platforms (Windows, Linux, Mac).

About Isabelle: «Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide».

Their html pages run well on IE, but not Chrome, since it’s still using frames (Windows 8, Feb2017):

See https://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html and https://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html

CSP: arriving at the CHANnel island(?)

I hope this is getting less and less true! It’s an old paper by me:

References

Wiki-refs: CSP (Communicating Sequential Processes), Flynn’s taxonomy, Process-Oriented programming, Process-oriented programming

  1. Dimensions of Object-Based Language Design by Peter Wegner, see http://www.cse.msu.edu/~stire/cse891/wegner.pdf. (The Simula-67 anniversary is described here)
  2. Extending Ravenscar with CSP Channels by Diyaa-Addein Atiya and Steve King, Department of Computer Science, University of York in T. Vardanega and A. Wellings (Eds.): Ada-Europe 2005, LNCS 3555, pp. 79–90, 2005. (c) Springer-Verlag Berlin Heidelberg 2005, read at https://www-users.cs.york.ac.uk/~king/papers/ExtendingRavenscar-AdaEur05.pdf
  3. A CSP Model for Java Multithreading by P. H. Welch and J. M. R. Martin. In P. Nixon and I. Ritchie, editors, Software Engineering for Parallel and Distributed Systems, pages 114–122. ICSE 2000, IEEE Computer Society Press, June 2000.
  4. Message Passing Concurrency Shootout by Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK, see http://wotug.org/cpa2015/programme.shtml#paper52
  5. What are Communicating Process Architectures? Towards a Framework for Evaluating Message-passing Concurrency Languages by Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK. Presented at CPA 2017, Aug2017. See http://wotug.org/cpa2017/programme.shtml#paper14
  6. Kotlin 1.1 Released with JavaScript Support, Coroutines and more, Kotlin Blog posted on March 1, 2017 by Roman Belov. See https://blog.jetbrains.com/kotlin/2017/03/kotlin-1-1/