Abstract
Direct Memory Access (DMA) is key to achieving high performance in system-level software for multicore processors such as the Cell Broadband Engine. Incorrectly orchestrated DMAs cause DMA races, leading to subtle bugs that are hard to reproduce and fix. In previous work, we have shown that k-induction yields an effective method for proving absence of a restricted class of DMA races. We extend this work to handle a larger class of DMA races. We show that the applicability of k-induction can be significantly improved when combined with three inexpensive static analyses: 1) abstract-interpretation-based static analysis; 2) chunking, a domain-specific invariant generation technique; and 3) code transformations based on statement independence. Our techniques are implemented in the SCRATCH tool. We evaluate our work on industrial benchmarks.
This research is supported by the the Toyota Motor Corporation, by the EU FP7 STREP MOGENTES (project ID ICT-216679), and by EPSRC grant EP/G051100.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Aho, A., Lam, M., Sethi, R., Ullman, J.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (2006)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)
Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20(4-5), 379–405 (2008)
Clarke, E., Kröning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)
Donaldson, A.F., Kroening, D., Rümmer, P.: Scratch: a tool for automatic analysis of DMA races. In: PPoPP (to appear, 2011)
Donaldson, A.F., Kroening, D., Rümmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 280–295. Springer, Heidelberg (2010)
Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4) (2003)
Engler, D., Ashcraft, K.: RacerX: Effective, static detection of race conditions and deadlocks. In: SOSP, pp. 237–252. ACM, New York (2003)
Flanagan, C., Freund, S.N.: Type-based race detection for Java. In: PLDI, pp. 219–232. ACM, New York (2000)
Floyd, R.W.: Assigning meanings to programs. Mathematical aspects of computer science. In: Proceedings of Symposia in Applied Mathematics pp. 19–32 (1967)
Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: FMCAD, pp. 109–117. IEEE, Los Alamitos (2008)
IBM: Example Library API Reference, version 3.1 (July 2008)
IBM: Cell BE resource center (2009), http://www.ibm.com/developerworks/power/cell/
Naik, M., Aiken, A., Whaley, J.: Effective static race detection for Java. In: PLDI, pp. 308–319. ACM, New York (2006)
Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5) (2007)
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)
Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Tip, F.: A survey of program slicing techniques. J. Prog. Lang. 3(3) (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Donaldson, A.F., Haller, L., Kroening, D. (2011). Strengthening Induction-Based Race Checking with Lightweight Static Analysis. In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science, vol 6538. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18275-4_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-18275-4_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18274-7
Online ISBN: 978-3-642-18275-4
eBook Packages: Computer ScienceComputer Science (R0)