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.