×

Denotational fixed-point semantics for constructive scheduling of synchronous concurrency. (English) Zbl 1325.68135

Summary: The synchronous model of concurrent computation (SMoCC) is well established for programming languages in the domain of safety-critical reactive and embedded systems. Translated into mainstream C/Java programming, the SMoCC corresponds to a cyclic execution model in which concurrent threads are synchronised on a logical clock that cuts system computation into a sequence of macro-steps. A causality analysis verifies the existence of a schedule on memory accesses to ensure each macro-step is deadlock-free and determinate. We introduce an abstract semantic domain \(I(\mathbb {D}, \mathbb {P})\) and an associated denotational fixed-point semantics for reasoning about concurrent and sequential variable accesses within a synchronous cycle-based model of computation. We use this domain for a new and extended behavioural definition of Berry’s causality analysis in terms of approximation intervals. The domain \(I(\mathbb {D}, \mathbb {P})\) extends the domain \(I(\mathbb {D})\) from our previous work and fixes a mistake in the treatment of initialisations. Based on this fixed-point semantics we propose the notion of Input Berry-constructiveness (IBC) for synchronous programs. This new IBC class lies properly between strong (SBC) and normal Berry-constructiveness (BC) defined in previous work. SBC and BC are two ways to interpret the standard constructive semantics of synchronous programming, as exemplified by imperative SMoCC languages such as Esterel or Quartz. SBC is often too restrictive as it requires all variables to be initialised by the program. BC can be too permissive because it initialises all variables to a fixed value, by default. Where the initialisation happens through the memory, e.g., when carrying values from one synchronous tick to the next, then IBC is more appropriate. IBC links two levels of execution, the macro-step level and the micro-step level. We prove that the denotational fixed-point analysis for IBC, and hence Berry’s causality analysis, is sound with respect to operational micro-level scheduling. The denotational model can thus be viewed as a compositional presentation of a synchronous scheduling strategy that ensures reactiveness and determinacy for imperative concurrent programming.

MSC:

