Abstract
Using a new domain-theoretic characterisation we show that Berry’s constructive semantics is a conservative approximation of the recently proposed sequentially constructive (SC) model of computation. We prove that every Berry-constructive program is deterministic and deadlock-free under sequentially admissible scheduling. This gives, for the first time, a natural interpretation of Berry-constructiveness for shared-memory, multi-threaded programming in terms of synchronous cycle-based scheduling, where previous results were cast in terms of synchronous circuits. This opens the door to a direct mapping of Esterel’s signal mechanism into boolean variables that can be set and reset under the programmer’s control within a tick. We illustrate the practical usefulness of this mapping by discussing how signal reincarnation is handled efficiently by this transformation, which is of linear complexity in program size, in contrast to earlier techniques that had quadratic overhead.
This work is part of the PRETSY project and supported by the German Science Foundation (DFG HA 4407/6-1 and ME 1427/6-1).
Chapter PDF
Similar content being viewed by others
References
Hansen, P.B.: Java’s insecure parallelism. SIGPLAN Not. 34, 38–45 (1999)
Lee, E.A.: The problem with threads. IEEE Computer 39, 33–42 (2006)
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for programming synchronous systems. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1987), Munich, Germany, pp. 178–188. ACM (1987)
Guernic, P.L., Goutier, T., Borgne, M.L., Maire, C.L.: Programming real time applications with SIGNAL. Proceedings of the IEEE 79, 1321–1336 (1991)
Berry, G., Gonthier, G.: The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming 19, 87–152 (1992)
Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Guernic, P.L., de Simone, R.: The Synchronous Languages Twelve Years Later. In: Proc. IEEE, Special Issue on Embedded Systems, Piscataway, NJ, USA, vol. 91, pp. 64–83. IEEE (2003)
André, C.: SyncCharts: A visual representation of reactive behaviors. Technical Report RR 95–52, rev. RR 96–56, I3S, Sophia-Antipolis, France (1996)
Schneider, K.: The synchronous programming language Quartz. Internal report, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany (2010), http://es.cs.uni-kl.de/publications/datarsg/Schn09.pdf
von Hanxleden, R., Mendler, M., Aguado, J., Duderstadt, B., Fuhrmann, I., Motika, C., Mercer, S., O’Brien, O., Roop, P.: Sequentially Constructive Concurrency—A conservative extension of the synchronous model of computation. Technical Report 1308, Christian-Albrechts-Universität zu Kiel, Department of Computer Science (2013) ) ISSN 2192-6247
von Hanxleden, R., Mendler, M., Aguado, J., Duderstadt, B., Fuhrmann, I., Motika, C., Mercer, S., O’Brien, O.: Sequentially Constructive Concurrency—A conservative extension of the synchronous model of computation. In: Proc. Design, Automation and Test in Europe Conference (DATE 2013), Grenoble, France, pp. 581–586. IEEE (2013)
Berry, G.: The foundations of Esterel. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 425–454. MIT Press, Cambridge (2000)
Schneider, K., Wenz, M.: A new method for compiling schizophrenic synchronous programs. In: International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES), Atlanta, Georgia, USA, pp. 49–58. ACM (2001)
Tardieu, O., de Simone, R.: Curing schizophrenia by program rewriting in Esterel. In: Proceedings of the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2004), San Diego, CA, USA (2004)
Aguado, J., Mendler, M., von Hanxleden, R., Fuhrmann, I.: Grounding synchronous deterministic concurrency in sequential programming. Technical report, Christian-Albrechts-Universität zu Kiel, Department of Computer Science (2014) ISSN 2192-6247
Berry, G.: The Constructive Semantics of Pure Esterel. Draft Book, Version 3.0, Centre de Mathématiques Appliqées, Ecole des Mines de Paris and INRIA, 2004 route des Lucioles, 06902 Sophia-Antipolis CDX, France (2002), http://www-sop.inria.fr/members/Gerard.Berry/Papers/EsterelConstructiveBook.zip
Mendler, M., Shiple, T.R., Berry, G.: Constructive boolean circuits and the exactness of timed ternary simulation. Formal Methods in System Design 40, 283–329 (2012)
Edwards, S.A.: Tutorial: Compiling concurrent languages for sequential processors. ACM Transactions on Design Automation of Electronic Systems 8, 141–187 (2003)
Potop-Butucaru, D., Edwards, S.A., Berry, G.: Compiling Esterel, vol. 86. Springer, P.O. Box 17, 3300 AA Dordrecht, The Netherlands (2007)
Boussinot, F.: Reactive C: An extension of C to program reactive systems. Software Practice and Experience 21, 401–428 (1991)
Boussinot, F.: Fairthreads: mixing cooperative and preemptive threads in C. Concurrency and Computation: Practice and Experience 18, 445–469 (2006)
Andalam, S., Roop, P.S., Girault, A.: Deterministic, predictable and light-weight multithreading using pret-c. In: Proceedings of the Conference on Design, Automation and Test in Europe (DATE 2010), Dresden, Germany, pp. 1653–1656 (2010)
von Hanxleden, R.: SyncCharts in C—A Proposal for Light-Weight, Deterministic Concurrency. In: Proceedings of the International Conference on Embedded Software (EMSOFT 2009), Grenoble, France, pp. 225–234. ACM (2009)
Tardieu, O., Edwards, S.A.: Scheduling-independent threads and exceptions in SHIM. In: Proceedings of the International Conference on Embedded Software (EMSOFT 2006), Seoul, South Korea, pp. 142–151. ACM (2006)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River (1985)
Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic verification of determinism for structured parallel programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 455–471. Springer, Heidelberg (2010)
Leung, A., Gupta, M., Agarwal, Y., Gupta, R., Jhala, R., Lerner, S.: Verifying GPU kernels by test amplification. In: Programming Language Design and Implementation, PLDI 2012, pp. 383–394. ACM, New York (2012)
Yuki, T., Feautrier, P., Rajopadye, S., Saraswat, V.: Array dataflow analysis for polyhedral X10 programs. In: Principles and Practice of Parallel Programming, PPoPP 2013, pp. 23–34. ACM, New York (2013)
Kuper, L., Turon, A., Krishnaswami, N.R., Newton, R.R.: Freeze after writing: Quasi-deterministic parallel programming with LVars. In: Principles of Programming Languages, POPL 2014. ACM, New York (2014)
Brzozowski, J.A., Seger, C.J.H.: Asynchronous Circuits. Springer, New York (1995)
Malik, S.: Analysis of cyclic combinational circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 13, 950–956 (1994)
Shiple, T.R., Berry, G., Touati, H.: Constructive Analysis of Cyclic Circuits. In: Proc. European Design and Test Conference (ED&TC 1996), Paris, France, Los Alamitos, California, USA, pp. 328–333. IEEE Computer Society Press (1996)
Schneider, K., Brandt, J., Schüle, T., Türk, T.: Improving constructiveness in code generators. In: Maraninchi, F., Pouzet, M., Roy, V. (eds.) Int’l Workshop on Synchronous Languages, Applications, and Programming, SLAP 2005, Edinburgh, Scotland, UK. ENTCS, pp. 1–19 (2005)
Mandel, L., Pasteur, C., Pouzet, M.: Time refinement in a functional synchronous language. In: ACM SIGPLAN Int. Symp. on Principles and Practice of Declarative Programming, PPDP 2013, pp. 169–180. ACM, New York (2013)
Gemünde, M.: Clock Refinement in Imperative Synchronous Languages. PhD thesis, University of Kaiserslautern (2013)
Schneider, K., Brandt, J., Schuele, T.: Causality analysis of synchronous programs with delayed actions. In: Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES), Washington, D.C., USA, pp. 179–189. ACM (2004)
Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. In: Proceedings of the IEEE, vol. 75, pp. 1235–1245. IEEE Computer Society Press (1987)
Edwards, S.A., Lee, E.A.: The Semantics and Execution of a Synchronous Block-Diagram Language. In: Science of Computer Programming, vol. 48, Elsevier (2003), http://www1.cs.columbia.edu/~sedwards/papers/edwards2003semantics.pdf
Pouzet, M., Raymond, P.: Modular static scheduling of synchronous data-flow networks: an efficient symbolic representation. In: EMSOFT, pp. 215–224 (2009)
Aguado, J., Mendler, M.: Constructive semantics for instantaneous reactions. Theoretical Computer Science 241, 931–961 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aguado, J., Mendler, M., von Hanxleden, R., Fuhrmann, I. (2014). Grounding Synchronous Deterministic Concurrency in Sequential Programming. In: Shao, Z. (eds) Programming Languages and Systems. ESOP 2014. Lecture Notes in Computer Science, vol 8410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54833-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-54833-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54832-1
Online ISBN: 978-3-642-54833-8
eBook Packages: Computer ScienceComputer Science (R0)