Efficient verification of symmetric concurrent systems
Authors:
- C.N. IpCIC.N. Ip
- D.L. DillDDD.L. Dill
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 230-234
Abstract
Previously, we proposed a reduction technique[ID93] based on symmetries to alleviate the state explosionproblem in automatic verification of concurrentsystems. This paper describes the results of testingthe technique on a wide range of algorithms andprotocols, including realistic multiprocessor synchronizationalgorithms and cache coherence protocols.Memory requirements were reduced by amountsranging from 83% to over 99%, and time requirementswere often reduced as well. We also consider ...Keywords
This publication has 5 references indexed in Scilit:
- Protocol verification as a hardware design aid2003
- The directory-based cache coherence protocol for the DASH multiprocessor2002
- The Stanford Dash multiprocessorComputer, 1992
- Algorithms for scalable synchronization on shared-memory multiprocessorsACM Transactions on Computer Systems, 1991
- Myths about the mutual exclusion problemInformation Processing Letters, 1981