Information Technology Reference
In-Depth Information
config.yml
file specifies which network principals will play which roles in this session
and the runtime sends invitation messages to each. The
join
method confirms that the
endpoint is joining the conversation as the principal
alice
playing the role
User
,and
returns a conversation channel object for performing the subsequent communication
operations. Once the invitations are sent and accepted (via
Conversation.join
), the
conversation is established and the intended message exchanges can proceed. As a result
of the initiation procedure, the runtime at every participant has a mapping (conversation
table) between each role and their AMQP addresses.
Conversation Message Passing.
Following its local protocol, the User program sends
a request to the
controller
, stating the duration for which it requires access to
agent
.
The
send
method called on the conversation channel
c
takes, in this order, the des-
tination role, message operator and payload values as arguments. This information is
embedded into the message payload as part of the conversation meta data, and is later
used by the monitor in the runtime verification. The
recv
method can take the source
role as a single argument, or additionally the operator of the desired message. Send is
asynchronous, meaning that the operation does not block on the corresponding receive;
however, the basic receive does block until the complete message has been received.
For asynchronous, non-blocking receives, the API provides
recv async
to be used in an
event-driven style.
Interrupt Handling via Conversation Scopes.
This example demonstrates a way of
handling conversation interrupts by combining conversation scopes with the Python
with
statement (an enhanced try-finally construct). We use
with
to conveniently cap-
ture interruptible conversation flows and the nesting of interruptible scopes, as well
as automatic
close
of interrupted channels in the standard manner, as follows. The
API provides the
c.scope()
method, as in line 10, to create and enter the scope of
an
interruptible
Scribble block (here, the outer interruptible of the RAC protocol).
The
timeout
and
stop
arguments associate these message signatures as interrupts to
this scope. The conversation channel
c1
returned by
scope
is a wrapper of the parent
channel
c
that (1) records the current scope of every message sent in its meta data, (2)
ensures every send and receive operation is guarded by a check on the local interrupt
queue, and (3) tracks the nesting of scope contexts through nested
with
statements. The
interruptible scope of
c1
is given by the enclosing
with
(lines 10-21); if, e.g., a
timeout
is received within this scope, the control flow will exit the
with
to line 22. The inner
with
(lines 13-17), corresponding to the inner interruptible block, is associated with the
pause
interrupt. When an interrupt, e.g.
pause
in line 17, is thrown (
send interrupt
)to
the other conversation participants, the local and receiver runtimes each raise an internal
exception that is either handled or propagated up, depending on the interrupts declared
at the current scope level, to direct the interrupted control flow accordingly. The de-
lineation of interruptible scopes by the global protocol, and its projection to each local
protocol, thus allows interrupted control flows to be coordinated between distributed
participants in a structured manner.
The scope wrapper channels are closed (via the
with
) after throwing or handling an
interrupt message. For example, using
c1
(outside its parent scope) after a
timeout
is
received will be flagged as an error. By identifying the scope of every message from its
