Denotational fixed-point semantics for constructive scheduling of synchronous concurrency

详细信息    查看全文

• 作者：Joaquín Aguado ; Michael Mendler ; Reinhard von Hanxleden ; Insa Fuhrmann
• 刊名：Acta Informatica
• 出版年：2015
• 出版时间：June 2015
• 年：2015
• 卷：52
• 期：4-5
• 页码：393-442
• 全文大小：1,682 KB
• 参考文献：1.Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409-70 (2000)MATH MathSciNet View Article
  2.Aceto, L., Ingolfsdottir, A.: CPO models for compact GSOS languages. Inf. Comput. 129(2), 107-41 (1996)MATH MathSciNet View Article
  3.Aguado, J., Mendler, M.: Constructive semantics for instantaneous reactions. Theor. Comput. Sci. 241, 931-61 (2011)MathSciNet View Article
  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-4). LNCS 8410, pp. 229-48. Springer, Grenoble, France (2014)
  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-349
  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-0), pp. 1653-656. 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 -3, pp. 11-2. ACM, New York, NY, USA (2013)
  8.Benveniste, A., Caillaud, B., Guernic, P.L.: Compositionality in dataflow synchronous languages: specification and distributed code generation 1,2,3. Inf. Comput. 163(1), 125-71 (2000)MATH View Article
  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-3. IEEE, Piscataway, NJ, USA (2003)
  10.Bergstra, J., Ponse, A., Smolka, S. (eds.): Handbook of Process Algebra. Elsevier (2001)
  11.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-54. MIT Press, Cambridge (2000)
  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)
  13.Berry, G., Curien, P.L., Lévy, J.J.: Full abstraction for sequential languages: the state of the art. In: Nivat, M., Reynolds, J.C. (eds.) Algebraic Semantics, pp. 89-32. Cambridge University Press, Cambridge (1985)
  14.Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87-52 (1992)MATH View Article
  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 -1, pp. 49-6. ACM, New York, NY, USA (2011)
  16.Boussinot, F.: Reactive C: an extension of C to program reactive systems. Softw. Pract. Exp. 21(4), 401-28 (1991)View Article
  17.Boussinot, F.: Fairthreads: mixing cooperative and preemptive threads in C. Concurr. Comput. Pract. Exp. 18(5), 445-69 (2006)View Article
  18.Brzozowski, J.A., Seger, C.J.H.: Asynchronous Circuits. Springer, New York (1995)View Article
  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-7), pp. 178-88. 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-1 (1998). CMCS-8, First Workshop on Coalgebraic Methods in Computer Science
  21.Cleaveland, R., Lüttgen, G., Mendler, M.: An algebraic theory of multiple clocks. In: CONCUR -7, LNCS, vol. 1243, pp. 166-80. Springer (1997)
  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-6, pp. 180-93. ACM, New York, NY, USA (2006)
  23.Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)MATH View Article
  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-99. Springer LNCS 6200 (2010)
  25.Duffin, R.J.: Topology of series-parallel networks. J. Math. Anal. Appl. 10(2), 303-18 (1965)MATH MathSciNet View Article
  26.Edwards, S.A.: Tutorial: compiling concurrent languages for sequential processors. ACM Trans. Design Autom. Electron. Syst. 8(2),
• 作者单位：Joaquín Aguado (1)
  Michael Mendler (1)
  Reinhard von Hanxleden (2)
  Insa Fuhrmann (2)
  
  1. Faculty of Information Systems and Applied Computer Sciences, Bamberg University, Bamberg, Germany
  2. Department of Computer Science, Kiel University, Kiel, Germany
  
• 刊物类别：Computer Science
• 刊物主题：Logics and Meanings of Programs
  Computer Systems Organization and Communication Networks
  Software Engineering, Programming and Operating Systems
  Data Structures, Cryptology and Information Theory
  Theory of Computation
  Information Systems and Communication Service
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1432-0525

文摘

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.