Abstract
The i-protocol, an optimized sliding-window protocol for GNU UUCP, came to our attention two years ago when we used the Con-currency Factory’s local model checker to detect, locate, and correct a non-trivial livelock in version 1.04 of the protocol. Since then, we have repeated this verification effort with five widely used model checkers, namely, COSPAN, Murϕ, SMV, SPIN, and XMC. It is our contention that the i-protocol makes for a particularly compelling case study in protocol verification and for a formidable benchmark of verification-tool performance, for the following reasons: 1) The i-protocol can be used to gauge a tool’s ability to detect and diagnose livelock errors. 2) The size of the i-protocol’s state space grows exponentially in the window size, and the entirety of this state space must be searched to verify that the protocol, with the livelock error eliminated, is deadlock- or livelock-free. 3) The i-protocol is an asynchronous, low-level software system equipped with a number of optimizations aimed at minimizing control-message and retransmission overhead. It lacks the regular structure that is often present in hardware designs. In this sense, it provides any verification tool with a vigorous test of its analysis capabilities.
Research supported in part by NSF Grants CCR-9505562 and CCR-9705998, and AFOSR grants F49620-95-1-0508 and F49620-96-1-0087.
Currently at: Sun Microsystems, Mountain View, CA 94043, USA.
Currently at: Department of Computer and Information Sciences, University of Pennsylvania, Philadelphia, PA 19104, USA.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and T. A. Henzinger, editors. Computer Aided Verification (CAV’ 96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996. Springer-Verlag.
A. T. Chamillard, L. A. Clarke, and G. S. Avrunin. Experimental design for comparing static concurrency analysis techniques. Technical Report 96-084, Computer Science Department, University of Massachusetts at Amherst, 1996.
E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. To appear.
R. Cleaveland, P. M. Lewis, S. A. Smolka, and O. Sokolsky. The Concurrency Factory: A development environment for concurrent systems. In Alur and Henzinger [AH96], pages 398–401.
K. M. Chandy and J. Misra. Parallel Program Design — A Foundation. Addison-Wesley, 1988.
E. M. Clarke, K. McMillan, S. Campos, and V. Hartonas-GarmHausen. Symbolic model checking. In Alur and Henzinger [AH96], pages 419–422.
J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 22(3):161–180, March 1996.
E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4es), December 1996.
D. L. Dill. The Murϕ Verification system. In Alur and Henzinger [AH96], pages 390–393.
R. H. Hardin, Z. Har’El, and R. P. Kurshan. COSPAN. In Alur and Henzinger [AH96], pages 423–427.
G. J. Holzmann and D. Peled. The state of SPIN. In Alur and Henzinger [AH96], pages 385–389.
N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. Srivas. PVS: Combining Specification, proof checking, and model checking. In Alur and Henzinger [AH96], pages 411–414.
Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. W. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV’ 97), volume 1254 of Lecture Notes in Computer Science, pages 143–154, Haifa, Israel, July 1997. Springer-Verlag.
Y. S. Ramakrishna and S. A. Smolka. Partial-order reduction in the weak modal mu-calculus. In A. Mazurkiewicz and J. Winkowski, editors, Proceedings of the Eighth International Conference on Concurrency Theory (CONCUR’ 97), volume 1243 of Lecture Notes in Computer Science, pages 5–24, Warsaw, Poland, July 1997. Springer-Verlag.
P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184–192, St. Petersburgh, January 1986.
XSB. The XSB logic programming system v1.7, 1997. Available by anonymous ftp from ftp.cs.sunysb.edu.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dong, Y. et al. (1999). Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49059-0_6
Download citation
DOI: https://doi.org/10.1007/3-540-49059-0_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65703-3
Online ISBN: 978-3-540-49059-3
eBook Packages: Springer Book Archive