1 External Events

dat transfers are followed by ack acknowledgments. req requests evoke the return of acs access permissions.

C.U.dat (e) U.C.dat (e)

C = data transfer channel. e = data value transferred.

C.U.dat is in the alphabets of channel end out (C) and the user process. U.C.dat is in the alphabets of channel end in (C) and the user process.

C.U.ack U.C.ack

C = data transfer channel.

C.U.ack is in the alphabets of channel end in (C) and the user process. U.C.ack is in the alphabets of channel end out (C) and the user process.

C.U.req U.C.req

C = access transfer channel.

C.U.req is in the alphabets of channel end out (C) and the user process. U.C.req is in the alphabets of channel end in (C) and the user process.

C.U.acs (F) U.C.acs (F)

C = access transfer channel F = channel end, access to which is transferred.

C.U.acs (F) is in the alphabets of channel end in (C) and the user process. U.C.acs (F) is in the alphabets of channel end out (C) and the user process.

2 Messages

2.1 Data Transfer Messages

ack is an acknowledgement of a dat message.

Q.P^{O}.dat (e, C) Q.P^{I}.dat (e, C)

P = port associated with channel end out (C). Q = port associated with in (C). e = data value transferred. C = data transfer channel.

dat output is in the alphabets of port P, channel end out (C), and the message delivery system. dat input is in the alphabets of port Q, channel end in (C), and the message delivery system.

P.Q^{O}.ack (C) P.Q^{I}.ack (C)

P = port associated with channel end out (C). Q = port associated with in (C). C = data transfer channel.

ack output is in the alphabets of port Q, channel end in (C), and the message delivery system. ack input is in the alphabets of port P, channel end out (C), and the message delivery system.

2.2 Access Transfer Messages

req requests access to some available channel end be transferred to a locally allocated port. “Acknowledgment” of the request goes through the control transfer messages introduced below.

Q.P^{O}.req (R, C) Q.P^{I}.req (R, C)

P = port associated with channel end out (C). Q = port associated with in (C). R = recipient port, to which access will be transferred. C = data transfer channel.

req output is in the alphabets of ports P and R, channel end out (C), and the message delivery system. req input is in the alphabets of port Q, channel end in (C), and the message delivery system.

2.3 Control Transfer Messages

The ini message is sent from a port process to its successor on termination of the former. It carries information needed to initialise the new port.

P.S^{O}.ini (E, Q, s, D) P.S^{I}.ini (E, Q, s, D)

P = port formerly associated with channel end E. S = successor port to P. E = a channel end. Q = port associated with partner of E. s = value defining a set of events pending on E at time of transfer. D = access transfer channel.

ini output is in the alphabets of channel end E, port P, and the message delivery system. ini input is in the alphabets of channel ends E and out (D), port S, and the message delivery system.

2.4 Port Repointing Messages

These messages are used during transfer of access to a channel end to inform the port associated with the partner channel end of the move. quo is an acknowledgement of a chg message.

Q.P^{O}.chg (E, S, D) Q.P^{I}.chg (E, S, D)

P = port formerly associated with channel end E. Q = port associated with partner of E. S = successor port to P. E = a channel end. D = access transfer channel.

chg output is in the alphabets of channel end in (D), port P, and the message delivery system. chg input is in the alphabets of port Q and the message delivery system.

P.Q^{O}.quo (E, D) P.Q^{I}.quo (E, D)

P = port formerly associated with channel end E. Q = port associated with partner of E. E = a channel end. D = access transfer channel.

quo output is in the alphabets of port Q, and the message delivery system. quo input is in the alphabets of port P and the message delivery system.

3 The Channel-End Process

Associated with each C-channel are an input channel-end process and an output channel-end process. These processes are largely formal devices, with no unique physical location. Their alphabets incorporate the events of the external interface of the C-channel. They are responsible for correct sequencing of the individual messages involved in communication on the C-channel.

3.1 Output channel-end

The alphabet of an output channel end process out (C) contains

Control transfer events

. ^{O}.ini (out (C), , , )
. ^{I}.ini (out (C), , , )

Data transfer events

C.U.dat
. ^{O}.dat ( , C)
. ^{I}.ack (C)
U.C.ack

Access transfer events

C.U.req
. ^{O}.req ( , C)
. ^{I}.ini ( , , , C)
U.C.acs

In this alphabet, the data and access transfer events together will be called “communication events”. Communication events excluding the input events on channels . ^{I} will be called “non-input communication events”. The traces of out (C) satisfy

