{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:43Z","timestamp":1750221283445,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,28]],"date-time":"2017-10-28T00:00:00Z","timestamp":1509148800000},"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":[],"published-print":{"date-parts":[[2017,10,28]]},"DOI":"10.1145\/3144555.3144557","type":"proceedings-article","created":{"date-parts":[[2017,10,31]],"date-time":"2017-10-31T12:31:37Z","timestamp":1509453097000},"page":"8-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Correct-by-Construction Interrupt Routing on Real Hardware"],"prefix":"10.1145","author":[{"given":"Lukas","family":"Humbel","sequence":"first","affiliation":[{"name":"Systems Group, Dept. of Computer Science, ETH Zurich"}]},{"given":"Reto","family":"Achermann","sequence":"additional","affiliation":[{"name":"Systems Group, Dept. of Computer Science, ETH Zurich"}]},{"given":"David","family":"Cock","sequence":"additional","affiliation":[{"name":"Systems Group, Dept. of Computer Science, ETH Zurich"}]},{"given":"Timothy","family":"Roscoe","sequence":"additional","affiliation":[{"name":"Systems Group, Dept. of Computer Science, ETH Zurich"}]}],"member":"320","published-online":{"date-parts":[[2017,10,28]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.244.4"},{"key":"e_1_3_2_1_2_1","unstructured":"ARM Ltd. 2011. CoreLink GIC-400 Generic Interrupt Controller - Technical Reference Manual (revision r0p0 ed.). ARM."},{"key":"e_1_3_2_1_3_1","unstructured":"ARM Ltd. 2016. ARM Generic Interrupt Controller - Architecture version 2.0 (issue b ed.). ARM."},{"key":"e_1_3_2_1_4_1","unstructured":"ARM Ltd. 2016. ARM Generic Interrupt Controller Architecture Specification - GIC architecture version 3.0 and version 4.0 (issue c ed.). ARM."},{"key":"e_1_3_2_1_5_1","volume-title":"The Barrelfish Research Operating System. (August","author":"Barrelfish","year":"2017","unstructured":"Barrelfish team. 2017. The Barrelfish Research Operating System. (August 2017). www.barrelfish.org."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629579"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"volume-title":"Linaro","author":"Devicetree Specification","key":"e_1_3_2_1_8_1","unstructured":"Devicetree.org. 2016. Devicetree Specification (release 0.1 ed.). Linaro, Ltd. http:\/\/www.devicetree.org\/specifications-pdf."},{"key":"e_1_3_2_1_9_1","first-page":"231468","article-title":"8259A - Programmable Interrupt Controller. Intel Corporation","author":"Intel Corporation","year":"1988","unstructured":"Intel Corporation. 1988. 8259A - Programmable Interrupt Controller. Intel Corporation. Order Number: 231468-003.","journal-title":"Order Number"},{"key":"e_1_3_2_1_10_1","first-page":"290566","article-title":"82093AA I\/O Advanced Programmable Interrupt Controller (IOAPIC). Intel Corporation","author":"Intel Corporation","year":"1996","unstructured":"Intel Corporation. 1996. 82093AA I\/O Advanced Programmable Interrupt Controller (IOAPIC). Intel Corporation. Order Number: 290566-001.","journal-title":"Order Number"},{"key":"e_1_3_2_1_11_1","unstructured":"Intel Corporation. 1997. MultiProcessor Specification (revision 006 ed.). Intel Corporation."},{"key":"e_1_3_2_1_12_1","volume-title":"Intel 64 Architecture x2APIC Specification","author":"Intel Corporation","year":"1814","unstructured":"Intel Corporation. 2014. Intel 64 Architecture x2APIC Specification. Intel Corporation. Reference Number: 318148-004."},{"volume-title":"Intel 64 and IA-32 Architectures Software Developer's Manual (volume 3, systems programming guide ed.)","author":"Intel Corporation","key":"e_1_3_2_1_13_1","unstructured":"Intel Corporation. 2016. Intel 64 and IA-32 Architectures Software Developer's Manual (volume 3, systems programming guide ed.). Intel Corporation."},{"volume-title":"Intel Virtualization Technology for Directed I\/O - Architecture Specification (revision 2.4 ed.)","author":"Intel Corporation","key":"e_1_3_2_1_14_1","unstructured":"Intel Corporation. 2016. Intel Virtualization Technology for Directed I\/O - Architecture Specification (revision 2.4 ed.). Intel Corporation."},{"volume-title":"irq_domain interrupt number mapping library","author":"Likely Grant","key":"e_1_3_2_1_15_1","unstructured":"Grant Likely, Linus Walleij, Jiang Liu, Jianyu Zhan, Marc Zyngier, Kevin Cernekee, Xishi Qiu, and Mark Brown. 2016. irq_domain interrupt number mapping library. The Linux Foundation. https:\/\/www.kernel.org\/doc\/Documentation\/IRQ-domain.txt."},{"key":"e_1_3_2_1_16_1","unstructured":"Larry Paulson Tobias Nipkow and Makarius Wenzel. 2017. Isabelle \/ HOL Proof Assistant. (August 2017). http:\/\/isabelle.in.tum.de."},{"volume-title":"PCI Local Bus Specification Revision 3.0 (revision 2.3 ed.)","author":"PCI Special Interest Group","key":"e_1_3_2_1_17_1","unstructured":"PCI Special Interest Group. 2004. PCI Local Bus Specification Revision 3.0 (revision 2.3 ed.). PCI Special Interest Group."},{"key":"e_1_3_2_1_18_1","unstructured":"Thierry Reding Rob Herring Grant Likely and Bjorn Helgaas. 2014. Specifying interrupt information for devices. Kernel.org. https:\/\/www.kernel.org\/doc\/Documentation\/devicetree\/bindings\/interrupt-controller\/interrupts.txt."},{"key":"e_1_3_2_1_19_1","unstructured":"Mark Rutland. 2013. Device Tree - The Disaster So Far. Online. (2013). ELC Europe. http:\/\/elinux.org\/images\/8\/8e\/Rutland-presentation_3.pdf."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950382"},{"volume-title":"Hardware Configuration with Dynamically-Queried Formal Models. Master's thesis","author":"Schwyn Daniel","key":"e_1_3_2_1_21_1","unstructured":"Daniel Schwyn. 2017. Hardware Configuration with Dynamically-Queried Formal Models. Master's thesis. Systems Group, ETH Zurich."},{"key":"e_1_3_2_1_22_1","unstructured":"Timothy Roscoe. 2013. Barrelfish Technical Note 2 -Mackerel User Guide (version 1.5 ed.). Barrelfish Project."},{"key":"e_1_3_2_1_23_1","unstructured":"UEFI Forum. 2017. Advanced Configuration and Power Interface Specification (version 6.2 ed.). UEFI Forum."}],"event":{"name":"SOSP '17: ACM SIGOPS 26th Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX Assoc USENIX Assoc"],"location":"Shanghai China","acronym":"SOSP '17"},"container-title":["Proceedings of the 9th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3144555.3144557","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3144555.3144557","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:22Z","timestamp":1750212682000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3144555.3144557"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,28]]},"references-count":23,"alternative-id":["10.1145\/3144555.3144557","10.1145\/3144555"],"URL":"https:\/\/doi.org\/10.1145\/3144555.3144557","relation":{},"subject":[],"published":{"date-parts":[[2017,10,28]]},"assertion":[{"value":"2017-10-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}