68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Abramsky, S; Jagadeesan, R; Malacaria, P, Full abstraction for PCF, Inf. Comput., 163, 409-470, (2000) · Zbl 1006.68028
[2] Aceto, L; Ingolfsdottir, A, CPO models for compact GSOS languages, Inf. Comput., 129, 107-141, (1996) · Zbl 1096.68623
[3] Aguado, J; Mendler, M, Constructive semantics for instantaneous reactions, Theor. Comput. Sci., 241, 931-961, (2011) · Zbl 1207.68202
[4] Aguado, J., Mendler, M., von Hanxleden, R., Fuhrmann, I.: Grounding synchronous deterministic concurrency in sequential programming. In: Proceedings of the 23rd European Symposium on Programming (ESOP’14). LNCS 8410, pp. 229-248. Springer, Grenoble, France (2014) · Zbl 1405.68068
[5] Aguado, J., Mendler, M., von Hanxleden, R., Fuhrmann, I.: Denotational fixed-point semantics for constructive scheduling of synchronous concurrency. Technical report 96, University of Bamberg, Faculty of Information Systems and Applied Computer Sciences (2015). ISSN 0937-3349 · Zbl 1325.68135
[6] 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’10), pp. 1653-1656. Dresden, Germany (2010)
[7] Baudart, G., Mandel, L., Pouzet, M.: Programming mixed music in ReactiveML. In: Proceedings of the First ACM SIGPLAN Workshop on Functional Art. Music, Modeling & #38; Design, FARM ’13, pp. 11-22. ACM, New York, NY, USA (2013) · Zbl 0772.68013
[8] Benveniste, A; Caillaud, B; Guernic, PL, Compositionality in dataflow synchronous languages: specification and distributed code generation 1,2,3, Inf. Comput., 163, 125-171, (2000) · Zbl 1003.68068
[9] Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Guernic, P.L., de Simone, R.: The Synchronous Languages Twelve Years Later. In: Proceedings of IEEE, Special Issue on Embedded Systems, vol. 91, pp. 64-83. IEEE, Piscataway, NJ, USA (2003)
[10] Bergstra, J., Ponse, A., Smolka, S. (eds.): Handbook of Process Algebra. Elsevier (2001) · Zbl 0971.00006
[11] Berry, G; Plotkin, G (ed.); Stirling, C (ed.); Tofte, M (ed.), The foundations of esterel, 425-454, (2000), Cambridge
[12] 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) · Zbl 1056.68099
[13] Berry, G; Curien, PL; Lévy, JJ; Nivat, M (ed.); Reynolds, JC (ed.), Full abstraction for sequential languages: the state of the art, 89-132, (1985), Cambridge
[14] Berry, G; Gonthier, G, The esterel synchronous programming language: design, semantics, implementation, Sci. Comput. Program., 19, 87-152, (1992) · Zbl 0772.68013
[15] Berry, G., Nicolas, C., Serrano, M.: Hiphop: A synchronous reactive extension for Hop. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Programming Language and Systems Technologies for Internet Clients. PLASTIC ’11, pp. 49-56. ACM, New York, NY, USA (2011)
[16] Boussinot, F, Reactive C: an extension of C to program reactive systems, Softw. Pract. Exp., 21, 401-428, (1991)
[17] Boussinot, F, Fairthreads: mixing cooperative and preemptive threads in C, Concurr. Comput. Pract. Exp., 18, 445-469, (2006)
[18] Brzozowski, J.A., Seger, C.J.H.: Asynchronous Circuits. Springer, New York (1995) · Zbl 0747.94024
[19] 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’87), pp. 178-188. ACM, Munich, Germany (1987)
[20] Caspi, P., Pouzet, M.: A co-iterative characterization of synchronous stream functions. Electron. Notes Theor. Comput. Sci. 11(0), 1-21 (1998). CMCS’98, First Workshop on Coalgebraic Methods in Computer Science · Zbl 0917.68046
[21] Cleaveland, R., Lüttgen, G., Mendler, M.: An algebraic theory of multiple clocks. In: CONCUR ’97, LNCS, vol. 1243, pp. 166-180. Springer (1997) · Zbl 1053.68066
[22] Cohen, A., Duranton, M., Eisenbeis, C., Pagetti, C., Plateau, F., Pouzet, M.: N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems. Symposium on Principles of Programming Languages. POPL’06, pp. 180-193. ACM, New York, NY, USA (2006) · Zbl 1369.68065
[23] Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002) · Zbl 1002.06001
[24] de Roever, W.P., Lüttgen, G., Mendler, M.: What is in a step: new perspectives on a classical question. In: Manna, Z., Peled, D.A. (eds.) Time for Verification, pp. 370-399. Springer LNCS 6200 (2010) · Zbl 1288.68172
[25] Duffin, RJ, Topology of series-parallel networks, J. Math. Anal. Appl., 10, 303-318, (1965) · Zbl 0128.37002
[26] Edwards, SA, Tutorial: compiling concurrent languages for sequential processors, ACM Trans. Design Autom. Electron. Syst., 8, 141-187, (2003)
[27] Edwards, SA; Lee, EA, The semantics and execution of a synchronous block-diagram language, Sci. Comput. Program., 48, 21-42, (2003) · Zbl 1056.68099
[28] 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) · Zbl 1056.68099
[29] Ésik, Z.: Axiomatizing the least fixed point operation and binary supremum. In: Clote, P., Schwichtenberg, H. (eds.) Computer Science Logic (CSL’00), LNCS 1862, pp. 302-316. Springer (2000) · Zbl 0973.08003
[30] Fiore, M; Moggi, E; Sangiorgi, D, A fully abstract model for the \(π \)-calculus, Inf. Comput., 179, 76-117, (2002) · Zbl 1053.68066
[31] Gamatié, A; Gonnord, L, Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems, ACM Sigplan Notices, 46, 71-80, (2011)
[32] Gemünde, M; Brandt, J; Schneider, K, Clock refinement in imperative synchronous languages, EURASIP J. Embed. Syst., 2013, 3, (2013)
[33] Groote, JF; Vaandrager, F, Structured operational semantics and bisimulation as a congruence, Inf. Comput., 100, 202-260, (1992) · Zbl 0752.68053
[34] Guernic, PL; Goutier, T; Borgne, ML; Maire, CL, Programming real time applications with SIGNAL, Proc. IEEE, 79, 1321-1336, (1991)
[35] Halbswachs, N.: Synchronous Programming of Reactive Systems. Kluwer Academic Publishers, Dordrecht (1993)
[36] Halbwachs, N; Caspi, P; Raymond, P; Pilaud, D, The synchronous data-flow programming language LUSTRE, Proc. IEEE, 79, 1305-1320, (1991)
[37] Hamon, G.: A denotational semantics for Stateflow. In: EMSOFT’05: Proceedings of the 5th ACM International Conference on Embedded Software, pp. 164-172. ACM Press, New York, NY, USA (2005)
[38] Harel, D, Statecharts: a visual formalism for complex systems, Sci. Comput. Program., 8, 231-274, (1987) · Zbl 0637.68010
[39] Harel, D; Naamad, A, The STATEMATE semantics of statecharts, ACM Trans. Softw. Eng., 5, 293-333, (1996)
[40] Hennessy, M, Acceptance trees, J. ACM, 32, 896-928, (1985) · Zbl 0633.68074
[41] Hennessy, M; Regan, T, A process algebra for timed systems, Inf. Comput., 117, 221-239, (1995) · Zbl 0826.68068
[42] Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River, NJ (1985) · Zbl 0637.68007
[43] Huizing, C., Gerth, R., de Roever, W.: Modeling Statecharts behavior in a fully abstract way. In: Dauchet, M., Nivat, M. (eds.) 13th CAAP (CAAP ’88). Lecture Notes in Computer Science, vol. 299, pp. 271-294. Springer, Nancy, France (1988) · Zbl 0647.68018
[44] Hyland, M; Ong, L, On full abstraction for PCF: I. II and III, Inf. Comput., 163, 285-408, (2000) · Zbl 1006.68027
[45] Ingólfsdóttir, A; Schalk, A, A fully abstract denotational model for observational precongruence, Theor. Comput. Sci., 254, 35-61, (2001) · Zbl 0972.68121
[46] Kahn, G.: The semantics of a simple language for parallel programming. In: Rosenfeld, J.L. (ed.) Information Processing 74: In: Proceedings of the IFIP Congress 74, pp. 471-475. North-Holland Publishing Co., IFIP (1974)
[47] Kahn, G., MacQueen, D.B.: Coroutines and networks of parallel processes. In: IFIP Congress, pp. 993-998 (1977) · Zbl 0363.68076
[48] Kok, J.N.: Denotational semantics of nets with nondeterminism. In: Robinet, B., Wilhelm, R. (eds.) European Symposium on Programming (ESOP’86), LNCS 213, pp. 237-249. Springer (1986) · Zbl 0587.68019
[49] Kozen, D, A completeness theorem for Kleene algebras and the algebra of regular events, Inf. Comput., 110, 366-390, (1994) · Zbl 0806.68082
[50] 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’14), pp. 257-270. ACM, New York, USA (2014) · Zbl 1284.68143
[51] Lavagno, L., Sentovich, E.: ECL: a specification environment for system-level design. In: Proceedings of 36th ACM/IEEE Conference on Design Automation (DAC’99), pp. 511-516. ACM (1999)
[52] Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. In: Proceedings of the IEEE, vol. 75, pp. 1235-1245. IEEE Computer Society Press (1987)
[53] 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, USA (2012)
[54] Luettgen, G; Mendler, M, The intuitionism behind statecharts steps, ACM Trans. Comput. Log., 3, 1-41, (2002) · Zbl 1365.68312
[55] Lüttgen, G., von der Beeck, M., Cleaveland, R.: Statecharts via process algebra. In: Proceedings of 10th International Conference on Concurrency Theory CONCUR’99, pp. 399-414 (1999) · Zbl 1365.68312
[56] Lüttgen, G., Mendler, M.: Towards a model-theory for Esterel. In: Maraninchi, F., Girault, A., Rutten, E. (eds.) SLAP 2002, ENTCS, vol. 65,5. Elsevier Science (2002) · Zbl 1207.68202
[57] Lynch, N.: Distributed Algorithms. Morgan Kaufmann Publishers, Los Altos (1996) · Zbl 0877.68061
[58] Malik, S, Analysis of cyclic combinational circuits, IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 13, 950-956, (1994) · Zbl 1303.94147
[59] Mandel, L., Pasteur, C., Pouzet, M.: Time refinement in a functional synchronous language. In: Principles and Practice of Declarative Programming (PPDP’13), pp. 169-180. ACM (2013)
[60] Mandel, L., Pouzet, M.: ReactiveML: a reactive extension to ML. In: Proceedings of 7th ACM SIGPLAN Int’l Conference on Principles and Practice of Declarative Programming, pp. 82-93 (2005)
[61] Maraninchi, F.: The Argos language: graphical representation of automata and description of reactive systems. In: IEEE Workshop on Visual Languages (1991) · Zbl 0972.68121
[62] Maraninchi, F; Rémond, Y, Argos: an automaton-based synchronous language, Comput. Lang., 27, 61-92, (2001) · Zbl 1050.68020
[63] Mendler, M; Lüttgen, G, Is observational congruence axiomatisable in equational Horn logic?, Inf. Comput., 208, 634-651, (2010) · Zbl 1205.68248
[64] Mendler, M; Shiple, TR; Berry, G, Constructive Boolean circuits and the exactness of timed ternary simulation, Form. Methods Syst. Des., 40, 283-329, (2012) · Zbl 1303.94148
[65] Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989) · Zbl 0683.68008
[66] Motika, C., von Hanxleden, R., Heinold, M.: Programming deterministice reactive systems with Synchronous Java (invited paper). In: Proceedings of the 9th Workshop on Software Technologies for Future Embedded and Ubiquitous Systems (SEUS 2013), IEEE Proceedings. Paderborn, Germany (2013)
[67] Ngo, V.C., Talpin, J.P., Gautier, T.: Precise deadlock detection for polychronous data-flow specifications. In: Proceedings of the Electronic System Level Synthesis Conference (ESLsyn), pp. 1-6. IEEE (2014) · Zbl 1437.68109
[68] Plotkin, G.D.: A Structural Approach to Operational Semantics. Technical report DAIMI FN-19, University of Aarhus, Denmark (1981)
[69] Pnueli, A., Shalev, M.: What is in a step: on the semantics of Statecharts. In: Proceedings of International Conference on Theoretical Aspects of Computer Software (TACS’91), pp. 244-264. Springer, London, UK (1991)
[70] Potop-Butucaru, D., Edwards, S.A., Berry, G.: Compiling Esterel. Springer, Berlin (2007)
[71] Pouzet, M; Raymond, P, Modular static scheduling of synchronous data-flow networks—an efficient symbolic representation, Des. Autom. Embed. Syst., 14, 165-192, (2010)
[72] Schneider, K.: The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany (2009)
[73] 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’04), pp. 179-189. ACM, Washington DC, USA (2004)
[74] Schneider, K., Brandt, J., Schuele, T., Tuerk, T.: Maximal causality analysis. In: Conference on Application of Concurrency to System Design (ACSD’05), pp. 106-115. IEEE Computer Society (2005)
[75] Schneider, K., Brandt, J., Schüle, T., Türk, T.: Improving constructiveness in code generators. In: Maraninchi, F., Pouzet, M., Roy, V. (eds.) International Workshop on Synchronous Languages, Applications, and Programming (SLAP’05), pp. 1-19. ENTCS, Edinburgh, Scotland, UK (2005) · Zbl 1303.94147
[76] Shiple, T.R., Berry, G., Touati, H.: Constructive Analysis of Cyclic Circuits. In: Proceedings of European Design and Test Conference (ED&TC’96), Paris, France, pp. 328-333. IEEE Computer Society Press (1996)
[77] Talpin, JP; Brandt, J; Gemünde, M; Schneider, K; Shukla, S, Constructive polychronous systems, Sci. Comput. Program., 96, 377-394, (2014) · Zbl 1437.68109
[78] Talpin, JP; Ouy, J; Gautier, T; Besnard, L; Guernic, PL, Compositional design of isochronous systems, Sci. Comput. Program., 77, 113-128, (2012) · Zbl 1250.68094
[79] Tardieu, O., Edwards, S.A.: Scheduling-independent threads and exceptions in SHIM. In: Proceedings of the International Conference on Embedded Software (EMSOFT’06), pp. 142-151. ACM (2006)
[80] Tardieu, O., Edwards, S.A.: Instanteneous transitions in Esterel. In: Proceedings of Model Driven High-Level Programming of Embedded Systems (SLA++P’07). Braga, Portugal (2007)
[81] Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic verification of determinism for structured parallel programs. In: Cousot, R., Martel, M. (eds.) Static Analysis (SAS 2010), LNCS, vol. 6337, pp. 455-471. Springer (2010) · Zbl 1306.68037
[82] von der Beeck, M.: A comparison of Statecharts variants. In: Langmaack, H., de Roever, W., Vytopil, J. (eds.) 3rd International School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT ’94), Lecture Notes in Computer Science, vol. 863, pp. 128-148. Springer (1994)
[83] von Hanxleden, R.: SyncCharts in C-A Proposal for Light-Weight, Deterministic Concurrency. In: Proceedingsof International Conference on Embedded Software (EMSOFT’09), pp. 225-234. ACM, Grenoble, France (2009)
[84] von Hanxleden, R., Duderstadt, B., Motika, C., Smyth, S., Mendler, M., Aguado, J., Mercer, S., O’Brien, O.: SCCharts: sequentially constructive statecharts for safety-critical applications. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14). ACM (2014)
[85] 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: Design, Automation and Test in Europe (DATE’13), pp. 581-586. IEEE (2013)
[86] 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. ACM Trans. Embed. Comput. Syst.,Special Issue on Applications of Concurrency to System Design 13(4s), 144:1-144:26 (2014) · Zbl 0826.68068
[87] 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 (2013) · Zbl 0633.68074
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.