Document Open Access Logo

Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle

Authors Sergey Bozhko, Björn B. Brandenburg

PDF
Thumbnail PDF

File

LIPIcs.ECRTS.2020.22.pdf
  • Filesize: 0.97 MB
  • 24 pages

Document Identifiers

Author Details

Sergey Bozhko
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany
Björn B. Brandenburg
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 803111). Funded in part by Deutsche Forschungsgemeinschaft (DFG) - 391919384.

Acknowledgements

We thank the members of the ANR-DFG joint project RT-PROOFS, in particular Maxime Lesourd and Sophie Quinton, for their valuable feedback and suggestions.

Cite AsGet BibTex

Sergey Bozhko and Björn B. Brandenburg. Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle. In 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 165, pp. 22:1-22:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECRTS.2020.22

Abstract

This paper introduces the first general and rigorous formalization of the classic busy-window principle for uniprocessors. The essence of the principle is identified as a minimal set of generic, high-level hypotheses that allow for a unified and general abstract response-time analysis, which is independent of specific scheduling policies, workload models, and preemption policy details. From this abstract core, the paper shows how to obtain concrete analysis instantiations for specific uniprocessor schedulers via a sequence of refinement steps, and provides formally verified response-time bounds for eight common schedulers and workloads, including the widely used fixed-priority (FP) and earliest-deadline first (EDF) scheduling policies in the context of fully, limited-, and non-preemptive sporadic tasks. All definitions and proofs in this paper have been mechanized and verified with the Coq proof assistant, and in fact form the common core and foundation for verified response-time analyses in the Prosa open-source framework for formally proven schedulability analyses.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Real-time systems
  • Software and its engineering → Scheduling
  • Theory of computation → Scheduling algorithms
Keywords
  • hard real-time systems
  • response-time analysis
  • uniprocessor
  • busy window
  • fixed priority
  • EDF
  • verification
  • Coq
  • Prosa
  • preemptive
  • non-preemptive
  • limited-preemptive

Metrics

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

Related Versions

Supplementary Materials

