research-article

A higher-order extension for imperative synchronous languages

Authors:

Jean-Pierre Talpin,

Sébastien BoisgéraultAuthors Info & Claims

SCOPES '10: Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems

Article No.: 7, Pages 1 - 10

https://doi.org/10.1145/1811212.1811222

Published: 28 June 2010 Publication History

Abstract

This article presents the very first effective design of higher-order modules in the synchronous programming language Esterel. Higher-order modules, together with the robust separate compilation scheme that implements it, allow us to address a yet unexplored application spectrum ranging from rapid prototyping of embedded functionality to hot reconfiguration of embedded software within the formal modeling framework of the "synchronous hypothesis". While extensions of data-flow synchronous languages had already been proposed for Lustre [11] and Signal [25], the adaptation of similar programming concepts to imperative synchronous frameworks like Esterel has long posed major technical challenges, due to the specificity of its model of computation. We present a framework including a formal semantics, a type system, and a modular code generator, that tackle this challenge. We consider a specific stack-based module call convention and a simple event pooling protocol; in consequence signals can refer to modules and modules can be transmitted and instantiated by referencing a signal. We define a type system that computes the potential emissions of a module and prove it sound. Our type system seamlessly fits an extension of Esterel's constructive semantics with higher-order modules.

References

[1]

A. Aho, R. Sethi, and J. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.

Digital Library

[2]

J. Armstrong, R. Virding, C. Wikström, and M. Williams. Concurrent Programming in ERLANG. Prentice Hall, Englewood Cliffs, New Jersey 07632, 1996.

Digital Library

[3]

A. Benveniste, P. Le Guernic, and P. Aubry. Compositionality in dataflow synchronous languages: Specification & code generation. Research Report 3310, INRIA, November 1997.

[4]

G. Berry. A hardware implementation of pure Esterel. In Workshop on Formal Methods in VLSI Design, Miami, Florida, 1991.

[5]

G. Berry. The constructive semantics of pure Esterel. http://www-sop.inria.fr/esterel.org, July 1999.

[6]

G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87--152, 1992.

Digital Library

[7]

G. Boudol. ULM: a core programming model for global computing. In European Symposium on Programming, ESOP'04, Barcelona, Spain, April 2004.

[8]

F. Boussinot. SugarCubes implementation of causality. Research Report 3487, INRIA, September 1998.

[9]

F. Boussinot and J.-F. Susini. The SugarCubes tool box: a reactive Java framework. Software-Practice and Experience, 28(14):1531--1550, December 1998.

Digital Library

[10]

E. Bruneton, T. Coupaye, M. Leclercq, V. Quéma, and J.-B. Stefani. An open component model and its support in Java. In Int. Symposium on Component Based Software Engineering, CBSE'04, Edinburgh, Scotland, May 2004.

[11]

P. Caspi and M. Pouzet. Synchronous Kahn networks. In Conference on Functional Programming (ICFP), pages 226--238, Philadelphia, USA, 1996. ACM.

Digital Library

[12]

E. Closse, M. Poize, J. Pulou, P. Venier, and D. Weil. SAXO-RT: Interpreting Esterel semantics on a sequential execution structure. Electronic Notes in Theoretical Computer Science (ENTCS), 65(5), 2002.

[13]

J.-L. Colaço, A. Girault, G. Hamon, and M. Pouzet. Towards a higher-order synchronous data-flow language. In G. Buttazzo, editor, International Conference on Embedded Software, EMSOFT'04, pages 230--239, Pisa, Italy, September 2004. ACM, New-York.

Digital Library

[14]

M. Conway. Design of a separable transition-diagram compiler. Communications of the ACM, 6(7), July 1963.

Digital Library

[15]

S. Edwards. An Esterel compiler for large control-dominated systems. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 21(2):169--183, February 2002.

Digital Library

[16]

O. Hainque, L. Pautet, Y. Le Biannic, and E. Nassor. Cronos: A separate compilation toolset for modular Esterel applications. In Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, 1999.

Digital Library

[17]

L. Hazard, J.-F. Susini, and F. Boussinot. The Junior reactive kernel. Research Report 3732, INRIA, July 1999.

[18]

R. Lublinerman and S. Tripakis. Modularity vs. reusability: Code generation from synchronous block diagrams. In Design, Automation and Test in Europe (DATE), 2008.

Digital Library

[19]

R. Milner. Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, June 1999.

Digital Library

[20]

