{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T16:30:36Z","timestamp":1781713836614,"version":"3.54.5"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,11,25]],"date-time":"2019-11-25T00:00:00Z","timestamp":1574640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGBED Rev."],"published-print":{"date-parts":[[2019,11,25]]},"abstract":"<jats:p>This article proposes an automata-based model for describing and verifying the behavior of thread management code in the Linux PREEMPT_RT kernel, on a single-core system. The automata model defines the events that influence the timing behavior of the execution of threads, and the relations among them. This article also presents the extension of the Linux trace features that enable the trace of such events in a real system. Finally, one example is presented of how the presented model and tracing tool helped catching an inefficiency bug in the scheduler code and ultimately led to improving the kernel.<\/jats:p>","DOI":"10.1145\/3373400.3373410","type":"journal-article","created":{"date-parts":[[2019,11,26]],"date-time":"2019-11-26T13:08:55Z","timestamp":1574773735000},"page":"63-68","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Modeling the behavior of threads in the PREEMPT_RT Linux kernel using automata"],"prefix":"10.1145","volume":"16","author":[{"given":"Daniel Bristot","family":"de Oliveira","sequence":"first","affiliation":[{"name":"Universidade Federal de Santa Catarina, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tommaso","family":"Cucinotta","sequence":"additional","affiliation":[{"name":"Scuola Superiore Sant'Anna, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R\u00f4mulo Silva","family":"de Oliveira","sequence":"additional","affiliation":[{"name":"Universidade Federal de Santa Catarina, Florian\u00f3polis, Brazil"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,11,25]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"384","volume-title":"Discrete Event Systems, 2006 8th International Workshop on","author":"Fabian M.","year":"2006","unstructured":"\u00c5 kesson, K., Fabian , M. , Flordal , H. , and Malik , R . Supremica - An integrated environment for verification, synthesis and simulation of discrete event systems . In Discrete Event Systems, 2006 8th International Workshop on ( 2006 ), pp. 384 -- 385 . \u00c5 kesson, K., Fabian, M., Flordal, H., and Malik, R. Supremica - An integrated environment for verification, synthesis and simulation of discrete event systems. In Discrete Event Systems, 2006 8th International Workshop on (2006), pp. 384--385."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186058"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTTAS.2002.1137388"},{"key":"e_1_2_1_4_1","first-page":"1","volume-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA, 2002), POPL '02, ACM","author":"Ball T.","unstructured":"Ball , T. , and Rajamani , S. K . The slam project: Debugging system software via static analysis . In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA, 2002), POPL '02, ACM , pp. 1 -- 3 . Ball, T., and Rajamani, S. K. The slam project: Debugging system software via static analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA, 2002), POPL '02, ACM, pp. 1--3."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2007.17"},{"key":"e_1_2_1_7_1","first-page":"111","volume-title":"Proceedings of the 27th IEEE International Real-Time Systems Symposium (Washington, DC, USA, 2006), RTSS '06, IEEE Computer Society","author":"Calandrino J. M.","unstructured":"Calandrino , J. M. , Leontyev , H. , Block , A. , Devi , U. C. , and Anderson , J. H . Litmusr t: A testbed for empirically comparing real-time multiprocessor schedulers . In Proceedings of the 27th IEEE International Real-Time Systems Symposium (Washington, DC, USA, 2006), RTSS '06, IEEE Computer Society , pp. 111 -- 126 . Calandrino, J. M., Leontyev, H., Block, A., Devi, U. C., and Anderson, J. H. Litmusr t: A testbed for empirically comparing real-time multiprocessor schedulers. In Proceedings of the 27th IEEE International Real-Time Systems Symposium (Washington, DC, USA, 2006), RTSS '06, IEEE Computer Society, pp. 111--126."},{"key":"e_1_2_1_8_1","volume-title":"Introduction to Discrete Event Systems","author":"Cassandras C. G.","year":"2010","unstructured":"Cassandras , C. G. , and Lafortune , S . Introduction to Discrete Event Systems , 2 nd ed. Springer Publishing Company, Inc orporated, 2010 . Cassandras, C. G., and Lafortune, S. Introduction to Discrete Event Systems, 2nd ed. Springer Publishing Company, Incorporated, 2010.","edition":"2"},{"key":"e_1_2_1_9_1","first-page":"19","volume-title":"Proceedings of the 9th Annual Workshop on Operating Systems Platforms for Embedded Real-Time applications","author":"Cerqueira F.","year":"2013","unstructured":"Cerqueira , F. , and Brandenburg , B . A comparison of scheduling latency in linux, preempt-rt, and litmus-rt . In Proceedings of the 9th Annual Workshop on Operating Systems Platforms for Embedded Real-Time applications ( 2013 ), pp. 19 -- 29 . Cerqueira, F., and Brandenburg, B. A comparison of scheduling latency in linux, preempt-rt, and litmus-rt. In Proceedings of the 9th Annual Workshop on Operating Systems Platforms for Embedded Real-Time applications (2013), pp. 19--29."},{"key":"e_1_2_1_10_1","volume-title":"May","author":"Corbet J.","year":"2006","unstructured":"Corbet , J. The kernel lock validator. https:\/\/lwn.net\/Articles\/185666\/ , May 2006 . Corbet, J. The kernel lock validator. https:\/\/lwn.net\/Articles\/185666\/, May 2006."},{"key":"e_1_2_1_11_1","unstructured":"de Oliveira D. B. ___schedule() being called twice the second in vain. http:\/\/bristot.me\/___schedule-being-called-twice-the-second-in-vain\/ July 2018.  de Oliveira D. B. ___schedule() being called twice the second in vain. http:\/\/bristot.me\/___schedule-being-called-twice-the-second-in-vain\/ July 2018."},{"key":"e_1_2_1_12_1","first-page":"6","article-title":"Timing analysis of the PREEMPT RT linux kernel. Softw","volume":"46","author":"de Oliveira D. B.","year":"2016","unstructured":"de Oliveira , D. B. , and de Oliveira , R. S . Timing analysis of the PREEMPT RT linux kernel. Softw ., Pract. Exper. 46 , 6 ( 2016 ), 789--819. de Oliveira, D. B., and de Oliveira, R. S. Timing analysis of the PREEMPT RT linux kernel. Softw., Pract. Exper. 46, 6 (2016), 789--819.","journal-title":"Pract. Exper."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2017.8247611"},{"key":"e_1_2_1_14_1","first-page":"483","volume-title":"International Symposium on Graph Drawing","author":"Ellson J.","year":"2001","unstructured":"Ellson , J. , Gansner , E. , Koutsofios , L. , North , S. C. , and Woodhull , G . Graphviz - open source graph drawing tools . In International Symposium on Graph Drawing ( 2001 ), Springer , pp. 483 -- 484 . Ellson, J., Gansner, E., Koutsofios, L., North, S. C., and Woodhull, G. Graphviz - open source graph drawing tools. In International Symposium on Graph Drawing (2001), Springer, pp. 483--484."},{"key":"e_1_2_1_15_1","volume-title":"Realtime Linux: academia v. reality. Linux Weekly News (July","author":"Gleixner T.","year":"2010","unstructured":"Gleixner , T. Realtime Linux: academia v. reality. Linux Weekly News (July 2010 ). Available at https:\/\/lwn.net\/Articles\/397422\/. Gleixner, T. Realtime Linux: academia v. reality. Linux Weekly News (July 2010). Available at https:\/\/lwn.net\/Articles\/397422\/."},{"key":"e_1_2_1_16_1","first-page":"58","volume-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA, 2002), POPL '02, ACM","author":"Henzinger T. A.","unstructured":"Henzinger , T. A. , Jhala , R. , Majumdar , R. , and Sutre , G . Lazy abstraction . In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA, 2002), POPL '02, ACM , pp. 58 -- 70 . Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. Lazy abstraction. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA, 2002), POPL '02, ACM, pp. 58--70."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_18_1","volume-title":"Intel\u00ae 64 and IA-32 Architectures Software Developer's Manual","author":"Intel Corporation","unstructured":"Intel Corporation . Intel\u00ae 64 and IA-32 Architectures Software Developer's Manual : Vol. 3 . No. 325384-060US. September 2016. Intel Corporation. Intel\u00ae 64 and IA-32 Architectures Software Developer's Manual: Vol. 3. No. 325384-060US. September 2016."},{"key":"e_1_2_1_19_1","first-page":"207","volume-title":"Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles (New York, NY, USA, 2009), SOSP '09, ACM","author":"Klein G.","unstructured":"Klein , G. , Elphinstone , K. , Heiser , G. , Andronick , J. , Cock , D. , Derrin , P. , Elkaduwe , D. , Engelhardt , K. , Kolanski , R. , Norrish , M. , Sewell , T. , Tuch , H. , and Winwood , S . sel4: Formal verification of an os kernel . In Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles (New York, NY, USA, 2009), SOSP '09, ACM , pp. 207 -- 220 . Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., and Winwood, S. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles (New York, NY, USA, 2009), SOSP '09, ACM, pp. 207--220."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_2"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2335"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17581-2_14"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1464245.1464246"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"e_1_2_1_27_1","first-page":"322","volume-title":"Proc. First IEEE Symp. on Logic in Computer Science","author":"Vardi M. Y.","year":"1986","unstructured":"Vardi , M. Y. , and Wolper , P . An automata-theoretic approach to automatic program verification . In Proc. First IEEE Symp. on Logic in Computer Science ( 1986 ), pp. 322 -- 331 . Vardi, M. Y., and Wolper, P. An automata-theoretic approach to automatic program verification. In Proc. First IEEE Symp. on Logic in Computer Science (1986), pp. 322--331."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321719"}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373400.3373410","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373400.3373410","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:16Z","timestamp":1750199896000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373400.3373410"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,25]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,11,25]]}},"alternative-id":["10.1145\/3373400.3373410"],"URL":"https:\/\/doi.org\/10.1145\/3373400.3373410","relation":{},"ISSN":["1551-3688"],"issn-type":[{"value":"1551-3688","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,25]]},"assertion":[{"value":"2019-11-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}