{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T21:43:02Z","timestamp":1760132582988,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T00:00:00Z","timestamp":1586908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Oracle"},{"name":"Swiss National Science Foundation","award":["513954, 514009"],"award-info":[{"award-number":["513954, 514009"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,4,15]]},"DOI":"10.1145\/3342195.3387544","type":"proceedings-article","created":{"date-parts":[[2020,5,4]],"date-time":"2020-05-04T07:19:58Z","timestamp":1588576798000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Provable multicore schedulers with Ipanema"],"prefix":"10.1145","author":[{"given":"Baptiste","family":"Lepers","sequence":"first","affiliation":[{"name":"University of Sydney"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Redha","family":"Gouicem","sequence":"additional","affiliation":[{"name":"Sorbonne Universit\u00e9, Inria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damien","family":"Carver","sequence":"additional","affiliation":[{"name":"Sorbonne Universit\u00e9, Inria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Pierre","family":"Lozi","sequence":"additional","affiliation":[{"name":"Oracle Labs"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Palix","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria-Virginia","family":"Aponte","sequence":"additional","affiliation":[{"name":"CNAM"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willy","family":"Zwaenepoel","sequence":"additional","affiliation":[{"name":"University of Sydney"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Sopena","sequence":"additional","affiliation":[{"name":"Sorbonne Universit\u00e9"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julia","family":"Lawall","sequence":"additional","affiliation":[{"name":"Sorbonne Universit\u00e9"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilles","family":"Muller","sequence":"additional","affiliation":[{"name":"Sorbonne Universit\u00e9"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_7"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125925"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_1_5_1","first-page":"53","volume-title":"Poland","author":"Bobot F.","year":"2011","unstructured":"Bobot , F. , Filli\u00e2tre , J.-C. , March\u00e9 , C. , and Paskevich , A . Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages (Wroc\u0142aw , Poland , August 2011 ), pp. 53 -- 64 . https:\/\/hal.inria.fr\/hal-00790310. Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., and Paskevich, A. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages (Wroc\u0142aw, Poland, August 2011), pp. 53--64. https:\/\/hal.inria.fr\/hal-00790310."},{"key":"e_1_3_2_1_6_1","volume-title":"https:\/\/bugs.freebsd.org\/bugzilla\/showbug.cgi?id=223914","author":"Bouron J.","year":"2017","unstructured":"Bouron , J. [PATCH] Fix bug in which the long term ULE load balancer is executed only once. https:\/\/bugs.freebsd.org\/bugzilla\/showbug.cgi?id=223914 , 2017 . Bouron, J. [PATCH] Fix bug in which the long term ULE load balancer is executed only once. https:\/\/bugs.freebsd.org\/bugzilla\/showbug.cgi?id=223914, 2017."},{"key":"e_1_3_2_1_7_1","first-page":"85","volume-title":"Linux CFS. In USENIX Annual Technical Conference (USENIX ATC)","author":"Bouron J.","year":"2018","unstructured":"Bouron , J. , Chevalley , S. , Lepers , B. , Zwaenepoel , W. , Gouicem , R. , Lawall , J. , Muller , G. , and Sopena , J . The battle of the schedulers: FreeBSD ULE vs . Linux CFS. In USENIX Annual Technical Conference (USENIX ATC) ( 2018 ), pp. 85 -- 96 . Bouron, J., Chevalley, S., Lepers, B., Zwaenepoel, W., Gouicem, R., Lawall, J., Muller, G., and Sopena, J. The battle of the schedulers: FreeBSD ULE vs. Linux CFS. In USENIX Annual Technical Conference (USENIX ATC) (2018), pp. 85--96."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-0676-1"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365137.3365400"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2016.28"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_13_1","first-page":"93","volume-title":"Linux Symposium","volume":"1","author":"Chen T.","year":"2007","unstructured":"Chen , T. , Ananiev , L. I. , and Tikhonov , A. V . Keeping kernel performance from regressions . In Linux Symposium ( 2007 ), vol. 1 , pp. 93 -- 102 . Chen, T., Ananiev, L. I., and Tikhonov, A. V. Keeping kernel performance from regressions. In Linux Symposium (2007), vol. 1, pp. 93--102."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Chong N. and Ishtiaq S. Reasoning about the ARM weakly consistent memory model. In Workshop on Memory systems performance and correctness: held in conjunction with the Thirteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2008) ACM pp. 16--19.  Chong N. and Ishtiaq S. Reasoning about the ARM weakly consistent memory model. In Workshop on Memory systems performance and correctness: held in conjunction with the Thirteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2008) ACM pp. 16--19.","DOI":"10.1145\/1353522.1353528"},{"key":"e_1_3_2_1_15_1","volume-title":"SMT Workshop: International Workshop on Satisfiability Modulo Theories","author":"Conchon S.","year":"2018","unstructured":"Conchon , S. , Coquereau , A. , Iguernlala , M. , and Mebsout , A . Alt-Ergo 2.2 . In SMT Workshop: International Workshop on Satisfiability Modulo Theories ( Oxford, United Kingdom , July 2018 ). Conchon, S., Coquereau, A., Iguernlala, M., and Mebsout, A. Alt-Ergo 2.2. In SMT Workshop: International Workshop on Satisfiability Modulo Theories (Oxford, United Kingdom, July 2018)."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451157"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.30"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2823400"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945468"},{"key":"e_1_3_2_1_21_1","first-page":"151","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"Erickson J.","year":"2010","unstructured":"Erickson , J. , Musuvathi , M. , Burckhardt , S. , and Olynyk , K . Effective data-race detection for the kernel . In Operating Systems Design and Implementation (OSDI) ( 2010 ), pp. 151 -- 162 . Erickson, J., Musuvathi, M., Burckhardt, S., and Olynyk, K. Effective data-race detection for the kernel. In Operating Systems Design and Implementation (OSDI) (2010), pp. 151--162."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0243-x"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294291"},{"key":"e_1_3_2_1_24_1","first-page":"653","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"Gu R.","year":"2016","unstructured":"Gu , R. , Shao , Z. , Chen , H. , Wu , X. N. , Kim , J. , Sj\u00f6berg , V. , and Costanzo , D . CertiKOS: an extensible architecture for building certified concurrent OS kernels . In Operating Systems Design and Implementation (OSDI) ( 2016 ), pp. 653 -- 669 . Gu, R., Shao, Z., Chen, H., Wu, X. N., Kim, J., Sj\u00f6berg, V., and Costanzo, D. CertiKOS: an extensible architecture for building certified concurrent OS kernels. In Operating Systems Design and Implementation (OSDI) (2016), pp. 653--669."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_26_1","first-page":"165","volume-title":"Operating Systems Design and Implementation (OSDI)","volume":"14","author":"Hawblitzel C.","year":"2014","unstructured":"Hawblitzel , C. , Howell , J. , Lorch , J. R. , Narayan , A. , Parno , B. , Zhang , D. , and Zill , B . Ironclad apps: End-to-end security via automated full-system verification . In Operating Systems Design and Implementation (OSDI) ( 2014 ), vol. 14 , pp. 165 -- 181 . Hawblitzel, C., Howell, J., Lorch, J. R., Narayan, A., Parno, B., Zhang, D., and Zill, B. Ironclad apps: End-to-end security via automated full-system verification. In Operating Systems Design and Implementation (OSDI) (2014), vol. 14, pp. 165--181."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127479.3128608"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2749469.2750392"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_2"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102980.3102984"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_34_1","volume-title":"https:\/\/linux-test-project.github.io\/","author":"Linux","year":"2012","unstructured":"Linux test project. https:\/\/linux-test-project.github.io\/ , 2012 . Linux test project. https:\/\/linux-test-project.github.io\/, 2012."},{"key":"e_1_3_2_1_35_1","first-page":"423","volume-title":"Networked Systems Design and Implementation (NSDI)","author":"Liu X.","year":"2008","unstructured":"Liu , X. , Guo , Z. , Wang , X. , Chen , F. , Lian , X. , Tang , J. , Wu , M. , Kaashoek , M. F. , and Zhang , Z . D3S: debugging deployed distributed systems . In Networked Systems Design and Implementation (NSDI) ( 2008 ), pp. 423 -- 437 . Liu, X., Guo, Z., Wang, X., Chen, F., Lian, X., Tang, J., Wu, M., Kaashoek, M. F., and Zhang, Z. D3S: debugging deployed distributed systems. In Networked Systems Design and Implementation (NSDI) (2008), pp. 423--437."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2901318.2901326"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451148"},{"key":"e_1_3_2_1_38_1","first-page":"17","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"M\u00e9rillon F.","year":"2000","unstructured":"M\u00e9rillon , F. , R\u00e9veill\u00e8re , L. , Consel , C. , Marlet , R. , and Muller , G . Devil: An IDL for hardware programming . In Operating Systems Design and Implementation (OSDI) ( 2000 ), pp. 17 -- 30 . M\u00e9rillon, F., R\u00e9veill\u00e8re, L., Consel, C., Marlet, R., and Muller, G. Devil: An IDL for hardware programming. In Operating Systems Design and Implementation (OSDI) (2000), pp. 17--30."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/566726.566732"},{"key":"e_1_3_2_1_40_1","first-page":"56","volume-title":"High-Assurance Systems Engineering (HASE)","author":"Muller G.","year":"2005","unstructured":"Muller , G. , Lawall , J. L. , and Duchesne , H . A framework for simplifying the development of kernel schedulers: Design and performance evaluation . In High-Assurance Systems Engineering (HASE) ( 2005 ), IEEE , pp. 56 -- 65 . Muller, G., Lawall, J. L., and Duchesne, H. A framework for simplifying the development of kernel schedulers: Design and performance evaluation. In High-Assurance Systems Engineering (HASE) (2005), IEEE, pp. 56--65."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060289.1060297"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168630"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451131"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Savage S. Burrows M. Nelson G. Sobalvarro P. and Anderson T. Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems (TOCS) 15 4 (Nov. 1997) 391--411.  Savage S. Burrows M. Nelson G. Sobalvarro P. and Anderson T. Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems (TOCS) 15 4 (Nov. 1997) 391--411.","DOI":"10.1145\/265924.265927"},{"key":"e_1_3_2_1_46_1","unstructured":"Scheduler domains. https:\/\/www.kernel.org\/doc\/html\/latest\/scheduler\/sched-domains.html.  Scheduler domains. https:\/\/www.kernel.org\/doc\/html\/latest\/scheduler\/sched-domains.html."},{"key":"e_1_3_2_1_47_1","volume-title":"Workshop on Managed Many-Core Systems","volume":"27","author":"Sch\u00fcpbach A.","year":"2008","unstructured":"Sch\u00fcpbach , A. , Peter , S. , Baumann , A. , Roscoe , T. , Barham , P. , Harris , T. , and Isaacs , R . Embracing diversity in the Barrelfish manycore operating system . In Workshop on Managed Many-Core Systems ( 2008 ), vol. 27 . Sch\u00fcpbach, A., Peter, S., Baumann, A., Roscoe, T., Barham, P., Harris, T., and Isaacs, R. Embracing diversity in the Barrelfish manycore operating system. In Workshop on Managed Many-Core Systems (2008), vol. 27."},{"key":"e_1_3_2_1_48_1","first-page":"309","volume-title":"File and Storage Technologies (FAST)","author":"Shen K.","year":"2005","unstructured":"Shen , K. , Zhong , M. , and Li , C . I\/O system performance debugging using model-driven anomaly characterization . In File and Storage Technologies (FAST) ( 2005 ), pp. 309 -- 322 . Shen, K., Zhong, M., and Li, C. I\/O system performance debugging using model-driven anomaly characterization. In File and Storage Technologies (FAST) (2005), pp. 309--322."},{"key":"e_1_3_2_1_49_1","first-page":"1","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson H.","year":"2016","unstructured":"Sigurbjarnarson , H. , Bornholt , J. , Torlak , E. , and Wang , X . Push-button verification of file systems via crash refinement . In Operating Systems Design and Implementation (OSDI) ( 2016 ), pp. 1 -- 16 . Sigurbjarnarson, H., Bornholt, J., Torlak, E., and Wang, X. Push-button verification of file systems via crash refinement. In Operating Systems Design and Implementation (OSDI) (2016), pp. 1--16."},{"key":"e_1_3_2_1_50_1","volume-title":"Data center computers: Modern challenges in CPU design","author":"Sites D.","year":"2015","unstructured":"Sites , D. Data center computers: Modern challenges in CPU design , 2015 . https:\/\/www.youtube.com\/watch?v=QBu2Ae8-8LM(56:32). Sites, D. Data center computers: Modern challenges in CPU design, 2015. https:\/\/www.youtube.com\/watch?v=QBu2Ae8-8LM(56:32)."},{"key":"e_1_3_2_1_51_1","unstructured":"Sysbench. https:\/\/github.com\/akopytov\/sysbench.  Sysbench. https:\/\/github.com\/akopytov\/sysbench."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970337"},{"key":"e_1_3_2_1_53_1","first-page":"1","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"Waldspurger C. A.","year":"1994","unstructured":"Waldspurger , C. A. , and Weihl , W. E . Lottery scheduling: Flexible proportional-share resource management . In Operating Systems Design and Implementation (OSDI) ( 1994 ), pp. 1 -- 11 . Waldspurger, C. A., and Weihl, W. E. Lottery scheduling: Flexible proportional-share resource management. In Operating Systems Design and Implementation (OSDI) (1994), pp. 1--11."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/800087.802786"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_56_1","volume-title":"Load balancing in parallel computers: theory and practice","author":"Xu C.","year":"1996","unstructured":"Xu , C. , and Lau , F. C. M . Load balancing in parallel computers: theory and practice , vol. 381 . Springer Science & Business Media , 1996 . Xu, C., and Lau, F. C. M. Load balancing in parallel computers: theory and practice, vol. 381. Springer Science & Business Media, 1996."},{"key":"e_1_3_2_1_57_1","volume-title":"Using model checking to find serious file system errors. ACM Transactions on Computer Systems (TOCS) 24, 4 (Nov","author":"Yang J.","year":"2006","unstructured":"Yang , J. , Twohey , P. , Engler , D. , and Musuvathi , M . Using model checking to find serious file system errors. ACM Transactions on Computer Systems (TOCS) 24, 4 (Nov . 2006 ), 393--423. Yang, J., Twohey, P., Engler, D., and Musuvathi, M. Using model checking to find serious file system errors. ACM Transactions on Computer Systems (TOCS) 24, 4 (Nov. 2006), 393--423."}],"event":{"name":"EuroSys '20: Fifteenth EuroSys Conference 2020","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Heraklion Greece","acronym":"EuroSys '20"},"container-title":["Proceedings of the Fifteenth European Conference on Computer Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3342195.3387544","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3342195.3387544","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:33:22Z","timestamp":1750199602000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3342195.3387544"}},"subtitle":["application to work conservation"],"short-title":[],"issued":{"date-parts":[[2020,4,15]]},"references-count":57,"alternative-id":["10.1145\/3342195.3387544","10.1145\/3342195"],"URL":"https:\/\/doi.org\/10.1145\/3342195.3387544","relation":{},"subject":[],"published":{"date-parts":[[2020,4,15]]},"assertion":[{"value":"2020-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}