Race analysis for SystemC using model checking

ABSTRACT

SystemC is a system-level modeling language that offers a wide range of features to describe concurrent systems at different levels of abstraction. The SystemC standard permits simulators to implement a deterministic scheduling policy, which often hides concurrency-related design flaws. We present a novel compiler for SystemC that integrates a formal and scalable race analysis. This analysis combines both classic static analysis and Model Checking techniques. The outcome of the analysis is not only valuable to diagnose the effect of race conditions, but can also be used to improve simulation performance dramatically. Our compiler produces a simulator that uses the race analysis information at runtime to perform partial-order reduction, thereby eliminating context switches that do not affect the result of the simulation. Experimental results show simulation speedups of one order of magnitude and better.

REFERENCES

• 1: N. Blanc, D. Kroening, and N. Sharygina, "Scoot: A tool for the analysis of SystemC models," in TACAS. Springer, 2008.
• 2: E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, "SATABS: SAT-based predicate abstraction for ANSI-C," in TACAS. Springer, 2005.
• 3: Robert H. B. Netzer , Barton P. Miller, What are race conditions?: Some issues and formalizations, ACM Letters on Programming Languages and Systems (LOPLAS), v.1 n.1, p.74-88, March 1992 [doi>10.1145/130616.130623]
• 4: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, ACM SIGPLAN Notices, v.35 n.5, p.219-232, May 2000
• 5: S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson, "Eraser: a dynamic data race detector for multithreaded programs," ACM, 1997.
• 6: Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 7: Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, ACM SIGPLAN Notices, v.41 n.6, June 2006
• 8: V. D'Silva, D. Kroening, and G. Weissenbacher, "A survey of automated techniques for formal software verification," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), vol. 27, no. 7, pp. 1165--1178, July 2008.
• 9: Moshe Y. Vardi, Formal techniques for SystemC verification, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California [doi>10.1145/1278480.1278527]
• 10: Thomas Witkowski , Nicolas Blanc , Daniel Kroening , Georg Weissenbacher, Model checking concurrent linux device drivers, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321719]
• 11: Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, ACM SIGPLAN Notices, v.39 n.6, May 2004
• 12: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 13: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 14: T. Ball and S. Rajamani, "Boolean programs: A model and process for software analysis," Microsoft Research, Tech. Rep., 2000.
• 15: Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005 [doi>10.1007/s10703-005-1489-x]
• 16: Alper Sen , Vinit Ogale , Magdy S. Abadir, Predictive runtime verification of multi-processor SoCs in SystemC, Proceedings of the 45th annual conference on Design automation, June 08-13, 2008, Anaheim, California [doi>10.1145/1391469.1391708]
• 17: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 18: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 19: C. Helmstetter , F. Maraninchi , L. Maillet-Contoz , M. Moy, Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip, Proceedings of the Formal Methods in Computer Aided Design, p.171-178, November 12-16, 2006 [doi>10.1109/FMCAD.2006.10]
• 20: Sudipta Kundu , Malay Ganai , Rajesh Gupta, Partial order reduction for scalable testing of systemC TLM designs, Proceedings of the 45th annual conference on Design automation, June 08-13, 2008, Anaheim, California [doi>10.1145/1391469.1391706]
• 21: C. Wang, Z. Yang, V. Kahlon, and A. Gupta, "Peephole partial order reduction," in TACAS, 2008.
• 22: Doron Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proceedings of the 6th International Conference on Computer Aided Verification, p.377-390, June 21-23, 1994
• 23: Doron Peled, All from One, One for All: on Model Checking Using Representatives, Proceedings of the 5th International Conference on Computer Aided Verification, p.409-423, June 28-July 01, 1993
• 24: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 25: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 26: Edmund Clarke , Himanshu Jain , Daniel Kroening, Verification of SpecC using predicate abstraction, Formal Methods in System Design, v.30 n.1, p.5-28, February 2007 [doi>10.1007/s10703-006-0020-3]
• 27: D. Kroening , N. Sharygina, Formal verification of SystemC by automatic hardware/software partitioning, Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design, p.101-110, July 11-14, 2005 [doi>10.1109/MEMCOD.2005.1487900]