{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T20:45:11Z","timestamp":1760647511073,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T00:00:00Z","timestamp":1635120000000},"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":[[2021,10,25]]},"DOI":"10.1145\/3477113.3487270","type":"proceedings-article","created":{"date-parts":[[2021,10,11]],"date-time":"2021-10-11T10:25:01Z","timestamp":1633947901000},"page":"69-75","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Generating correct initial page tables from formal hardware descriptions"],"prefix":"10.1145","author":[{"given":"Reto","family":"Achermann","sequence":"first","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Cock","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roni","family":"Haecki","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nora","family":"Hossle","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lukas","family":"Humbel","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Timothy","family":"Roscoe","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Schwyn","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,10,25]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_2_1_1","DOI":"10.1145\/3458336.3465273"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_2_1","DOI":"10.4204\/eptcs.244.4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_3_1","DOI":"10.1007\/978-3-319-94821-8_1"},{"unstructured":"ARM Ltd. 2019. Development Tools and Software: Fast Models. https:\/\/www.arm.com\/products\/development-tools\/simulation\/fast-models","key":"e_1_3_2_2_4_1"},{"unstructured":"ARM Ltd. 2021. Arm TrustZone Technology. https:\/\/developer.arm.com\/ip-products\/security-ip\/trustzone.","key":"e_1_3_2_2_5_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_6_1","DOI":"10.1145\/1629575.1629579"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_7_1","DOI":"10.5555\/2831090.2831106"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_8_1","DOI":"10.1145\/3365137.3365401"},{"unstructured":"Intel Corporation. 2014. Intel Xeon Phi Coprocessor System Software Developers Guide.","key":"e_1_3_2_2_9_1"},{"key":"e_1_3_2_2_10_1","volume-title":"Device Tree Source Format (version 1). Linux. Retrieved","author":"Documentation Linux Kernel","year":"2021","unstructured":"Linux Kernel Documentation. 2019. Device Tree Source Format (version 1). Linux. Retrieved 06 August 2021 from https:\/\/git.kernel.org\/pub\/scm\/utils\/dtc\/dtc.git\/plain\/Documentation\/dts-format.txt"},{"unstructured":"Arm Ltd. 2021. ATF - Translation (XLAT) Tables Library. https:\/\/trustedfirmware-a.readthedocs.io\/en\/latest\/components\/xlat-tables-lib-v2-design.html","key":"e_1_3_2_2_11_1"},{"unstructured":"Red Hat Bugzilla 2010. Bug 654665 - EFI\/UEFI page table initialization is incorrect for x86_64 in physical mode. Red Hat Bugzilla. https:\/\/bugzilla.redhat.com\/show_bug.cgi?id=654665","key":"e_1_3_2_2_12_1"},{"unstructured":"sunxi 2012. Unable to pass memory configuration from u-boot to kernel. sunxi. https:\/\/github.com\/linux-sunxi\/u-boot-sunxi\/issues\/11","key":"e_1_3_2_2_13_1"},{"unstructured":"Kernel.org Bugzilla 2013. Bug 56461 - Memory corruption on PAE x86 systems. Kernel.org Bugzilla. https:\/\/bugzilla.kernel.org\/show_bug.cgi?id=56461","key":"e_1_3_2_2_14_1"},{"unstructured":"Linux Kernel Mailing List 2017. efi\/x86: Prune invalid memory map entries and fix boot regression. Linux Kernel Mailing List. https:\/\/lore.kernel.org\/patchwork\/patch\/752197\/","key":"e_1_3_2_2_15_1"},{"unstructured":"launchpad 2019. Full RAM on Pi4 isn't accessible when using u-boot. launchpad. https:\/\/bugs.launchpad.net\/ubuntu\/+source\/u-boot\/+bug\/1847500","key":"e_1_3_2_2_16_1"},{"unstructured":"UEFI Forum Inc. 2021. Advanced Configuration and Power Interface (ACPI) Specification. UEFI Forum Inc. https:\/\/uefi.org\/htmlspecs\/ACPI_Spec_6_4_html\/","key":"e_1_3_2_2_17_1"},{"volume-title":"Arm Trusted Firmware","author":"Ltd Arm","unstructured":"Arm Ltd. 2021. Arm Trusted Firmware. Arm Ltd. https:\/\/github.com\/ARM-software\/arm-trusted-firmware","key":"e_1_3_2_2_18_1"},{"unstructured":"Linux 2021. Linux x86 boot code. Linux. https:\/\/github.com\/torvalds\/linux\/blob\/master\/arch\/x86\/boot\/compressed\/head_64.S","key":"e_1_3_2_2_19_1"},{"unstructured":"UEFI Forum Inc. 2021. Unified Extensible Firmware Interface (UEFI) Specification. UEFI Forum Inc. https:\/\/uefi.org\/sites\/default\/files\/resources\/UEFI_Spec_2_9_2021_03_18.pdf","key":"e_1_3_2_2_20_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_21_1","DOI":"10.1145\/1629575.1629583"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_22_1","DOI":"10.1145\/1950365.1950382"},{"doi-asserted-by":"publisher","unstructured":"Daniel Schwyn. 2017. Hardware Configuration With Dynamically-Queried Formal Models. Master's Thesis. Department of Computer Science ETH Zurich Switzerland. https:\/\/doi.org\/10.3929\/ethz-b-000203075","key":"e_1_3_2_2_23_1","DOI":"10.3929\/ethz-b-000203075"},{"unstructured":"Sockeye Project. 2021. Sockeye Compiler Code Repository. https:\/\/github.com\/Sockeye-Project\/sockeye-compiler","key":"e_1_3_2_2_24_1"},{"unstructured":"Ulf Frisk. 2018. Total Meltdown? http:\/\/blog.frizk.net\/2018\/03\/total-meltdown.html","key":"e_1_3_2_2_25_1"}],"event":{"sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"acronym":"SOSP '21","name":"SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles","location":"Virtual Event Germany"},"container-title":["Proceedings of the 11th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477113.3487270","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3477113.3487270","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:14Z","timestamp":1750193354000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477113.3487270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,25]]},"references-count":25,"alternative-id":["10.1145\/3477113.3487270","10.1145\/3477113"],"URL":"https:\/\/doi.org\/10.1145\/3477113.3487270","relation":{},"subject":[],"published":{"date-parts":[[2021,10,25]]},"assertion":[{"value":"2021-10-25","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}