×

zbMATH — the first resource for mathematics

A resource semantics and abstract machine for Safe: a functional language with regions and explicit deallocation. (English) Zbl 1358.68059
Summary: In this paper we summarise Safe, a first-order functional language for programming small devices and embedded systems with strict memory requirements, which has been introduced elsewhere. It has some unusual memory management features such as heap regions and explicit cell deallocation. It is targeted at a proof carrying code environment, and consistently with this aim the Safe compiler provides machine checkable certificates about important safety properties such as the absence of dangling pointers and bounded memory consumption.
The kernel of the paper is devoted to developing part of the Safe compiler’s back-end, by deriving an appropriate abstract machine from the language semantics, by providing the code generation functions, and by formally proving that the translation is sound, both in the semantic and in the memory consumption senses.

MSC:
68N18 Functional programming and lambda calculus
68N20 Theory of compilers and interpreters
Software:
Isabelle/HOL; LLVM
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Necula, G. C., Proof-carrying code, (Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’97, (1997), ACM Press), 106-119
[2] Siebert, F., Hard realtime garbage collection in modern object oriented programming, (2002), Books on Demand GmbH
[3] Montenegro, M.; Peña, R.; Segura, C., A type system for safe memory management and its proof of correctness, (Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP’08, (2008), ACM Press), 152-162
[4] Montenegro, M.; Peña, R.; Segura, C., An inference algorithm for guaranteeing safe destruction, (Selected Papers of the 18th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR’08, Lect. Notes Comput. Sci., vol. 5438, (2009), Springer), 135-151 · Zbl 1185.68200
[5] Montenegro, M.; Peña, R.; Segura, C., A simple region inference algorithm for a first-order functional language, (Selected Papers of the 18th International Workshop on Functional and (Constraint) Logic Programming, WFLP’09, Lect. Notes Comput. Sci., vol. 5979, (2009), Springer), 145-161
[6] Montenegro, M.; Peña, R.; Segura, C., A space consumption analysis by abstract interpretation, (Selected Papers of the 1st International Workshop on Foundational and Practical Aspects of Resource Analysis, FOPARA’09, Lect. Notes Comput. Sci., vol. 6324, (2009), Springer), 34-50 · Zbl 1305.68062
[7] de Dios, J.; Montenegro, M.; Peña, R., Certified absence of dangling pointers in a language with explicit deallocation, (Proceedings of the 8th International Conference on Integrated Formal Methods, IFM’10, Lect. Notes Comput. Sci., vol. 6396, (2010), Springer), 305-319
[8] de Dios, J.; Peña, R., Certification of safe polynomial memory bounds, (Int. Symp. on Formal Methods, FM’11, Lect. Notes Comput. Sci., vol. 6664, (2011), Springer), 184-199
[9] de Dios, J.; Peña, R., Formal certification of a resource-aware language implementation, (Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOL’09, Lect. Notes Comput. Sci., vol. 5674, (2009), Springer), 196-211 · Zbl 1252.68070
[10] de Dios, J.; Peña, R., A certified implementation on top of the Java virtual machine, (Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems, FMICS’09, Lect. Notes Comput. Sci., vol. 5825, (2009), Springer), 1-16
[11] Montenegro, M.; Peña, R.; Segura, C., A resource-aware semantics and abstract machine for a functional language with explicit deallocation, Selected Papers of the 17th Workshop on Functional and (Constraint) Logic Programming, WFLP’08, Electron. Notes Theor. Comput. Sci., 246, 167-182, (2009) · Zbl 1347.68054
[12] Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/HOL. A proof assistant for higher-order logic, Lect. Notes Comput. Sci., vol. 2283, (2002), Springer · Zbl 0994.68131
[13] Flanagan, C.; Sabry, A.; Duba, B. F.; Felleisen, M., The essence of compiling with continuations, (Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI’93, (1993), ACM), 237-247
[14] Tofte, M.; Talpin, J.-P., Region-based memory management, Inf. Comput., 132, 109-176, (1997) · Zbl 0876.68027
[15] Aiken, A.; Fähndrich, M.; Levien, R., Better static memory management: improving region-based analysis of higher-order languages, (Proceedings of the ACM SIGPLAN 1995 Conference on Programming Language Design and Implementation, PLDI’95, (1995)), 174-185
[16] Birkedal, L.; Tofte, M.; Vejlstrup, M., From region inference to von Neumann machines via region representation inference, (Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (1996), ACM Press), 171-183
[17] Tofte, M.; Birkedal, L.; Elsman, M.; Hallenberg, N.; Olesen, T. H.; Sestoft, P., Programming with regions for the mlkit, (2006), University of Copenhagen, Technical Report
[18] Fluet, M.; Morrisett, G.; Ahmed, A., Linear regions are all you need, (15th European Symposium on Programming, ESOP 2006, (2006), Springer), 7-21 · Zbl 1178.68151
[19] Peña, R.; Segura, C.; Montenegro, M., A sharing analysis for SAFE, (Trends in Functional Programming, vol. 7, Selected Papers of the 7th Symposium on Trends in Functional Programming, TFP’06, (2007), Intellect), 109-128
[20] Montenegro, M., Safety properties and memory bound analysis in a functional language without a garbage collector, (2011), Facultad de Informática, Universidad Complutense de Madrid, PhD thesis
[21] Hofmann, M.; Jost, S., Static prediction of heap space usage for first-order functional programs, (Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (2003)), 185-197 · Zbl 1321.68180
[22] Hannan, J.; Miller, D., From operational semantics to abstract machines, Math. Struct. Comput. Sci., 2, 415-459, (1992) · Zbl 0798.68099
[23] Ager, M. S.; Biernacki, D.; Danvy, O.; Midtgaard, J., A functional correspondence between evaluators and abstract machines, (Proceedings of the 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP’03, (2003), ACM Press), 8-19
[24] Kluge, W., Abstract computing machines: A lambda calculus perspective, Texts Theor. Comput. Sci., (2005), Springer · Zbl 1075.68003
[25] Sestoft, P., Deriving a lazy abstract machine, J. Funct. Program., 7, 3, 231-264, (1997) · Zbl 0881.68049
[26] de la Encina, A.; Peña, R., From natural semantics to C: A formal derivation of two STG machines, J. Funct. Program., 19, 1, 47-94, (2008) · Zbl 1159.68005
[27] Landin, P., The mechanical evaluation of expressions, Comput. J., 6, 4, 308-320, (1964) · Zbl 0122.36106
[28] Gaertner, D.; Kluge, W., π-RED^+ - an interactive compiling graph reduction system for an applied λ-calculus, J. Funct. Program., 6, 5, 723-757, (1996)
[29] Aspinall, D.; Beringer, L.; Hofmann, M.; Loidl, H.-W.; Momigliano, A., A program logic for resources, Theor. Comput. Sci., 389, 411-445, (2007) · Zbl 1133.68010
[30] Hofmann, M.; Jost, S., Static prediction of heap space usage for first-order functional programs, (Proceedings of the 30th ACM Symposium on Principles of Programming Languages, POPL’03, (2003), ACM Press), 185-197 · Zbl 1321.68180
[31] Hoffmann, J.; Hofmann, M., Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs, (Proceedings of the 19th European Symposium on Programming, ESOP’10, Lect. Notes Comput. Sci., vol. 6012, (2010), Springer), 287-306 · Zbl 1260.68074
[32] Jost, S.; Hammond, K.; Loidl, H.-W.; Hofmann, M., Static determination of quantitative resource usage for higher-order programs, (Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL’10, (2010)), 223-236 · Zbl 1312.68039
[33] Shkaravska, O.; van Eekelen, M. C.J. D.; van Kesteren, R., Polynomial size analysis of first-order shapely functions, Log. Methods Comput. Sci., 5, (2009) · Zbl 1163.68009
[34] Dave, M. A., Compiler verification: a bibliography, SIGSOFT Softw. Eng. Notes, 28, (2003), 2-2
[35] Dold, A.; Vialard, V., A mechanically verified compiling specification for a lisp compiler, (Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’01, Lect. Notes Comput. Sci., vol. 2245, (2001), Springer), 144-155 · Zbl 1052.68584
[36] Strecker, M., Formal verification of a Java compiler in isabelle, (CADE-18, 18th International Conference on Automated Deduction, CADE’02, Lect. Notes Comput. Sci., vol. 2392, (2002), Springer), 63-77 · Zbl 1072.68593
[37] Klein, G.; Nipkow, T., Verified bytecode verifiers, Theor. Comput. Sci., 298, 583-626, (2003) · Zbl 1038.68109
[38] Klein, G.; Nipkow, T., A machine-checked model for a Java-like language, virtual machine and compiler, ACM Trans. Program. Lang. Syst., 28, 4, 619-695, (2006)
[39] Berghofer, S.; Strecker, M., Extracting a formally verified, fully executable compiler from a proof assistant, Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler, COCV’03, Electron. Notes Theor. Comput. Sci., 82, 2, 377-394, (2004)
[40] Blazy, S.; Dargaye, Z.; Leroy, X., Formal verification of a C compiler front-end, (Proceedings of the 14th Symposium on Formal Methods, FM’06, Lect. Notes Comput. Sci., vol. 4085, (2006), Springer), 460-475
[41] Leroy, X., Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, (Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’06, (2006), ACM Press), 42-54 · Zbl 1369.68124
[42] Leroy, X., A formally verified compiler back-end, J. Autom. Reason., 43, 4, 363-446, (2009) · Zbl 1185.68215
[43] Lattner, C.; Adve, V., LLVM: A compilation framework for lifelong program analysis & transformation, (Proceedings of the 2004 International Symposium on Code Generation and Optimization, CGO’04, (2004), ACM), 75-87
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.