×

Towards “mouldable code” via nested code graph transformation. (English) Zbl 1371.68051

Summary: Program transformation is currently de facto restricted to abstract syntax tree rewriting. However, many program transformation patterns, in particular in the realm of high-performance code generation, can more naturally be understood and expressed as graph transformations. We describe the conceptual organisation of a system based on application of algebraic graph transformation rules to data-flow and control-flow graphs, and outline the work, both theoretical and of implementation nature, that still needs to be done to realise this long-term project.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q42 Grammars and rewriting systems
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Anand, C. K.; Kahl, W., Multiloop: efficient software pipelining for modern hardware, (Spencer, B.; Storey, M.-A.; Stewart, D., Proc. CASCON 2007, (2007), IBM Centre for Advanced Studies Toronto), 260-263
[2] Allan, V. H.; Jones, R. B.; Lee, R. M.; Allan, S. J., Software pipelining, ACM Comput. Surv., 27, 367-432, (1995)
[3] Burstall, R.; Darlington, J., A transformation system for developing recursive programs, J. ACM, 24, 44-67, (1977) · Zbl 0343.68014
[4] Bauer, F.; Berghammer, R.; Broy, M.; Dosch, W.; Geiselbrechtinger, F.; Gnatz, R.; Hangel, E.; Hesse, W.; Krieg-Brückner, B.; Laut, A.; Matzner, T.; Möller, B.; Nickl, F.; Partsch, H.; Pepper, P.; Samelson, K.; Wirsing, M.; Wössner, H., The Munich project CIP. vol. I: the wide spectrum language CIP-L, LNCS, vol. 183, (1985), Springer-Verlag Berlin/Heidelberg/New York
[5] Bauer, F.; Ehler, H.; Horsch, A.; Möller, B.; Partsch, H.; Paukner, O.; Pepper, P., The Munich project CIP. vol. II: the transformation system CIP-S, LNCS, vol. 292, (1987), Springer-Verlag Berlin
[6] Bauer, F.; Möller, B.; Partsch, H.; Pepper, P., Formal program construction by transformations — computer-aided, intuition-guided programming, IEEE Trans. Softw. Eng., 15, 165-180, (1989) · Zbl 0664.68017
[7] (Broy, M.; Wirsing, M., Methods of Programming, Selected Papers of the CIP-project, LNCS, vol. 544, (1991), Springer) · Zbl 0875.00050
[8] Steinbrüggen, R., The use of nested scheme parameters in the system CIP, (Wilhelm, R., GI — 10. Jahrestagung, Saarbrücken, Informatik Fachberichte, vol. 33, (1980), Springer-Verlag), 106, extended abstract
[9] Klop, J. W., Combinatory reduction systems, (1980), Centre for Mathematics and Computer Science Amsterdam, Mathematical Centre Tracts 127, PhD thesis · Zbl 0466.03006
[10] Kelsey, R.; Hudak, P., Realistic compilation by program transformation — detailed summary, (16th POPL, (1989), ACM Press), 281-292
[11] Pettorossi, A.; Proietti, M., Rules and strategies for transforming functional and logic programs, ACM Comput. Surv., 28, 360-414, (1996)
[12] Pettorossi, A.; Proietti, M., Future directions in program transformation, (Position Statement at the Workshop on Strategic Directions in Computing Research, (June 14-15, 1996), MIT Cambridge, MA, USA), ACM Comput. Surv., 28, 4es, 99-102, (December 1996), Article 171
[13] Paige, R., Future directions in program transformations, SIGPLAN Not., 32, 94-98, (1997)
[14] Bird, R. S.; de Moor, O., Algebra of programming, International Series in Computer Science, vol. 100, (1997), Prentice Hall
[15] Visser, E., A survey of strategies in rule-based program transformation systems, Reduction Strategies in Rewriting and Programming, J. Symb. Comput., 40, 831-873, (2005), (special issue) · Zbl 1129.68043
[16] Kats, L. C.L.; Visser, E., The spoofax language workbench. rules for declarative specification of languages and ides, (Rinard, M., Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno, NV, USA, (2010)), 444-463
[17] Zierer, H.; Schmidt, G.; Berghammer, R., An interactive graphical manipulation system for higher objects based on relational algebra, (Tinhofer, G.; Schmidt, G., Graph-Theoretic Concepts in Computer Science, WG ’86, LNCS, vol. 246, (1986), Springer), 68-81
[18] Bayer, A.; Kahl, W., The higher-object programming system “HOPS”, (Buth, B.; Berghammer, R., Systems for Computer-Aided Specification, Development and Verification, Bericht Nr. 9416, Universität Kiel, (1994)), 154-171
[19] Bayer, A.; Grobauer, B.; Kahl, W.; Kempf, P.; Schmalhofer, F.; Schmidt, G.; Winter, M., The higher object programming system HOPS, (1996), Inst. für Informatik der Univ. der Bundeswehr München, Internal Report. 206 pp
[20] Bayer, A.; Derichsweiler, F., HOPS as a link between functional and data-flow oriented programming, (Berghammer, R.; Simon, F., Programming Languages and Fundamentals of Programming, Bericht Nr. 9717, (1997), Universität Kiel, Institut für Informatik und Praktische Mathematik), 209-217, Bericht Nr. 9717
[21] Derichsweiler, F., Strategy driven program transformation within the higher object programming system HOPS, (Poetzsch-Heffter, A.; Meyer, J., Programmiersprachen und Grundlagen der Programmierung, Informatik Berichte 263 — 1/2000, FU Hagen, (1999)), 165-172
[22] Kahl, W., Internally typed second-order term graphs, (Hromkovič, J.; Sýkora, O., Graph Theoretic Concepts in Computer Science, WG ’98, LNCS, vol. 1517, (1998), Springer), 149-163 · Zbl 0918.68086
[23] Kahl, W., The term graph programming system HOPS, (Berghammer, R.; Lakhnech, Y., Tool Support for System Specification, Development and Verification, Advances in Computing Science, (1999), Springer-Verlag Wien), 136-149 · Zbl 0979.68510
[24] Kahl, W.; Derichsweiler, F., Declarative term graph attribution for program generation, J. Univers. Comput. Sci., 7, 54-70, (2001) · Zbl 0973.68021
[25] Hoare, T., The verifying compiler: A grand challenge for computing research, J. ACM, 50, 63-69, (2003) · Zbl 1032.68868
[26] Leroy, X., Formal verification of a realistic compiler, Commun. ACM, 52, 107-115, (2009)
[27] (Beckert, B.; Hähnle, R.; Schmitt, P. H., Verification of Object-Oriented Software: The KeY Approach, LNCS, vol. 4334, (2007), Springer-Verlag)
[28] Cuoq, P.; Kirchner, F.; Kosmatov, N.; Prevosto, V.; Signoles, J.; Yakobowski, B., Frama-c: a software analysis perspective, (Proceedings of the 10th International Conference on Software Engineering and Formal Methods, SEFM’12, (2012), Springer-Verlag Berlin, Heidelberg), 233-247
[29] Krone, J.; Ogden, W. F.; Sitaraman, M.; Weide, B. W., Refocusing the verifying compiler grand challenge, (2008), School of Computing, Clemson University Clemson, SC, Tech. Report RSRG-08-01
[30] Kiczales, Gregor; Lamping, John; Mendhekar, Anurag; Maeda, Chris; Lopes, Christina; Loingtier, Jean-Marc; Irwin, John, Aspect-oriented programming, (Aksit, M.; Matsuoka, S., ECOOP’97 — Object-Oriented Programming, LNCS, vol. 1241, (1997), Springer), 220-242
[31] Gray, J., What next?: A dozen information-technology research goals, J. ACM, 50, 41-57, (2003)
[32] Gadducci, F., On the algebraic approach to concurrent term rewriting, (1996), Università degli studi di Pisa, Dipartimento di Informatica, PhD thesis
[33] Corradini, A.; Gadducci, F., An algebraic presentation of term graphs, via gs-monoidal categories, Appl. Categ. Struct., 7, 299-331, (1999) · Zbl 0949.68121
[34] Hasegawa, M., Models of sharing graphs, a categorical semantics of let and letrec, (1997), University of Edinburgh, PhD thesis
[35] Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G., Fundamentals of algebraic graph transformation, (2006), Springer · Zbl 1095.68047
[36] Kahl, W., Algebraische termgraphersetzung mit gebundenen variablen, reihe informatik, (1996), Herbert Utz Verlag Wissenschaft München, also Doctoral Diss. at Univ. der Bundeswehr München, Fakultät für Informatik
[37] Kahl, W., A fibred approach to rewriting — how the duality between adding and deleting cooperates with the difference between matching and rewriting, (1997), Fakultät für Informatik, Universität der Bundeswehr München, Technical Report 9702
[38] Anand, C. K.; Kahl, W., Synthesizing and verifying multicore parallelism in categories of nested code graphs, (Alexander, M.; Gardner, W., Process Algebra for Parallel and Distributed Processing, CRC Computational Science Series, vol. 2, (2009), Chapman & Hall), 3-45 · Zbl 1172.68403
[39] Dobrogost, M.; Anand, C. K.; Kahl, W., Verified multicore parallelism using atomic verifiable operations, (Qadri, M. Y.; Sangwine, S. J., Multicore Technology: Architecture, Reconfiguration, and Modeling, (2013), CRC Press), 107-151
[40] Baldan, P.; Corradini, A.; Ehrig, H.; Heckel, R., Compositional semantics for open Petri nets based on deterministic processes, Math. Struct. Comput. Sci., 15, 1-35, (2005) · Zbl 1089.68068
[41] Baldan, P.; Corradini, A.; Ehrig, H.; Heckel, R.; König, B., Bisimilarity and behaviour-preserving reconfigurations of open Petri nets, (Mossakowski, T.; Montanari, U.; Haveraaen, M., Algebra and Coalgebra in Computer Science, LNCS, vol. 4624, (2007), Springer Berlin, Heidelberg), 126-142 · Zbl 1214.68243
[42] Anand, C. K.; Kahl, W., An optimized cell BE special function library generated by coconut, IEEE Trans. Comput., 58, 1126-1138, (2009) · Zbl 1367.65203
[43] IBM, Cell BE SDK 3.1, This is the latest version of IBM’s Cell SDK and includes 32 single-precision special functions in in-lineable generated C header files, and as a library of long-vector functions scheduled by Coconut, and 32 double-precision special functions in in-lineable generated C header files, and as a library of long-vector functions all generated by Coconut., 2008.
[44] Kahl, W.; Anand, C. K.; Carette, J., Control-flow semantics for assembly-level data-flow graphs, (McCaull, W.; Winter, M.; Düntsch, I., 8th Intl. Seminar on Relational Methods in Computer Science, RelMiCS 8, Feb. 2005, LNCS, vol. 3929, (2006), Springer), 147-160 · Zbl 1185.68223
[45] Norell, U., Towards a practical programming language based on dependent type theory, (2007), Department of Computer Science and Engineering, Chalmers University of Technology, PhD thesis
[46] Kahl, W., Dependently-typed formalisation of relation-algebraic abstractions, (de Swart, H., Relational and Algebraic Methods in Computer Science, RAMiCS 2011, LNCS, vol. 6663, (2011), Springer), 230-247 · Zbl 1329.68063
[47] Kahl, W., Relation-algebraic theories in agda — RATH-agda-2.0.0, (2014), Mechanically checked Agda theories available for download, with 467 pages literate document output
[48] Hoffmann, B.; Plump, D., Implementing term rewriting by jungle evaluation, Inform. Théor. Appl., 25, 445-472, (1991) · Zbl 0706.68061
[49] Corradini, A.; Rossi, F., Hyperedge replacement jungle rewriting for term-rewriting systems and logic programming, Theor. Comput. Sci., 109, 1-2, 7-48, (1993) · Zbl 0781.68074
[50] Kozen, D., Typed Kleene algebra, (1998), Computer Science Department, Cornell University, Technical Report 98-1669
[51] Kahl, W., Refactoring heterogeneous relation algebras around ordered categories and converse, J. Relat. Methods Comput. Sci., 1, 277-313, (2004)
[52] Kahl, W., Dependently-typed formalisation of typed term graphs, (Echahed, R., Proc. of 6th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2011, EPTCS, vol. 48, (2011)), 38-53
[53] Kahl, W., Towards certifiable implementation of graph transformation via relation categories, (Kahl, W.; Griffin, T. G., Relational and Algebraic Methods in Computer Science, RAMiCS 2012, LNCS, vol. 7560, (2012), Springer), 82-97 · Zbl 1364.68309
[54] Kahl, W., Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types, J. Log. Algebr. Program., 76, 60-89, (2008) · Zbl 1139.18005
[55] Bishop, E., Foundations of constructive analysis, (1967), McGraw-Hill · Zbl 0183.01503
[56] Palmgren, E., Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Ann. Pure Appl. Log., 163, 1384-1399, (2012) · Zbl 1257.03095
[57] Sacerdoti Coen, C.; Tassi, E., Formalizing overlap algebras in matita, Math. Struct. Comput. Sci., 21, 1-31, (2011) · Zbl 1223.68102
[58] Pitts, A. M., Categorical logic, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. 5, (2001), Oxford University Press), 39-128
[59] Banach, R., A fibration semantics for extended term graph rewriting, (Sleep, M.; Plasmeijer, M.; van Eekelen, M., Term Graph Rewriting: Theory and Practice, (1993), Wiley), 91-100
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.