{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:36Z","timestamp":1779836736033,"version":"3.53.1"},"reference-count":40,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2013,10,29]],"date-time":"2013-10-29T00:00:00Z","timestamp":1383004800000},"content-version":"unspecified","delay-in-days":120,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as those of Linux, FreeBSD or Mac OS X, where the scheduler and processes interact in complex ways. We propose the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components. The logic hides the manipulation of control by the scheduler when reasoning about preemptable code and soundly inherits proof rules from concurrent separation logic to verify it thread-modularly. We illustrate the power of our logic by verifying an example scheduler, which includes some of the key features of the scheduler from Linux 2.6.11 challenging for verification.<\/jats:p>","DOI":"10.1017\/s0956796813000075","type":"journal-article","created":{"date-parts":[[2013,10,29]],"date-time":"2013-10-29T10:36:59Z","timestamp":1383043019000},"page":"452-514","source":"Crossref","is-referenced-by-count":6,"title":["Modular verification of preemptive OS kernels"],"prefix":"10.1017","volume":"23","author":[{"given":"ALEXEY","family":"GOTSMAN","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"HONGSEOK","family":"YANG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2013,10,29]]},"reference":[{"key":"S0956796813000075_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_8"},{"key":"S0956796813000075_ref11","first-page":"173","volume-title":"European Conference on Programming (ESOP'07)","author":"Feng","year":"2007"},{"key":"S0956796813000075_ref7","first-page":"53","volume-title":"European Conference on Object-Oriented Programming (ECOOP'01)","author":"Clarke","year":"2001"},{"key":"S0956796813000075_ref26","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Symposium on Operating Systems Principles (SOSP'09)","author":"Klein","year":"2009"},{"key":"S0956796813000075_ref15","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1145\/1133981.1134028","volume-title":"Conference on Programming Language Design and Implementation (PLDI'06)","author":"Feng","year":"2006"},{"key":"S0956796813000075_ref18","first-page":"171","article-title":"Precision and the conjunction rule in concurrent separation logic","volume":"276","author":"Gotsman","year":"2011","journal-title":"ENTCS"},{"key":"S0956796813000075_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90005-2"},{"key":"S0956796813000075_ref12","first-page":"67","volume-title":"Workshop on Types in Language Design and Implementation (TLDI'07)","author":"Feng","year":"2007"},{"key":"S0956796813000075_ref3","volume-title":"Understanding the Linux Kernel","author":"Bovet","year":"2005"},{"key":"S0956796813000075_ref2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020891112409"},{"key":"S0956796813000075_ref32","first-page":"247","volume-title":"Symposium on Principles of Programming Languages (POPL'05)","author":"Parkinson","year":"2005"},{"key":"S0956796813000075_ref5","first-page":"366","volume-title":"Symposium on Logic in Computer Science (LICS'07)","author":"Calcagno","year":"2007"},{"key":"S0956796813000075_ref13","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1145\/1375581.1375603","volume-title":"Conference on Programming Language Design and Implementation (PLDI'08)","author":"Feng","year":"2008"},{"key":"S0956796813000075_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0002-4"},{"key":"S0956796813000075_ref10","first-page":"504","volume-title":"European Conference on Object-Oriented Programming (ECOOP'10)","author":"Dinsdale-Young","year":"2010"},{"key":"S0956796813000075_ref17","unstructured":"Gotsman A. (2009) Logics and Analyses for Concurrent Heap-Manipulating Programs. PhD Thesis, University of Cambridge."},{"key":"S0956796813000075_ref16","first-page":"1","volume-title":"Conference on Theorem Proving in Higher-Order Logics (TPHOLs'05)","author":"Gargano","year":"2005"},{"key":"S0956796813000075_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"S0956796813000075_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20920-8_10"},{"key":"S0956796813000075_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000075"},{"key":"S0956796813000075_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24754-8_17"},{"key":"S0956796813000075_ref24","unstructured":"Jones C. B. (1983) Specification and design of (parallel) programs. In IFIP Congress, pp. 321\u2013332."},{"key":"S0956796813000075_ref28","volume-title":"Linux Kernel Development","author":"Love","year":"2010"},{"key":"S0956796813000075_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.022"},{"key":"S0956796813000075_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02002-5_10"},{"key":"S0956796813000075_ref30","first-page":"320","volume-title":"Symposium on Principles of Programming Languages (POPL'06)","author":"Ni","year":"2006"},{"key":"S0956796813000075_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"S0956796813000075_ref34","first-page":"55","volume-title":"Symposium on Logic in Computer Science (LICS'02)","author":"Reynolds","year":"2002"},{"key":"S0956796813000075_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45788-7_10"},{"key":"S0956796813000075_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_32"},{"key":"S0956796813000075_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/1859204.1859226"},{"key":"S0956796813000075_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"S0956796813000075_ref37","first-page":"139","volume-title":"Symposium on Principles of Programming Languages (POPL'03)","author":"Thielecke","year":"2003"},{"key":"S0956796813000075_ref38","first-page":"247","volume-title":"Symposium on Principles of Programming Languages (POPL'11)","author":"Turon","year":"2011"},{"key":"S0956796813000075_ref40","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1145\/1806596.1806610","volume-title":"Conference on Programming Language Design and Implementation (PLDI'10)","author":"Yang","year":"2010"},{"key":"S0956796813000075_ref39","first-page":"256","volume-title":"Conference on Concurrency Theory (CONCUR'07)","author":"Vafeiadis","year":"2007"},{"key":"S0956796813000075_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_42"},{"key":"S0956796813000075_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"S0956796813000075_ref9","first-page":"287","volume-title":"Symposium on Principles of Programming Languages (POPL'13)","author":"Dinsdale-Young","year":"2013"},{"key":"S0956796813000075_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.029"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796813000075","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:05Z","timestamp":1779834965000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796813000075\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["S0956796813000075"],"URL":"https:\/\/doi.org\/10.1017\/s0956796813000075","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}