Algorithmic Verification of Invalidation-Based Protocols

We propose an extension of the model of Broadcast Protocols in which individual processes are allowed to have unbounded local data and to communicate via value passing. Our specification language is based on multiset rewriting over first order atomic formulas enriched with a mechanism for global synchronization to model broadcasts, and constraints to model the relations over internal data and value passing. For this new class of parameterized systems, we provide a symbolic validation procedure for checking safety properties, and termination conditions defined on special classes of multiset rewriting systems with linear constraints. We report here on practical experiments with coherence protocols for virtual shared memory, and multiprocessors systems in which the number of processors, pages or cache lines are left as parameters.