Module xchan.occ - an occam model of Oyvind's 'XCHAN' (CPA 2012)

This is an asynchronous write for an XCHAN. It never blocks and returns with an indication of whether it was able to perform the write.

Commonly, this is the first thing tried by a writing process: if it fails, then the ALTing pattern on the ready channel may be engaged (PATTERN.A) rather than continued attempts to write using this process.

This is a synchronous write for an XCHAN. It will block until the XCHAN is able to take the message.

This procedure would not normally be used (since a primitive channel or conventional blocking FIFO process would be more efficient). It is included for completeness.

This is a one-place buffered XCHAN process.

Its behaviour is exactly that of an auto-prompter, a common occam idiom.

This is a standard one-place blocking buffer, commonly known as an id-process. It just copies input to output.

This is a standard blocking buffer process with application-defined capacity, implemented as a pipeline of one-place blocking buffers (buffer.one). For this implementation, the capacity must be more than one.

Warning: this process does not compile (because occam-pi runtime sized channel arrays currently have to be built from arrays of mobile channel-ends - see buffer.b). It is presented here for easier understanding of its code (and because occam-pi will eventually compile it).

This is a standard blocking buffer process with application-defined capacity, implemented as a pipeline of one-place blocking buffers (buffer.one). This implementation will compile and run correctly.

This is a standard blocking buffer process with application-defined capacity, implemented as classic ring buffer. However, this needs a request channel that the reader process must signal before reading.

This is a standard blocking buffer process with application-defined capacity, implemented as classic ring buffer. It eliminates the need for a request channel by pipelining buffer.c with an auto-prompter (which is, of course, xchan.one).

This is a one-buffered XCHAN process with application-defined capacity.

It is built from a one-place buffered XCHAN process (xchan.one) pipelined with a standard blocking buffer (buffer.d).

This is a standard one-place blocking buffer, commonly known as an id-process. It just copies input to output.

Standard ring buffer modified to provide an XCHAN ready signal.

This is a service process for the xchan.buffered.b (below). It should not be used directly by systems.

There must be an xchan.one auto-prompter driving the prompt and out channels. There must be a buffer.one.bool id-process forwarding ready signals.

A 'ready' signal is offered if and only if space is available to buffer another item of data. Events 'ready' and 'in' must strictly alternate, starting with 'ready'.

To write to 'in', a 'ready' signal (forwarded by 'id.bool') must first be accepted by the writer. Disregarding this protocol leads to this process STOPping and probable deadlock.

This is a one-buffered XCHAN process with application-defined capacity.

Historical note: this was the original version (just before CPA 2012).

This is a zero-buffered XCHAN (simple behaviour).

It fishes for a reader by offering an extended output (out !!). When a reader is caught, it fishes for a writer by signalling on ready. When it has caught both, the data is transferred. No buffering is introduced by this process in the connection between its writer and reader.

Its weakness is that a reader is sought before there is any indication that a write is pending. This is addressed in xchan.zero.b.

Warning: this process will not compile since extended output is not yet supported by occam-pi. See xchan.zero.a2 for a work-around.

This is a zero-buffered XCHAN (better behaviour).

It fixes the weakness noted in the documentation for xchan.zero.a. However, it requires slightly different logic for an application process that writes to it (xchan.async.write.b, xchan.blocking.write.b and PATTERN.B). Note: these revised processes and pattern may also be used with all other versions of buffered and unbuffered XCHANs (with only a slight overhead cost).

For a writer to this process, the values from its ready channel are significant. This is because this process first fishes for writer by sending a FALSE signal on ready. As normal, when and only when the writer has something to send, it waits for a signal on ready. However, if that signal was FALSE, the writer must keep waiting until it gets a TRUE. All this waiting can, of course, be done whilst processing other events (using ALT). Meanwhile a writer, by accepting the FALSE, lets this process know that it has something to send and this process then fishes for a reader (using extended output, out !!). Once found, the reader is committed and this process now sends TRUE on ready to encourage the writer to write something (which need not, of course, be what it originally had to send). The writer writes, this process forwards, the reader reads and no buffering semantics have been introduced.

The reader from an xchan.zero.b just does a normal read, as before. Disregarding the new writer protocol leads to deadlock. Checking that a writer has followed this protocol can be done by a simple visual check of the code (to ensure a write follows, and only follows, a TRUE on 'ready') or, automatically, by a specialised tool or simple model check.

Warning: this process will not compile since extended output is not yet supported by occam-pi. See xchan.zero.b2 for a work-around.

This is an asynchronous write for a xchan.zero.b (a zero-buffered XCHAN). It never blocks and returns with an indication of whether it was able to perform the write.

A writer could simply keep using this process when it has data to send. There will be at least one FALSE result (maybe many) before a TRUE. It is up to the writer whether to keep sending the same data until success or fresh data. When a write has succeeded, the writer can be assured the reader has taken it (or is about to take it).

Commonly, this is the first thing tried by a writing process: if it fails, then the ALTing PATTERN.B on the ready channel may be engaged (rather than continued attempts to write using this process).

This is a synchronous write for an XCHAN. It will block until the XCHAN is able to take the message.

This procedure would not normally be used (since a primitive channel or conventional blocking FIFO process would be more efficient). It is included here for completeness.

Note: the loop in the code is not needed (see the comments). However, if this process is used for writing to buffered XCHANS or the previous version of an unbuffered XCHAN (xchan.zero.a), the comments do not apply: there will only be one TRUE signal and this coding still works.

This is a zero-buffered XCHAN (simple behaviour).

See xchan.zero.a for documentation. This process works around the current non-implementation of extended output in occam-pi by applying the standard transformation (given in OEP 42).

However, the transformation also requires a reader from this XCHAN to read twice, discarding the first item received (DUMMY.STUFF). See xchan.zero.sync.read and PATTERN.C.

This is a zero-buffered XCHAN (better behaviour).

See xchan.zero.b for documentation. This process works around the current non-implementation of extended output in occam-pi by applying the standard transformation (given in OEP 42).

However, the transformation also requires a reader from this XCHAN to read twice, discarding the first item received (DUMMY.STUFF). See xchan.zero.sync.read and PATTERN.C.

This is a trivial process to perform a blocking read from the current work arounds for zero buffered XCHANs (xchan.zero.a2 or xchan.zero.b2). It reads from the XCHAN twice, discarding the first value and returning the second. It's not really needed and only included for completeness.

This is a XCHAN process with application-defined capacity.

If the capacity is set to zero, the implementation uses the simple behaviour of the logic documented in xchan.zero.a.

If the capacity is zero, reading from this XCHAN must follow the read-discard-read-keep pattern (xchan.zero.sync.read or PATTERN.C). If the capacity is non-zero, an occam primitive read (?) must be used.

For writing, xchan.async.write, xchan.blocking.write or PATTERN.A should be used, regardless of buffering capacity.

This is a XCHAN process with application-defined capacity.

If the capacity is set to zero, the implementation uses the better behaviour of the logic documented in xchan.zero.b.

If the capacity is zero, reading from this XCHAN must follow the read-discard-read-keep pattern (xchan.zero.sync.read or PATTERN.C). If the capacity is non-zero, an occam primitive read (?) must be used.

For writing, xchan.async.write.b, xchan.blocking.write.b or PATTERN.B should be used, regardless of buffering capacity. However, if the capacity is non-zero, xchan.async.write, xchan.blocking.write or PATTERN.A are marginally more efficient.