Abstract
We rationally reconstruct the core of the Coccinelle system, used for automating and documenting collateral evolutions in Linux device drivers. A denotational semantics of the system’s underlying semantic patch language (SmPL) is developed, and extended to include variables. The semantics is in essence a higher-order functional program and so executable; but is inefficient and limited to straight-line source programs. A richer and more efficient SmPL version is defined, implemented by compiling to the temporal logic CTL-V (CTL with existentially quantified variables ranging over source code parameters and program points; defined using the staging concept from partial evaluation). The compilation is formally proven correct and a model check algorithm is outlined.
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.
References
Bravenboer, M., Kalleberg, K.T., Vermaas, R., Visser, E.: Stratego/XT 0.16. Components for transformation systems. In: PEPM 2006, Charleston, South Carolina (January 2006)
Buckley, J., Mens, T., Zenger, M., Rashid, A., Kniesel, G.: Towards a taxonomy of software change. Journal of Software Maintenance and Evolution: Research and Practice 309–332 (2005)
Chapin, N., Hale, J.E., Khan, K.M., Ramil, J.F., Than, W.-G.: Types of software evolution and software maintenance. Journal of software maintenance and evolution: Research and Practice 13, 3–30 (2001)
De Moor, O., Lacey, D., van Wyk, E.: Universal regular path queries. Higher-order and Symbolic Computation 16(1-2), 15–35 (2003)
Dig, D., Johnson, R.: How do APIs evolve? a story of refactoring. Journal of Software Maintenance and Evolution: Research and Practice 18(2), 83–107 (2006)
Fiuczynski, M., Grimm, R., Coady, Y., Walker, D.: Patch (1) considered harmful. In: Workshop on Hot Topics in Operating Systems (2005)
Fiuczynski, M.E.: Better tools for kernel evolution, please! LOGIN 30(5), 8–10 (2006)
Godfrey, M.W., Tu, Q.: Evolution in open source software: A case study. In: ICSM, pp. 131–142 (2000)
Hansen, R.R., Jones, N.D.: The semantics of semantic patches in Coccinelle: Program transformation for the working programmer (full paper). Project home page: http://www.emn.fr/x-info/coccinelle/
Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2004)
Lacey, D., Jones, N.D., Van Wyk, E., Frederiksen, C.C.: Compiler optimization correctness by temporal logic. Higher Order and Symbolic Computation 17(3), 173–206 (2004)
Lacey, D.: Program Transformation using Temporal Logic Specifications. PhD thesis, Oxford University Computing Laboratory (2003)
Lacey, D., de Moor, O.: Imperative Program Transformation by Rewriting. In: Wilhelm, R. (ed.) CC 2001 and ETAPS 2001. LNCS, vol. 2027, pp. 52–68. Springer, Heidelberg (2001)
Lacey, D., Jones, N.D., van Wyk, E., Frederiksen, C.C.: Proving correctness of compiler optimizations by temporal logic. In: POPL 2002, vol. 29, pp. 283–294 (2002)
Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: PLDI 2003, pp. 220–231. ACM Press, New York (2003)
Liu, Y.A., Rothamel, T., Yu, F., Stoller, S.D., Hu, N.: Parametric regular path queries. In: PLDI 2004, pp. 219–230 (2004)
Padioleau, Y., Hansen, R.R., Lawall, J.L., Muller, G.: Semantic patches for documenting and automating collateral evolutions in Linux device drivers. In: PLOS 2006. Proc. of Workshop on Programming Languages and Operating Systems, p. 10 (2006)
Padioleau, Y., Lawall, J.L., Muller, G.: Understanding collateral evolution in Linux device drivers. In: EuroSys 2006, pp. 59–71 (2006)
Steffen, B.: Optimal run time optimization proved by a new look at abstract interpretation. In: Ehrig, H., Levi, G., Montanari, U. (eds.) CAAP 1987 and TAPSOFT 1987. LNCS, vol. 249, Springer, Heidelberg (1987)
Stuart, H., Hansen, R., Lawall, J.L., Andersen, J., Padioleau, Y., Muller, G.: Towards easing the diagnosis of bugs in OS code. In: PLOS 2007 (to appear, 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jones, N.D., Hansen, R.R. (2007). The Semantics of “Semantic Patches” in Coccinelle: Program Transformation for the Working Programmer . In: Shao, Z. (eds) Programming Languages and Systems. APLAS 2007. Lecture Notes in Computer Science, vol 4807. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76637-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-76637-7_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76636-0
Online ISBN: 978-3-540-76637-7
eBook Packages: Computer ScienceComputer Science (R0)