Document Open Access Logo

SlackCheck: A Linux Kernel Module to Verify Temporal Properties of a Task Schedule

Authors Michele Castrovilli , Enrico Bini

PDF
Thumbnail PDF

File

LIPIcs.ECRTS.2024.2.pdf
  • Filesize: 1 MB
  • 24 pages

Document Identifiers

Author Details

Michele Castrovilli
  • University of Turin, Italy
Enrico Bini
  • University of Turin, Italy

Funding

This work has been partially supported by the spoke "FutureHPC and BigData" of the ICSC - Centro Nazionale di Ricerca in High-Performance Computing, Big Data and Quantum Computing funded by European Union - NextGenerationEU.

Cite AsGet BibTex

Michele Castrovilli and Enrico Bini. SlackCheck: A Linux Kernel Module to Verify Temporal Properties of a Task Schedule. In 36th Euromicro Conference on Real-Time Systems (ECRTS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 298, pp. 2:1-2:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECRTS.2024.2

Abstract

The Linux Kernel offers several scheduling classes. From SCHED_DEADLINE down to SCHED_FIFO, SCHED_RR and SCHED_OTHER, the scheduling classes can provide different responsiveness to very diverse user workloads. Still, Linux does not offer any mechanism to take some action upon the violation of temporal constraints at runtime. The lack of such a feature is also due to the difficulty of extending the established notion of deadline to workloads which are not releasing periodic/sporadic jobs. Exploiting the notion of supply functions for any resource schedule, we implemented SlackCheck, a kernel module which is capable to verify at runtime if a given task is assigned a desired amount of resource or not. SlackCheck adds a constant-time check at every scheduling decision and leverages the recent availability of a Runtime Verification engine in the kernel.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Scheduling
  • Theory of computation → Verification by model checking
  • Proper nouns: People, technologies and companies → Linux
  • Computer systems organization → Real-time operating systems
  • Software and its engineering → Operating systems
Keywords
  • Linux scheduler
  • Runtime verification
  • bounded-delay resource partition
  • supply function
  • service curve
  • real-time calculus
  • network calculus

Metrics

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

References

  1. Benny Åkesson and Kees Goossens. Architectures and modeling of predictable memory controllers for improved system integration. In Design, Automation & Test in Europe Conference & Exhibition, pages 851-856, 2011. URL: https://doi.org/10.1109/DATE.2011.5763145.
  2. Luca Abeni and Giorgio Buttazzo. Integrating multimedia applications in hard real-time systems. In Proceedings 19th IEEE Real-Time Systems Symposium (Cat. No. 98CB36279), pages 4-13. IEEE, 1998. URL: https://doi.org/10.1109/REAL.1998.739726.
  3. Luca Abeni, Tommaso Cucinotta, Giuseppe Lipari, Luca Marzario, and Luigi Palopoli. Qos management through adaptive reservations. Real-Time Systems, 29:131-155, 2005. URL: https://doi.org/10.1007/s11241-005-6882-0.
  4. Luca Abeni, Ashvin Goel, Charles Krasic, Jim Snow, and Jonathan Walpole. A measurement-based analysis of the real-time performance of linux. In Proceedings of the 8th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2002), 24-27 September 2002, San Jose, CA, USA, pages 133-142. IEEE, 2002. URL: https://doi.org/10.1109/RTTAS.2002.1137388.
  5. Shareef Ahmed and James H. Anderson. Tight tardiness bounds for pseudo-harmonic tasks under global-edf-like schedulers. In Björn B. Brandenburg, editor, 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021), volume 196 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:24, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECRTS.2021.11.
  6. Luís Almeida and Paulo Pedreiras. Scheduling within temporal partitions: response-time analysis and server design. In Proceedings of the 4^th ACM International Conference on Embedded Software, pages 95-103, Pisa, Italy, September 2004. ACM. URL: https://doi.org/10.1145/1017753.1017772.
  7. Luís Almeida, Paulo Pedreiras, and José Alberto G. Fonseca. The FTT-CAN protocol: Why and how. IEEE Transaction on Industrial Electronics, 49(6):1189-1201, December 2002. URL: https://doi.org/10.1109/TIE.2002.804967.
  8. François Baccelli, Guy Cohen, Geert Jan Olsder, and Jean-Pierre Quadrat. Synchronization and linearity, volume 3. Wiley New York, 1992. Google Scholar
  9. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to runtime verification. In Lectures on Runtime Verification, volume 10457, pages 1-33. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  10. Enrico Bini, Marko Bertogna, and Sanjoy Baruah. Virtual multiprocessor platforms: Specification and use. In Proceedings of the 30th IEEE Real-Time Systems Symposium, RTSS 2009, Washington, DC, USA, 1-4 December 2009, pages 437-446, Washinghton, DC, USA, December 2009. URL: https://doi.org/10.1109/RTSS.2009.35.
  11. Daniel Bristot de Oliveira, Daniel Casini, and Tommaso Cucinotta. Operating system noise in the linux kernel. IEEE Transactions on Computers, 72(1):196-207, 2023. URL: https://doi.org/10.1109/TC.2022.3187351.
  12. Daniel Bristot de Oliveira, Tommaso Cucinotta, and Rômulo Silva de Oliveira. Efficient formal verification for the linux kernel. In Software Engineering and Formal Methods - 17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings, volume 11724, pages 315-332. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30446-1_17.
  13. Artem Burmyakov, Enrico Bini, and Eduardo Tovar. Compositional multiprocessor scheduling: the GMPR interface. Real-Time Systems, 50(3):342-376, 2014. URL: https://doi.org/10.1007/s11241-013-9199-8.
  14. John M Calandrino, Hennadiy Leontyev, Aaron Block, UmaMaheswari C Devi, and James H Anderson. LITMUS^RT: A testbed for empirically comparing real-time multiprocessor schedulers. In Proceedings of the 27th IEEE Real-Time Systems Symposium (RTSS 2006), 5-8 December 2006, Rio de Janeiro, Brazil, pages 111-126. IEEE, 2006. URL: https://doi.org/10.1109/RTSS.2006.27.
  15. Felipe Cerqueira and Björn Brandenburg. A comparison of scheduling latency in linux, preempt-rt, and litmus rt. In 9th Annual workshop on operating systems platforms for embedded real-time applications, pages 19-29. SYSGO AG, 2013. Google Scholar
  16. Anton Cervin, Johan Eker, Bo Bernhardsson, and Karl-Erik Årzén. Feedback-feedforward scheduling of control tasks. Real-Time Systems, 23(1-2):25-53, 2002. URL: https://doi.org/10.1023/A:1015394302429.
  17. Marcello Cinque, Raffaele Della Corte, Antonio Eliso, and Antonio Pecchia. Rt-cases: Container-based virtualization for temporally separated mixed-criticality task sets. In 31st Euromicro Conference on Real-Time Systems (ECRTS 2019), volume 133, pages 5:1-5:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ECRTS.2019.5.
  18. Fernando J Corbató, Marjorie Merwin-Daggett, and Robert C Daley. An experimental time-sharing system. In Proceedings of the 1962 spring joint computer conference, AFIPS 1962 (Spring), San Francisco, California, USA, May 1-3, 1962, pages 335-344. ACM, 1962. URL: https://doi.org/10.1145/1460833.1460871.
  19. Rene L. Cruz. A calculus for network delay, part I: network elements in isolation. IEEE Transactions on Information Theory, 37(1):114-131, January 1991. URL: https://doi.org/10.1109/18.61109.
  20. Tommaso Cucinotta, Dhaval Giani, Dario Faggioli, and Fabio Checconi. Providing performance guarantees to virtual machines using real-time scheduling. In European Conference on Parallel Processing, volume 6586, pages 657-664. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-21878-1_81.
  21. UmaMaheswari C Devi and James H Anderson. Tardiness bounds under global EDF scheduling on a multiprocessor. Real-Time Systems, 38(2):133-189, 2008. URL: https://doi.org/10.1007/s11241-007-9042-1.
  22. Dario Faggioli, Fabio Checconi, Michael Trimarchi, and Claudio Scordino. An edf scheduling class for the linux kernel. In Proceedings of the 11th Real-Time Linux Workshop, pages 1-8, 2009. Google Scholar
  23. Joël Goossens, Shelby Funk, and Sanjoy Baruah. Priority-driven scheduling of periodic task systems on multiprocessors. Real-Time Systems, 25(2-3):187-205, 2003. URL: https://doi.org/10.1023/A:1025120124771.
  24. Michael B Jones, Daniela Roşu, and Marcel-Cătălin Roşu. CPU reservations and time constraints: Efficient, predictable scheduling of independent activities. ACM SIGOPS Operating Systems Review, 31(5):198-211, 1997. URL: https://doi.org/10.1145/268998.266689.
  25. Paraskevas Karachatzis, Jan Ruh, and Silviu S Craciunas. An evaluation of time-triggered scheduling in the linux kernel. In Proceedings of the 31st International Conference on Real-Time Networks and Systems, RTNS 2023, Dortmund, Germany, June 7-8, 2023, pages 119-131. ACM, 2023. URL: https://doi.org/10.1145/3575757.3593660.
  26. Neil Klingensmith and Suman Banerjee. Hermes: A real time hypervisor for mobile and iot systems. In Proceedings of the 19th International Workshop on Mobile Computing Systems & Applications, HotMobile 2018, Tempe, AZ, USA, February 12-13, 2018, pages 101-106. ACM, 2018. URL: https://doi.org/10.1145/3177102.3177103.
  27. Jean-Yves Le Boudec and Patrick Thiran. Network Calculus: A Theory of Deterministic Queuing Systems for the Internet, volume 2050 of Lecture Notes in Computer Science. Springer, 2001. URL: https://doi.org/10.1007/3-540-45318-0.
  28. Juri Lelli, Claudio Scordino, Luca Abeni, and Dario Faggioli. Deadline scheduling in the linux kernel. Software: Practice and Experience, 46(6):821-839, 2016. URL: https://doi.org/10.1002/spe.2335.
  29. Hennadiy Leontyev, Samarjit Chakraborty, and James H Anderson. Multiprocessor extensions to real-time calculus. Real-Time Systems, 47(6):562-617, 2011. URL: https://doi.org/10.1007/s11241-011-9135-8.
  30. Giuseppe Lipari and Enrico Bini. Resource partitioning among real-time applications. In 15th Euromicro Conference on Real-Time Systems (ECRTS 2003), 2-4 July 2003, Porto, Portugal, Proceedings, pages 151-158, Porto, Portugal, July 2003. URL: https://doi.org/10.1109/EMRTS.2003.1212738.
  31. Chenyang Lu, John A Stankovic, Sang H Son, and Gang Tao. Feedback control real-time scheduling: Framework, modeling, and algorithms. Real-Time Systems, 23(1-2):85-126, 2002. URL: https://doi.org/10.1023/A:1015398403337.
  32. Martina Maggio, Juri Lelli, and Enrico Bini. rt-muse: measuring real-time characteristics of execution platforms. Real-Time Systems, 53(6):857-885, November 2017. URL: https://doi.org/10.1007/s11241-017-9284-5.
  33. Miguel Masmano, Ismael Ripoll, Alfons Crespo, and J Metge. Xtratum: a hypervisor for safety critical embedded systems. In 11th Real-Time Linux Workshop, volume 9, 2009. Google Scholar
  34. Aloysius K. Mok, Xiang Feng, and Deji Chen. Resource partition for real-time systems. In Proceedings of the 7th IEEE Real-Time Technology and Applications Symposium (RTAS 2001), 30 May - 1 June 2001, Taipei, Taiwan, pages 75-84, Taipei, Taiwan, May 2001. URL: https://doi.org/10.1109/RTTAS.2001.929867.
  35. Shuichi Oikawa and Ragunathan Rajkumar. Portable RK: A portable resource kernel for guaranteed and enforced timing behavior. In Proceedings of the Fifth IEEE Real-Time Technology and Applications Symposium, RTAS'99, Vancouver, British Columbia, Canada, June 2-4, 1999, pages 111-120. IEEE, 1999. URL: https://doi.org/10.1109/RTTAS.1999.777666.
  36. Abhay K Parekh and Robert G Gallager. A generalized processor sharing approach to flow control in integrated services networks: the single-node case. IEEE/ACM transactions on networking, 1(3):344-357, 1993. URL: https://doi.org/10.1109/90.234856.
  37. Rodolfo Pellizzoni, Bach Duy Bui, Marco Caccamo, and Lui Sha. Coscheduling of CPU and I/O transactions in COTS-based embedded systems. In Proceedings of the 29th IEEE Real-Time Systems Symposium, RTSS 2008, Barcelona, Spain, 30 November - 3 December 2008, pages 221-231. IEEE, 2008. URL: https://doi.org/10.1109/RTSS.2008.42.
  38. John Regehr and John A. Stankovic. HLS: A framework for composing soft real-time schedulers. In Proceedings of the 22nd IEEE Real-Time Systems Symposium (RTSS 2001), London, UK, 2-6 December 2001, pages 3-14, London, United Kingdom, 2001. URL: https://doi.org/10.1109/REAL.2001.990591.
  39. Insik Shin, Arvind Easwaran, and Insup Lee. Hierarchical scheduling framework for virtual clustering of multiprocessors. In 20th Euromicro Conference on Real-Time Systems, ECRTS 2008, 2-4 July 2008, Prague, Czech Republic, Proceedings, pages 181-190, Prague, Czech Republic, July 2008. URL: https://doi.org/10.1109/ECRTS.2008.28.
  40. Insik Shin and Insup Lee. Periodic resource model for compositional real-time guarantees. In Proceedings of the 24th IEEE Real-Time Systems Symposium (RTSS 2003), 3-5 December 2003, Cancun, Mexico, pages 2-13, Cancun, Mexico, December 2003. URL: https://doi.org/10.1109/REAL.2003.1253249.
  41. Dimitrios Stiliadis and Anujan Varma. Latency-rate servers: a general model for analysis of traffic scheduling algorithms. IEEE/ACM Transactions on networking, 6(5):611-624, 1998. URL: https://doi.org/10.1109/90.731196.
  42. Ion Stoica, Hussein Abdel-Wahab, Kevin Jeffay, Sanjoy K Baruah, Johannes E Gehrke, and C Greg Plaxton. A proportional share resource allocation algorithm for real-time, time-shared systems. In Proceedings of the 17th IEEE Real-Time Systems Symposium (RTSS '96), December 4-6, 1996, Washington, DC, USA, pages 288-299. IEEE, 1996. URL: https://doi.org/10.1109/REAL.1996.563725.
  43. Lothar Thiele, Samarjit Chakraborty, and Martin Naedele. Real-time calculus for scheduling hard real-time systems. In IEEE International Symposium on Circuits and Systems, ISCAS 2000, Emerging Technologies for the 21st Century, Geneva, Switzerland, 28-31 May 2000, Proceedings, pages 101-104, 2000. URL: https://doi.org/10.1109/ISCAS.2000.858698.
  44. Paolo Valente. Using a lag-balance property to tighten tardiness bounds for global EDF. Real-Time Systems, 52(4):486-561, 2016. URL: https://doi.org/10.1007/s11241-015-9237-9.
  45. Y-C Wang and K-J Lin. Implementing a general real-time scheduling framework in the red-linux real-time kernel. In Proceedings of the 20th IEEE Real-Time Systems Symposium, Phoenix, AZ, USA, December 1-3, 1999, pages 246-255. IEEE, 1999. URL: https://doi.org/10.1109/REAL.1999.818850.
  46. Sisu Xi, Meng Xu, Chenyang Lu, Linh TX Phan, Christopher Gill, Oleg Sokolsky, and Insup Lee. Real-time multi-core virtual machine scheduling in xen. In 2014 International Conference on Embedded Software, EMSOFT 2014, New Delhi, India, October 12-17, 2014, pages 27:1-27:10. ACM, 2014. URL: https://doi.org/10.1145/2656045.2656066.
  47. Heechul Yun, Gang Yao, Rodolfo Pellizzoni, Marco Caccamo, and Lui Sha. Memory bandwidth management for efficient performance isolation in multi-core platforms. IEEE Transactions on Computers, 65(2):562-576, February 2016. URL: https://doi.org/10.1109/TC.2015.2425889.
  48. Peter Zijlstra. An update on real-time scheduling on linux (keynote talk). In 19th Euromicro Conference on Real-Time Systems, 2017. 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