1: \section{The \mob Abstract Machine}
2: \label{sec:mobam}
3:
4: We provide the semantics for a \mob network in the form of an abstract state
5: transition machine. A \mob network is composed by a set of hosts,
6: which are abstractions for network nodes. Hosts define the boundaries
7: where computations take place in a \mob network. The computing units
8: of the \mob language are agents. There may be several agents running
9: concurrently in a given host at any given time. In our approach there
10: is no distinction between clients and servers, any agent may behave as
11: a client requesting a service while also providing services to
12: others. This is achieved by implementing multi-threaded agents to
13: handle multiple requests concurrently. The threads in an agent share
14: the same heap space whilst having independent control data-structures.
15:
16: Before defining the structure of the network, of agents and of threads we
17: first introduce the syntactic categories and auxiliary
18: functions.
19:
20: \subsection{Syntactic Categories and Data-Structures}
21:
22: Besides the syntactic categories of the language, the abstract machine
23: requires a new set of categories\footnote{We denote the syntactic
24: definition of methods in the language and their internal
25: representation in the abstract machine with the same letter
26: $\mathmob{M}$. We choose to do so because both relate to the same
27: information, although with different representations.} defined in table \ref{fig:vmcats}.
28:
29: \begin{table}
30: \begin{center}
31: \begin{tabular}{lcll}
32: $\mathmob{a, b}$ & $\in$ & \text{AgentKey} & \text{Agent key} \\
33: $\mathmob{C}$ & $\in$ & \text{Code} & \text{Code for the class and agent definitions} \\
34: $\mathmob{M}$ & $\in$ & \text{Method} & \text{Methods of a
35: definition} \\
36: $\mathmob{H}$ & $\in$ & \text{Heap} & \text{Address space for the agent} \\
37: $\mathmob{r}$ & $\in$ & \text{HeapRef} & \text{Heap reference} \\
38: $\mathmob{t}$ & $\in$ & \text{ThreadRef} & \text{Thread reference}
39: \\
40: $\mathmob{K}$ & $\in$ & \text{Closure} & \text{Closure} \\
41: $\mathmob{u}$ & $\in$ & \text{Value} & \text{Constant value or a
42: heap reference} \\
43: $\mathmob{T}$ & $\in$ & \text{Pool(RunningThread)} \quad & \text{Pool of flows of execution} \\
44: $\mathmob{B}$ & $\in$ & \Environment & \text{Environment of a
45: thread} \\
46: $\mathmob{Q}$ & $\in$ & \text{CodeStack} & \text{Stack of interrupted blocks of code} \\
47: $\mathmob{W}$ & $\in$ & \text{SuspendedThread} & \text{Threads suspended (waiting) on a heap
48: reference} \\
49: $\calA$ & $\in$ & \text{Pool(Agent)} & \text{Pool of
50: agents}\\
51: $\alpha$ & $\in$ & \text{Type} & \text{Type of a service}
52: \\
53: $\ns$ & $\in$ & \NS & \text{Name resolver} \\
54: $\mathmob{ANS}$ & $\in$ & \ANS & \text{Agent name resolver}
55: \\ $\mathmob{SNS}$ & $\in$ & \SNS & \text{Service name resolver} \\
56: $\calN$ & $\in$ & \text{Network} & \text{Network}
57: \end{tabular}
58: \end{center}
59: \caption{Syntactic categories of the \mob virtual machine}
60: \label{fig:vmcats}
61: \end{table}
62:
63: %\subsection{The Data Structures}
64:
65: The abstract machine has two layers: agents and threads. A
66: network is described as a set of agents running concurrently plus a
67: resolver for agents and services. Agents are described as collections of threads
68: running concurrently and sharing the agent's resources, namely its code and
69: address space.
70: %
71: Agents are abstractions for autonomous programs running on network
72: hosts, that interact with the network by spawning new agents or moving
73: between hosts. Inter-agent interaction is performed by invoking methods.
74: %
75: The abstract machine requires some syntactic categories and
76: data-structures to be defined:
77:
78: \begin{itemize}
79:
80: \item an \emph{Agent Key} is an element of the set $\AgentName \subset
81: \String$, ranged over by $\mathmob{a, b}$, and represents a unique,
82: network-wide, key for an agent;
83:
84: \item a \emph{Host} is an element of the set $\Host \subset \String$,
85: ranged over by $\mathmob{h}$, and represents a unique, network-wide,
86: host identifier;
87:
88: \item an \emph{Instruction} is an element of the set $\Instruction$,
89: ranged over by $\mathmob{I}$, and represents a \mob instruction. A
90: sequence of instructions separated by \textbf{;} is denoted by $\mathmob{P} \in \text{InstructionSeq}$;
91:
92: \item \emph{Method} represents a set of methods and is a map of the
93: form $\Method = \MethodId \mapsto \Var^* \times \InstructionSeq$,
94: ranged over by $\mathmob{M}$, and represents the methods in a class
95: or an agent;
96:
97: \item the \emph{Code} repository for an agent is a map defined as
98: $\Code = \Class \mapsto \Bool \times \Var^* \times
99: \Method \times \Code \times \ServiceId^*$, ranged over by $\mathmob{C}$ and
100: represents the all the code required by a class or agent. The
101: boolean value makes the distinction between the two (\truek\ = agent,
102: \falsek\ = class);
103:
104:
105: \item a \emph{Heap Reference} is an element of the set $\HeapRef$,
106: ranged over by $\mathmob{r}$, and is an abstraction for an address
107: in the address space of an agent.
108: %
109: Heap references in \mob are qualified with the key of their hosting
110: agent (e.g., reference $\mathmob{r}$ in the heap of agent
111: $\mathmob{a}$ should be interpreted as $\mathmob{r@a}$) and thus are
112: unique in the network. To ease the reading of the rules we omit the
113: qualifier of a heap reference when it is accessed from within its
114: hosting agent. The value $\nullr \in \HeapRef$ represents an
115: undefined heap reference;
116:
117: \item a \emph{Thread Reference} is an element of the $\ThreadRef
118: \subset \HeapRef$, ranged over by $\mathmob{t}$, and represents a
119: reference to a thread. Note that this subset includes $\nullr$;
120:
121: \item a \emph{Constant} is an element of the set $\Constant = \Bool
122: \cup \Int \cup \String$, ranged over by $\mathmob{c}$, and represents a
123: primitive value of the language;
124:
125: \item a \emph{Value} is an element of the set $\Value = \Constant \cup
126: \HeapRef$, ranged over by $\mathmob{u}$;
127:
128: \item an \emph{Environment} is a map defined as $\Environment = \Var
129: \mapsto \Value$, ranged over by $\mathmob{B}$, that represents a map from
130: identifiers in the code to constants or references in the heap. We will represent
131: the binding from an identifier $\mathmob{x}$ to a value $\mathmob{u}$ as $\mathmob{x:u}$;
132:
133: \item a \emph{Closure} is an element of the set $\Closure = \Bool
134: \times \Environment \times \Class$, ranged over by $\mathmob{K}$,
135: and represents the closure for an instance of a class or an agent
136: located in an address space. The boolean value makes the distinction
137: between instances of classes and agents;
138:
139: \item a \emph{Heap} is a map defined as $\Heap = \HeapRef \mapsto
140: \ThreadRef \times (\Closure \cup \Value)$, \linebreak ranged over by
141: $\mathmob{H}$, and represents the address space of an agent. The contents
142: associated with heap references may be accessed with mutual
143: exclusion using locks. The thread reference
144: in the image of a reference indicates which thread holds the lock
145: to the contents. Unlocked references hold $\nullr$ has their
146: thread reference;
147:
148: \item a \emph{Code Stack} is an element of the set $\Stack =
149: Stack(\Environment \times \InstructionSeq)$, ranged over by $\mathmob{Q}$, and
150: represents the stack of blocks of code, used as a mechanism to
151: implement \whilek loops. The block of the top of the stack is the
152: one currently being executed by the machine. As soon as it
153: terminates, it is popped from the stack and the execution continues
154: with the code of the block found at the top of the stack. We refer to elements
155: of the stack as \emph{code-blocks};
156:
157: \item a \emph{Pool of Running Threads} is an element of the set
158: $\Pool(\RunningThread)$, ranged over by $\mathmob{T}$, where
159: $\RunningThread = \ThreadRef \times \Stack \times \HeapRef$
160: represents a flow of execution. In the definition of a thread
161: $\mathmob{(t, Q, r)}$, the thread reference $\mathmob{t}$ is a
162: location in the heap to which the thread is bound. The reference
163: $\mathmob{r}$ is a heap reference where the thread may place a
164: result;
165:
166: \item a \emph{Suspended Thread} is a map defined as $\SuspendedThread
167: = \HeapRef \mapsto 2^\RunningThread$, ranged over by $\mathmob{W}$, and
168: represents threads suspended (waiting) on heap references;
169:
170: \item a \emph{Pool of Agents} is an element of the set
171: $\Pool(\Agent)$, ranged over by $\calA$, where $\Agent = \AgentName
172: \times \Host \times \Code \times \Heap \times \Pool(\RunningThread)
173: \times \SuspendedThread$ represents a multi-threaded autonomous
174: computation. We write an agent $\mathmob{(a,h,C,H,T,W)}$ as
175: $\mathmob{a(h,C,H,T,W)}$ thus exposing the agent's key;
176:
177: \item a \emph{Service Type} is an element of the set $\Type$, ranged
178: over by $\alpha$;
179:
180: \item a \emph{Name Resolver}, $\calR$, is composed by two maps, $\NS = \ANS \times$ \linebreak
181: $\SNS$. The first, defined as $\ANS = \HeapRef \mapsto \Host$, ranged
182: over by $\mathmob{ANS}$, represents a network-wide name resolver for locating
183: agents. The second, defined as $\SNS = \ServiceId \mapsto \Type
184: \times 2^\HeapRef$, ranged over by $\mathmob{SNS}$, represents a network-wide
185: name resolver for obtaining the type and implementations of a service;
186:
187: % and the set of
188: % agents that implement it, denoted by $I$; ????????????????
189:
190: \item a \emph{Network} is an element of the set $\Network =
191: \Pool(\Agent) \times \NS$, ranged over by $\calN$, and
192: represents a \mob network computation.
193:
194: \end{itemize}
195:
196: \subsection{Auxiliary Definitions}
197: Function \access checks if, in a heap $\mathmob{H}$, the access to the value
198: located at $\mathmob{r}$ is granted to a thread identified by $\mathmob{t}$.
199:
200: \begin{step}
201: \begin{array}{rlll}
202: \access: \Heap \times \HeapRef \times \ThreadRef & \mapsto & \Bool \\
203: \access(\mathmob{H, r, t}) & = &
204: \left \{
205: \begin{array}{ll}
206: \truek, & \text{if}\ \mathmob{H(r) = (t, \_)} \;\text{or}\; \mathmob{H(r) = (\nullr, \_)}\\
207: \falsek, & \text{if}\ \mathmob{H(r) = (t', \_)} \;\text{and}\; \mathmob{t' \not = t}
208: \end{array} \right.
209: \end{array}
210: \end{step}
211:
212: Function \locked tries to grant the lock for a value located at
213: $\mathmob{r}$, in a heap $\mathmob{H}$,
214: to a thread identified by $\mathmob{t}$. Function \unlocked tries
215: to release the lock for a value located at $\mathmob{r}$ in a heap $\mathmob{H}$. The
216: result of both functions is a heap modified (or not) by the operation,
217: and a boolean value indicating if the operation was successful. Both
218: these functions are atomic.
219:
220: \begin{step}
221: \begin{array}{rlll}
222: \locked: \Heap \times \HeapRef \times \ThreadRef & \mapsto & \Heap \times \Bool \\
223: \locked(\mathmob{H, r, t}) & = &
224: \left \{
225: \begin{array}{ll}
226: \mathmob{(H + \{r : (t, K)\}, \truek)}, & \text{if}\ \mathmob{\access(H, r, t) =
227: \truek}\\ & \text{and}\ \mathmob{H(r) = (\_, K)}\\
228: \mathmob{(H + \{r : (t, u)\}, \truek)}, & \text{if}\ \mathmob{\access(H, r, t) =
229: \truek}\\ & \text{and}\ \mathmob{H(r) = (\_, u)}\\
230: \mathmob{(H, \falsek)}, & \text{if}\ \mathmob{\access(H, r, t) = \falsek}
231: \end{array} \right.
232: \end{array}
233: \end{step}
234:
235: %%\vspace{11pt}
236: \begin{step}
237: \begin{array}{l}
238: \unlocked: \Heap \times
239: \HeapRef \times \ThreadRef \mapsto \Heap \times \Bool \\
240: \hspace{3.5cm} \unlocked(\mathmob{H, r, t}) =
241: \left \{
242: \begin{array}{ll}
243: \mathmob{(H + \{r : (\nullr, K)\}, \truek)}, & \text{if}\ \mathmob{\access(H, r, t) =
244: \truek}\ \\ & \text{and}\ \mathmob{H(r) = (\_, K)}\\
245: \mathmob{(H + \{r : (\nullr, u)\}, \truek)}, & \text{if}\ \mathmob{\access(H, r, t) =
246: \truek}\\ & \text{and}\ \mathmob{H(r) = (\_, u)}\\
247: \mathmob{(H, \falsek)}, & \text{if}\ \mathmob{\access(H, r, t) = \falsek}
248: \end{array} \right.
249: \end{array}
250: \end{step}
251:
252: %%\vspace{11pt}
253: Remember that unlocked references have $\nullr$ as their locking reference.
254:
255: Function \codeOf returns the code for a method $\mathmob{m}$ from a
256: given class or agent representation:
257:
258: \begin{step}
259: \begin{array}{rlll}
260: \codeOf: (\Var^* \times \Method \times \ServiceId^*) \times \MethodId
261: & \mapsto & \Var^* \times \InstructionSeq \\
262: \mathmob{\codeOf((\tilde x, M, \tilde S), m)} & = & \mathmob{M(m)}
263: \end{array}
264: \end{step}
265:
266: Function \codein returns the code closure for a set of methods. The
267: result is a code repository, built from another received as argument,
268: that is composed of the code for all the classes referenced in the set of methods.
269:
270: \begin{step}
271: \begin{array}{rlll}
272: \codein: \Code \times \Method & \mapsto & \Code\\
273: \mathmob{\codein(C, M \cdot (\tilde x, x = \newk\ X(\tilde v); P))} & = & \mathmob{\{X : C(X)\} +\codein(C, M \cdot (\tilde x, P))}\\
274: \mathmob{\codein(C, M \cdot (\tilde x, I; P))} & = & \mathmob{\codein(C, M \cdot (\tilde x, P))} & \text{if}\ \mathmob{I \not = x = \newk\ X(\tilde v);}\\
275: \mathmob{\codein(C, M \cdot (\tilde x, \epsilon))} & = & \mathmob{\codein(C, M)}\\
276: \mathmob{\codein(\emptyset)} & = & \emptyset
277: \end{array}
278: \end{step}
279:
280:
281:
282:
283: Function \evalseq returns the evaluation of a sequence of expressions,
284: each element being evaluated by the \evalone function. The evaluation
285: requires the knowledge of the state of the heap $\mathmob{H}$, the heap
286: reference of the thread computing the expression $\mathmob{r}$, and its
287: environment $\mathmob{B}$. The evaluation is fairly standard, however a particularity requires some closer attention.
288: A variable may contain a heap reference whose value is another
289: reference, which forces the resolution of the indirection.
290:
291: % ; and
292: % when the evaluation of an expression accesses a heap reference locked
293: % by some other thread, the function is recursively called until the
294: % value may be accessed.
295:
296: The value of a constant is given by the built-in \textsf{val}
297: function, and the result of the relational and arithmetic built-in
298: operations is given by the \textsf{bop} and
299: \textsf{uop} built-in functions.
300:
301: \begin{step}
302: \evalseq : (\Heap \times \ThreadRef \times \Environment \times
303: \Expression^*) & \mapsto & \Value^* \\
304: \mathmob{\evalseq(H, t, B, v\ \tilde v)} & = & \mathmob{\evalone(H, t, B, v)\ \evalseq(H, t, B, \tilde v)} \\
305: \mathmob{\evalseq(H, t, B, \epsilon)} & = & \mathmob{\epsilon}
306: \end{step}
307:
308: \begin{step}
309: \begin{array}{rlll}
310: \evalone : (\Heap \times \ThreadRef \times \Environment \times
311: \Expression) & \mapsto & \Value\\
312: \mathmob{\evalone(H, t, B, c)} & = & \textsf{val}(\mathmob{c}) \\
313: \mathmob{\evalone(H, t, B, \nullk)} & = & \nullr\\
314: \mathmob{\evalone(H, t, B, x)} & = & \textsf{val}(\mathmob{c}) & \text{if}\ \mathmob{B(x) = c} \\
315: \mathmob{\evalone(H, t, B, x)} & = & \nullr & \text{if}\ \mathmob{B(x) = \nullr}\\
316: \mathmob{\evalone(H, t, B, x)} & = & \mathmob{t'} & \text{if}\ \mathmob{B(x) = t'} \\
317: \mathmob{\evalone(H, t, B, x)} & = & \mathmob{r} & \text{if}\ \mathmob{B(x) = r}\ \text{and}\ \mathmob{H(r) = (\_, K)} \\
318: \mathmob{\evalone(H, t, B, x)} & = & \mathmob{u} & \text{if}\ \mathmob{B(x) = r}\ \text{and}\ \mathmob{H(r) = (\_, u)} \\
319: % \mathmob{\evalone(H, t, B, v\ eop\ v')} & = & \textsf{eop}(\mathmob{u, u'}) &
320: % \text{if}\ \mathmob{\evalone(H, t, B, v) = u}\ \\
321: % &&& \text{and}\ \mathmob{\evalone(H, t, B, v') = u'} \\
322: \mathmob{\evalone(H, t, B, e\ bop\ e')} & = & \textsf{bop}(\mathmob{u, u'}) \qquad& \text{if}\
323: \mathmob{\evalone(H, t, B, e) = u}\\
324: &&& \text{and}\ \mathmob{\evalone(H, t, B, e') = u'} \\
325: \mathmob{\evalone(H, t, B, uop\ e)} & = & \textsf{uop}(\mathmob{u}) & \text{if}\ \mathmob{\evalone(H, t, B, e) = u}\
326: \end{array}
327: \end{step}
328:
329: Function $\mathmob{\copyseq_{ab}}$ returns a copy of the closures for a sequence
330: of values located in the heap of an agent $\mathmob{a}$, plus all the code they
331: require. The new references created to duplicate the given closure
332: are located in the target agent $\mathmob{b}$. The function takes as arguments
333: the code repository $\mathmob{C}$ and heap $\mathmob{H}$ of the original agent $\mathmob{a}$, and the
334: sequence of values to be copied $\mathmob{\tilde u}$. The copy of each value is
335: computed by function $\mathmob{\copyone_{ab}}$.
336:
337: \begin{step}
338: \begin{array}{rlll}
339: \mathmob{\copyseq_{ab}}: \Code \times \Heap \times \Value^* & \mapsto & \Code \times \Heap \times \Value^* \\
340: \mathmob{\copyseq_{ab}(C, H, u\ \tilde u)} & = & \mathmob{(C' + C'', H' + H'', u' \tilde
341: u')} & \text{where}\ \mathmob{\copyone_{ab}(C, H, u) = (C', H', u')}\\
342: &&& \text{and}\ \mathmob{\copyseq_{ab}(C, H, \tilde u) = (C'', H'', \tilde u')} \\
343: \mathmob{\copyseq_{ab}(C, H, \epsilon)} & = & \mathmob{(\emptyset, \emptyset, \epsilon)}
344: \end{array}
345: \end{step}
346:
347: \begin{step}
348: \begin{array}{rlll}
349: \mathmob{\copyone_{ab}}: \Code \times \Heap \times \Value & \mapsto & \Code \times \Heap \times \Value \\
350: \mathmob{\copyone_{ab}(C, H, r@a)} & = & \mathmob{(\{X : C(X)\} + C', H' + \{r'@b :
351: (\nullr, (\falsek, \{\tilde x : \tilde u'\}, X)\}, r'@b))}\\
352: \end{array}
353: \end{step}
354:
355: %%\vspace{-25pt}
356: \begin{step}
357: \hspace{1.9cm}
358: \begin{array}{rlll}
359: &&& \text{if}\ \mathmob{H(r@a) = (\_, (\falsek, \{\tilde x : \tilde u\}, X))}\\
360: &&& \text{where}\ \mathmob{\copyseq_{ab}(C, H, \tilde u) = (C', H',
361: \tilde u')} \\
362: &&& \text{and}\ \mathmob{r'@b} \in \HeapRef\ \fresh \\
363: %%%%%%%%%%%%%%%%%%%%%
364: \mathmob{\copyone_{ab}(C, H, r@a)} & = & \mathmob{(\emptyset, \emptyset, r@a)}\ &
365: \text{if}\ \mathmob{H(r@a) = (\_, (\truek, \{\tilde x : \tilde u\}, X))} \\
366: %%%%%%%%%%%%%%%%%%%%%
367: \mathmob{\copyone_{ab}(C, H, r@a)} & = & \mathmob{(C', H' + \{r'@b : u'\}, r'@b)} & \text{if}\ \mathmob{H(r@a) = (\_, u)}\\
368: &&& \text{where}\ \mathmob{\copyone_{ab}(C, H, u) = (C', H', u')}\\
369: &&&\text{and}\ \mathmob{r'@b} \in \HeapRef\ \fresh \\
370: %%%%%%%%%%%%%%%%%%%%%%%5\\
371: \mathmob{\copyone_{ab}(C, H, r@a')} & = & \mathmob{(\emptyset,
372: \emptyset, r@a')}\ & \text{if}\ \mathmob{a' \not = a \not = b} \\
373: %%%%%%%%%%%%%%%%%%\\
374: \mathmob{\copyone_{ab}(C, H, c)} & = & \mathmob{(\emptyset, \emptyset, c)}
375: \end{array}
376: \end{step}
377:
378:
379:
380:
381:
382: The \run function places a set of pool of running threads in concurrent
383: execution.
384:
385: \begin{step}
386: \begin{array}{rlll}
387: \run: 2^{\RunningThread} & \mapsto & \Pool(\RunningThread)\\
388: \mathmob{\run(\{(t_1, Q_1, r_1), \dots, (t_n, Q_n, r_n)\})} & =& \mathmob{(t_1, Q_1, r_1) \conc \cdots \conc (t_n, Q_n, r_n)}
389: \end{array}
390: \end{step}
391:
392:
393:
394:
395: \subsection{The Initial and Final States}
396:
397: Based on the above definitions, we may write the syntax for a network
398: as follows:
399:
400: \begin{xalignat*}{2}
401: \mathmob{\calN} \grmeq & \mathmob{\calA, \ns} & \text{Network} \\
402: \mathmob{\calA} \grmeq & \mathmob{\calA \conc \calA} & \text{Concurrent agents} \\
403: \grmor & \mathmob{a(h, C,H,T,W)} & \text{Running agent} \\
404: \grmor & \mathmob{\zeroka} & \text{Terminated agent} \\
405: \mathmob{T} \grmeq & \mathmob{T \conc T} & \text{Concurrent threads} \\
406: \grmor & \mathmob{(t, Q, r)} & \text{Running thread}\\
407: %% \grmor & \notify(r) & \text{A Notifying Thread}\\
408: \grmor & \mathmob{\zerokt} & \text{Terminated thread}
409: \end{xalignat*}
410:
411: For the sake of simplicity we assume that agents run in a static
412: network with no failures. In other words, the set of available hosts, \Host,
413: is constant. Here we describe the
414: abstract machine from the point of view of the execution of one
415: agent. Thus, when we start running an agent, the network may already
416: have a pool of agents $\calA$ running concurrently and distributed among
417: the network nodes in the set $\Host$, together with the resolver $\ns$:
418:
419: %%\vspace{-6pt}
420: \begin{equation*}
421: \calA , \ns
422: \end{equation*}
423:
424: We launch a program ($\mathmob{\tilde D\ P}$) in the network by encapsulating its code
425: ($\mathmob{P}$) in
426: an agent that is placed in a host specified by the user.
427: %The code is
428: %followed by an \exitk instruction to terminate its execution. As we
429: %shall explain ahead, agents are daemons and must be explicitly
430: %terminated.
431: %
432: The code repository for the program is collected at compile-time with
433: function $\codeclo$ that we will defined ahead. Thus, when the agent
434: is launched into the network it already contains all the code it
435: requires. The initial state of the execution of a program with code
436: $\mathmob{\tilde D\ P}$ is thus:
437:
438: \begin{step}
439: \mathmob{a(h, \codeclo(\tilde D), \emptyset, \launchT(\emptyset, P, \nullr),\emptyset) \conc \calA, \ns}
440: \end{step}
441:
442: \noindent
443: where $\mathmob{a}$ is a fresh agent key, $\mathmob{h}$ is the local
444: host and $\mathmob{\launchT(B,P,r)}$ is a macro that creates a new
445: thread with an environment $\mathmob{B}$ (here $\emptyset$), a code
446: $\mathmob{P}$ (here $\mathmob{P}$) and a return reference
447: $\mathmob{r}$ (here $\nullr$):
448:
449: \begin{step}
450: \mathmob{a(h, C, H, \launchT(B, P, r) \conc T, W) \conc \calA, \calR} & \eqdef &\\
451: \mathmob{a(h, C, H + \{t : (t, \nullr)\}, (t, (B, P), r) \conc T, W) \conc \calA, \calR} && \qquad \mathmob{t} \in
452: \ThreadRef\ \fresh
453: \end{step}
454:
455: %%\vspace{-8pt}
456: Note that no heap reference is associated with the agent $\mathmob{a}$, since a
457: program does not provide any methods, nor has attributes. Moreover,
458: $\mathmob{a}$ is not registered in $\ns$, and thus is not accessible to the
459: network.
460: %
461: The registry is a precondition for an agent to migrate (further detail
462: in rule \rulename{Go}), and thus, \mob programs cannot migrate, just agents.
463:
464: Agents are daemons by default and must be explicitly terminated by the
465: \exitk instruction, which produces the terminated agent
466: $\mathmob{\zeroka}$. Thus, at the end of the program running in agent
467: $\mathmob{a}$, the configuration of the network will be of the form:
468:
469: \begin{step}
470: \zeroka \conc \calA', \ns'
471: \end{step}
472:
473: %%\vspace{-11pt}
474: Such an agent can thus be garbage collected and produce the state:
475:
476: \begin{step}
477: \calA', \ns'
478: \end{step}
479:
480: %%\vspace{-11pt}
481: \subsection{Code Collection}
482:
483: The compile-time code collection is defined by function $\codeclo: \Def^* \mapsto \Code$ that
484: returns a code repository with all the code required by a sequence of class and
485: agent definitions. We present the function in a case by case analysis.
486:
487: A service specifies an interface implemented by some \mob agent.
488: Service definitions are used to supply information to the type-system.
489: Type-checking of a \mob program is performed at compile-time by
490: matching the inferred types for services required or implemented by
491: the agents with their definitions kept in the resolver. If the service
492: is required by the program or if the program implements a known
493: service in the network then its inferred type must match the interface
494: for the service kept in the resolver. If the service is introduced for
495: the first time by the program (an interface for it does not yet exist
496: in the resolver) then the type inferred for the service will become
497: the adopted interface for the service as registered in the resolver.
498: So, when the agent is created, the $\mathmob{SNS}$ map is updated by
499: adding the reference of the agent to every entry associated to a
500: one of the implemented services.
501: %
502: Anyway, these are handled at compile time and there is no need for
503: them in the abstract machine.
504:
505: \begin{step}
506: \mathmob{\codeclo(\servicek\ S\ \{ \tilde m\}\ \tilde D)} & = & \mathmob{\codeclo(\tilde D)}
507: \end{step}
508:
509: Simple classes define abstract data-types and we call their instances
510: \emph{objects}. The entry in the code repository associated with this
511: definition contains a closure with slots for the code for all the
512: classes and agents that are required by this class, its attributes,
513: the code for its methods, and an empty sequence of implemented
514: services, since an object does not provide any services. Remember that
515: \falsek\ indicates that the entry contains the code of a class.
516:
517: \begin{step}
518: \begin{array}{rlll}
519: \mathmob{\codeclo(\classk\ X(\tilde x)\ \{ m_1 ( \tilde{x}_1 )\ \{\ P_1\ \} \dots m_n ( \tilde{x}_n
520: )\ \{\ P_n\ \} \}\ \tilde D)} & = & \\
521: \mathmob{\{X: (\falsek, \tilde{x}, M', \codein(M'), \epsilon) \} +
522: \codeclo(\tilde D)}
523: \end{array}
524: \end{step}
525:
526: \noindent
527: where $\mathmob{M' = \{m_1 : (\tilde{x}_1,P_1), \dots, m_n : (\tilde{x}_n,P_n)\}}$.
528:
529:
530:
531: Some classes are special in the fact that they represent full computations. We
532: call their instances \emph{agents}, and we use a different
533: keyword to differentiate them. Otherwise, the definition of an agent is very much
534: like that of a regular class, it contains the code for all the
535: classes and agents required, the attributes, the code for the methods
536: and indicates which services are provided by the agent.
537:
538: The \requiresk keyword supplies information to the type-system,
539: indicating which services are required by the agent and that their
540: uses must be checked against the definitions in the $\mathmob{SNS}$.
541: The \implementsk keyword does not only supply information to the
542: type-system, but also states which service entries must be updated
543: whenever an instance of the agent is created (rule
544: \rulename{NewAgent}). To hold this information when necessary, we
545: keep this sequence in the agent's code closure.
546:
547: \begin{step}
548: \begin{array}{rlll}
549: \mathmob{\codeclo(\agentk\ X(\tilde x)\ \implementsk\ \tilde S\
550: \requiresk\ \tilde S'\ \{ m_1 ( \tilde{x}_1 )\ \{\ P_1\ \} \dots m_n ( \tilde{x}_n
551: )\ \{\ P_n\ \} \}\ \tilde D)} & = & \\
552: \mathmob{\{X: (\truek, \tilde{x}, M', \codein(M'), \tilde S) \} +
553: \codeclo(\tilde D)}
554: \end{array}
555: \end{step}
556:
557: \noindent
558: where $\mathmob{M' = \{m_1 : (\tilde{x}_1,P_1), \dots, m_n : (\tilde{x}_n,P_n)\}}$.
559:
560: Note that agents may not always implement or require services and thus
561: both $\mathmob{\tilde S}$ or $\mathmob{\tilde S'}$ may be empty
562: sequences.
563:
564:
565: The \requiresk\ keyword can be also used by itself to indicate which are
566: the services required by a program. Once again this only provides
567: information to the compile time type checking, and thus there is no
568: need to pass it to the run-time. Here we also present the base case
569: for the recursion.
570:
571: \begin{step}
572: \begin{array}{rlll}
573: \mathmob{\codeclo(\requiresk\ \tilde S\ \tilde D)} & = & \mathmob{\codeclo(\tilde D)}\\
574: \mathmob{\codeclo(\epsilon)} & = & \emptyset
575: \end{array}
576: \end{step}
577:
578: \subsection{The Congruence Rules}
579: The computation in the abstract machine is driven by a set of
580: \emph{reduction rules} that operate over the thread or the agent at
581: the most left in the respective pool.
582: %
583: Thus, in order to be able to commute, associate and garbage collect threads and
584: agents in their pools, we need a set of \emph{congruence rules}. These
585: will allow for the re-writing of both pools, into semantically
586: equivalent ones, where the configuration is accordingly to the
587: reduction rules to be applied.
588: %
589: The congruence rules for a pool of agents are:
590: %, until a reduction rule may be
591: %applied. Thus, we define $\equiv$ as the smallest congruence
592: %relation over a \mob agent, defined by the following rules:
593:
594: \begin{multicols}{2}
595: \crule{
596: \rulename{AgentSwap}
597: }{
598: \calA \conc \calA'
599: }{
600: \calA' \conc \calA
601: }
602:
603: \crule{
604: \rulename{AgentAssoc}
605: }{
606: \calA \conc (\calA' \conc \calA'')
607: }{
608: (\calA \conc \calA') \conc \calA''
609: }
610:
611: \crule{
612: \rulename{AgentGC}
613: }{
614: \zeroka \conc \calA
615: }{
616: \calA
617: }
618:
619: % \pcrule{
620: % \rulename{AgentAlpha}
621: % }{
622: % \calA \eqva \calA'
623: % }{
624: % \calA
625: % }{
626: % \calA'
627: % }
628:
629: \end{multicols}
630: \bigskip
631:
632: %&
633: %\end{tabular}
634:
635: The congruence rules for threads for threads are:
636: %Notice that no garbage collection rule is required, since the
637: %reduction rules collect all terminated threads.
638:
639: \begin{multicols}{2}
640: \crule{
641: \rulename{ThreadSwap}
642: }{
643: T \conc T'
644: }{
645: T' \conc T
646: }
647:
648: \crule{
649: \rulename{ThreadAssoc}
650: }{
651: T \conc (T' \conc T'')
652: }{
653: (T \conc T') \conc T''
654: }
655:
656: \crule{
657: \rulename{ThreadGC}
658: }{
659: \zerokt \conc T
660: }{
661: T
662: }
663:
664: %\pcrule{
665: % \rulename{ThreadAlpha}
666: %}{
667: % T \eqva T'
668: %}{
669: % T
670: %}{
671: % T'
672: %}
673: \end{multicols}
674: \bigskip
675:
676: Rule \rulename{ThreadInAgent} allows the use of the congruence rules
677: for threads in the layer of agent states:
678:
679: \pcrule{
680: \rulename{ThreadInAgent}
681: }{
682: T \equiv T'
683: }{
684: a(h, C, H, T \conc T'', W)
685: }{
686: a(h, C, H, T' \conc T'', W)
687: }
688:
689:
690: %$\eqva$ denotes alpha-congruence relation, defined as usual.
691:
692:
693: \subsection{The Reduction Rules}
694: \label{sec:vm:rrules}
695:
696: Each \mob instruction requires at least one machine transition to be
697: processed. The rules are written using the usual forms in the
698: definition of operational semantics.
699: %
700: The rules are of two forms: the first are denoted by
701:
702: \begin{step}
703: \calA \reduces \calA'
704: \end{step}
705:
706: %%\vspace{-11pt}
707: \noindent
708: and operate simply over a pool of
709: threads. They are used whenever the operation to be performed does
710: not modify the name resolver $\ns$.
711: %
712: The second, denoted by
713:
714: \begin{step}
715: \calA, \ns \reduces \calA', \ns'
716: \end{step}
717:
718: %%\vspace{-11pt}
719: \noindent
720: include the resolver and are used whenever the operation requests data
721: from the resolver or modifies its contents in some way.
722: %
723: To widen the scope of the first form of reductions to whole network we define rule
724: rule \rulename{AgentRed}. This allows us to define rules focused on one agent
725: alone, whenever the remainder of the network is not affected.
726:
727:
728: \pcrrule{
729: \rulename{AgentRed}
730: }{
731: \quad \incnrule{\calA}{\calA''}
732: }{
733: \calA \conc \calA', \ns
734: }{
735: \calA'' \conc \calA', \ns
736: }
737:
738:
739: Rule \rulename{Cong} allows reduction to occur under structural
740: congruence:
741:
742: \pcrrule{
743: \rulename{Cong}
744: }{
745: \calA \equiv \calA' \quad
746: \incnrule{\calA', \ns}{\calA'', \ns''} \quad
747: \calA'' \equiv \calA''' \quad
748: }{
749: \calA', \ns
750: } {
751: \calA''', \ns''
752: }
753:
754:
755:
756: Next we provide the rules for the language constructs.
757:
758:
759:
760: \subsubsection*{Creation of Objects and Agents}
761:
762: The instantiation of a regular class creates a new object. It reserves
763: a block of heap space for a closure representing the object. The
764: closure holds the values of the attributes, a special attribute
765: \selfk, that is a reference to the object itself, and keeps a link for the code
766: of the class.
767:
768: \pnrule{
769: \rulename{NewObject}
770: }{
771: \evalseq(H, t, B, \tilde v) = \tilde u \quad
772: C(X) = (\falsek, \tilde x, \_, \_, \epsilon) \quad
773: r' \in \HeapRef\ \fresh
774: }{
775: a(h, C, H, (t, (B, x = \newk\ X (\tilde v)\ P) :: Q, r) \conc T, W)
776: }{
777: a(h, C, H+\{r':(\nullr, (\falsek, \{\selfk : r', \tilde x : \tilde u\},
778: X))\}, (t, (B + \{x : r'\}, P) :: Q, r) \conc T, W)
779: }
780:
781:
782: Agents in \mob{} are similar to objects, but they have an execution
783: unit associated to them. A new agent is placed in the network's pool
784: of agents. In the beginning, its location is the same as the agent
785: that created it. It is initiated with a heap containing its closure
786: at $\mathmob{r'}$ (as in the \rulename{NewObject} rule). A new thread
787: is created to execute the code of the agent's \maink\ method with the
788: agent's environment $\mathmob{B'}$, given by the attributes and
789: \selfk. \maink is a required method that defines the agent's initial
790: behavior, an approach common to many programming languages. The
791: parent agent keeps a binding to the reference $\mathmob{r'@b}$ of the
792: created agent in $\mathmob{x}$.
793:
794: The code repository for the new agent is
795: composed of the code required
796: by the values given as argument to the constructor ($\mathmob{C'}$),
797: plus all the code required by the agent definition ($\{\mathmob{X : C(X)}\}$).
798:
799: \pppcnnrule{
800: \rulename{NewAgent}
801: }{
802: \evalseq(H, t, B, \tilde v) = \tilde u \quad
803: \copyseq_{ab}(C, H, \tilde u) = (C', H', \tilde u') \quad
804: C(X) = (\truek, \tilde x, M, \_, S_1\ \cdots\ S_k)
805: }{
806: \codeOf(C(X), \maink) = (\epsilon, P') \quad
807: B' = \{\selfk : r', \tilde x : \tilde u'\} \quad
808: b \in \AgentName\ \text{and}\ r'@b \in \HeapRef\ \fresh
809: }{
810: SNS(S_1) = (\alpha_1 , K_1)\ \cdots\
811: SNS(S_k) = (\alpha_k , K_k) \quad K_1 = \{ r@_i \conc i \in \{1,
812: \dots, n\}\}\ \cdots\ K_k = \{ r@_i \conc i \in \{1, \dots, m\}\}
813: }{
814: a(h, C, H, (t, (B, x = \newk\ X(\tilde v)\ P) :: Q, r) \conc T, W) \conc
815: \calA, (ANS, SNS)
816: }{
817: a(h, C, H, (t, (B+\{x:r'@b\}, P) :: Q, r) \conc T, W)\ \conc
818: }{
819: b(h, C' + \{ X : C(X)\}, H' + \{ r': (\nullr, (\truek, B', X))\}, \launchT(B', P', \nullr), \emptyset) \conc \calA,
820: }{
821: % , r'':(r'', \nullr)\}, (r'', B', y = \selfk.\maink(), \epsilon), \emptyset) \conc \\
822: (ANS + \{r'@b : h\}, SNS + \{S_1 : (\alpha_1, K_1 + \{r'@b\}),
823: \dots, S_k: (\alpha_k, K_k + \{r'@b\})\}
824: }
825: %{
826: %SNS + \{S_1 : (\alpha_1, \{r@a_{1_1}, \dots, r@a_{1_m}, r'@b\}), \dots, S_n : (\alpha_n, \{r@a_{n_1}, \dots, r@a_{n_k}, r'@b\})\}
827: %}
828:
829: \noindent
830: where $\mathmob{k}$ denotes the number of services implemented by the
831: agent, and $\mathmob{n}$ and $\mathmob{m}$ denote, respectively, the
832: number of implementations of services $\mathmob{S_1}$ and
833: $\mathmob{S_k}$ in the network.
834:
835:
836: Note that both maps of the resolver are updated. The reference
837: $\mathmob{r'@b}$ holding the agent's closure will be the key in the
838: $\mathmob{ANS}$ map to locate the agent's current host $\mathmob{(r'@b
839: : h)}$. Every entry of the $\mathmob{SNS}$ map corresponding to each
840: of the agent's implemented services given as $\mathmob K_1, \dots,
841: \mathmob K_n$, will be updated with $\mathmob{r'@b}$, e. g.,
842: $\mathmob{(S_1 : (\alpha_1, K_1 + \{r'@b\}))}$ for the implemented
843: service $\mathmob{S_1}$.
844:
845: \subsubsection*{Multi-threaded Agents}
846:
847: The \forkk{} instruction allows the explicit creation of a new thread
848: by the programmer. The new thread inherits the environment of its
849: creator and a handle is returned to the caller. This handle is
850: associated to a newly created heap reference, that contains a $\nullr$
851: value and is used for inter-thread synchronization. The
852: synchronization is achieved by granting the thread exclusive access to
853: itself (see \rulename{Join} rules).
854:
855: \pnrule{
856: \rulename{Fork}
857: }{
858: t' \in \ThreadRef\ \fresh
859: }{
860: a(h, C, H, (t, (B, x = \forkk\ \{ P' \}\ ; P) :: Q, r) \conc T, W)
861: }{
862: a(h, C, H + \{t' : (t', \nullr) \}, (t, (B+\{x:t'\}, P) :: Q, r) \conc
863: (t', (B, P'), \nullr) \conc T, W)
864: }
865:
866:
867:
868:
869:
870: A thread can suspend waiting for the completion of another thread
871: using the instruction \joink{}. The instruction uses the thread's
872: handle returned by a previous \forkk{} statement. While it is running,
873: a given thread has a reference in the heap associated to it
874: ($\mathmob{t'}$). In this scenario, any other thread that tries to
875: perform the \joink operation will suspend on $\mathmob{t'}$.
876:
877:
878: \prule{
879: \rulename{JoinSuspend}
880: }{
881: \evalone(H, t, B, x) = t' \quad
882: H(t') = (t', \nullr) \quad t' \not = t
883: }{
884: a(h, C, H, (t, (B, \joink(x)\ ; P) :: Q, r) \conc T, W)
885: }{
886: a(h, C, H, T, W + \{t' : (t, (B, P) :: Q, r)\})
887: }
888:
889: If the thread on which the synchronization is performed is no longer
890: running, the reference associated to it is no longer locked. In this
891: case, the operation succeeds and the execution continues.
892:
893: \prule{
894: \rulename{Join}
895: }{
896: \evalone(H, t, B, x) = t' \quad (t = t'\ \vee\ H(t') = (\nullr, \nullr))
897: }{
898: a(h, C, H, (t, (B, \joink(x)\ ; P) :: Q, r) \conc T, W)
899: }{
900: a(h, C, H, (t, (B, P) :: Q, r) \conc T, W)
901: }
902:
903: If the code currently under execution terminates and the stack has no
904: more elements, the thread has run out of code to execute and
905: terminates, as in rule \rulename{End}. To give a more expressive
906: writing of the reduction rules involving synchronization, we define the
907: \notify macro. The macro represents a thread that wakes up all the
908: threads suspended on reference $\mathmob{r}$.
909:
910: %\vspace{-22pt}
911: \begin{center}
912: \macrorule{
913: }{
914: \notify(r)
915: }{
916: (\nullr, \epsilon, r)
917: }
918: \end{center}
919: %%\vspace{-11pt}
920:
921: When a thread terminates its execution it uses
922: this macro to wake up all the threads suspended on it.
923:
924: % We place
925: % $\nullr$ in the result slot, since every thread returning a result
926: % must terminate with a \returnk instruction and cannot reach this
927: % state.
928:
929:
930:
931:
932: \cnrule{
933: \rulename{End}
934: }{
935: % t \in dom(H)
936: %}{
937: a(h, C, H, (t, (B, \epsilon), \nullr) \conc T, W)
938: }{
939: a(h, C, H, \notify(t) \conc T, W)
940: }
941:
942:
943: The \rulename{NotifyThread} rule wakes up every thread
944: suspended on the given reference. $\mathmob{W(r)}$ is the set of threads
945: suspended on the reference $\mathmob{r}$.
946:
947:
948: \cnrule{
949: \rulename{NotifyThread}
950: }{
951: a(h, C, H, \notify(r) \conc T, W)
952: }{
953: a(h, C, H, T \conc \run(W(r)), W|_{\dom(W)- \{r\}})
954: }
955:
956: %% \prule{
957: %% \rulename{Release}
958: %% }{
959: %% H(\lockable{r'}{}) = \_
960: %% }{
961: %% a(h, C, H, T, W + \{r' : (r,B,I,Q)\})
962: %% }{
963: %% a(h, C, H, (r,B,I,Q) \conc T, W)
964: %% }
965:
966:
967: Explicit synchronization is also supported in \mob by the \waitk and \notifyk instructionsm, that
968: The first allows a thread to suspend on a reference, while the second is the language support to create to
969: a \notify thread, and thus wake every thread suspended on the given reference.
970:
971: \prule{
972: \rulename{Wait}
973: }{
974: \evalone(H, t, B, x) = r' \quad r' \not = t
975: }{
976: a(h, C, H, (t, (B, \waitk(x)\ ; P) :: Q, r) \conc T, W)
977: }{
978: a(h, C, H, T, W + \{r' : (t, (B, P) :: Q, r)\})
979: }
980:
981: \prule{
982: \rulename{Notify}
983: }{
984: \evalone(H, t, B, x) = r'
985: }{
986: a(h, C, H, (t, (B, \notifyk(x)\ ; P) :: Q, r) \conc T, W)
987: }{
988: a(h, C, H, \notify(r) \conc (t, (B, P) :: Q, r) \conc T, W)
989: }
990:
991:
992:
993: \subsubsection*{Agent Movement and Discovery}
994:
995: An agent may move to another host, changing the topology of the
996: distributed computation, rule \rulename{Go}. The original host will
997: proceed without the agent, and the later will resume its
998: execution concurrently with the agents at the target host. In order to
999: migrate an agent must be registered in the $\mathmob{ANS}$ map.
1000: %
1001: The reference associated to the agent in $\Ans$ is discovered by following the
1002: binding for the \selfk identifier. This can be done, since the \gok
1003: instruction can only appear inside the body of an agent definition's
1004: method.
1005:
1006: \pnrule{
1007: \rulename{Go}
1008: }{
1009: \evalone(H, t, B, v) = h' \quad
1010: B(\selfk) = r'@a \quad
1011: r'@a \in \dom(ANS) \quad
1012: h' \in \Host \quad
1013: }{
1014: a(h, C, H, (t, (B, \gok(v)\ ; P) :: Q, r) \conc T, W)\ |\ \calA, (ANS, SNS)
1015: }{
1016: a(h', C, H, (t, (B, P) :: Q, r) \conc T, W)\ |\ \calA, (ANS + \{r'@a : h'\}, SNS)
1017: }
1018:
1019: An agent may invoke a method in another agent only if it has a binding
1020: for the target agent's closure. Agent discovery in \mob is
1021: service-oriented, meaning that agents are discovered for the services
1022: they implement. The instruction $\bindk$ consults the network
1023: resolver and retrieves a heap reference, $\mathmob{r'@b}$, associated
1024: with an agent that implements a service $\mathmob{S}$ and is presently
1025: running in host $\mathmob{h}$. Note that an agent cannot obtain a
1026: binding for itself.
1027:
1028: \ppnrule{
1029: \rulename{Bind}
1030: }{
1031: \evalone(H, t, B, v) = h' \quad
1032: % B(x) = b \quad
1033: \Sns(S) = (\alpha, \{r@a_1, \dots, r@a_n\})
1034: }{
1035: \exists r'@b \in \{r@a_1, \dots, r@a_n\}\ :\ ANS(r'@b) = h'\ \wedge\ b \not = a
1036: }{
1037: a(h, C, H, (t, (B, x = \bindk(S\ v)\ ; P) :: Q, r) \conc T, W)\ |\ \calA, (\Ans, \Sns)
1038: }{
1039: a(h, C, H, (t, (B + \{x : r'@b\}, P) :: Q, r) \conc T, W)\ |\ \calA, (\Ans, \Sns)
1040: }
1041:
1042: However, sometimes the host where the agent is running is irrelevant
1043: and is not taken is consideration when the reference is picked. In
1044: both these rules, the criteria used in choosing an agent is left to
1045: the implementation.
1046:
1047: \pnrule{
1048: \rulename{BindAny}
1049: }{
1050: SNS(S) = (\alpha, \{r@a_1, \dots, r@a_n\}) \quad
1051: \exists r'@b \in \{r@a_1, \dots, r@a_n\}\ :\ b \not = a
1052: }{
1053: a(h, C, H, (t, (B, x = \bindk(S)\ ; P) :: Q, r) \conc T, W)\ |\ \calA, (ANS, SNS)
1054: }{
1055: a(h, C, H, (t, (B + \{x : r'@b\}, P) :: Q, r) \conc T, W)\ |\ \calA, (ANS, SNS)
1056: }
1057: %%\vspace{-11pt}
1058:
1059: \subsubsection*{Current Host}
1060:
1061: The next rule returns the host where the agent is running.
1062:
1063: \cnrule{
1064: \rulename{Host}
1065: }{
1066: a(h, C, H, (t, (B, x = \hostk()\ ; P) :: Q, r) \conc T, W)
1067: }{
1068: a(h, C, H, (t, (B + \{x : h\}, P) :: Q, r) \conc T, W)
1069: }
1070: %%\vspace{-11pt}
1071:
1072: \subsubsection*{Local Method Invocation}
1073:
1074: Method invocation in objects can only be done within an agent. All
1075: objects are encapsulated within agents and thus, invoking a method in
1076: an object located in the address space of some other agent is not
1077: possible, unless the target agent's interface provides some means to
1078: access the object. Methods of the agent itself can of course be
1079: invoked both from within the agent, and from other remote agents.
1080: Rule \rulename{LocalInvoke} applies to the scenario of local
1081: invocations, both in objects and in agents. We guarantee this
1082: restriction by qualifying the reference with its location.
1083:
1084: The method invocation simulates a call stack by suspending the current
1085: thread, and by creating a new one, bound to the same heap reference
1086: ($\mathmob{t}$), to execute the body of the method. The environment
1087: of the new thread is obtained from the target object's environment
1088: modified with the values assigned to the method's parameters. The
1089: result location is a fresh heap reference $\mathmob{r''}$, locked by the current thread
1090: and holding no value $\mathmob{(r'' : (t, \nullr))}$.
1091: %%
1092: The current thread is then suspended on that reference $\mathmob{r''}$, waiting for
1093: the result. Its environment is modified by the binding of variable $\mathmob{x}$
1094: to $\mathmob{r''}$, so that $\mathmob{x}$ holds the returned value once the current thread
1095: resumes its execution.
1096: %
1097: By associating the new thread to the same heap reference as the one that invokes the method,
1098: the former gains access to all the resources locked by the
1099: later.
1100:
1101:
1102: \uppnrule{
1103: \rulename{LocalInvoke}
1104: }{
1105: \evalseq(H, t, B, \tilde v) = \tilde u \quad
1106: B(o)= r'@a \quad
1107: \access(H, r'@a, t) = \truek \quad
1108: H(r'@a) = (\_, (\_, B', X))
1109: }{
1110: \codeOf(C(X), m) = (\tilde{x}, P') \quad
1111: r'' \in \HeapRef\ \fresh
1112: }{
1113: a(h, C, H, (t, (B, x = o.m(\tilde v)\ ; P) :: Q, r) \conc T, W)
1114: }{
1115: a(h, C, H+\{r'' : (t, \nullr)\}, (t, (B' + \{\tilde x : \tilde
1116: u\}, P'), r''), W + \{ r'' : (t, (B + \{x : r''\}, P) :: Q, r) \})
1117: }
1118:
1119: Note that elements of the heap of the form $\mathmob{r'' : (t,
1120: \nullr)}$ (with $\mathmob r \not \in \ThreadRef$ and $\mathmob t
1121: \not = \nullr$) denote uniquely references waiting for results. This
1122: will be important when encoding \mob to the target process calculus.
1123:
1124: Rule \rulename{LocalInvokeLocked} states that if the object on which
1125: the method its to be invoked is locked by another thread, the current
1126: thread suspends on that object.
1127:
1128: %%\vspace{-11pt}
1129: \uprule{
1130: \rulename{LocalInvokeLocked}
1131: }{
1132: B(o)= r'@a \quad
1133: \access(H, r'@a, t) = \falsek \quad
1134: }{
1135: a(h, C, H, (t, (B, x = o.m(\tilde v)\ ; P) :: Q, r) \conc T, W)
1136: }{
1137: a(h, C, H, T, W + \{r' : (t, (B, x = o.m(\tilde v)\ ; P) :: Q, r)\})
1138: }
1139:
1140: The \returnk instruction terminates the execution of the current
1141: thread, places the result in the dedicated heap reference
1142: $\mathmob{r}$, releasing its lock, and spawns a \notify thread to wake
1143: up the thread waiting for the result.
1144: %%
1145: Thus, the image of $\mathmob{r}$ in the heap will now hold the returned
1146: value $\mathmob{(\nullr, u)}$.
1147: %%
1148: The \notify thread will cause any thread in $\mathmob{W}$ waiting on
1149: $\mathmob{r}$ to resume, simulating the call stack.
1150:
1151: %%\vspace{-11pt}
1152: \uprule{
1153: \rulename{LocalReturn}
1154: }{
1155: % B(x) = v
1156: \evalone(H, t, B, v) = u
1157: }{
1158: a(h, C, H, (t, (B, \returnk(v)\ ; P) :: Q, r) \conc T, W) %com I?
1159: }{
1160: a(h, C, H + \{r : (\nullr, u)\}, \notify(r) \conc T, W)
1161: }
1162:
1163: %%\vspace{-11pt}
1164: \subsubsection*{Remote Method Invocation in an Agent}
1165:
1166: As in local method invocations, remote method invocations always
1167: launch a new thread ($\mathmob{t'}$) in the target agent to execute
1168: the corresponding code\footnote{From a practical point of view, the
1169: maximum number of threads allowed for one agent is
1170: implementation-dependent. Note that remote invocations are not
1171: anonymous, the invoking agent may be identified, since the agent's
1172: name qualifies the reference $\mathmob{r''@a}$. This means that
1173: precautions to avoid abusive use from other agents may be achieved
1174: by adding a set of new preconditions to the rule. This, can be used
1175: for instance to avoid denial-of-service attacks.}. The difference
1176: lies in the fact that the result slot of the thread,
1177: $\mathmob{r''@a}$, is now a heap reference from the heap of the
1178: calling agent. Moreover, this thread in the case of remote
1179: invocations, does not execute the body of the method, but rather
1180: triggers a local invocation. This allows for the application of the
1181: \rulename{LocalInvoke} reduction rule to execute the method locally at the remote agent.
1182:
1183: The values assigned to the method's parameters are passed by value,
1184: except agents that are passed by reference\footnote{Passing them by
1185: value would constitute a new form of migration.}. A copy of the
1186: arguments must be sent to the target agent and since this may include
1187: objects, a closure with the values and the classes they use must be
1188: constructed, using function \copyseq. The local invocation performed
1189: at the target agent has arguments $\mathmob{\tilde x}$, bound to the
1190: clones of the original values assigned to the arguments in the calling
1191: thread.
1192:
1193: %%\vspace{-11pt}
1194: \ppcnnrule{
1195: \rulename{RemoteInvoke}
1196: }{
1197: \evalseq(H, t, B, \tilde v) = \tilde u \quad
1198: B(o)= \at{r'}{b} \quad
1199: % \access(H', r'@b, t@a) = \truek \quad
1200: H'(\at{r'}{b}) = (\_, (\truek, B', X))
1201: }{
1202: \copyseq_{ab}(C, H, \tilde u) = (C'', H'', \tilde u') \quad
1203: % |\tilde u'| = |\tilde x| \quad
1204: % \codeOf(C'(A), m) = (\tilde{x})P' \quad
1205: r''@a \in\ \HeapRef\ \fresh
1206: }{
1207: (a(h, C, H, (t, (B, x = o.m(\tilde v)\ ; P) :: Q, r) \conc\ T, W) \conc\ b(h', C', H', T', W')) \conc \calA, \ns
1208: }{
1209: (a(h, C, H + \{r'' : (t, \nullr)\}, T, W + \{r'' : (t, (B + \{x :
1210: r''\}, P) :: Q, r) \}) \conc\
1211: }{
1212: % b(h', C' + C'', H' + H'' + \{t' : (t', \nullr)\}, (t', (\{x_1 :
1213: % u'_1, \dots, x_n : u'_n\}, x = o.m(x_1\ \dots\ x_n) ; \returnk\ x),
1214: % r''@a) \conc\ T', W') \conc \calA, \ns
1215: b(h', C' + C'', H' + H'', \launchT(\{\selfk: r', \tilde x : \tilde u'\}, x = \selfk.m(\tilde x) ; \returnk\ x, r''@a) \conc\ T', W')) \conc \calA, \ns
1216: }
1217:
1218:
1219:
1220: % If the agent on which the method is to be invoked is locked, the
1221: % thread to be launched is placed in its set of suspended threads,
1222: % instead of its pool of running threads. This guarantees that the thread
1223: % will not begin its execution until the agent is freed.
1224:
1225: % \newpage
1226: % \ppcnnrule{
1227: % \rulename{RemoteInvokeLocked}
1228: % }{
1229: % \evalseq(H, t, B, \tilde v) = \tilde u \quad
1230: % B(o)= r'@b \quad
1231: % \access(H', r'@b, t@a) = \falsek \quad
1232: % H'(\at{r'}{b}) = (B', A)
1233: % }{
1234: % \copyseq_{ab}(C, H, \tilde u) = (C'', H'', \tilde u') \quad
1235: % \codeOf(C'(A), m) = (\tilde{x})P' \quad
1236: % t'@b\ \text{and}\ r''@a\ \fresh
1237: % }{
1238: % a(h, C, H, (t, (B, x = o.m(\tilde v)\ ; P) :: Q, r) \conc\ T, W) \conc\ b(h', C', H', T', W') \conc \calA, \ns
1239: % }{
1240: % a(h, C, H + \{r'' : (\nullr, \nullr)\}, T, W + \{r'' : (t, (B +
1241: % \{x : r''\}, P) :: Q, r) \}) \conc\
1242: % }{
1243: % b(h', C' + C'', H' + H'' + \{t' : (t', \nullr)\}, T', W' + \{r' :
1244: % (t', (B' + \{\tilde x : \tilde u'\}, P'), r''@a)\}) \conc \calA, \ns
1245: % }
1246:
1247:
1248: The return value from a remote method invocation must be placed in a
1249: reference in the heap of the calling agent. This value may include
1250: objects, and thus a closure with the value and the classes it uses
1251: must be constructed. Finally, a \notify thread is placed in the pool of
1252: threads of the calling agent, that will trigger the \rulename{Notify}
1253: rule and awake the thread that performed the invocation.
1254:
1255:
1256: \pnrule{
1257: \rulename{RemoteReturn}
1258: }{
1259: \evalone(H, t, B, v) = u \quad
1260: \copyone_{ab}(C, H, u) = (C'',H'', u')
1261: }{
1262: (a(h, C, H, (t, (B, \returnk(v)\ ; P) :: Q, r@b) \conc T, W) \conc\
1263: b(h', C', H', T', W')) \conc \calA, \ns
1264: }{
1265: (a(h, C, H, T, W) \conc
1266: b(h', C'+C'', H'+H''+\{r : (\nullr, u')\}, \notify(r) \conc T', W')) \conc \calA, \ns
1267: }
1268:
1269: \subsubsection*{Exclusive Access}
1270:
1271: Values in the heap may be shared by several threads, therefore it is
1272: necessary to supply a mechanism to ensure that a thread may gain
1273: exclusive access to a given value. The \lockk instruction gives
1274: exclusive access to a reference to the current thread. The operation
1275: is only allowed if no other thread has exclusive access over the
1276: reference. Note that although the inspected agent is the only one
1277: under the rule's scope, we qualify $\mathmob{r'}$ with its location.
1278: This is to point out that exclusive access operations can only be
1279: performed on references owned by the agent.
1280:
1281: \prule{
1282: \rulename{Lock}
1283: }{
1284: \evalone(H, t, B, x) = r'@a \quad
1285: % B(x) = r' \quad
1286: \locked(H, r'@a, t) = (H', \truek)
1287: }{
1288: a(h, C, H, (t, (B, \lockk(x)\ ; P) :: Q, r)\ |\ T, W)
1289: }{
1290: a(h, C, H', (t, (B, P) :: Q, r)\ |\ T, W)
1291: }
1292:
1293: A thread that tries to obtain the lock of a locked reference suspends on the
1294: reference.
1295:
1296: \uprule{
1297: \rulename{LockFailed}
1298: }{
1299: \evalone(H, t, B, x) = r'@a \quad
1300: % B(x) = r' \quad
1301: \locked(H, r'@a, t) = (H, \falsek)
1302: }{
1303: a(h, C, H, (t, (B, \lockk(x)\ ; P) :: Q, r)\ |\ T, W)
1304: }{
1305: a(h, C, H, T, W + \{r'@a : (t, (B, \lockk(x)\ ; P) :: Q, r)\})
1306: }
1307:
1308: Instruction \unlockk returns the public access to a given heap reference and
1309: notifies every thread suspended on it, so that they may
1310: resume their execution.
1311:
1312:
1313: \uprule{
1314: \rulename{Unlock}
1315: }{
1316: \evalone(H, t, B, x) = r'@a \quad
1317: % B(x) = r' \quad
1318: \unlocked(H, r'@a, t) = (H', \truek)
1319: % H(r') = (r, K) \vee H(r') = (\nullr, K)
1320: }{
1321: a(h, C, H, (t, (B, \unlockk(x)\ ; P) :: Q, r)\ |\ T, W)
1322: }{
1323: a(h, C, H', \notify(r'@a) \conc (t, (B, P) :: Q, r) \conc T, W)
1324: }
1325:
1326: If a thread tries to
1327: free an object without having exclusive access to it, the operation is
1328: ignored.
1329:
1330: \prule{
1331: \rulename{UnlockIgnore}
1332: }{
1333: \evalone(H, t, B, x) = r'@a \quad
1334: % B(x) = r' \quad
1335: \unlocked(H, r'@a, t) = (H, \falsek)
1336: }{
1337: a(h, C, H, (t, (B, \unlockk(x)\ ; P) :: Q, r) \conc T, W)
1338: }{
1339: a(h, C, H, (t, (B, P) :: Q, r)\ |\ T, W)
1340: }
1341:
1342:
1343:
1344:
1345:
1346:
1347:
1348:
1349:
1350: \subsubsection*{Control Flow}
1351:
1352: The machine defines a basic set of instructions dedicated to control
1353: the flow of execution (\ifk{}, \whilek{}, and \breakk).
1354: %
1355: The \ifk instruction requires two reduction rules, selecting the
1356: branch according to the boolean value resulting of the evaluation of
1357: value $\mathmob{v}$. Each of them executes the code of the selected branch
1358: followed by the instruction's continuation ($\mathmob{P}$).
1359:
1360: \prule{
1361: \rulename{IfTrue}
1362: }{
1363: \evalone(H, t, B, v) = \truek
1364: % B(x) = \truek
1365: }{
1366: a(h, C, H, (t, (B, \ifk\ (v)\ \{ P' \}\ \elsek\ \{ P'' \}\ ; P) :: Q, r) \conc T, W)
1367: }{
1368: a(h, C, H, (t, (B, P' ; P) :: Q, r) \conc T, W)
1369: }
1370:
1371:
1372: \prule{
1373: \rulename{IfFalse}
1374: }{
1375: \evalone(H, r, B, v) = \falsek
1376: % B(x) = \falsek
1377: }{
1378: a(h, C, H, (t, (B, \ifk\ (v)\ \{ P' \}\ \elsek\ \{ P'' \}\ ; P) :: Q, r) \conc T, W)
1379: }{
1380: a(h, C, H, (t, (B, P'' ; P) :: Q, r) \conc T, W)
1381: }
1382:
1383:
1384: The \whilek instruction requires three rules. Rule \rulename{PushCont}
1385: simply pushes the continuation of the instruction to the stack. This
1386: is required to allow the use of the \breakk instruction to branch out
1387: of the loop (see rule \rulename{Break}).
1388:
1389: \ucnrule{
1390: \rulename{PushCont}
1391: }{
1392: a(h, C, H, (t, (B, \whilek(v)\ \{ P' \} ; P) :: Q, r) \conc T, W)
1393: }{
1394: a(h, C, H, (t, (B, P' ; \whilek(v)\ \{ P' \}) :: (B, P) :: Q, r) \conc\ T, W)
1395: }
1396:
1397:
1398: Rule \rulename{WhileTrue} executes the body of the \whilek instruction
1399: composed with the instruction again, performing the loop. The process
1400: eventually stops when the value $\mathmob{v}$ evaluates to \falsek.
1401: The execution then continues with the continuation popped from the
1402: stack.
1403:
1404: \uprule{
1405: \rulename{WhileTrue}
1406: }{
1407: % B(x) = \truek
1408: \evalone(H, t, B, v) = \truek
1409: }{
1410: a(h, C, H, (t, (B, \whilek(v)\ \{ P \}) :: Q, r) \conc T, W)
1411: }{
1412: a(h, C, H, (t, (B, P\ ; \whilek(v)\ \{ P \}) :: Q, r) \conc\ T, W)
1413: }
1414:
1415:
1416: Rule \rulename{WhileFalse} emulates the end of the loop resorting to
1417: the \breakk instruction.
1418:
1419:
1420: \prule{
1421: \rulename{WhileFalse}
1422: }{
1423: % B(x) = \falsek
1424: \evalone(H, t, B, v) = \falsek
1425: }{
1426: a(h, C, H, (t, (B, \whilek\ (v)\ \{ P \}) :: Q, r) \conc T, W)
1427: }{
1428: a(h, C, H, (t, (B, \breakk) :: Q, r) \conc T, W)
1429: }
1430:
1431: The \breakk instruction branches out of the loop. It pops the current
1432: code-block from the stack and begins the execution of the continuation
1433: (the new top of the stack). The environment of the continuation is
1434: updated with the modifications performed during the execution of the
1435: loop.
1436:
1437: %% , rule \rulename{Break}, this if the code-block on the top
1438: %% of the stack is not waiting for a result (from a method call), rule
1439: %% \rulename{BreakIgnore}.
1440:
1441: \ucnrule{
1442: \rulename{Break}
1443: }{
1444: a(h, C, H, (t, (B, \breakk\ ; P) :: (B', P') :: Q, r) \conc T, W)
1445: }{
1446: a(h, C, H, (t, ((B' + B)|_{\dom(B')}, P') :: Q, r) \conc T, W)
1447: }
1448:
1449:
1450: %% \rule{
1451: %% \rulename{BreakIgnore}
1452: %% }{
1453: %% a(h, C, H, (r, B, \breakk; I, (r', B', I') :: Q) \conc T, W)
1454: %% }{
1455: %% a(h, C, H, (r, B, I, (r', B, I') :: Q) \conc\ T, W)
1456: %% }
1457:
1458: %% ?????????? a syntatic restriction????? no break out of a if or while
1459:
1460: %\subsubsubsection**{Garbage Collection}
1461:
1462: %References that do not hold any value, are not under any access
1463: %restriction, and have no thread suspend upon them can be removed.
1464:
1465: %\prule{
1466: % \rulename{GC}
1467: %}{
1468: % r' \not \in S [A DEFINIR]
1469: %}{
1470: % a(h, C, H\cdot\{\lockable{r'}{}: ?\}, T, W)
1471: %}{
1472: % a(h, C, H, T, W)
1473: %}
1474:
1475: %%\vspace{-11pt}
1476: \subsubsection*{Execute External Services}
1477:
1478:
1479: The \execk instruction allows the interaction with external services.
1480: This interaction is defined by an interface of seven possible actions.
1481:
1482: %%\vspace{-11pt}
1483: \begin{itemize}
1484: \item \texttt{init}: opens a session with a service, and returns a session identifier;
1485: %%\vspace*{-5pt}
1486: \item \texttt{read}: reads a given number of bytes from a session;
1487: %%\vspace*{-5pt}
1488: \item \texttt{readLine}: reads a line from a session;
1489: %%\vspace*{-5pt}
1490: \item \texttt{write}: writes the given data to a session;
1491: %%\vspace*{-5pt}
1492: \item \texttt{action}: posts an action to be performed by the service associated to the session;
1493: %%\vspace*{-5pt}
1494: \item \texttt{isAlive}: checks if the session is still active;
1495: %%\vspace*{-5pt}
1496: \item \texttt{close}: closes the session.
1497: \end{itemize}
1498:
1499: %%\vspace{-11pt}
1500: The syntax of the \execk\ instruction requires the existence of three
1501: arguments, of which the first is the string that determines which
1502: action is to be performed.
1503: %
1504: The second argument is an integer value that, when the action is
1505: \texttt{init}, corresponds to the identifier of the service to be
1506: requested, and otherwise corresponds to the session identifier.
1507: %
1508: The third argument is a string used to pass values to the action.
1509: %
1510: The operation is performed by an internal built-in function
1511: \textsf{exec} that executes synchronously. Asynchronous calls can be
1512: performed by encapsulating the \execk instruction in a new thread.
1513:
1514: \uprule{
1515: \rulename{Exec}
1516: }{
1517: \evalseq(H, t, B, v_1\ v_2\ v_3) = u_1\ u_2\ u_3 \quad
1518: \textsf{exec}(u_1\ u_2\ u_3) = u
1519: }{
1520: a(h, C,H,(t, (B, x = \execk(v_1\ v_2\ v_3)\ ; P) :: Q, r) \conc T,W)
1521: }{
1522: a(h, C, H,(t , (B + \{x : u\}, P) :: Q, r) \conc T,W)
1523: }
1524:
1525:
1526: The protocol to interact with an external service is initiated by the \texttt{init} action, that
1527: receives as argument an integer value that identifies the service, and returns the session identifier.
1528: %
1529: Once the session is opened, a series of \texttt{read},
1530: \texttt{readLine}, \texttt{write}, \texttt{action}, and
1531: \texttt{isAlive} actions may be performed.
1532: %
1533: To terminate the session, the \texttt{close} action must be used.
1534: Below is an example of a session with a FTP server. We assume that the
1535: FTP service identifier is 4.
1536:
1537: \begin{step}
1538: \begin{array}{l}
1539: \mathmob{x = \execk(\texttt{"init"}\ 4\ \texttt{"ftp.adomain"});}\\
1540: \mathmob{x' = \execk(\texttt{"action"}\ x\ \texttt{"GET afile"});}\\
1541: \mathmob{x' = \execk(\texttt{"read"}\ x\ \texttt{"4096"});}\\
1542: \mathmob{y = x'\ != \texttt{""};}\\
1543: \mathmob{\whilek\ (y)\ \{}\\
1544: \quad \mathmob{x' = \execk(\texttt{"read"}\ x\ \texttt{"4096"});}\\
1545: \quad \mathmob{y = x'\ != \texttt{""};}\\
1546: \mathmob{\}}\\
1547: \mathmob{x' = \execk(\texttt{"close"}\ x\ \texttt{""})}
1548: \end{array}
1549: \end{step}
1550:
1551: The example begins by opening a FTP session with a server located at
1552: \texttt{ftp.adomain}. The correspondent session identifier is placed
1553: on $\mathmob{x}$. Next, it posts the \texttt{GET afile} action to fetch file
1554: \texttt{afile}, and reads its contents in chunks of 4096 bytes.
1555: Once the file is read, it closes the session.
1556:
1557:
1558: %\subsubsection*{Assignment of Expressions and Null}
1559: %%\vspace{-11pt}
1560: \subsubsection*{Assignment of Expressions}
1561:
1562: The result of the computation of an expression may be assigned to a variable. The assignment involves adding
1563: a new entry in the environment ($\mathmob{B}$) of the thread.
1564:
1565: \prule{
1566: \rulename{Assignment}
1567: }{
1568: \evalone(H, t, B, e) = u
1569: }{
1570: a(h, C,H,(t, (B, x = e\ ; P) :: Q, r) \conc T,W)
1571: }{
1572: a(h, C,H,(t , (B + \{x : u\}, P) :: Q, r) \conc T,W)
1573: }
1574:
1575: % Assigning \nullk to a variable adds a new binding from the target
1576: % variable to $\nullr$.
1577:
1578: % \cnrule{
1579: % \rulename{NullAssignment}
1580: % }{
1581: % a(h, C,H,(t, (B, x = \nullk\ ; P) :: Q, r) \conc T,W)
1582: % }{
1583: % a(h, C,H,(t , (B + \{x : \nullr\}, P) :: Q, r) \conc T,W)
1584: % }
1585:
1586: %%\vspace{-11pt}
1587: \subsubsection*{Handling Attributes}
1588:
1589: Assigning a value to an attribute of an object involves modifying the
1590: object's closure. Thus, an inspection to the status of both the object
1591: and the attribute is required. If the access to both is granted to the
1592: current thread, the binding of the given attribute in the object's
1593: closure is modified.
1594:
1595: \uppnrule{
1596: \rulename{AttrAssignment}
1597: }{
1598: \evalone(H, t, B, v) = u \quad
1599: B(\selfk) = r' \quad
1600: H(r') = (t', (bool, B', X)) \quad \access(H, r', t) = \truek
1601: }{
1602: (\evalone(H, t, B', x) = r'' \wedge \access(H, r'', t) = \truek) \vee \evalone(H, t, B', x) = c
1603: }{
1604: a(h, C, H,(t, (B, \selfk.x = v\ ; P) :: Q, r) \conc T,W)
1605: }{
1606: a(h, C, H + \{r' : (t', (bool, B' + \{x : u\}, X))\},(t ,(B, P) :: Q, r) \conc T,W)
1607: }
1608:
1609: If not, the current thread may suspend on the reference holding the
1610: object, or on the one holding the actual attribute. Rule
1611: \rulename{AttrAssignmentLocked} covers the first case, where the
1612: thread cannot access the object.
1613:
1614: \uprule{
1615: \rulename{AttrAssignmentLocked}
1616: }{
1617: B(\selfk) = r' \quad
1618: \access(H, r', t) = \falsek
1619: }{
1620: a(h, C, H,(t, (B, \selfk.x = v\ ; P) :: Q, r) \conc T,W)
1621: }{
1622: a(h, C, H, T, W + \{r' : (t, (B, \selfk.x = v\ ; P) :: Q, r)\})
1623: }
1624:
1625: Rule \rulename{AttrAssignmentLockedInAttr} covers the second case,
1626: where the thread has access to the object, but not to the attribute.
1627:
1628: \upnrule{
1629: \rulename{AttrAssignmentLockedInAttr}
1630: }{
1631: B(\selfk) = r' \quad
1632: H(r') = (t', (bool, B', X)) \quad
1633: \access(H, r', t) = \truek
1634: }{
1635: \evalone(H, t, B', x) = r'' \quad
1636: \access(H, r'', t) = \falsek
1637: }{
1638: a(h, C, H,(t, (B, \selfk.x = v\ ; P) :: Q, r) \conc T,W)
1639: }{
1640: a(h, C, H, T, W + \{r'' : (t, (B, \selfk.x = v\ ; P) :: Q, r)\})
1641: }
1642:
1643: There is no access restriction on the reading of attributes.
1644: The rule simply retrieves the value of the attribute and binds the given variable to it.
1645: %
1646: To ensure that correctness of the information to be read, the
1647: programmer must protect the access with a lock to the object.
1648:
1649: % Reading the attributes of an object or agent is handled by two rules. Both resolve the
1650: % binding for the object ($\mathmob{o}$) and check if access is granted. The
1651: % affirmative case is covered by rule \rulename{ReadAttr}, that binds the
1652: % variable $\mathmob{x}$ to the value bound to $\mathmob{y}$.
1653:
1654:
1655:
1656: \prule{
1657: \rulename{ReadAttr}
1658: }{
1659: B(o) = r' \quad H(r') = (\_, (\_, B', X)) \quad B'(y) = u
1660: }{
1661: a(h, C,H,(t, (B, x = \selfk.y\ ; P) :: Q, r) \conc T,W)
1662: }{
1663: a(h, C,H,(t , (B + \{x : u\}, P) :: Q, r) \conc T,W)
1664: }
1665:
1666: % The negative case is covered
1667: % by rule \rulename{ReadAttrLocked}, that suspends the thread upon the
1668: % reference where the object is located.
1669:
1670: % \prule{
1671: % \rulename{ReadAttrLocked}
1672: % }{
1673: % B(o) = r' \quad \access(H, r', t) = \falsek
1674: % }{
1675: % a(h, C,H,(t, (B, x = o.y\ ; P) :: Q, r) \conc T,W)
1676: % }{
1677: % a(h, C,H, T, W + \{r' : ,(t, (B, x = ��o.y\ ; P) :: Q, r)\})
1678: % }
1679:
1680: \subsubsection*{Terminate an Agent}
1681:
1682: Finally, the \rulename{Exit} rule terminates the execution of an
1683: agent. This is required because agents are daemons and their
1684: execution must be explicitly terminated by the \exitk\ instruction.
1685: %
1686: All the references to the agent in the network must be removed.
1687:
1688: \uppnrule{
1689: \rulename{Exit}
1690: }{
1691: B(\selfk) = r \quad
1692: H(r) = (\_, (\_, \_, X)) \quad
1693: C(X) = (\_, \_, \_, \_, S_1\ \cdots\ S_n) \quad
1694: }{
1695: SNS(S_1) = (\alpha_1 , \{r@a_{1_1}, \dots, r@a, \dots, r@a_{1_m}\})\ \dots\ SNS(S_n) = (\alpha_n , \{r@a_{n_1}, \dots, r@a, \dots, r@a_{n_k}\})
1696: }{
1697: a(h, C, H,(t, (B, \exitk\ ; P) :: Q, r) \conc T,W) \conc \calA, (ANS, SNS)
1698: }{
1699: \calA, (\Ans|_{\dom(\Ans) - \{a\}},
1700: SNS + \{S_1 : (\alpha_1, \{r@a_{1_1}, \dots, r@a_{1_m}\}), \dots, S_n : (\alpha_n, \{r@a_{n_1}, \dots, r@a_{n_k}\})\})
1701: }
1702:
1703: %%% Local Variables:
1704: %%% mode: latex
1705: %%% TeX-master: "main"
1706: %%% End:
1707:
1708: