Skip to main content
SpringerLink
Log in
Book cover

Models, Mindsets, Meta: The What, the How, and the Why Not? pp 45–67Cite as

Logic Meets Algebra: Compositional Timing Analysis for Synchronous Reactive Multithreading

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11200))

Abstract

The intuitionistic theory of the real interval [0, 1], known as Skolem-Gödel-Dummet logic (SGD), generates a well-known Heyting algebra intermediate between intuitionistic and classical logic. Originally of purely mathematical interest, it has recently received attention in Computer Science, notably for its potential applications in concurrency theory. In this paper we show how the logical operators of SGD over the discrete frame \({\mathbb Z} _\infty \), extended by the additive group structure \(({\mathbb Z}, 0, +)\), provides an expressive and yet surprisingly economic calculus to specify the quantitative stabilisation behaviour of synchronous programs. This is both a new application of SGD and a new way of looking at the semantics of synchronous programming languages. We provide the first purely algebraic semantics of timed synchronous reactions which adapts Berry’s semantics for Esterel to work on general concurrent/sequential control-flow graphs. We illustrate the power of the algebra for the modular analysis of worst-case reaction time (WCRT) characteristics for time-predictable reactive processors with hardware-supported multi-threading.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Dummett (1959) calls it LC, yet Skolem (1931) and Gödel (1932) studied LC earlier.

  2. 2.

    In the KEP processor the join is executed at each tick until both threads have terminated, during which time it invokes some constant overhead cost.

References

  1. Aguado, J., Mendler, M., Wang, J.J., Bodin, B., Roop, P.: Compositional timing-aware semantics for synchronous programming. In: Forum on Specification & Design Languages (FDL 2017), pp. 1–8. IEEE, Verona, September 2017

    Google Scholar 

  2. Baccelli, F.L., Cohen, G., Olsder, G.J., Quadrat, J.P.: Synchronisation and Linearity. Wiley, New York (1992)

    MATH  Google Scholar 

  3. Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 389–448. Springer, Heidelberg (1985). https://doi.org/10.1007/3-540-15670-4_19

    Chapter  Google Scholar 

  4. Boldt, M., Traulsen, C., von Hanxleden, R.: Compilation and worst-case reaction time analysis for multithreaded Esterel processing. EURASIP J. Embed. Syst. 2008(1), 4 (2008)

    Article  Google Scholar 

  5. van Dalen, D.: Intuitionistic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. III, chap. 4, pp. 225–339. Reidel, Dordrecht (1986)

    Google Scholar 

  6. Dummett, M.: A propositional calculus with a denumerable matrix. J. Symb. Log. 24, 97–106 (1959)

    Article  MathSciNet  Google Scholar 

  7. Edwards, S.A., Lee, E.A.: The case for the precision timed (PRET) machine. In: DAC 2007, San Diego, USA, June 2007

    Google Scholar 

  8. Edwards, S.A., Kim, S., Lee, E.A., Liu, I., Patel, H.D., Schoeberl, M.: A disruptive computer design idea: architectures with repeatable timing. In: Proceedings of IEEE International Conference on Computer Design (ICCD 2009). IEEE, October 2009

    Google Scholar 

  9. Fermüller, C.G.: Parallel dialogue games and hypersequents for intermediate logics. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS (LNAI), vol. 2796, pp. 48–64. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45206-5_7

    Chapter  Google Scholar 

  10. Geilen, M., Stuijk, S.: Worst-case performance analysis of synchronous dataflow networks. In: CODES+ISSS 2010. ACM, Scottsdale, October 2010

    Google Scholar 

  11. Hájek, P.: Metamathematics of Fuzzy Logic. Kluwer, Dordrecht (1998)

    Book  Google Scholar 

  12. von Hanxleden, R., Li, X., Roop, P., Salcic, Z., Yoong, L.H.: Reactive processing for reactive systems. ERCIM News 66, 28–29 (2006)

    Google Scholar 

  13. von Hanxleden, R., Mendler, M., Traulsen, C.: WCRT algebra and scheduling interfaces for Esterel-style synchronous multi-threading. Technical report 0807, Christian-Albrechts-Univ. Kiel, Department of Computer Science, June 2008. http://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/report-0807.pdf

  14. Hirai, Y.: A lambda calculus for Gödel–Dummett logic capturing waitfreedom. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 151–165. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29822-6_14

    Chapter  MATH  Google Scholar 

  15. Ju, L., Huynh, B.K., Chakraborty, S., Roychoudhury, A.: Context-sensitive timing analysis of Esterel programs. In: Proceedings of 46th Annual Design Automation Conference (DAC 2009), pp. 870–873. ACM, New York (2009)

    Google Scholar 

  16. Ju, L., Huynh, B.K., Roychoudhury, A., Chakraborty, S.: Performance debugging of Esterel specifications. Real-Time Syst. 48(5), 570–600 (2012)

    Article  Google Scholar 

  17. Kuo, M., Sinha, R., Roop, P.S.: Efficient WCRT analysis of synchronous programs using reachability. In: Proceedings of 48th Design Automation Conference (DAC 2011), pp. 480–485 (2011)

    Google Scholar 

  18. Li, X., von Hanxleden, R.: Multi-threaded reactive programming–the Kiel Esterel Processor. IEEE Trans. Comput. 61(3), 337–349 (2012)

    Article  MathSciNet  Google Scholar 

  19. Lickly, B., Liu, I., Kim, S., Patel, H.D., Edwards, S.A., Lee, E.A.: Predictable programming on a precision timed architecture. In: Proceedings of the Conference on Compilers, Architectures, and Synthesis of Embedded Systems (CASES 2008), Atlanta USA, October 2008, pp. 137–146 (2008)

    Google Scholar 

  20. Mendler, M., Bodin, B., Roop, P., Wang, J.J.: WCRT for synchronous programs: studying the tick alignment problem. Technical report 95, University of Bamberg, Faculty for Information Systems and Applied Computer Sciences, August 2014

    Google Scholar 

  21. Mendler, M.: An algebra of synchronous scheduling interfaces. In: Legay, A., Caillaud, B. (eds.) Proceedings Foundations for Interface Technologies (FIT 2010), EPTCS, Paris, France, vol. 46, pp. 28–48 (2010)

    Article  Google Scholar 

  22. Mendler, M., von Hanxleden, R., Traulsen, C.: WCRT algebra and interfaces for Esterel-Style synchronous processing. In: Proceedings of Design, Automation and Test in Europe Conference (DATE 2009), Nice, France, April 2009

    Google Scholar 

  23. Mendler, M., Roop, P.S., Bodin, B.: A novel WCET semantics of synchronous programs. In: Fränzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 195–210. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-44878-7_12

    Chapter  MATH  Google Scholar 

  24. Raymond, P., Maiza, C., Parent-Vigouroux, C., Carrier, F., Asavoae, M.: Timing analysis enhancement for synchronous programs. Real-Time Syst. 51, 192–220 (2015)

    Article  Google Scholar 

  25. Roop, P.S., Andalam, S., von Hanxleden, R., Yuan, S., Traulsen, C.: Tight WCRT analysis of synchronous C programs. In: Proceedings of Compilers, Architecture, and Synthesis for Embedded Systems (CASES 2009), pp. 205–214 (2009)

    Google Scholar 

  26. Schoeberl, M.: Time-predictable computer architecture. EURASIP J. Embed. Syst. 2009, 2:1–2:17 (2009)

    Google Scholar 

  27. Waez, M.T.B., Dingel, J., Rudie, K.: A survey of timed automata for the development of real-time systems. Comput. Sci. Rev. 9, 1–26 (2013)

    Article  Google Scholar 

  28. Wang, J., Mendler, M., Roop, P., Bodin, B.: Timing analysis of synchronous programs using WCRT algebra: scalability through abstraction. ACM TECS 16(5s), 177:1–177:19 (2017)

    Google Scholar 

  29. Wang, J.J., Roop, P.S., Andalam, S.: ILPc: a novel approach for scalable timing analysis of synchronous programs. In: CASES 2013, Montreal, Canada, September–October 2013, pp. 20:1–20:10 (2013)

    Google Scholar 

  30. Yip, E., Roop, P.S., Biglari-Abhari, M., Girault, A.: Programming and timing analysis of parallel programs on multicores. In: Proceedings on Application of Concurrency to System Design (ACSD 2013), pp. 160–169. IEEE (2013)

    Google Scholar 

