=Paper=
{{Paper
|id=None
|storemode=property
|title=Equations for Asynchronous Message Passing
|pdfUrl=https://ceur-ws.org/Vol-928/0061.pdf
|volume=Vol-928
|dblpUrl=https://dblp.org/rec/conf/csp/Czaja12
}}
==Equations for Asynchronous Message Passing==
https://ceur-ws.org/Vol-928/0061.pdf
Equations for Asynchronous Message Passing
Ludwik Czaja1,2
1
Institute of Informatics, The University of Warsaw
2
University of Economics and Computer Science Vistula in Warsaw
lczaja@mimuw.edu.pl
1 Introduction
In [Cza 2006] fix-point equations specifying synchronous (”hand-shaking”)
communication in distributed systems have been proposed. Their solution
yielded a communication network of agents, directly presented as a Petri
net-like structure, and determined the global state of the specified system.
The net-places represented agents, while transitions - transfer of messages. A
special algebra being a semi-ring with ”addition” (nondeterministic choice)
and ”multiplication” (simultaneity) was a formal basis for the equations
and their solving procedure. Here, the equations are modified to specify
asynchronous communication, that is, such that the senders, after sending
message, continue their performance without waiting for reception. This re-
quired introducing a new type of objects called buffers or mailboxes - apart
from the agents (senders/receivers), and changing the semi-ring into a dis-
tributive lattice of the agents and mailboxes. In the asynchronous commu-
nication, solution to the fix-point equations should determine that: (1) the
sender can send message as soon as mailboxes of its simultaneous receivers
can store the message, no matter whether the receivers are ready to get it or
not. (2) in the resulting net, the mailboxes are included as net-places too,
each one collecting messages from its senders (possibly a number of senders)
and transferring them to its (exactly one) receiver for which it is the unique
mailbox. The proposed modelling of communication takes some (but only
some!) ideas from CSP [Hoa 1978, 1985], CCS [Mil 1980, 1989] (e.g. a con-
cept of agents, ports, synchronization between senders and mailboxes or its
absence: no synchronization between senders and receivers, communication
media or channels), Petri nets [Rei 1985] (e.g. graphical presentation of
solution to the communication equations) or practice of computer networks
and distributed systems [C-D-K 2005] (e.g. multicasting and broadcasting,
1
blocking/non-blocking, connection-oriented/connectionless communication
mode). The communication equations may be treated as specifying inter-
connection system among agents, while net-structures resulted from their
solution - as ”implementation” of this system. The correctness of such im-
plementation is ensured by identity of each group of receivers from a given
sender (and, symmetrically, of each group of senders to a given receiver),
both in specification and implementation.
2 Two algebraic systems
In the following two algebras will be needed:
(1) A semiring of terms
Let X be a set of atomic arguments partitioned into the set C of constants
and the set V of variables: X = C∪V, C∩V = ∅. Each x ∈ X is a term; if K
and L are terms then strings (K + L) and (K • L) are too, called a sum and
product. We say “terms over X”, their set T[X]. Addition and multiplication
of terms is defined as follows: K ⊕ L = (K + L), K ⊗ L = (K • L), but
+ and • are used for ⊕ and ⊗. It is required that the system (T[X], +, •)
obeys the following axioms for all K, L, M ∈ T[X] :
(i) K +K =K
(ii) K +L=L+K
(iii) K + (L + M ) = (K + L) + M
(iv) K •L=L•K
(v) K • (L • M ) = (K • L) • M
(vi) K • (L + M ) = K • L + K • M
(vii) K ∈X⇒K •K =K
By assuming that • binds stronger than + and by (iii) and (v), some paren-
theses may be dropped. Two terms are equal (=) iff one may be transformed
into the other by means of the axioms. A partial order (v) between terms
is defined as K v L iff L = L + K. If a term K is composed of atoms
x, y, ..., z at the most, we write K(x, y, ..., z). That is, some of them may
be absent in K. A power of K is defined by K 1 = K, K n+1 = K • K n .
This algebra enjoys the properties:
(a) Each term may be transformed by means of equations (i)−(vii) to a sum
of products of arguments and then simplified. Such form is called canonical
(b) If n ≤ m then K n v K m .
(2) A distributive lattice of terms over constants
For the lattice the same operators + and • are used, thus, the algebraic
system (T[C], +, •) of terms with constants only is required to obey axioms
(i) − (vii) and additionally for K, L ∈ T[C]:
(viii) K •L+K =K
This algebra enjoys the following:
(c) If K = K1 +K2 +...+Kn where Ki ∈ T[X], is a product of arguments,
then K n = K n+j for j ≥ 0. In particular, for any term K there exists a
number n such that K n = K n+j for j ≥ 0. Define a maximal power of K
as p(K) = min(n| ∀j ≥ 0 : K n = K n+j ). For instance, the maximal power
of a • x + b with a, b ∈ C, x ∈ V is 2 since (a • x + b)2 = a • x + a • b • x + b,
(b • a + c)2 = (b • a + c)2+j for j ≥ 0, and a • x + b 6= (a • x + b)2 . Note
that if K ∈ T[C] then p(K) = 1.
(d ) There exist solutions to equation x = K • x + L and their general form
p(K)
is x = K • (L + P ) + L, where p(K) is the maximal power of K and
P is arbitrary term not containing x. In particular, general form of solution
to equation x = K • x is x = K p(K) • P .
Interpretations: In Section 3 constants will play part of agents represented
by places in nets obtained as solutions to the specification equations, while
some products of the constants - transitions meant as actions of message
transfer. In Section 4, apart for aforesaid role of constants, some of them
will also play part of mailboxes. These products will be monomials in terms,
being values of unknowns (send and receive variables) in the specification
equations presented in the following two sections.
3 Equations of specification - synchronous mode
Synchronous mode of communication (in a fairly abstract setting) has been
introduced in [Hoa 1978], in extended form presented in [Hoa 1985] and
implemented in some programming languages, e.g. [OCCAM 1984]. To
formulate specification equations for such mode, suppose that with each
agent-constant c ∈ C is bijectively associated:
• its co-agent denoted c and belonging to C
• its send-variable denoted c! and belonging to V
• its receive-variable denoted c? and belonging to V
The send and receive variables will get values being solutions to equations
set up as follows. For i ≤ n, j ≤ m, bj , ai ∈ C let Ki (b1 ?, ..., bm ?) be
a term composed only of receive-variables bj ? and Lj (a1 !, ..., an !) - a term
composed only of send-variables ai !. The specification equations are of the
form:
ai ! = ai • Ki (b1 ?, ..., bm ?) (agent ai sends to b1 , ..., bm ) (1)
bj ? = bj • Lj (a1 !, ..., an !) (agent bj gets from a1 , ..., an ) (2)
with the requirement:
bj ? occurs in Ki (b1 ?, ..., bm ?) iff ai ! occurs in Lj (a1 !, ..., an !)
The requirement is a consistency property of the equations. Variables ai !,
bj ? are unknown quantities, while constants ai , bj are known. A region
of receivers from the agent-sender ai is a subset of the set {b1 , ..., bm } of
receivers to which ai sends a message simultaneously. Symmetrically, a
region of senders to receiver bj is a subset of the set {a1 , ..., an } of senders
from which bj receives a message simultaneously. Simultaneous message
transfer (”multicast message”) is represented by product ”•” of agents. The
constants and variables will also be interpreted as propositional functions
of state s of the distributed system such that ai is ready to send a message
in a state s iff ai (s) is true and it can send message iff ai !(s) is true.
Similarly, bj is ready to receive a message in a state s iff bj (s) is true and
it can receive message iff bj ?(s) is true. Solutions to equations (1), (2)
yield in particular net structures, but also a global information on capability
of sending/receiving messages. The information is collected from a local
information of agents’ readiness to do this. Existence of the solutions to
these equations follows from the general fact concerning equations for formal
power series (their finite version) considered in [Sa-So 1978].
Remarks and intuitions
(1) The specification equations formalize the following (recursive) phrases:
• ”an agent a can send a message if it is ready to do this and each agent
in a certain region of its receivers can receive this message from a”
• ”an agent b can receive a message if it is ready to do this and each
agent in a certain region of its senders can send this message to b”
(2) Readiness of an agent to send/receive a message is determined by its
internal control pointing to a send/receive instruction within the agent’s
program.
(3) In semiring defined by axioms (i)-(vii) in Section 2, but without (viii),
that make it a lattice, the specification equations may have more than one
solution. A solution which reflects the communication structure specified by
equations (1), (2) is the one where each sender (resp. receiver) has the same
regions of receivers (resp. senders) as specified in these equations. Such solu-
tion is unique and in [Cza 2006] called ”appropriate”. Note that appropriate
solution is, in fact, the ”correct” one if ”correctness” is understood as con-
formity with specification. In this perspective, solving the equations means
implementing the specified interrelation of communicating agents in terms
of net-structures, along with ensuring correctness of the implementation.
Example 1
Synchronous communication (specification):
a! = a • (x? • y? + y?) (a sends simultaneously to x and y or only to y)
b! = b • (y? • z? + y?) (b sends simultaneously to y and z or only to y)
x? = x • a! (x gets from a)
y? = y • (a! + a! • b! + b!) (y gets only from a or simultaneously from a and b
or only from b)
z? = z • b! (z gets from b)
A solution; products represent transitions in the net representation - Fig.1:
Fig.1
a! = a • x • y + a • b • y
b! = b • y • z + a • b • y
x? = a • x • y
y? = a • x • y + a • b • y + b • y • z
z? = b • y • z
There are two regions of receivers from agent a: {x, y}, {y}, two regions of
receivers from agent b: {y, z}, {y}, as well as one region of senders to agent
x: {a}, one region of senders to agent z: {b}, and three regions of senders
to agent y: {a}, {b}, {a, b}. The solution is ”appropriate” since the regions
of senders and receicers are the same as in the specification equations.
Agents as propositional functions of state
A state of the communication structure specified by equations (1), (2) is a
function s : C → D where D is a set of data the agents intercommunicate.
In particular, if a solution is presented as a place/transition net then D = N
(natural numbers). With each agent a propositional function (denoted by
the same symbol as the agent and called a readiness condition) of state is
associated:
true if a is ready to send a message in state s
For a ∈ C: a(s) =
false otherwise
true if a is ready to receive a message in state s
For a ∈ C: a(s) =
false otherwise
The functions are extended to terms over the set of agents: for K, L ∈ T[C]:
(K + L)(s) = K(s) ∨ L(s)
(K • L)(s) = K(s) ∧ L(s)
Thus, solutions ai ! = K and bj ? = L to the equations (1), (2) become
propositional functions of state, defined by ai !(s) = K(s) and bj ?(s) =
L(s). This justifies phrases ”sender” and ”receiver”, since agent a can send
(receive) a message, in a state s iff a!(s) = true (a?(s) = true).
Products of agents (monomials in terms) as state transformers
The products in solutions to equations (1), (2) play part of state transform-
ers. This interpretation is more abstract than interpretation of transitions
in Petri nets because of more general meaning of state (”marking”) and its
transformation. Let t1 + ... + tp be a solution (in canonical form) to a! or
a?, that is ti = (a1 • ... • aqi ) • (b1 • ... • bri ) with a1 , ..., aqi , b1 , ..., bri ∈ C.
The product ti will represent a transition with preset a1 , ..., aqi and postset
b1 , ..., bri . Its firing rule (semantics) is given by a relation [[ti ]] ⊆ S × S
(S = DC is the set of all states) satisfying: if (s, s0 ) ∈ [[ti ]] then
(loc) s|(C\• t•i ) = s0 |(C\• t•i ) (locality condition)
(f ir) a1 (s)∧...∧aqi (s)∧b1 (s)∧...∧bri (s) is true (firability condition)
where • t•i = {a1 , ..., aqi , b1 , ..., bri } (”neighbourhood” of ti ) and | - ”re-
striction to...”. Consequently, by [[a!]] ([[a?]] respectively) is denoted the
relation [[t1 ]] ∪ ... ∪ [[tp ]]. We say that ti transforms s into s0 . Note that
the condition (f ir) may be written ”ti (s) is true”.
Solutions to equations (1), (2) as net structures
As shown in Example 1, a solution to (1), (2) is directly mapped onto a
net structure with places representing agents and transitions - some of their
products. This net-structure is, in fact, identical with a set of its transitions
defined above as ti = (a1 •...•aqi )•(b1 •...•bri ). Such a net-structure exhibits
admissible communication network specified by the equations. Fixing the set
D of values, the relations [[ti ]] and the readiness conditions of agents, various
classes of nets are obtained. For instance, in [Cza 2006], P/T and coloured
nets (with and without capacity of places and arrow weights) are generated
this way. The synchronous (handshaking [Hoa 1985], [Mil 1989], [OCCAM
1984] or blocking [C-D-K 2005]) mode of communication is determined by
the form of terms being solutions to specification equations. Transitions
ti as state transformers, are interpreted as actions producing messages for
agents b1 , ..., bri out of messages delivered by agents a1 , ..., aqi . Such abstract
setting allows to think of transitions as transformers of various types of data
[Cza 2007]. Note that ti may also be thought of as an exit (not entry!)
junction-box (or port) shared by agents a1 , ..., aqi and entry junction-box
shared by agents b1 , ..., bri . From the perspective of programming practice,
a transition acts somewhat like a shared procedure statement taking data
from agents a1 , ..., aqi and forwarding results to b1 , ..., bri with no side-effects
(because of the condition (loc)). Note that semantics of aSnet-structure N ,
which is a set of transitions, may be defined as [[N ]] = [[t]]
t∈N
4 From synchronous to asynchronous mode
In contrast to synchronized communication, in the asynchronous mode (im-
plemented e.g. in Linda [C-G 1989]), the senders dispatch messages to re-
ceivers through mailboxes of the latter. A sender may send message to a
number of mailboxes and each mailbox may get message from a number of
senders. However each receiver has exactly one mailbox and each mailbox
has exactly one receiver. To formulate the respective equations suppose that
with each agent a ∈ C is bijectively associated its mailbox denoted hai and
with hai is bijectively associated:
• its co-mailbox hai
• its send-variable denoted hai!
• its receive-variable denoted hai?
Now, the specification equations for the asynchronous mode of communica-
tion are:
ai ! = ai •Ki (hb1 i?, ..., hbm i?) (senders send to mailboxes of receivers) (3)
hbj i? = hbj i•Lj (a1 !, ..., an !) (mailboxes of receivers get from senders) (4)
hbj i! = hbj i•bj ? (mailboxes of receivers send to the latter) (5)
bj ? = bj •hbj i! (receivers get from their mailboxes) (6)
with the requirement:
hbj i? occurs in Ki (hb1 i?, ..., hbm i?) iff ai ! occurs in Lj (a1 !, ..., an !)
Note that equations (5), (6) representing delivery of messages to receivers
from their mailboxes have straightforward solutions:
hbj i! = hbj i • bj
bj ? = bj • hbj i
Equations (3), (4) are solved like those in (1), (2) in Section 3. The senders’
capability of sending message depends here on capability of reception by
mailboxes only. The readiness of a mailbox to get messages from senders
means that it is not filled up, while its readiness to deliver a message to its
receiver means that it is not empty. Therefore we consider:
Mailboxes as propositional functions of state
true if hbi is ready to deliver a message in state s
For hbi ∈ C: hbi(s) =
false otherwise
true if hbi is ready to get a message in state s
For hbi ∈ C: hbi(s) =
false otherwise
The functions are extended to terms as formerly in the case of agents.
Example 2
Asynchronous communication (specification):
a! = a • (hxi? • hyi? + hyi?) (a sends simultaneously to mailboxes
hxi and hyi or only to hyi)
b! = b • (hyi? • hzi? + hyi?) (b sends simultaneously to mailboxes
hyi and hzi or only to hyi)
hxi? = hxi • a! (hxi gets from a)
hyi? = hyi • (a! + a! • b! + b!) (hyi gets only from a or simultaneously from
a and b or only from b)
hzi? = hzi • b! (hzi gets from b)
hxi! = hxi • x? (hxi delivers to x)
hyi! = hyi • y? (hyi delivers to y)
hzi! = hzi • z? (hzi delivers to z)
x? = x • hxi! (x gets from hxi)
y? = y • hyi! (y gets from hyi)
z? = z • hzi! (z gets from hzi)
A solution:
Fig.2
a! = a • hxi • hyi + a • b • hyi
b! = b • hyi • hzi + a • b • hyi
hxi? = a • hxi • hyi
hyi? = a • hxi • hyi + a • b • hyi + b • hyi • hzi
hzi? = b • hyi • hzi
hxi! = hxi • x
hyi! = hyi • y
hzi! = hzi • z
x? = x • hxi
y? = y • hyi
z? = z • hzi
The solution exhibits directly data channels (links) of the agents’ commu-
nication and their capability to transfer the data in a given state. For
instance, agent y can receive a message from its mailbox hyi in a state s iff
y?(s) = y(s) ∧ hyi(s) is true, meaning that the control in y reached its
receive statement (instruction) and its mailbox is not empty. The mailbox
hyi in a state s can receive a message either from a only or from b only, or
one message from a and the other from b simultaneously iff
hyi?(s) = a(s) ∧ hxi(s) ∧ hyi(s) ∨ a(s) ∧ b(s) ∧ hyi(s) ∨ b(s) ∧ hyi(s) ∧ hzi(s)
is true, meaning that the control in a reached its send statement and neither
of the mailboxes hxi, hyi is filled up or the controls in a and b reached their
send statements and the maibox hyi is not filled up or the control in b reached
its send statement and neither of the mailboxes hyi, hzi is filled up.
5 Final notes
(1) The role of variables ai !, bj ? is similar to that of ”meta variables” (non-
terminals) in BNF: they assume terms, that is strings of constants (termi-
nals), as values. Also the role of constants is similar: they assume elements
of D, the set of data, as values.
(2) Solutions to specification equations for synchronous (blocking) and asyn-
chronous (non-blocking) mode, describe a kind of intercommunication where
communication lines between the agents are fixed for a given computational
session. The lines are pictorialy visible as arcs of nets representing the so-
lutions. The interesting issue is to adjust the idea to systems where the
lines are being established dynamicaly - during the session. To this end,
the idea of self-modifying nets, introduced by Ruediger Valk [Val 1978], [Val
1981], or perhaps, stratified nets [B-D 1997], seems promissing. Also, mod-
elling of the so-called connection oriented (sender and receiver set up a line
and make an arrangement on some details of communication prior to the
communication itself; the line remains as long as it is needed during com-
munication) and connectionless communication (e.g. [C-D-K 2005]) in the
framework pursued here is a research challenge, close to practical applica-
tion. Another approach to self-modification is based on the abovementioned
view of a net-structure as a collection of transitions, each being a pair of
two sets of agents (places). Firing transition would, then, encompass not
only change of marking but also modification of the set of transitions that
constitutes the net-structure (motivation: users of distributed systems un-
dertake send/receive actions independently of any external control). This is
a work in progress.
6 References
[B-D 1997] Badouel E., Darondeau P.: Stratified Petri Nets, FCT’97, Lecture
Notes in Computer Science vol. 1279 (1979), pp. 117-128
[C-G 1989] Carriero N, Gelernter D.: Linda in Context, Comm. of the ACM,
1989
[C-D-K 2005] Coulouris G, Dollimore J, Kindberg T: Distributed Systems.
Concepts and Design. Addison Wesley, Editions: 1988, 1994, 1995, 1996,
2005.
[Cza 2006] Czaja L.: Equations for Message Passing, Fundamenta Infor-
maticae, Vol. 72, Numbers, 1-3, July/August 2006, pp. 81-93
[Cza 2007] Czaja L.: Interpreted Nets, Fundamenta Informaticae, Vol.79,
Numbers 3-4, September 2007, pp.283-293
[Hoa 1978] Hoare C.A.R.: Communicating Sequential Processes, Comm. of
the ACM, Vol 21, pp. 666-677, 1978
[Hoa 1985] Hoare C.A.R.: Communicating Sequential Processes, Prentice-
Hall, 1985
[Mil 1980] Milner A.J.R.G.: A Calculus of Communicating Systems, Lecture
Notes in Computer Science vol. 92 (1980)
[Mil 1989] Milner A.J.R.G.: A Calculus of Communicating Systems, Prentice-
Hall, 1989
[OCCAM 1984] INMOS Limited: OCCAM Programming Manual, Prentice-
Hall, 1984
[Rei 1985] Reisig W.: Petri Nets, An Introduction, EATC Monographs on
Theoretical Computer Science, Springer-Verlag, 1985
[Sa-So 1978] Salomaa A., Soittola M., Automata-Theoretic Aspects of Formal
Power Series, Springer, 1978
[Val 1978] Valk R.: Self-Modifying Nets, a Natural Extension of Petri Nets,
Icalp’78, Lecture Notes in Computer Science vol. 62 (1978), pp. 464-476
[Val 1981] Valk R.: Generalization of Petri Nets, MFCS’81 Lecture Notes
in Computer Science vol. 118 (1981), pp. 140-155