×

zbMATH — the first resource for mathematics

Region analysis for race detection. (English) Zbl 1248.68152
Palsberg, Jens (ed.) et al., Static analysis. 16th international symposium, SAS 2009, Los Angeles, CA, USA, August 9–11, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03236-3/pbk). Lecture Notes in Computer Science 5673, 171-187 (2009).
Summary: Automatic race detection of C programs requires fast, yet sufficiently precise analysis of dynamic memory. Therefore, we present a region-based pointer analysis which seeks to identify disjoint regions of dynamically allocated objects to ensure that write accesses to the same region are always protected by the same mutexes. Our approach has been implemented within the interprocedural analyzer of concurrent C programs GobLint and we have successfully applied it on code from the Linux kernel, such as the access vector cache. This code relies on a synchronized hash table where an array of doubly linked lists is protected by an array of locks.
For the entire collection see [Zbl 1169.68005].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68P05 Data structures
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Boyapati, C., Salcianu, A., Beebee, W., Rinard, M.: Ownership types for safe region-based memory management in real-time java. In: PLDI 2003, pp. 324–337. ACM Press, New York (2003)
[2] Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009, pp. 289–300. ACM Press, New York (2009) · Zbl 1315.68085
[3] Chatterjee, S., Lahiri, S., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing Low-Level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007) · Zbl 1186.68108 · doi:10.1007/978-3-540-71209-1_4
[4] Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA 1998, pp. 48–64. ACM Press, New York (1998) · Zbl 0924.68038
[5] Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Recursive Programs. In: Neuhold, E. (ed.) Formal Descriptions of Programming Concepts, pp. 237–277. North-Holland Publishing Company, Amsterdam (1977) · Zbl 0393.68080
[6] Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: OSDI 2000, pp. 1–16. USENIX Association (2000)
[7] Fecht, C., Seidl, H.: A Faster Solver for General Systems of Equations. Sci. Comput. Programming 35(2), 137–161 (1999) · Zbl 0948.68016 · doi:10.1016/S0167-6423(99)00009-X
[8] Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL 2005, pp. 338–350. ACM Press, New York (2005) · Zbl 1369.68138
[9] Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: POPL 2009, pp. 239–251. ACM Press, New York (2009) · Zbl 1315.68094
[10] Gulwani, S., Tiwari, A.: An abstract domain for analyzing heap-manipulating low-level software. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 379–392. Springer, Heidelberg (2007) · Zbl 1135.68366 · doi:10.1007/978-3-540-73368-3_42
[11] Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL 2005, pp. 310–323. ACM Press, New York (2005) · Zbl 1369.68140
[12] Hind, M., Burke, M., Carini, P., Choi, J.-D.: Interprocedural pointer alias analysis. ACM Trans. Prog. Lang. Syst. 21(4), 848–894 (1999) · Zbl 01935253 · doi:10.1145/325478.325519
[13] Karr, M.: Affine relationships among variables of a program. Acta Inf. 6(2), 133–151 (1976) · Zbl 0358.68025 · doi:10.1007/BF00268497
[14] Knoop, J., Steffen, B.: The Interprocedural Coincidence Theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol. 641, pp. 125–140. Springer, Heidelberg (1992) · doi:10.1007/3-540-55984-1_13
[15] Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., Berdine, J.: Heap decomposition for concurrent shape analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 363–377. Springer, Heidelberg (2008) · Zbl 1149.68358 · doi:10.1007/978-3-540-69166-2_24
[16] Müller-Olm, M., Seidl, H.: A note on Karr’s algorithm. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016–1028. Springer, Heidelberg (2004) · Zbl 1099.68022 · doi:10.1007/978-3-540-27836-8_85
[17] Müller-Olm, M., Seidl, H.: Upper adjoints for fast inter-procedural variable equalities. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 178–192. Springer, Heidelberg (2008) · Zbl 1133.68321 · doi:10.1007/978-3-540-78739-6_15
[18] Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: POPL 2007, pp. 327–338. ACM Press, New York (2007) · Zbl 1295.68073
[19] Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: Cil: An infrastructure for C program analysis and transformation. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002) · Zbl 1051.68756 · doi:10.1007/3-540-45937-5_16
[20] Pratikakis, P., Foster, J.S., Hicks, M.: Existential label flow inference via CFL reachability. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 88–106. Springer, Heidelberg (2006) · Zbl 1225.68075 · doi:10.1007/11823230_7
[21] Pratikakis, P., Foster, J.S., Hicks, M.: Locksmith: Context-sensitive correlation analysis for detecting races. In: PLDI 2006, pp. 320–331. ACM Press, New York (2006)
[22] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE Computer Society Press, Los Alamitos (2002)
[23] Rugina, R., Rinard, M.C.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. ACM Trans. Prog. Lang. Syst. 27(2), 185–235 (2005) · Zbl 05459330 · doi:10.1145/1057387.1057388
[24] Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Syst. 24(3), 217–298 (2002) · Zbl 05459332 · doi:10.1145/514188.514190
[25] Seidl, H., Vene, V., Müller-Olm, M.: Global invariants for analyzing multithreaded applications. Proc. of the Estonian Academy of Sciences: Phys., Math. 52(4), 413–436 (2003) · Zbl 1091.68520
[26] Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, pp. 189–234 (1981)
[27] Tofte, M., Birkedal, L.: A region inference algorithm. ACM Trans. Prog. Lang. Syst. 20(4), 724–767 (1998) · Zbl 0974.68078 · doi:10.1145/291891.291894
[28] Vojdani, V., Vene, V.: Goblint: Path-sensitive data race analysis. Annales Univ. Sci. Budapest., Sect. Comp. 30, 141–155 (2009) · Zbl 1199.68107
[29] Wang, X., Xu, Z., Liu, X., Guo, Z., Wang, X., Zhang, Z.: Conditional correlation analysis for safe region-based memory management. In: PLDI 2008, pp. 45–55. ACM Press, New York (2008)
[30] Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent linux device drivers. In: ASE 2007, pp. 501–504. ACM Press, New York (2007)
[31] Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008) · Zbl 1155.68359 · doi:10.1007/978-3-540-70545-1_36
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.