Download references

Acknowledgements

This work was supported by the German Research Council DFG under grant ME-1427/6-2 (PRETSY2).

Author information

Authors and Affiliations

  1. Faculty of Information Systems and Applied Computer Sciences, Bamberg University, Bamberg, Germany

    Michael Mendler & Joaquín Aguado

  2. Department of Computer Science, Edinburgh University, Edinburg, UK

    Bruno Bodin

  3. Department of Electrical and Computer Engineering, Auckland University, Auckland, New Zealand

    Partha Roop

  4. Department of Computer Science, Christian-Albrechts-Universität zu Kiel, Kiel, Germany

    Reinhard von Hanxleden

Authors
  1. Michael Mendler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joaquín Aguado
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bruno Bodin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Partha Roop
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Reinhard von Hanxleden
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Mendler .

Editor information

Editors and Affiliations

  1. Lero–The Irish Software Research Center, University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. Verimag Laboratory, Grenoble, France

    Susanne Graf

  3. Aalborg University, Aalborg, Denmark

    Kim G. Larsen

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Mendler, M., Aguado, J., Bodin, B., Roop, P., von Hanxleden, R. (2019). Logic Meets Algebra: Compositional Timing Analysis for Synchronous Reactive Multithreading. In: Margaria, T., Graf, S., Larsen, K. (eds) Models, Mindsets, Meta: The What, the How, and the Why Not?. Lecture Notes in Computer Science(), vol 11200. Springer, Cham. https://doi.org/10.1007/978-3-030-22348-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-22348-9_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-22347-2

  • Online ISBN: 978-3-030-22348-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation