Document Open Access Logo

History-Based Run-Time Requirement Enforcement of Non-Functional Properties on MPSoCs

Authors Khalil Esper, Jürgen Teich

PDF
Thumbnail PDF

File

OASIcs.NG-RES.2024.4.pdf
  • Filesize: 0.55 MB
  • 11 pages

Document Identifiers

Author Details

Khalil Esper
  • Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), Germany
Jürgen Teich
  • Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), Germany

Funding

This work is funded by the Deutsche Forschungsgemeinschaft (DFG, German Research-Foundation) - Project Number 146371743 - TRR 89 Invasive Computing.

Cite AsGet BibTex

Khalil Esper and Jürgen Teich. History-Based Run-Time Requirement Enforcement of Non-Functional Properties on MPSoCs. In Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024). Open Access Series in Informatics (OASIcs), Volume 117, pp. 4:1-4:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.NG-RES.2024.4

Abstract

Embedded system applications usually have requirements regarding non-functional properties of their execution like latency or power consumption. Enforcement of such requirements can be implemented by a reactive control loop, where an enforcer determines based on a system response (feedback) how to control the system, e.g., by selecting the number of active cores allocated to a program or by scaling their voltage/frequency mode. It is of a particular interest to design enforcement strategies for which it is possible to provide formal guarantees with respect to requirement violations, especially under a largely varying environmental input (workload) per execution. In this paper, we consider enforcement strategies that are modeled by a finite state machine (FSM) and the environment by a discrete-time Markov chain. Such a formalization enables the formal verification of temporal properties (verification goals) regarding the satisfaction of requirements of a given enforcement strategy. In this paper, we propose history-based enforcement FSMs which compute a reaction not just on the current, but on a fixed history of K previously observed system responses. We then analyze the quality of such enforcement FSMs in terms of the probability of satisfying a given set of verification goals and compare them to enforcement FSMs that react solely on the current system response. As experimental results, we present three use cases while considering requirements on latency and power consumption. The results show that history-based enforcement FSMs outperform enforcement FSMs that only consider the current system response regarding the probability of satisfying a given set of verification goals.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Multicore architectures
  • Theory of computation → Linear logic
  • Theory of computation → Modal and temporal logics
  • Hardware → Finite state machines
  • Computer systems organization → Self-organizing autonomic computing
  • Theory of computation → Verification by model checking
  • Mathematics of computing → Probabilistic representations