1. The trace restricted to control transfer events and non-input events (ie, excluding input communication events) is a prefix of a sequence built from the atomic subsequences

⟨c⟩, where c is any non-input communication event, and ⟨ . ^{O}.ini (out (C), , s, ), . ^{I}.ini (out (C), , , )⟩

2. The trace restricted to communication events is a prefix of a sequence built from the atomic subsequences ⟨C.U.dat (e), . ^{O}.dat (e, C), . ^{I}.ack (C), U.C.ack ⟩, and ⟨C.U.req , . ^{O}.req (R, C), R. ^{I}.ini (F, , , C), U.C.acs (F)⟩

3. If one of the atomic subsequences in 2 is interrupted by an ini output, the s field in that output contains sufficient information to determine how to resume the subsequence at the point of interruption.

3.2 Input channel-end

The alphabet of an input channel end process in (C) contains

Control transfer events

. ^{O}.ini (in (C), , , ) . ^{I}.ini (in (C), , , )

Data transfer events

. ^{I}.dat ( , C) U.C.dat C.U.ack . ^{O}.ack (C)

Access transfer events

. ^{I}.req ( , C) U.C.req C.U.acs . ^{O}.chg ( , , C)

The traces of in (C) satisfy

1. The trace restricted to control transfer events and non-input events (ie, excluding input communication events) is a prefix of a sequence built from the atomic subsequences

⟨c⟩, where c is any non-input communication event, and ⟨ . ^{O}.ini (in (C), , s, ), . ^{I}.ini (in (C), , , )⟩

2. The trace restricted to communication events is a prefix of a sequence built from the atomic subsequences

⟨ . ^{I}.dat (e, C), U.C.dat (e), C.U.ack , . ^{O}.ack (C)⟩, and ⟨ . ^{I}.req (R, C), U.C.req , C.U.acs (F), . ^{O}.chg (F, R, C)⟩

3. (As for output channel-end).

Requirement 1 implies that the only event that can occur between output of an ini message and its subsequent receipt is an input communication event. During this interval the channel end is “moving”, and most types of event are disabled. Inputs from the message system cannot be disabled here, because (as it will turn out) this would violate the important eager readership assumption. Requirement 3 implies that resumption of a channel-end process after moving to a different processor doesn’t depend on any miraculous non-local transfer of information. For example, suppose the move of an input channel-end, implied by insertion of an ini subsequence, occurred after reception of a dat (e, C) message from the message delivery system, but before delivery of the datum e to the user process. The s field in the ini message would have to include the value of e.

Eventually it will be necessary to put some further restrictions on these traces, to avoid other forms of non-locality.

4 The Port Process

A port process may be “initialised” or “uninitialised”. An initialised port is associated from the outset with some channel end out (C) or in (C). It has a partner initialised port, associated with opposite other channel end. An uninitialised port starts off in the “free pool” of ports. Port P is allocated from this pool when it successfully engages in a . ^{O}.req(P, ) event.

The alphabet of a port process P contains

Main control thread events

. ^{O}.req (P, ) P. ^{I}.ini .P^{O}.ini

Repointing events

P. ^{I}.chg .P^{O}.quo .P^{O}.chg P. ^{I}.quo

Communication events

.P^{O}.dat P. ^{I}.ack .P^{O}.req P. ^{I}.dat .P^{O}.ack P. ^{I}.req

The traces of P satisfy

1. The trace restricted to main thread events and chg output events is a prefix of some sequence

⟨ .P^{O}.chg ( , R, D), R.P^{O}.ini ( , , , D)⟩

if P is an initialised port, or

⟨ . ^{O}.req(P, ), P. ^{I}.ini , .P^{O}.chg ( , R, D), R.P^{O}.ini ( , , , D)⟩

if it is uninitialised. Moreover, req (P, ) output can only occur as the first event of the full trace, and ini output can only occur as the last.

2. In the trace restricted to ini input events and output events on the channels .P^{O}, an ini event can only appear in the first position of the sequence, and a chg output event can only appear in the last. (ie, no outputs are initiated before initialisation, or after initiation of a “move”).

3. The trace restricted to repointing events is a prefix of a sequence built from any number of atomic subsequences of the form

⟨P.Q^{I}.chg (E, , D), Q.P^{O}.quo (E, D)⟩ terminated by one subsequence from

⟨ .P^{O}.chg , P. ^{I}.quo ⟩, ⟨ .P^{O}.chg , P. ^{I}.chg ⟩, or ⟨P. ^{I}.chg , .P^{O}.chg ⟩

