Abstract
The growing popularity of multi-threading has led to a great number of software libraries that support access by multiple threads. We present Local/Global Finite State Machines (LGFSMs) as a model for a certain class of multithreaded libraries. We have developed a tool called Beacon that does parameterized model checking of LGFSMs. We demonstrate the expressiveness of LGFSMs as models, and the effectiveness of Beacon as a model checking tool by (1) modeling a multithreaded memory manager Rockall developed at Microsoft Research as an LGFSM, and (2) using Beacon to check a critical safety property of Rockall.
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
P. A. Abdulla, K. Cerans, B. Jonsson, and T. Yih-Kuen. General decidability theorems for infinite-state systems. LICS’ 96: 11th IEEE Symp. Logic in Computer Science, pages 313–321, July 1996.
P. A. Abdulla and B. Jonsson. Ensuring completeness of symbolic verificatiom methods for infinite-state systems. Theoretical Computer Science, 1997.
Thomas Ball, Sagar Chaki, and Sriram K. Rajamani. Parameterized verification of multithreaded software libraries. Technical Report MSRTR-2000-116, Microsoft Research, December 2000.
T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. SPIN 00: SPIN Workshop, Lecture Notes in Computer Science 1885, pages 113–130. Springer-Verlag, 2000.
T. Ball and S. K. Rajamani. Boolean programs: A model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research, February 2000.
James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. ICSE 2000: International Conference on Software Engineering, 2000.
G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. CAV 00: Computer Aided Verification, Lecture Notes in Computer Science 1855, pages 53–68. Springer-Verlag, 2000.
J. Esparza and M. Nielsen. Decibility issues for petri nets-a survey. Journal of Informatik Processing and Cybernetics, 30(3):143–160, 1994.
E. A. Emerson and K. S. Namjoshi. Automatic Verification of Parameterized Synchronous Systems. CAV 96: Computer Aided Verification, Lecture Notes in Computer Science 1102, pages 87–98. Springer-Verlag, 1996.
A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89:144–179, 1990.
A. Finkel. The minimal coverability graph for petri nets. Advances in Petri Nets, Lecture Notes in Computer Sceince, 674:210–243, 1993.
A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 2000. To appear.
S. M. German and A. P. Sistla. Reasoning about systems with many processes. JACM, 39(3), July 1992.
K. Havelund and T. Pressburger. Model checking Java programs using JavaPathFinder. STTT: International Journal on Software Tools for Technology Transfer, 2(4), April 2000.
R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3:147–195, 1969.
R. J. Lipton. The reachability problem requires exponential space. Technical report, Department of Computer Science, Yale University, 1976.
K.L. McMillan. http://www-cad.eecs.berkeley.edu/~kenmcmil.
C. Petri. Fundamentals of a theory of asynchronous information flow. Information Processing 62, Proceedings of the 1962 IFIP Congress, pages 386–390, 1962.
C. Rackoff. The covering and boundedness problem for vector addition systems. Theoretical Computer Science, 6:223–231, 1978.
G. Ramalingam. Context sensitive synchronization sensitive analysis is undecidable. Technical Report RC21493, IBM T.J.Watson Research, May 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ball, T., Chaki, S., Rajamani, S.K. (2001). Parameterized Verification of Multithreaded Software Libraries. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_12
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive