research-article

ReCaml: execution state as the cornerstone of reconfigurations

Authors:

Jérémy Buisson,

Fabien DagnatAuthors Info & Claims

ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming

Pages 27 - 38

https://doi.org/10.1145/1863543.1863550

Published: 27 September 2010 Publication History

Abstract

To fix bugs or to enhance a software system without service disruption, one has to update it dynamically during execution. Most prior dynamic software updating techniques require that the code to be changed is not running at the time of the update. However, this restriction precludes any change to the outermost loops of servers, OS scheduling loops and recursive functions. Permitting a dynamic update to more generally manipulate the program's execution state, including the runtime stack, alleviates this restriction but increases the likelihood of type errors. In this paper we present ReCaml, a language for writing dynamic updates to running programs that views execution state as a delimited continuation. ReCaml includes a novel feature for introspecting continuations called match_cont which is sufficiently powerful to implement a variety of updating policies. We have formalized the core of ReCaml and proved it sound (using the Coq proof assistant), thus ensuring that state-manipulating updates preserve type-safe execution of the updated program. We have implemented ReCaml as an extension to the Caml bytecode interpreter and used it for several examples.

Supplementary Material

JPG File (icfp-mon-1150-buisson.jpg)

Download
13.40 KB

MOV File (icfp-mon-1150-buisson.mov)

Download
102.83 MB

References

[1]

}}Gautam Altekar, Ilya Bagrak, Paul Burstein, and Andrew Schultz. Opus: online patches and updates for security. In USENIX Security Symposium, pages 287--302, Baltimore, Maryland, USA, August 2005.

Digital Library

[2]

}}Pascalin Amagbégnon, Loïc Besnard, and Paul Le Guernic. Implementation of the dataflow synchronous language SIGNAL. ACM SIGPLAN Notices, 30(6):163--173, June 1995.

Digital Library

[3]

}}Jonathan Appavoo, Kevin Hui, Craig Soules, Robert Wisniewski, Dilma Da Silva, Orran Krieger, Marc Auslander, David Edelsohn, Ben Gamsa, Gregory Ganger, Paul McKenney, Michal Ostrowski, Bryan Rosenburg, Michael Stumm, and Jimi Xenidis. Enabling autonomic behavior in systems software with hot swapping. IBM Systems Journal, 42(1):60--76, 2003.

Digital Library

[4]

}}Jeff Arnold and M. Frans Kaashoek. Ksplice: automatic rebootless kernel updates. In European Conference on Computer Systems, pages 187--198, Nuremberg, Germany, April 2009.

Digital Library

[5]

}}Kenichi Asai and Yukiyoshi Kameyama. Polymorphic delimited continuations. In Asian Symposium on Programming Languages and Systems, volume 4807 of LNCS, pages 239--254, Singapore, December 2007.

Digital Library

[6]

}}Brian Aydemir, Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, Stephanie Weirich, and Steve Zdancewic. Using proof assistants for programming language research or, how to write your next popl paper in coq. http://www.cis.upenn.edu/~plclub/popl08-tutorial/, 2008. POPL 2008 tutorial.

[7]

}}Andrew Baumann, Jonathan Appavoo, Robert Wisniewski, Dilma Da Silva, Orran Krieger, and Gernot Heiser. Reboots are for hardware: challenges and solutions to updating an operating system on the fly. In USENIX Annual Technical Conference, Santa Clara, California, USA, June 2007.

Digital Library

[8]

}}Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith Wansbrough. Dynamic rebinding for mashalling and update, with destruct-time λ. In International Conference on Functional Programming, pages 99--110, Uppsala, Sweden, August 2003.

Digital Library

[9]

}}Eric Bruneton, Thierry Coupaye, Matthieu Leclerq, Vivien Quéma, and Jean-Bernard Stefani. The Fractal component and its support in java. Software: Practice & Experience, special issue on experiences with auto-adaptive and reconfigurable systems, 36(11-12):1257--1284, September 2006.

Digital Library

[10]

}}Jérémy Buisson and Fabien Dagnat. Introspecting continuations in order to update active code. In Workshop on Hot Topics in Software Upgrades, Nashville, Tennessee, USA, October 2008.

Digital Library

[11]

}}Acacio Cruz. Official Gmail Blog: Update on today's Gmail outage. http://gmailblog.blogspot.com/2009/02/update-on-todays-gmail-outage.html, February 2009.

[12]

}}Mikhail Dmitriev. Safe class and data evolution in large and long-lived java applications. Technical Report TR-2001-98, Sun Microsystems, August 2001.

Digital Library

