tailieunhanh - CONCUR 2004 – Concurrency Theory- P4

CONCUR 2004 – Concurrency Theory- P4: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | 76 . Amadio and S. Dal Zilio f with arbitrary parameters and store. Note that an expression can never read or write a register. To determine the sets R f we perform an iterative computation according to the equations above. The iteration stops when either 1 we reach a fixpoint and we are sure that the property holds or 2 we notice that a word in the current approximation of R f contains the same register twice thus we never need to consider words whose length is greater than the number of registers . If the first situation occurs then for every function symbol f that returns a behaviour we can obtain a list of registers ry that a thread starting from control point may read. We are going to consider these registers as hidden parameters variables of the function . If the second condition occurs we cannot guarantee the read once property and we stop analysing the code. Example 3. This will be the running example for this section. We consider the representation of signals as in Example 1 3 . We assume two signals sig and ring. The behaviour alarm n m will emit a signal on ring if it detects that no signal is emitted on sig for m consecutive instants. The alarm delay is reset to n if the signal sig is present. alarm x z ring alarm x s y match sig with prst next. alarm x x _ alarm x y By computing R on this example we obtain R alarm e .R ring U 7 match sig with . e e U sig e e sig . Control Points We define a symbolic representation of the set of states reachable by a thread based on the control flow graph of its behaviours. A control point is a triple p 6e z where intuitively is the currently called function p represents the patterns crossed so far in the function definition plus possibly the registers that still have to be read be is the continuation and i is an integer flag in 0 1 2 that will be used to associate with the control point various kinds of conditions. We associate with a system satisfying the read once condition a finite number