References

  1. AbstractRTA - ECRTS'20 Artifact Evaluation. URL: https://people.mpi-sws.org/~sbozhko/ECRTS20/AbstractRTA.html.
  2. Neil C. Audsley, Alan Burns, Robert I. Davis, Ken Tindell, and Andy J. Wellings. Fixed priority pre-emptive scheduling: An historical perspective. Real-Time Systems, 8(2-3):173-198, 1995. URL: https://doi.org/10.1007/BF01094342.
  3. Neil C. Audsley, Alan Burns, Mike M. Richardson, Ken Tindell, and Andy J. Wellings. Applying new scheduling theory to static priority pre-emptive scheduling. Software Engineering Journal, 8(5):284-292, 1993. URL: https://doi.org/10.1049/sej.1993.0034.
  4. Sanjoy K. Baruah. The limited-preemption uniprocessor scheduling of sporadic task systems. In 17th Euromicro Conference on Real-Time Systems, ECRTS 2005, pages 137-144. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/ECRTS.2005.32.
  5. Marko Bertogna and Sanjoy K. Baruah. Limited preemption EDF scheduling of sporadic task systems. IEEE Trans. Industrial Informatics, 6(4):579-591, 2010. URL: https://doi.org/10.1109/TII.2010.2049654.
  6. Sergey Bozhko and Björn B. Brandenburg. Abstract response-time analysis: A formal foundation for the busy-window principle (extended version). Technical Report MPI-SWS-2020-003, Max Planck Insitute for Software Systems, 2020. URL: https://www.mpi-sws.org/tr/2020-003.pdf.
  7. Reinder J. Bril, Johan J. Lukkien, and Wim F. J. Verhaegh. Worst-case response time analysis of real-time tasks under fixed-priority scheduling with deferred preemption revisited. In 19th Euromicro Conference on Real-Time Systems, ECRTS 2007, pages 269-279. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/ECRTS.2007.38.
  8. Reinder J. Bril, Johan J. Lukkien, and Wim F. J. Verhaegh. Worst-case response time analysis of real-time tasks under fixed-priority scheduling with deferred preemption. Real-Time Systems, 42(1-3):63-119, 2009. URL: https://doi.org/10.1007/s11241-009-9071-z.
  9. John Carpenter, Shelby Funk, Philip Holman, Anand Srinivasan, James Anderson, and Sanjoy K. Baruah. A categorization of real-time multiprocessor scheduling problems and algorithms, 2004. Google Scholar
  10. Felipe Cerqueira, Felix Stutz, and Björn B. Brandenburg. PROSA: A case for readable mechanized schedulability analysis. In 28th Euromicro Conference on Real-Time Systems, ECRTS 2016, pages 273-284. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/ECRTS.2016.28.
  11. Jian-Jia Chen, Geoffrey Nelissen, Wen-Hung Huang, Maolin Yang, Björn B. Brandenburg, Konstantinos Bletsas, Cong Liu, Pascal Richard, Frédéric Ridouard, Neil C. Audsley, Raj Rajkumar, Dionisio de Niz, and Georg von der Brüggen. Many suspensions, many problems: a review of self-suspending tasks in real-time systems. Real-Time Systems, 55(1):144-207, 2019. URL: https://doi.org/10.1007/s11241-018-9316-9.
  12. Robert I. Davis, Alan Burns, Reinder J. Bril, and Johan J. Lukkien. Controller area network (CAN) schedulability analysis: Refuted, revisited and revised. Real-Time Systems, 35(3):239-272, 2007. URL: https://doi.org/10.1007/s11241-007-9012-7.
  13. Robert I. Davis, A. Zabos, and Alan Burns. Efficient exact schedulability tests for fixed priority real-time systems. IEEE Trans. Computers, 57(9):1261-1276, 2008. URL: https://doi.org/10.1109/TC.2008.66.
  14. Bruno Dutertre. Formal analysis of the priority ceiling protocol. In 21st IEEE Real-Time Systems Symposium, RTSS 2000, pages 151-160. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/REAL.2000.896005.
  15. Pascal Fradet, Xiaojie Guo, Jean-François Monin, and Sophie Quinton. A generalized digraph model for expressing dependencies. In 26th International Conference on Real-Time Networks and Systems, RTNS 2018, pages 72-82. ACM, 2018. URL: https://doi.org/10.1145/3273905.3273918.
  16. Pascal Fradet, Xiaojie Guo, Jean-François Monin, and Sophie Quinton. CertiCAN: A tool for the Coq certification of CAN analysis results. In 25th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2019, pages 182-191. IEEE, 2019. URL: https://doi.org/10.1109/RTAS.2019.00023.
  17. Laurent George, Nicolas Rivierre, and Marco Spuri. Preemptive and Non-Preemptive Real-Time UniProcessor Scheduling. Technical Report RR-2966, INRIA, 1996. Google Scholar
  18. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, pages 653-669. USENIX Association, 2016. URL: https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu.
  19. Nan Guan and Wang Yi. General and efficient response time analysis for EDF scheduling. In Design, Automation & Test in Europe Conference & Exhibition, DATE 2014, pages 1-6. European Design and Automation Association, 2014. URL: https://doi.org/10.7873/DATE.2014.268.
  20. Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, and Zhong Shao. Integrating formal schedulability analysis into a verified OS kernel. In 31st International Conference on Computer Aided Verification, CAV 2019, pages 496-514. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_28.
  21. José C. Palencia Gutiérrez and Michael González Harbour. Offset-based response time analysis of distributed systems scheduled under EDF. In 15th Euromicro Conference on Real-Time Systems, ECRTS 2003, pages 3-12. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/EMRTS.2003.1212721.
  22. José C. Palencia Gutiérrez and Michael González Harbour. Response time analysis of EDF distributed real-time systems. J. Embedded Computing, 1(2):225-237, 2005. URL: http://content.iospress.com/articles/journal-of-embedded-computing/jec00017.
  23. Zain Alabedin Haj Hammadeh, Rolf Ernst, Sophie Quinton, Rafik Henia, and Laurent Rioux. Bounding deadline misses in weakly-hard real-time systems with task dependencies. In Design, Automation & Test in Europe Conference & Exhibition, DATE 2017, pages 584-589. IEEE, 2017. URL: https://doi.org/10.23919/DATE.2017.7927054.
  24. Michael González Harbour and José C. Palencia Gutiérrez. Response time analysis for tasks scheduled under EDF within fixed priorities. In 24th IEEE Real-Time Systems Symposium, RTSS 2003, pages 200-209. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/REAL.2003.1253267.
  25. Michael González Harbour, Mark H. Klein, and John P. Lehoczky. Fixed priority scheduling periodic tasks with varying execution priority. In 12th IEEE Real-Time Systems Symposium, RTSS 1991, pages 116-128. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/REAL.1991.160365.
  26. Rafik Henia, Arne Hamann, Marek Jersak, Razvan Racu, Kai Richter, and Rolf Ernst. System level performance analysis-the SymTA/S approach. IEE Proceedings-Computers and Digital Techniques, 152(2):148-166, 2005. Google Scholar
  27. Kevin Jeffay, Donald F. Stanat, and Charles U. Martel. On non-preemptive scheduling of periodic and sporadic tasks. In 12th IEEE Real-Time Systems Symposium, RTSS 1991, pages 129-139. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/REAL.1991.160366.
  28. Mathai Joseph and Paritosh K. Pandya. Finding response times in a real-time system. Comput. J., 29(5):390-395, 1986. URL: https://doi.org/10.1093/comjnl/29.5.390.
  29. Paul K. Harter Jr. Response times in level structured systems. Technical Report CU-CS-269-84, University of Colorado, 1984. Google Scholar
  30. John P. Lehoczky. Fixed priority scheduling of periodic task sets with arbitrary deadlines. In 11th IEEE Real-Time Systems Symposium, RTSS 1990, pages 201-209. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/REAL.1990.128748.
  31. C. L. Liu and James W. Layland. Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM, 20(1):46-61, 1973. URL: https://doi.org/10.1145/321738.321743.
  32. Assia Mahboubi and Enrico Tassi. Mathematical components, 2017. Google Scholar
  33. Geoffrey Nelissen, José Carlos Fonseca, Gurulingesh Raravi, and Vincent Nélis. Timing analysis of fixed priority self-suspending sporadic tasks. In 27th Euromicro Conference on Real-Time Systems, ECRTS 2015, pages 80-89. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/ECRTS.2015.15.
  34. Paul K. Harten Jr. Response times in level-structured systems. ACM Trans. Comput. Syst., 5(3):232-248, 1987. URL: https://doi.org/10.1145/24068.24069.
  35. Prosa: The proven schedulability analysis repository, project web site. URL: http://prosa.mpi-sws.org.
  36. Johannes Schlatow and Rolf Ernst. Response-time analysis for task chains in communicating threads. In 22th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016, pages 245-254. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/RTAS.2016.7461359.
  37. Simon Schliecker, Jonas Rox, Matthias Ivers, and Rolf Ernst. Providing accurate event models for the analysis of heterogeneous multiprocessor systems. In 6th International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2008, pages 185-190. ACM, 2008. URL: https://doi.org/10.1145/1450135.1450177.
  38. Lui Sha, Tarek F. Abdelzaher, Karl-Erik Årzén, Anton Cervin, Theodore P. Baker, Alan Burns, Giorgio C. Buttazzo, Marco Caccamo, John P. Lehoczky, and Aloysius K. Mok. Real time scheduling theory: A historical perspective. Real-Time Systems, 28(2-3):101-155, 2004. URL: https://doi.org/10.1023/B:TIME.0000045315.61234.1e.
  39. Lui Sha, Ragunathan Rajkumar, and John P. Lehoczky. Priority inheritance protocols: An approach to real-time synchronization. IEEE Trans. Computers, 39(9):1175-1185, 1990. URL: https://doi.org/10.1109/12.57058.
  40. Michael Short. Improved schedulability analysis of implicit deadline tasks under limited preemption EDF scheduling. In 16th IEEE Conference on Emerging Technologies & Factory Automation, ETFA 2011, pages 1-8. IEEE, 2011. URL: https://doi.org/10.1109/ETFA.2011.6059008.
  41. Marco Spuri. Analysis of Deadline Scheduled Real-Time Systems. Technical Report RR-2772, INRIA, 1996. Google Scholar
  42. The Coq proof assistant, project web site. URL: https://coq.inria.fr.
  43. Ken Tindell, Alan Burns, and Andy J. Wellings. An extendible approach for analyzing fixed priority hard real-time tasks. Real-Time Systems, 6(2):133-151, 1994. URL: https://doi.org/10.1007/BF01088593.
  44. Yun Wang and Manas Saksena. Scheduling fixed-priority tasks with preemption threshold. In 6th International Workshop on Real-Time Computing and Applications Symposium, RTCSA 1999, page 328. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/RTCSA.1999.811269.
  45. Matthew Wilding. A machine-checked proof of the optimality of a real-time scheduling policy. In 10th International Conference on Computer Aided Verification, CAV 1998, pages 369-378. Springer, 1998. URL: https://doi.org/10.1007/BFb0028759.
  46. Gang Yao, Giorgio C. Buttazzo, and Marko Bertogna. Feasibility analysis under fixed priority scheduling with limited preemptions. Real-Time Systems, 47(3):198-223, 2011. URL: https://doi.org/10.1007/s11241-010-9113-6.
  47. Man-Ki Yoon, Sibin Mohan, Chien-Ying Chen, and Lui Sha. TaskShuffler: A schedule randomization protocol for obfuscation against timing inference attacks in real-time systems. In 22th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016, pages 111-122. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/RTAS.2016.7461362.
  48. Xingyuan Zhang, Christian Urban, and Chunhan Wu. Priority inheritance protocol proved correct. J. Autom. Reasoning, 64(1):73-95, 2020. URL: https://doi.org/10.1007/s10817-019-09511-5.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact