TY - GEN
T1 - Fighting livelock in the i-protocol
T2 - 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1999
AU - Dong, Yifei
AU - Du, Xiaoqun
AU - Ramakrishna, Y. S.
AU - Ramakrishnan, C. R.
AU - Ramakrishnan, I. V.
AU - Smolka, Scott A.
AU - Sokolsky, Oleg
AU - Stark, Eugene W.
AU - Warren, David S.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84948982875
U2 - 10.1007/3-540-49059-0_6
DO - 10.1007/3-540-49059-0_6
M3 - Conference contribution
AN - SCOPUS:84948982875
SN - 3540657037
SN - 9783540657033
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 74
EP - 88
BT - Tools and Algorithms for the Construction and Analysis of Systems - 5th International Conference, TACAS 1999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1999, Proceedings
A2 - Rance Cleaveland, W.
PB - Springer Verlag
Y2 - 22 March 1999 through 28 March 1999
ER -