All incoming chg messages are acknowledged. The three possibilities for termination embody the only slightly subtle part of the repointing protocol.

4. In any event from

Q.P^{O}.dat Q.P^{O}.ack Q.P^{O}.req Q.P^{O}.chg .P^{O}.ini ( , Q, , )

appearing in a trace, the Q field must have the same value as the Q field in the most recent preceding event of type

P. ^{I}.chg (Q, )

If there is no preceding chg input, the Q field must match either the initial value for the partner port (if P is initialised), or the value in the trace’s (compulsory)

P. ^{I}.ini ( , Q, , )

event (if it is uninitialised). These constraints impose that communications are always sent to the active partner port.

5. The trace must be constructed from

. ^{O}.req (P, ) P. ^{I}.ini (out(C), , , ) .P^{O}.ini (out(C), , , ) P. ^{I}.chg .P^{O}.chg ( , out(C), ) .P^{O}.dat ( , C) P. ^{I}.ack (C) .P^{O}.req ( , C)

or (exclusively) from

. ^{O}.req (P, ) P. ^{I}.ini (in(C), , , ) .P^{O}.ini (in(C), , , ) P. ^{I}.chg

.P^{O}.chg ( , in(C), )
.P^{I}.dat ( , C)
P. ^{O}.ack (C)
.P^{I}.req ( , C)

where the value of the C field is common to all events in a trace. (MISSING quo EVENTS HERE). If P is an initialised port with channel end out (C) the first set is applicable; if it is initialised with in (C) the second set applies. A port will only support one channel end throughout its life. (IT’S LIKELY THAT I WANT TO REMOVE SOME UNNECESSARY RESTRICTIONS ON INPUT EVENTS).

5 “Solving” the Trace Restrictions

Suppose C is some channel name, and P , Q are non-empty sequences of port names, with n = #P , m = #Q. Introduce the sets of event sequences:

P_{⟩|}^{∞}(D) = {⟨Q_{j}.P_{i}^{O}.chg (out (C), P_{i+1}, D)⟩}
P_{⟩|}^{∈}(D) = {⟨Q_{j}.P_{i}^{I}.chg (out (C), P_{i+1}, D)⟩}
P_{⟩|}^{∋}(D) = {⟨P_{i}.Q_{j}^{O}.quo (out (C), D)⟩}
P_{⟩|}^{△}(D) = {⟨P_{i}.Q_{j}^{I}.quo (out (C), D),
P_{i+1}.P_{i}^{O}.ini (out (C), Q_{j}, s, D),

P_{i+1}.P_{i}^{I}.ini (out (C), Q_{j}, s, D)⟩ | s ∈ Contexts}

for 0 ≤ i < n − 1, 0 ≤ j < m, and

Q_{⟩|}^{∞}(D) = {⟨P_{i}.Q_{j}^{O}.chg (in (C), Q_{j+1}, D)⟩}
Q_{⟩|}^{∈}(D) = {⟨P_{i}.Q_{j}^{I}.chg (in (C), Q_{j+1}, D)⟩}
Q_{⟩|}^{∋}(D) = {⟨Q_{j}.P_{i}^{O}.quo (in (C), D)⟩}
Q_{⟩|}^{△}(D) = {⟨Q_{j}.P_{i}^{I}.quo (in (C), D),
Q_{j+1}.Q_{j}^{O}.ini (in (C), P_{i}, s, D),

Q_{j+1}.Q_{j}^{I}.ini (in (C), P_{i}, s, D)⟩ | s ∈ Contexts}

for 0 ≤ i < n, 0 ≤ j < m − 1, and

\overline{P}_{ij}^{4}(D, D′) = \{⟨P_{i}.Q_{j}^{I}.chg (in (C), Q_{j+1}, D′),
P_{i+1}.P_{i}^{O}.ini (out (C), Q_{j+1}, s, D),

P_{i+1}.P_{i}^{I}.ini (out (C), Q_{j+1}, s, D)⟩ | s ∈ Contexts}

\overline{Q}_{ij}^{4}(D, D′) = \{⟨Q_{j}.P_{i}^{I}.chg (out (C), P_{i+1}, D),

Q_{j+1}.Q_{j}^{O}.ini (in (C), P_{i+1}, s, D′),
Q_{j+1}.Q_{j}^{I}.ini (in (C), P_{i+1}, s, D′)⟩ | s ∈ Contexts}