[13]

}}Kent Dybvig, Simon Peyton-Jones, and Amr Sabry. A monadic framework for delimited continuations. Journal of Functional Programming, 17(6):687--730, November 2007.

Digital Library

[14]

}}Ericsson AB. Erlang 5.6.3 Reference manual, chapter 12. Compilation and code loading. 2008. http://www.erlang.org/doc/reference_manual/part_frame.html.

[15]

}}Matthias Felleisen. The theory and practice of first-class prompts. In Principles of Programming Languages, pages 180--190, San Diego, California, USA, January 1988.

Digital Library

[16]

}}Stephen Gilmore, Dilsun Kirli, and Christopher Walton. Dynamic ML without dynamic types. Technical Report ECS-LFCS-97-379, University of Edinburgh, December 1997.

[17]

}}Carl A. Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In International Conference on Functional Programming Languages and Computer Architecture, pages 12--23, La Jolla, California, USA, June 1995.

Digital Library

[18]

}}Deepak Gupta, Pankaj Jalote, and Gautam Barua. A formal framework for on-line software version change. IEEE Transactions on Software Engineering, 22(2):120--131, February 1996.

Digital Library

[19]

}}Jennifer Hamilton, Michael Magruder, James Hogg, William Evans, Vance Morrison, Lawrence Sullivan, Sean Trowbridge, Jason Zander, Ian Carmichael, Patrick Dussud, John Hamby, John Rivard, Li Zhang, Mario Chenier, Douglas Rosen, Steven Steiner, Peter Hallam, Brian Crawford, James Miller, Sam Spencer, and Habib Heydarian. Method and system for program editing and debugging in a common language runtime environment. Patent US7516441, Microsoft Corporation, April 2009.

[20]

}}Christine Hofmeister and James Purtilo. Dynamic reconfiguration in distributed systems: adapting software modules for replacement. In International Conference on Distributed Computing Systems, pages 101--110, Pittsburgh, Pennsylvania, USA, May 1993.

[21]

}}Oleg Kiselyov. How to remove a dynamic prompt: static and dynamic delimited continuation operators are equally expressible. Technical Report TR611, Indiana University, March 2005.

[22]

}}Jeff Kramer and Jeff Magee. The evolving philosophers problem: dynamic change management. IEEE Transactions on Software Engineering, 16(11):1293--1306, November 1990.

Digital Library

[23]

}}Xavier Leroy. The ZINC experiment, an economical implementation of the ML language. Technical Report 117, INRIA, 1990.

[24]

}}Xavier Leroy. Polymorphism by name for references and continuations. In Principles of Programming Languages, pages 220--231, Charleston, South Carolina, USA, January 1993.

Digital Library

[25]

}}Kristis Makris and Rida Bazzi. Multi-threaded dynamic software updates using stack reconstruction. In USENIX Annual Technical Conference, San Diego, California, USA, June 2009.

Digital Library

[26]

}}Kristis Makris and Kyung Dong Ryu. Dynamic and adaptive updates of non-quiescent subsystems in commodity operating system kernels. In European Conference on Computer Systems, pages 327--340, Lisboa, Portugal, March 2007.

Digital Library

[27]

}}Simon Marlow and Simon Peyton-Jones. Making a fast curry: push/enter vs eval/apply for higher-order languages. Journal of Functionnal Programming, 16(4-5):415--449, July 2006.

Digital Library

[28]

}}Iulian Neamtiu, Micheal Hicks, Gareth Stoyle, and Manuel Oriol. Practical dynamic software updating for C. In Conference on Programming Language Design and Implementation, pages 72--83, Ottawa, Ontario, Canada, June 2006.

Digital Library

[29]

}}Greg Pettyjohn, John Clements, Joe Marshall, Shriram Krishnamurthi, and Matthias Felleisen. Continuations from generalized stack inspection. In International Conference on Functional Programming, pages 216--227, Tallinn, Estonia, September 2005.

Digital Library

[30]

}}Benjamin Pierce. Lambda, the ultimate TA: Using a proof assistant to teach programming language foundations, September 2009. Keynote address at International Conference on Functional Programming.

Digital Library

[31]

}}Benjamin Pierce, Chris Casinghino, and Michael Greenberg. Software foundations. 2010. http://www.cis.upenn.edu/~bcpierce/sf/.

[32]

}}Tiark Rompf, Ingo Maier, and Martin Odersky. Implementing firstclass polymorphic delimited continuations by a type-directed selective CPS transform. In International Conference on Functional Programming, Edinburgh, Scotland, UK, September 2009.

Digital Library

[33]

}}Peter Sewell, Gareth Stoyle, Michael Hicks, Gavin Bierman, and Keith Wansbrough. Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction. Journal of Functional Programming, 18(4):437--502, July 2008.