K. Moessner, S. Hope, P. Cook, W. Tuttlebee, and R. Tafazolli. The RMA - a framework for reconfiguration of SDR equipement. IEICE Trans. on Communications, E85-B(12):2573--2580, December 2002.

[21]

D. Potop-Butucaru and R. de Simone. Optimizations for faster execution of Esterel programs. In International Conference on Formal Methods and Models for Co-Design (MEMOCODE), Mont Saint-Michel, France, 2003.

Digital Library

[22]

D. Potop-Butucaru, S. Edwards, and G. Berry. Compiling Esterel. Springer, 2007.

Digital Library

[23]

G. Rose. Authentication and security in mobile phones. In Australian Unix Users Group conference, AUUG99, Melbourne, Australia, September 1999.

[24]

K. Schneider, J. Brandt, and E. Vecchié. Modular compilation of synchronous programs. In IFIP Conference on Distributed and Parallel Embedded Systems (DIPES), Braga, Portugal, 2006.

[25]

J.-P. Talpin and D. Nowak. A synchronous semantics of higher-order processes for modeling reconfigurable reactive systems. In Proceedings of the 18th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 78--89, London, UK, 1998. Springer-Verlag.

Digital Library

[26]

J. Zeng and S. Edwards. Separate compilation for synchronous modules. In International Conference on Embedded Software and Systems (ICESS), Xian, China, 2005.

Digital Library

Cited By

Gretz FGrosch FMendler MScheele S(2024)Synchronized Shared Memory and Black-box Procedural Abstraction: Toward a Formal Semantics of BlechACM Transactions on Embedded Computing Systems10.1145/357158523:5(1-45)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.1145/3571585
Gretz FGrosch FMendler MScheele S(2020)Synchronized Shared Memory and Procedural Abstraction: Towards a Formal Semantics of Blech2020 Forum for Specification and Design Languages (FDL)10.1109/FDL50818.2020.9232942(1-8)Online publication date: 15-Sep-2020
https://doi.org/10.1109/FDL50818.2020.9232942
Malik AGirault ASalcic Z(2011)A GALS Language for Dynamic Distributed and Reactive ProgramsProceedings of the 2011 Eleventh International Conference on Application of Concurrency to System Design10.1109/ACSD.2011.30(173-182)Online publication date: 20-Jun-2011
https://dl.acm.org/doi/10.1109/ACSD.2011.30

A higher-order extension for imperative synchronous languages
1. Software and its engineering
  1. Software notations and tools

Recommendations

Pilsner: a compositionally verified compiler for a higher-order imperative language
ICFP '15

Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different ...
Definitional Interpreters for Higher-Order Programming Languages

Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters that are themselves written in a programming language based on the lambda calculus (i.e., an applicative language ...
Pilsner: a compositionally verified compiler for a higher-order imperative language
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SCOPES '10: Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems

June 2010

91 pages

ISBN:9781450300841

DOI:10.1145/1811212

General Chair:
Ed Deprettere
Leiden University, NL
,
Program Chair:
Todor Stefanov
Leiden University, NL

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

EDAA: European Design Automation Association

In-Cooperation

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 June 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

SCOPES '10

Sponsor:

EDAA

SCOPES '10: 13th International Workshop on Software and Compilers for Embedded Systems

June 28 - 29, 2010

St. Goar, Germany

Acceptance Rates

Overall Acceptance Rate 38 of 79 submissions, 48%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
64
Total Downloads

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

Reflects downloads up to 02 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gretz FGrosch FMendler MScheele S(2024)Synchronized Shared Memory and Black-box Procedural Abstraction: Toward a Formal Semantics of BlechACM Transactions on Embedded Computing Systems10.1145/357158523:5(1-45)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.1145/3571585
Gretz FGrosch FMendler MScheele S(2020)Synchronized Shared Memory and Procedural Abstraction: Towards a Formal Semantics of Blech2020 Forum for Specification and Design Languages (FDL)10.1109/FDL50818.2020.9232942(1-8)Online publication date: 15-Sep-2020
https://doi.org/10.1109/FDL50818.2020.9232942
Malik AGirault ASalcic Z(2011)A GALS Language for Dynamic Distributed and Reactive ProgramsProceedings of the 2011 Eleventh International Conference on Application of Concurrency to System Design10.1109/ACSD.2011.30(173-182)Online publication date: 20-Jun-2011
https://dl.acm.org/doi/10.1109/ACSD.2011.30

View Options

Get Access

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.

Media

Figures

Other

Tables

View Table of Contents