3 Enforcing a link between agent and the channel names they declare
The link between agents and the names they have declared is usually lost by a-conversion. We propose to restore this link by enriching the syntax of
the p-calculus with markers. An unambiguous marker is inferred to
each instance of agent and then, each channel name is stamped with the
marker of its creating instance. This way a name is entirely identified
by the restriction operator which has declared it and its marker.
3.1 Agent markers
The marker of an agent is the history of the replications which had
led to its creation.
We first locate each action of the system by using a finite set of
labels L. We assume that neither the symbol 0 or
e are elements of L.
An agent marker is a word on the alphabet S=(LÈ{0})2È{Ext}.
-
Initial thread markers are the empty word;
- when computing agents, markers are always passed to agents
in the continuation;
- when fetching a resource, spawned agents are allocated a new
marker constructed as follows:
-
if the output agent belongs to
the system, the new marker is given by (i,j).id where i is the label of the
replication guard, j
is the label of the output action and id is the marker of the output agent,
- if the output agent belongs to the context,
the new marker is given by (i,0).id where
i is the label of the
replication guard and
id is a fresh marker in the set Ext*.
3.2 Consistency
During a given computation sequence, the same marker can never be
created twice.
This is still valid while only keeping the second component of each label pair in markers.
3.3 Name markers
Channel names are just stamped with the marker of the agent which has
declared them.
In the case where a name is declared by the context, it is given a
marker in Ext*.
Because of marker consistency, if two names are stamped
with the same agent marker, they have been declared by the same
instance of an agent.