Abstract
Concurrent trace programs (CTPs) are slices of the concurrent programs that generate the concrete program execution traces, where inter-thread event order specific to the given traces are relaxed. For such CTPs, we introduce transaction sequence graph (TSG) as a model for efficient concurrent data flow analysis. The TSG is a digraph of thread-local control nodes and edges corresponding to transactions and possible context-switches. Such a graph captures all the representative interleavings of these nodes/transactions. We use a mutually atomic transaction (MAT) based partial order reduction to construct such a TSG. We also present a non-trivial improvement to the original MAT analysis to further reduce the TSG sizes. As an application, we have used interval analysis in our experiments to show that TSG leads to more precise intervals and more time/space efficient concurrent data flow analysis than the standard models such as concurrent control flow graph.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. (1997)
Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomcity checker for multithreaded programs. In: Proc. of IPDPS (2004)
Xu, M., Bodik, R., Hill, M.D.: A serializability violation detector for shared-memory server programs. In: Programming Language Design and Implementation (2005)
Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Transactions on Software Engineering (2006)
Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 52–65. Springer, Heidelberg (2008)
Sadowski, C., Freund, S.N., Flanagan, C.: Singletrack: A dynamic determinism checker for multithreaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 394–409. Springer, Heidelberg (2009)
Farzan, A., Madhusudan, P.: Meta-analysis for atomicity violations under nested locking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123. Springer, Heidelberg (2008)
Wang, L., Stoller, S.D.: Accurate and efficient runtime detection of atomicity errors in concurrent programs. In: Symposium on Principles and Practice of Parallel Programming (2006)
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proc. of POPL (2005)
Musuvathi, M., Quadeer, S.: CHESS: Systematic stress testing of concurrent software. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 15–16. Springer, Heidelberg (2007)
Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: A Runtime Model Checker for Multi-threaded C Programs. Technical Report UUCS-08-004, University of Utah (2008)
Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 328–342. Springer, Heidelberg (2010)
Kundu, S., Ganai, M., Wang, C.: CONTESSA: CONcurrency TESting Augmented with Symbolic Analysis. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. LNCS, vol. 6174. Springer, Heidelberg (2010)
Long, D.L., Clarke, L.A.: Task interaction graphs for concurrent analysis. In: International Conference on Software Engineering (1989)
Dwyer, M.B., Clarke, L.A.: Data flow analysis for verifying properties of concurrent programs. In: International Symposium on the Foundations of Software Engineering (1994)
Lee, J., Padua, D.A., Midkiff, S.P.: Basic compiler algorithms for parallel programs. Symposium on Principles and Practice of Parallel Programming (1999)
Farzan, A., Madhusudan, P.: Causal dataflow analysis for concurrent programs. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 102–116. Springer, Heidelberg (2007)
Chugh, R., Voung, J.W., Jhala, R., Lerer, S.: Dataflow analysis for concurrent programs using datarace detection. In: Programming Language Design and Implementation (2008)
Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 282–298. Springer, Heidelberg (2008)
Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic reduction of thread interleavings in concurrent programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 134-138. Springer, Heidelberg (2009)
Chen, F., Roşu, G.: Parametric and sliced causality. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 240–253. Springer, Heidelberg (2007)
Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 95–112. Springer, Heidelberg (2007)
Edelstein, O., Farchi, E., Goldin, E., Nir, Y., Ratsaby, G., Ur, S.: Framework for Testing Multi-threaded Java Programs. In: Concurrency and Computation: Practice and Experience (2003)
Sen, K.: Race directed random testing of concurrent programs. In: PLDI (2008)
Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions. In: ESEC-FSE (2009)
Ganai, M.K., Kundu, S.: Reduction of Verification Conditions for Concurrent System using Mutually Atomic Transactions. In: Păsăreanu, C.S. (ed.) SPIN Workshop. LNCS, vol. 5578, pp. 68–87. Springer, Heidelberg (2009)
Lamport, L.: How to make multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers (1979)
Ganai, M. K.: Conference Notes, http://www.nec-labs.com/~malay/notes.htm
Rugina, R., Rinard, M.C.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In: Programming Language Design and Implementation (2000)
Lu, S., Tucekt, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access interleaving invariants. In: Architectural Support for Programming Languages and Operating Systems (2006)
Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: Parallel and Distributed Processing Symposium (2003)
System Analysis and Verification Team. NECLA SAV Benchmarks, http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganai, M.K., Wang, C. (2010). Interval Analysis for Concurrent Trace Programs Using Transaction Sequence Graphs. In: Barringer, H., et al. Runtime Verification. RV 2010. Lecture Notes in Computer Science, vol 6418. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16612-9_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-16612-9_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16611-2
Online ISBN: 978-3-642-16612-9
eBook Packages: Computer ScienceComputer Science (R0)