Add support for ordered transmission

[jeltsch]

Currently, the Thorn_Calculus session supports asynchronous and synchronous communication. What is currently lacking is support for a form of communication that has the following properties:

• Sending a value and receiving it do not have to happen at the same time, like with asynchronous communication.
• Values are received in the order they are sent, like with synchronous communication.

We shall add support for such a form of communication, which we call ordered transmission.

The typical way to implement ordered transmission is via FIFO channels. A FIFO channel contains at any given time a sequence of values. Sending to the channel adds a value to the beginning of the sequence, and receiving from the channel reads the value at the end of the sequence and removes it from the sequence.

Despite the ubiquity of the FIFO channel approach, we shall implement a form of ordered transmission that is distinguished from that approach by having processes maintain sending and receiving positions explicitly in the form of pure values, which we call cursors. The communication operations are intended to work as follows:

• Sending adds a given value at the point of a given cursor and returns a new cursor that points to the position after the added value.
• Receiving reads a value, if present, at the point of a given cursor and returns a new cursor that points to the position after the read value.

Because cursors aren’t mutable but are handled in the manner of purely functional programming, it is possible to use the same cursor for multiple sends and multiple receives. Such usage results in the following behaviors:

• Multiple sends with the same cursor introduce a fork, and later receives with this cursor non-deterministically pick one of the arising branches.
• Multiple receives with the same cursor deliver the same value, except when there is a fork, in which case they deliver values from the same set of possible next values.

It is easy to see that using this alternative approach to ordered transmission is equivalent to using a FIFO channel when there is exactly one sender and one receiver. If there are several senders or several receivers, its behavior differs from the FIFO channel behavior though. This is sometimes seen as a weakness. However, we consider it also a strength, in particular, because, in the case of one sender and multiple receivers, this alternative approach realizes a form of order-preserving broadcast.