Digital Library

[34]

}}Chung-Chieh Shan. Shift to control. In ACM SIGPLAN Scheme Workshop, Snowbird, Utah, USA, September 2004.

[35]

}}Mads Tofte. Type inference for polymorphic references. Information and computation, 89(1):1--34, November 1990.

Digital Library

[36]

}}Yves Vandewoude, Peter Ebraert, Yolande Berbers, and Theo D'Hondt. Tranquility: a low disruptive alternative to quiescence for ensuring safe dynamic updates. IEEE Transactions on Software Engineering, 33(12):856--868, December 2007.

Digital Library

[37]

}}Andrew Wright. Polymorphism for imperative languages without imperative types. Technical Report TR93--200, Rice University, February 1993.

Cited By

Buisson JCalvacante EDagnat FLeroux EMartinez SSeinturier LAlmeida ECarlson J(2014)Coqcots & pycotsProceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering10.1145/2602458.2602459(85-90)Online publication date: 27-Jun-2014
https://dl.acm.org/doi/10.1145/2602458.2602459
Seifzadeh HAbolhassani HMoshkenani M(2012)A survey of dynamic software updatingJournal of Software: Evolution and Process10.1002/smr.155625:5(535-568)Online publication date: 25-Apr-2012
https://doi.org/10.1002/smr.1556
Cortier ABesnard LBodeveix JBuisson JDagnat FFilali MGarcia GOuy JPantel MRugina AStrecker MTalpin J(2010)Synoptic: A Domain-Specific Modeling Language for Space On-board Application SoftwareSynthesis of Embedded Software10.1007/978-1-4419-6400-7_3(79-119)Online publication date: 26-Jun-2010
https://doi.org/10.1007/978-1-4419-6400-7_3
Show More Cited By

Index Terms

ReCaml: execution state as the cornerstone of reconfigurations
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. General programming languages
      1. Language features
        Control structures
      2. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

ReCaml: execution state as the cornerstone of reconfigurations
ICFP '10

To fix bugs or to enhance a software system without service disruption, one has to update it dynamically during execution. Most prior dynamic software updating techniques require that the code to be changed is not running at the time of the update. ...
Dynamic software updates: a VM-centric approach
PLDI '09

Software evolves to fix bugs and add features. Stopping and restarting programs to apply changes is inconvenient and often costly. Dynamic software updating (DSU) addresses this problem by updating programs while they execute, but existing DSU systems ...
Dynamic software updates: a VM-centric approach
PLDI '09: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation

Software evolves to fix bugs and add features. Stopping and restarting programs to apply changes is inconvenient and often costly. Dynamic software updating (DSU) addresses this problem by updating programs while they execute, but existing DSU systems ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming

September 2010

398 pages

ISBN:9781605587943

DOI:10.1145/1863543

General Chair:
Paul Hudak
Yale University, USA
,
Program Chair:
Stephanie Weirich
University of Pennsylvania, USA

ACM SIGPLAN Notices Volume 45, Issue 9
ICFP '10
September 2010
382 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1932681
Issue’s Table of Contents

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 September 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '10

Sponsor:

SIGPLAN

ICFP '10: ACM SIGPLAN International Conference on Functional Programming

September 27 - 29, 2010

Maryland, Baltimore, USA

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
282
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Buisson JCalvacante EDagnat FLeroux EMartinez SSeinturier LAlmeida ECarlson J(2014)Coqcots & pycotsProceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering10.1145/2602458.2602459(85-90)Online publication date: 27-Jun-2014
https://dl.acm.org/doi/10.1145/2602458.2602459
Seifzadeh HAbolhassani HMoshkenani M(2012)A survey of dynamic software updatingJournal of Software: Evolution and Process10.1002/smr.155625:5(535-568)Online publication date: 25-Apr-2012
https://doi.org/10.1002/smr.1556
Cortier ABesnard LBodeveix JBuisson JDagnat FFilali MGarcia GOuy JPantel MRugina AStrecker MTalpin J(2010)Synoptic: A Domain-Specific Modeling Language for Space On-board Application SoftwareSynthesis of Embedded Software10.1007/978-1-4419-6400-7_3(79-119)Online publication date: 26-Jun-2010
https://doi.org/10.1007/978-1-4419-6400-7_3
(2019)Formal methods in dynamic software updatingInternational Journal of Critical Computer-Based Systems10.5555/3337432.33374369:1-2(76-114)Online publication date: 25-May-2019
https://dl.acm.org/doi/10.5555/3337432.3337436

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

EPUB

View this article in ePub.

Media

Figures

Other

Tables

View Table of Contents