{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:52:16Z","timestamp":1750308736548,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,10,1]],"date-time":"2013-10-01T00:00:00Z","timestamp":1380585600000},"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":[[2013,10]]},"abstract":"<jats:p>\n            This paper presents a preliminary study of applying partitioned scheduling in the seL4 microkernel. This microkernel is the first operating system kernel ever to be formally proven for its functional correctness. Even though the kernel is completely verified it still delivers high performance comparable to other L4 kernels. The seL4 kernel implements\n            <jats:italic>isolation<\/jats:italic>\n            of components in terms of the memory resource and security. However, there is still a missing part when it comes to isolation and that is time partitioning. Time partitioning can be implemented inside the kernel (privileged mode) or in user space (user mode). The latter is done using regular user-space thread(s) and can easily be modified while the other approach requires re-verification of the kernel whenever modifications to the time-partitioning policy is done. On the other hand, having the time-partitioning mechanism in privileged mode would yield better performance. We have implemented time partitioning (partitioned scheduling) in the seL4 user space and we elaborate on its performance in terms of overhead costs.\n          <\/jats:p>","DOI":"10.1145\/2544350.2544352","type":"journal-article","created":{"date-parts":[[2013,11,26]],"date-time":"2013-11-26T13:23:15Z","timestamp":1385472195000},"page":"15-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Towards a user-mode approach to partitioned scheduling in the seL4 microkernel"],"prefix":"10.1145","volume":"10","author":[{"given":"Mikael","family":"\u00c5sberg","sequence":"first","affiliation":[{"name":"MRTC\/M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}]},{"given":"Thomas","family":"Nolte","sequence":"additional","affiliation":[{"name":"MRTC\/M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2013,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694613"},{"volume-title":"Airlines Electronic Engineering Committee (AEEC)","year":"1996","author":"ARINC. ARINC","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2012.9"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2011.24"},{"volume-title":"Proc. of the 10th International Conference on Real-Time Systems (RTS)","year":"2002","author":"Barreto L. P.","key":"e_1_2_1_5_1"},{"volume-title":"Proc. of the 4th International Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT)","year":"2008","author":"Behnam M.","key":"e_1_2_1_6_1"},{"volume-title":"QEMU, A Fast and Portable Dynamic Translator. In Proc. of the 23rd USENIX Annual Technical Conference (ATEC)","year":"2005","author":"Bellard F.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:TIME.0000048932.30002.d9"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2005.25"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/827269.828992"},{"volume-title":"Proc. of the 11th Real-Time Linux Workshop (RTLWS)","year":"2009","author":"Faggioli D.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529723"},{"volume-title":"Proc. of the 23rd IEEE Real-Time Systems Symposium (RTSS)","year":"2002","author":"Feng X.","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999435"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1622103.1622106"},{"volume-title":"Visualizing and Measuring the Behavior of Real-Time Systems. In Proc. of the 1st International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS)","year":"2010","author":"Holenderski M.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2011.6059016"},{"volume-title":"Proc. of the 7th International Workshop on Real-Time Computing and Applications Symposium (RTCSA)","year":"2000","author":"Kim D.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"volume-title":"The Linux Foundation","year":"2009","author":"Kroah-Hartman G.","key":"e_1_2_1_21_1"},{"volume-title":"Li. A Fixed-Priority-Driven Open Environment for Real-Time Applications. In Proc. of the 20th IEEE Real-Time Systems Symposium (RTSS)","year":"1999","author":"Kuo T.-W.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1014007.1014016"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2005.80"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/518908.828478"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMRTS.2003.1212738"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2005.43"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2236576.2236578"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/520050.828443"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.v39:1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2007.14"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/956418.956611"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/882482.883804"},{"volume-title":"Proc. of the 12th International VDI Congress Electronic Systems for Vehicles","year":"2005","author":"Scharnhorst T.","key":"e_1_2_1_35_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/956418.956612"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1315580.1315593"},{"volume-title":"Proc. of the WIP session at the 30th IEEE Real-Time Systems Symposium (RTSS)","year":"2009","author":"M. M. H.","key":"e_1_2_1_38_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/827271.829093"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967021.1967025"}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2544350.2544352","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2544350.2544352","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:04Z","timestamp":1750278124000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2544350.2544352"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,10]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["10.1145\/2544350.2544352"],"URL":"https:\/\/doi.org\/10.1145\/2544350.2544352","relation":{},"ISSN":["1551-3688"],"issn-type":[{"type":"electronic","value":"1551-3688"}],"subject":[],"published":{"date-parts":[[2013,10]]},"assertion":[{"value":"2013-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}