for 0 ≤ i < n − 1, 0 ≤ j < m − 1. Next, define recursively A_{⟩|}(D) =

(⋃_{D′} A_{⟩−∞,|}(D′)P_{⟩−∞,|}^{∋}(D′)P_{⟩−∞,|}^{△}(D′)P_{⟩|}^{∞}(D)P_{⟩|}^{∈}(D)) ∪

(⋃_{D′} B_{⟩,|−∞}(D′)Q_{⟩,|−∞}^{∋}(D′)((P_{⟩|}^{∞}(D)P_{⟩|}^{∈}(D)) + Q_{⟩,|−∞}^{△}(D′))) ∪

( ⋃_{D′,D′′} C_{⟩−∞,|−∞}(D′, D′′)((\overline{P}_{⟩−∞,|−∞}^{△}(D′)P_{⟩|}^{∞}(D)P_{⟩|}^{∈}(D)) + \overline{Q}_{⟩−∞,|−∞}^{△}(D′′)))

for 0 ≤ i < n − 1, 0 ≤ j < m, and B_{⟩|}(D) =

(⋃_{D′} A_{⟩−∞,|}(D′)P_{⟩−∞,|}^{∋}(D′)(P_{⟩−∞,|}^{△}(D′) + (Q_{⟩|}^{∞}(D)Q_{⟩|}^{∈}(D)))) ∪

(⋃_{D′} B_{⟩,|−∞}(D′)Q_{⟩,|−∞}^{∋}(D′)Q_{⟩,|−∞}^{△}(D′)Q_{⟩|}^{∞}(D)Q_{⟩|}^{∈}(D)) ∪

( ⋃_{D′,D′′} C_{⟩−∞,|−∞}(D′, D′′)(\overline{P}_{⟩−∞,|−∞}^{△}(D′) + (\overline{Q}_{⟩−∞,|−∞}^{△}(D′′)Q_{⟩|}^{∞}(D)Q_{⟩|}^{∈}(D))))

for 0 ≤ i < n, 0 ≤ j < m − 1, and C_{⟩|}(D, D′) =

(⋃_{D′′} A_{⟩−∞,|}(D′′)P_{⟩−∞,|}^{∋}(D′′)((P_{⟩−∞,|}^{△}(D′′)P_{⟩|}^{∞}(D)) + Q_{⟩|}^{∞}(D′))) ∪

(⋃_{D′′} B_{⟩,|−∞}(D′′)Q_{⟩,|−∞}^{∋}(D′′)(P_{⟩|}^{∞}(D) + (Q_{⟩,|−∞}^{△}(D′′)Q_{⟩|}^{∞}(D′))) ∪

( ⋃_{D′′,D′′′} C_{⟩−∞,|−∞}(D′′, D′′′)((\overline{P}_{⟩−∞,|−∞}^{△}(D′′)P_{⟩|}^{∞}(D)) + (\overline{Q}_{⟩−∞,|−∞}^{△}(D′′′)Q_{⟩|}^{∞}(D′))))

for 0 ≤ i < n − 1, 0 ≤ j < m − 1. Here, juxtaposition of sequence sets implies concatentation of elements, and ‘+’ means interleaving of elements. The conventions: A_{−∞,′} = B_{′,−∞} = C_{−∞,−∞} = P_{−∞,⟩}^{∋} = P_{−∞,⟩}^{△} = \overline{P}_{−∞,⟩−∞}^{△} = Q_{⟩,−∞}^{∋} = Q_{⟩,−∞}^{△} = \overline{Q}_{⟩−∞,−∞}^{△} = \{⟨⟩\} for i ≥ 0, and A_{−∞,⟩} = B_{−∞,⟩} = C_{−∞,⟩−∞} = A_{⟩,−∞} = B_{⟩,−∞} = C_{⟩−∞,−∞} = ∅ for i > 0, supply the base cases for the recurrence.

Finally we construct:

M(C, P , Q) =

(⋃_{D} A_{⟩−∞,|}(D)P_{⟩−∞,|}^{∋}(D)P_{⟩−∞,|}^{△}(D)) ∪

(⋃_{D} B_{⟩,|−∞}(D)Q_{⟩,|−∞}^{∋}(D)Q_{⟩,|−∞}^{△}(D)) ∪

( ⋃_{D,D′} C_{⟩−∞,|−∞}(D, D′)(\overline{P}_{⟩−∞,|−∞}^{△}(D) + \overline{Q}_{⟩−∞,|−∞}^{△}(D′)))

where i = n − 1, j = m − 1.