Formal Methods in System Design

, Volume 41, Issue 3, pp 295–320 | Cite as

InterAspect: aspect-oriented instrumentation with GCC

  • Justin Seyster
  • Ketan Dixit
  • Xiaowan Huang
  • Radu Grosu
  • Klaus Havelund
  • Scott A. Smolka
  • Scott D. Stoller
  • Erez Zadok


We present the InterAspect instrumentation framework for GCC, a widely used compiler infrastructure. The addition of plug-in support in the latest release of GCC makes it an attractive platform for runtime instrumentation, as GCC plug-ins can directly add instrumentation by transforming the compiler’s intermediate representation. Such transformations, however, require expert knowledge of GCC internals. InterAspect addresses this situation by allowing instrumentation plug-ins to be developed using the familiar vocabulary of Aspect-Oriented Programming: pointcuts, join points, and advice functions. Moreover, InterAspect uses specific information about each join point in a pointcut, possibly including results of static analysis, to support powerful customized instrumentation. We describe the InterAspect API and present several examples that illustrate its practical utility as a runtime-verification platform. We also introduce a tracecut system that uses InterAspect to construct program monitors that are formally specified as regular expressions.


Program instrumentation Aspect-oriented programming GCC Monitoring Tracecut 



We thank the anonymous reviewers for their valuable comments. Part of the research described herein was carried out at the Jet Propulsion Laboratory (JP), California Institute of Technology, under a contract with the National Aeronautics and Space Administration. Research described here was supported in part by AFOSR Grant FA9550-09-1-0481, NSF Grants CCF-0926190, CCF-0613913, CNS-0831298, and CNS-0509230, and ONR Grants N00014-07-1-0928 and N00014-09-1-0651.


  1. 1.
    GCC 4.5 release series changes, new features, and fixes.
  2. 2.
  3. 3.
  4. 4.
    Adams B, Herzeel C, Gybels K (2008) cHALO, stateful aspects in C. In: ACP4IS ’08: Proceedings of the 2008 AOSD workshop on aspects, components, and patterns for infrastructure software, New York, NY, USA. ACM, New York, pp 1–6 CrossRefGoogle Scholar
  5. 5.
    Allan C, Avgustinov P, Christensen AS, Hendren L, Kuzins S, Lhoták O, de Moor O, Sereni D, Sittamplan G, Tibble J (2005) Adding trace matching with free variables to AspectJ. In: Proceedings of the 20th annual ACM SIGPLAN conference on object-oriented programming, systems, languages and applications (OOPSLA’05). ACM Press, New York Google Scholar
  6. 6.
  7. 7.
  8. 8.
    Avgustinov P, Christensen AS, Hendren L, Kuzins S, Lhoták J, Lhoták O, de Moor O, Sereni D, Sittampalam G, Tibble J (2005) Abc: An extensible AspectJ compiler. In: Proceedings of the fourth international conference on aspect-oriented software development. ACM Press, New York Google Scholar
  9. 9.
    Bodden E, Havelund K (2008) Racer: Effective race detection using AspectJ. In: Proceedings of the ACM/SIGSOFT international symposium on software testing and analysis (ISSTA). ACM, New York, pp 155–165 Google Scholar
  10. 10.
    Callanan S, Dean DJ, Zadok E (2007) Extending GCC with modular GIMPLE optimizations. In: Proceedings of the 2007 GCC developers’ summit, Ottawa, Canada, July, pp 31–37 Google Scholar
  11. 11.
    Chen F, Roşu G (2007) MOP: an efficient and generic runtime verification framework. In: Proceedings of the 22nd annual ACM SIGPLAN conference on object-oriented programming, systems, languages and applications (OOPSLA’07) Google Scholar
  12. 12.
    Chiba S (1995) A metaobject protocol for C++. In: Proceedings of the ACM conference on object-oriented programming systems, languages, and applications, October, pp 285–299 Google Scholar
  13. 13.
    Chiba S (2000) Load-time structural reflection in Java. In: Proceedings of the 14th European conference on object-oriented programming. LNCS, vol 1850. Springer, Berlin, pp 313–336 Google Scholar
  14. 14.
    Coady Y, Kiczales G, Feeley M, Smolyn G (2001) Using AspectC to improve the modularity of path-specific customization in operating system code. In: Proceedings of the 9th ACM SIGSOFT symposium on the foundations of software engineering (FSE), pp 88–98 Google Scholar
  15. 15.
    Douence R, Fritz T, Loriant N, Menaud J-M, Ségura-Devillechaise M, Südholt M (2005) An expressive aspect language for system applications with Arachne. In: Proceedings of the 4th international conference on aspect-oriented software development (AOSD). ACM Press, New York Google Scholar
  16. 16.
    Eclipse Foundation T AspectJ.
  17. 17.
    Fei L, Midkiff SP (2005) Artemis: Practical runtime monitoring of applications for errors. Tech Rep TR-ECE-05-02, Electrical and Computer Engineering, Purdue University.
  18. 18.
    AT&T Research Labs. Graphviz, 2009.
  19. 19.
    Huang X, Seyster J, Callanan S, Dixit K, Grosu R, Smolka SA, Stoller SD, Zadok E (2012) Software monitoring with controllable overhead. Int J Softw Tools Technol Transf 14(3):327–347 CrossRefGoogle Scholar
  20. 20.
  21. 21.
    Kiczales G, Hilsdale E, Hugunin J, Kersten M, Palm J, Griswold WG (2001) An overview of AspectJ. In: Proceedings of the 15th European conference on object-oriented programming. LNCS, vol 2072, pp 327–355 Google Scholar
  22. 22.
    Kneschke J (2009) Lighttpd.
  23. 23.
    Meredith PO, Jin D, Griffith D, Chen F, Roşu G (2011) An overview of the MOP runtime verification framework. Int J Softw Tech Technol Transf, to appear Google Scholar
  24. 24.
    Necula GC, McPeak S, Rahul SP, Weimer W (2002) CIL: Intermediate language and tools for analysis and transformation of C programs. In: Proceedings of the 11th international conference on compiler construction. Springer, Berlin, pp 213–228 Google Scholar
  25. 25.
    Nicoara A, Alonso G, Roscoe T (2008) Controlled, systematic, and efficient code replacement for running Java programs. In: Proceedings of the ACM EuroSys conference, Glasgow, Scotland, UK, April Google Scholar
  26. 26.
  27. 27.
    Poskanzer J (2006) http_load.
  28. 28.
    Rohlik O, Pasetti A, Cechticky V, Birrer I (2004) Implementing adaptability in embedded software through aspect oriented programming. IEEE Mechatron Robot 85–90 Google Scholar
  29. 29.
    Seyster J, Dixit K, Huang X, Grosu R, Havelund K, Smolka SA, Stoller SD, Zadok E (2010) Aspect-oriented instrumentation with GCC. In: Proc. of the 1st international conference on runtime verification (RV), November. Lecture Notes in Computer Science. Springer, Berlin Google Scholar
  30. 30.
    Spinczyk O, Lohmann D (2007) The design and implementation of AspectC++. Knowl-Based Syst 20(7):636–651 CrossRefGoogle Scholar
  31. 31.
  32. 32.
    Walker R, Viggers K (2004) Implementing protocols via declarative event patterns. In: Taylor R, Dwyer M (eds) ACM Sigsoft 12th international symposium on foundations of software engineering (FSE-12). ACM Press, New York, pp 159–169 Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  • Justin Seyster
    • 1
  • Ketan Dixit
    • 1
  • Xiaowan Huang
    • 1
  • Radu Grosu
    • 1
  • Klaus Havelund
    • 2
  • Scott A. Smolka
    • 1
  • Scott D. Stoller
    • 1
  • Erez Zadok
    • 1
  1. 1.Department of Computer ScienceStony Brook UniversityStony BrookUSA
  2. 2.Jet Propulsion LaboratoryCalifornia Institute of TechnologyPasadenaUSA

Personalised recommendations