Keywords
  • Verification
  • Runtime Requirement Enforcement
  • History
  • Latency

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Nidhi Anantharajaiah, Tamim Asfour, Michael Bader, Lars Bauer, Jürgen Becker, Simon Bischof, Marcel Brand, Hans-Joachim Bungartz, Christian Eichler, Khalil Esper, Joachim Falk, Nael Fasfous, Felix Freiling, Andreas Fried, Michael Gerndt, Michael Glaß, Jeferson Gonzalez, Frank Hannig, Christian Heidorn, Jörg Henkel, Andreas Herkersdorf, Benedict Herzog, Jophin John, Timo Hönig, Felix Hundhausen, Heba Khdr, Tobias Langer, Oliver Lenke, Fabian Lesniak, Alexander Lindermayr, Alexandra Listl, Sebastian Maier, Nicole Megow, Marcel Mettler, Daniel Müller-Gritschneder, Hassan Nassar, Fabian Paus, Alexander Pöppl, Behnaz Pourmohseni, Jonas Rabenstein, Phillip Raffeck, Martin Rapp, Santiago Narváez Rivas, Mark Sagi, Franziska Schirrmacher, Ulf Schlichtmann, Florian Schmaus, Wolfgang Schröder-Preikschat, Tobias Schwarzer, Mohammed Bakr Sikal, Bertrand Simon, Gregor Snelting, Jan Spieck, Akshay Srivatsa, Walter Stechele, Jürgen Teich, Isaías A. Comprés Ureña, Ingrid Verbauwhede, Dominik Walter, Thomas Wild, Stefan Wildermann, Mario Wille, Michael Witterauf, and Li Zhang. Invasive Computing. FAU University Press, 2022. Google Scholar
  2. Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. On the Logical Characterisation of Performability Properties. In Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings, volume 1853 of Lecture Notes in Computer Science, pages 780-792. Springer, 2000. Google Scholar
  3. Christel Baier, Joost-Pieter Katoen, and Holger Hermanns. Approximate symbolic model checking of continuous-time markov chains. In CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, volume 1664 of Lecture Notes in Computer Science, pages 146-161. Springer, 1999. Google Scholar
  4. Dwaipayan Biswas, Vibishna Balagopal, Rishad A. Shafik, Bashir M. Al-Hashimi, and Geoff V. Merrett. Machine learning for run-time energy optimisation in many-core systems. In David Atienza and Giorgio Di Natale, editors, Design, Automation & Test in Europe Conference & Exhibition, DATE 2017, Lausanne, Switzerland, March 27-31, 2017, pages 1588-1592. IEEE, 2017. Google Scholar
  5. Roderick Bloem, Bettina Könighofer, Robert Könighofer, and Chao Wang. Shield synthesis: Runtime Enforcement for Reactive Systems. In Tools and Algorithms for the Construction and Analysis of Systems, volume 9035 of Lecture Notes in Computer Science, pages 533-548. Springer, 2015. Google Scholar
  6. Sophie Cerf, Raphaël Bleuse, Valentin Reis, Swann Perarnau, and Eric Rutten. Sustaining performance while reducing energy consumption: a control theory approach. In Euro-Par 2021: Parallel Processing: 27th International Conference on Parallel and Distributed Computing, Lisbon, Portugal, September 1-3, 2021, Proceedings 27, pages 334-349. Springer, 2021. Google Scholar
  7. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer, 1981. Google Scholar
  8. Junio Cezar Ribeiro Da Silva, Lorena Leão, Vinicius Petrucci, Abdoulaye Gamatié, and Fernando Magno Quintão Pereira. Mapping computations in heterogeneous multicore systems with statistical regression on program inputs. ACM Transactions on Embedded Computing Systems (TECS), 20(6):1-35, 2021. Google Scholar
  9. Kalyanmoy Deb, Samir Agrawal, Amrit Pratap, and T. Meyarivan. A fast and elitist multiobjective genetic algorithm: NSGA-II. IEEE Trans. Evol. Comput., 6(2):182-197, 2002. Google Scholar
  10. Khalil Esper, Jan Spieck, Pierre-Louis Sixdenier, Stefan Wildermann, and Jürgen Teich. RAVEN: reinforcement learning for generating verifiable run-time requirement enforcers for MPSoCs. In Fourth Workshop on Next Generation Real-Time Embedded Systems, NG-RES 2023, January 18, 2023, Toulouse, France, volume 108 of OASIcs, pages 7:1-7:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  11. Khalil Esper, Stefan Wildermann, and Jürgen Teich. Enforcement FSMs: specification and verification of non-functional properties of program executions on MPSoCs. In MEMOCODE '21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Virtual Event, China, November 20-22, 2021, pages 21-31. ACM, 2021. Google Scholar
  12. Khalil Esper, Stefan Wildermann, and Jürgen Teich. Multi-requirement enforcement of non-functional properties on MPSoCs using enforcement FSMs - A case study. In Third Workshop on Next Generation Real-Time Embedded Systems, NG-RES@HiPEAC 2022, June 22, 2022, Budapest, Hungary, volume 98 of OASIcs, pages 2:1-2:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  13. Khalil Stefan Wildermann Esper and Jürgen Teich. Automatic synthesis of FSMs for enforcing non-functional requirements on MPSoCs using multi-objective evolutionary algorithms. ACM Trans. Des. Autom. Electron. Syst., August 2023. Google Scholar
  14. Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, and Jean-Luc Richier. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design, 38(3):223-262, 2011. Google Scholar
  15. Xinwei Fang, Sinem Getir Yaman, Radu Calinescu, Julie Wilson, and Colin Paterson. Predicting nonfunctional requirement violations in autonomous systems. ACM Transactions on Autonomous and Adaptive Systems, 2023. Google Scholar
  16. Connor Imes, David HK Kim, Martina Maggio, and Henry Hoffmann. POET: a portable approach to minimizing energy under soft real-time constraints. In 21st IEEE Real-Time and Embedded Technology and Applications Symposium, pages 75-86. IEEE Computer Society, 2015. Google Scholar
  17. Syed Muhammad Zeeshan Iqbal, Yuchen Liang, and Håkan Grahn. Parmibench - An open-source benchmark for embedded multiprocessor systems. IEEE Comput. Archit. Lett., 9(2):45-48, 2010. Google Scholar
  18. Wolfram Just, Thomas Bernard, Matthias Ostheimer, Ekkehard Reibold, and Hartmut Benner. Mechanism of time-delayed feedback control. Physical Review Letters, 78(2):203, 1997. Google Scholar
  19. David H. K. Kim, Connor Imes, and Henry Hoffmann. Racing and pacing to idle: Theoretical and empirical analysis of energy optimization heuristics. In 2015 IEEE 3rd International Conference on Cyber-Physical Systems, Networks, and Applications, CPSNA 2015, Kowloon, Hong Kong, China, August 19-21, 2015, pages 78-85. IEEE Computer Society, 2015. Google Scholar
  20. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585-591. Springer, 2011. Google Scholar
  21. Yiyi Liao, Jun Xie, and Andreas Geiger. KITTI-360: A novel dataset and benchmarks for urban scene understanding in 2d and 3d. CoRR, abs/2109.13410, 2021. Google Scholar
  22. Martin Lukasiewycz, Michael Glaß, Felix Reimann, and Jürgen Teich. Opt4j: a modular framework for meta-heuristic optimization. In Proceedings of the 13th annual conference on Genetic and evolutionary computation, pages 1723-1730, 2011. Google Scholar
  23. Sumit K. Mandal, Ganapati Bhat, Janardhan Rao Doppa, Partha Pratim Pande, and Ümit Y. Ogras. An energy-aware online learning framework for resource management in heterogeneous platforms. ACM Trans. Design Autom. Electr. Syst., 25(3):28:1-28:26, 2020. Google Scholar
  24. Sumit K. Mandal, Ganapati Bhat, Chetan Arvind Patil, Janardhan Rao Doppa, Partha Pratim Pande, and Ümit Y. Ogras. Dynamic resource management of heterogeneous mobile platforms via imitation learning. IEEE Trans. Very Large Scale Integr. Syst., 27(12):2842-2854, 2019. Google Scholar
  25. Maxime Mirka, Gilles Sassatelli, and Abdoulaye Gamatié. Online learning for dynamic control of openmp workloads. In 9th International Conference on Modern Circuits and Systems Technologies, MOCAST 2020, Bremen, Germany, September 7-9, 2020, pages 1-6. IEEE, 2020. Google Scholar
  26. Anway Mukherjee and Thidapat Chantem. Energy management of applications with varying resource usage on smartphones. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 37(11):2416-2427, 2018. Google Scholar
  27. Thannirmalai Somu Muthukaruppan, Mihai Pricopi, Vanchinathan Venkataramani, Tulika Mitra, and Sanjay Vishin. Hierarchical power management for asymmetric multi-core in dark silicon era. In The 50th Annual Design Automation Conference 2013, DAC '13, Austin, TX, USA, May 29 - June 07, 2013, pages 174:1-174:9. ACM, 2013. Google Scholar
  28. Sascha Roloff, Frank Hannig, and Jürgen Teich. Modeling and Simulation of Invasive Applications and Architectures. Computer Architecture and Design Methodologies. Springer, 2019. Google Scholar
  29. Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC), 3(1):30-50, 2000. Google Scholar
  30. Jan Spieck, Pierre-Louis Sixdenier, Khalil Esper, Stefan Wildermann, and Jürgen Teich. Hybrid genetic reinforcement learning for generating run-time requirement enforcers. In 2023 21st ACM-IEEE International Symposium on Formal Methods and Models for System Design (MEMOCODE), pages 23-35, 2023. Google Scholar
  31. Jürgen Teich, Michael Glaß, Sascha Roloff, Wolfgang Schröder-Preikschat, Gregor Snelting, Andreas Weichslgartner, and Stefan Wildermann. Language and Compilation of Parallel Programs for *-Predictable MPSoC Execution Using Invasive Computing. In 10th IEEE International Symposium on Embedded Multicore/Many-core Systems-on-Chip, MCSOC 2016, Lyon, France, September 21-23, 2016, pages 313-320. IEEE Computer Society, 2016. Google Scholar
  32. Jürgen Teich, Jörg Henkel, Andreas Herkersdorf, Doris Schmitt-Landsiedel, Wolfgang Schröder-Preikschat, and Gregor Snelting. Invasive computing: An overview. In Multiprocessor System-on-Chip - Hardware Design and Tool Integration, pages 241-268. Springer, 2011. Google Scholar
  33. Jürgen Teich, Pouya Mahmoody, Behnaz Pourmohseni, Sascha Roloff, Wolfgang Schröder-Preikschat, and Stefan Wildermann. Run-Time Enforcement of Non-functional Program Properties on MPSoCs. In A Journey of Embedded and Cyber-Physical Systems, pages 125-149. Springer, 2021. Google Scholar
  34. Jürgen Teich, Behnaz Pourmohseni, Oliver Keszöcze, Jan Spieck, and Stefan Wildermann. Run-Time Enforcement of Non-Functional Application Requirements in Heterogeneous Many-Core Systems. In 25th Asia and South Pacific Design Automation Conference, ASP-DAC 2020, Beijing, China, January 13-16, 2020, pages 629-636. IEEE, 2020. Google Scholar
  35. Xiaohang Wang, Amit Kumar Singh, Bing Li, Yang Yang, Hong Li, and Terrence S. T. Mak. Bubble budgeting: Throughput optimization for dynamic workloads by exploiting dark cores in many core systems. IEEE Trans. Computers, 67(2):178-192, 2018. URL: https://doi.org/10.1109/TC.2017.2735967.
  36. Dong Yue and Qing-Long Han. Delayed feedback control of uncertain systems with time-varying input delay. Automatica, 41(2):233-240, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact