Next: Related Works
Up: An Overview of MSR():
Previous: Implementation in CLP
Applications
As a first application
we studied mutual exclusion properties for different
formulations of the ticket protocol. As shown in
[10], this protocol has an infinite-state space even for
system configurations with only 2 processes. We have considered both
a multi-client, single-server formulation, i.e. with
an arbitrary but finite number of dynamically generated
clients but a single shared resource, and a multi-client,
multi-server system in which both clients and servers are
created dynamically. Both examples have been modeled using
multiset rewriting rules with linear constraints,
that sup.pngport arithmetic operations like increment and
decrement of data variables. Our models are faithful to the
original formulation of the algorithm, in that we do not abstract
away global and local integer variables attached to individual
clients that in fact can still grow unboundedly. Using our
symbolic backward reachability procedure combined with the dynamic
use of abstractions, we have automatically verified that both
models are safe for any number of clients and servers and
for any values of local and global variables [8].
The second application of our method was the analysis of
a coherence protocol for virtual shared memory
proposed by Li and Hudak in [24] and previously analyzed in
[20]. Using our technique, we found an inconsistency in one
of the Colored Petri Nets model proposed in [20].
After having corrected the error, we have
automatically verified a new model of the protocol in which the
number of threads, processors, and pages of virtual memory are
unbounded parameters [8].
Finally, we have automatically validate
coherence protocols for multiprocessors systems (M.S.I., M.E.S.I.,
Synapse) in which number of processors, cache lines and memory
locations are left as unbounded parameters [15].
We are currently working on the application of this methodology to the validation of
security and authentication protocols and of abstraction of concurrent programs.
Next: Related Works
Up: An Overview of MSR():
Previous: Implementation in CLP
Giorgio Delzanno
2003-02-03