Abstract
Code generation is gaining popularity as a technique to bridge the gap between high-level models and executable code. We describe the theory underlying the PVS2C code generator that translates functional programs written using the PVS specification language to standalone, efficiently executable C code. We outline a correctness argument for the code generator. The techniques used are quite generic and can be applied to transform programs written in functional languages into imperative code. We use a formal model of reference counting to capture memory management and safe destructive updates for a simple first-order functional language with arrays. We exhibit a bisimulation between the functional execution and the imperative execution. This bisimulation shows that the generated imperative program returns the same result as the functional program.
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
Similar content being viewed by others
Notes
- 1.
We had initially used a different semantics for the imperative language based on call stacks and program counters that is closer to the machine execution, but this led to a fairly cumbersome definition of the bisimulation. We found the mechanization (https://github.com/SRI-CSL/PVSCodegen) of the correspondence quite challenging. The correspondence given here between RL and KL executions has not yet been formalized using a proof assistant, but we expect it to be a significantly easier exercise.
- 2.
Note that due to the recursion on type structure, the termination proofs do not need to assume that the store is non-cyclic. In our mechanization, we use a slightly different definition and exploit Invariant 13 and the invariant (also implicit in \(\mathbf {decref}\)) that \(\mathcal {M}\) contains no (dangling) references that are not in the domain of \(\mathcal {M}\) so that the total reference count in \(\mathcal {M}\) decreases with each call to \(\mathbf {decref}\).
References
Appel, A.W., Blazy, S.: Separation logic for small-step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74591-4_3
Aspinall, D., Hofmann, M.: Another type system for in-place update. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 36–52. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45927-8_4
Bevier, W.R., Hunt, W.A., Moore Jr., J.S., Young, W.D.: An approach to systems verification. J. Autom. Reason. 5(4), 411–428 (1989)
Chirimar, J., Gunter, C.A., Riecke, J.G.: Reference counting as a computational interpretation of linear logic. J. Funct. Program. 6(2), 195–244 (1996)
Collins, G.E.: A method for overlapping and erasure of lists. Commun. ACM 3(12), 655–657 (1960)
Didrich, K., Fett, A., Gerke, C., Grieskamp, W., Pepper, P.: OPAL: design and implementation of an algebraic programming language. In: Gutknecht, J. (ed.) Programming Languages and System Architectures. LNCS, vol. 782, pp. 228–244. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-57840-4_34
Draghicescu, M., Purushothaman, S.: A uniform treatment of order of evaluation and aggregate update. Theor. Comput. Sci. 118(2), 231–262 (1993)
Emmi, M., Jhala, R., Kohler, E., Majumdar, R.: Verifying reference counting implementations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 352–367. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_30
Felleisen, M.: On the expressive power of programming languages. In: Jones, N. (ed.) ESOP 1990. LNCS, vol. 432, pp. 134–151. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52592-0_60
Férey, G., Shankar, N.: Code Generation using a formal model of reference counting. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 150–165. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_12
Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations (with retrospective). In: McKinley, K.S. (ed.) Best of PLDI, pp. 502–514. ACM (1993)
Gopinath, K., Hennessy, J.L.: Copy elimination in functional languages. In: 16th ACM Symposium on Principles of Programming Languages. Association for Computing Machinery, January 1989
Hudak, P.: A semantic model of reference counting and its abstraction (detailed summary). In: Proceedings 1986 ACM Conference on LISP and Functional Programming, pp. 351–363. ACM, August 1986
Hudak, P., Bloss, A.: The aggregate update problem in functional programming systems. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1985, pp. 300–314. ACM, New York (1985)
Kanade, A., Sanyal, A., Khedker, U.: A PVS based framework for validating compiler optimizations. In: Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006) (2006)
Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 179–191. ACM, New York (2014)
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Harold McBeth, J.: On the reference counter method. Commun. ACM 6(9), 575 (1963)
Moreau, L., Duprat, J.: A construction of distributed reference counting. Acta Inf. 37(8), 563–595 (2001)
Polak, W.: Compiler Specification and Verification. Springer, Berlin (1981)
Schulte, W.: Deriving residual reference count garbage collectors. In: Hermenegildo, M., Penjam, J. (eds.) PLILP 1994. LNCS, vol. 844, pp. 102–116. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58402-1_9
Shankar, N.: Static analysis for safe destructive updates in a functional language. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol. 2372, pp. 1–24. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45607-4_1
Shankar, N.: A brief introduction to the PVS2C code generator. In: Dutertre, B., Shankar, N. (eds.) AFM@NFM, EasyChair, vol. 5, pp. 109–116. Kalpa Publications in Computing (2017)
David W.J.: Stringer-Calvert. Mechanical Verification of Compiler Correctness. Ph.D. thesis, University of York, Department of Computer Science, York, England, March 1998
Ullrich, S., de Moura, L.: Counting immutable beans: Reference counting optimized for purely functional programming. CoRR, abs/1908.05647, 2019. Appears in pre-conference proceedings of IFL2019: http://2019.iflconference.org/pre-conference-proceedings.pdf
Wand, M., Clinger, W.D.: Set constraints for destructive array update optimization. In: Proceedings of the IEEE Conference on Computer Languages 1998, pp. 184–193. IEEE, April 1998
Acknowledgment
This work was supported by the National Institute of Aerospace Award C18-201097-SRI, NSF Grant SHF-1817204, and DARPA under agreement number HR001119C0075. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of NASA, NSF, DARPA, or the U.S. Government. We thank the anonymous referees for their constructive feedback.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Courant, N., Séré, A., Shankar, N. (2020). The Correctness of a Code Generator for a Functional Language. In: Beyer, D., Zufferey, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2020. Lecture Notes in Computer Science(), vol 11990. Springer, Cham. https://doi.org/10.1007/978-3-030-39322-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-39322-9_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-39321-2
Online ISBN: 978-3-030-39322-9
eBook Packages: Computer ScienceComputer Science (R0)