{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T15:13:24Z","timestamp":1765466004388,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,3,22]]},"DOI":"10.1145\/3760250.3762233","type":"proceedings-article","created":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T15:06:36Z","timestamp":1765465596000},"page":"234-248","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Sequential Specifications for Precise Hardware Exceptions"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6549-3817","authenticated-orcid":false,"given":"Yulun","family":"Yao","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6847-6599","authenticated-orcid":false,"given":"Drew","family":"Zagieboylo","sequence":"additional","affiliation":[{"name":"NVIDIA, Westford, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5819-7588","authenticated-orcid":false,"given":"Andrew C.","family":"Myers","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6409-9888","authenticated-orcid":false,"given":"G. Edward","family":"Suh","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA and NVIDIA, Westford, MA, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,12,11]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"1","volume-title":"Proc. ACM on Programming Languages","volume":"3","author":"Armstrong Alasdair","year":"2019","unstructured":"Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, et al., 2019. ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Proc. ACM on Programming Languages, Vol. 3, POPL (2019), 1-31."},{"key":"e_1_3_2_1_2_1","first-page":"15","volume-title":"Hannover","author":"A\u015filio\u011flu G\u00f6rkem","year":"2010","unstructured":"G\u00f6rkem A\u015filio\u011flu, Emine Merve Kaya, and O\u011fuz Ergin. 2010. Complexity-effective rename table design for rapid speculation recovery. In Architecture of Computing Systems-ARCS 2010: 23rd Int'l Conf., Hannover, Germany, February 22-25, 2010. Proceedings 23. Springer, 15-24."},{"key":"e_1_3_2_1_3_1","volume-title":"CV32RT: Enabling fast interrupt and context switching for RISC-V microcontrollers","author":"Balas Robert","year":"2024","unstructured":"Robert Balas, Alessandro Ottaviano, and Luca Benini. 2024. CV32RT: Enabling fast interrupt and context switching for RISC-V microcontrollers. IEEE Transactions on Very Large Scale Integration (VLSI) Systems (2024)."},{"key":"e_1_3_2_1_4_1","unstructured":"Drew Barbier and A. C. Palmer Dabbelt. 2020. RISC-V platform-level interrupt controller specification."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2010.05.011"},{"key":"e_1_3_2_1_6_1","volume-title":"Proc. 49th Annual Design Automation Conf., 1226-1232","author":"Chan Carven","year":"2012","unstructured":"Carven Chan, Daniel Schwartz-Narbonne, Divjyot Sethi, and Sharad Malik. 2012. Specification and synthesis of hardware checkpointing and rollback mechanisms. In Proc. 49th Annual Design Automation Conf., 1226-1232."},{"key":"e_1_3_2_1_7_1","first-page":"1","volume-title":"Proc. ACM on Programming Languages","volume":"1","author":"Choi Joonwon","year":"2017","unstructured":"Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: A platform for high-level parametric hardware specification and its modular verification. Proc. ACM on Programming Languages, Vol. 1, ICFP (2017), 1-30."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2011.2110592"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3012866"},{"key":"e_1_3_2_1_11_1","first-page":"24","article-title":"Vivado design suite","volume":"5","author":"Feist Tom","year":"2012","unstructured":"Tom Feist. 2012. Vivado design suite. White Paper, Vol. 5, 30 (2012), 24.","journal-title":"White Paper"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579371.3589087"},{"key":"e_1_3_2_1_13_1","volume-title":"Proc. 14th annual international symposium on Computer architecture. 18-26","author":"W.","unstructured":"Wen-mei W. Hwu and Yale N. Patt. 1987. Checkpoint repair for out-of-order execution machines. In Proc. 14th annual international symposium on Computer architecture. 18-26."},{"key":"e_1_3_2_1_14_1","unstructured":"Cadence Design Systems Inc. 2020a. Innovus implementation system. (2020)."},{"key":"e_1_3_2_1_15_1","unstructured":"Synopsys Inc. 2020b. Design compiler RTL synthesis solution. (2020)."},{"key":"e_1_3_2_1_16_1","volume-title":"SiFive interrupt cookbook. version","author":"SiFive Inc.","year":"2020","unstructured":"SiFive Inc., 2020c. SiFive interrupt cookbook. version, Vol. 1.2 (2020)."},{"key":"e_1_3_2_1_17_1","volume-title":"Intel\u00ae 64 and IA-32 architectures software developer's manual","author":"Intel Corporation","year":"2011","unstructured":"Intel Corporation. 2011. Intel\u00ae 64 and IA-32 architectures software developer's manual. Volume 3B: system programming guide, part, Vol. 2, 11 (2011), 0-40."},{"key":"e_1_3_2_1_18_1","first-page":"28","volume-title":"Proc. ACM on Programming Languages","volume":"8","author":"Jang Minseong","year":"2024","unstructured":"Minseong Jang, Jungin Rhee, Woojin Lee, Shuangshuang Zhao, and Jeehoon Kang. 2024. Modular hardware design of pipelined circuits with hazards. Proc. ACM on Programming Languages, Vol. 8, PLDI (2024), 28-51."},{"key":"e_1_3_2_1_19_1","volume-title":"Proc. 2019 ACM\/SIGDA Int'l Symp. on Field-Programmable Gate Arrays. 242-251","author":"Lai Yi-Hsiang","year":"2019","unstructured":"Yi-Hsiang Lai, Yuze Chi, Yuwei Hu, Jie Wang, Cody Hao Yu, Yuan Zhou, Jason Cong, and Zhiru Zhang. 2019. HeteroCL: A multi-paradigm programming infrastructure for software-defined reconfigurable computing. In Proc. 2019 ACM\/SIGDA Int'l Symp. on Field-Programmable Gate Arrays. 242-251."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_21_1","first-page":"179","article-title":"Time, clocks, and the ordering of events in a distributed system","author":"Lamport Leslie","year":"2019","unstructured":"Leslie Lamport. 2019. Time, clocks, and the ordering of events in a distributed system. In Concurrency: The Works of Leslie Lamport. 179-196.","journal-title":"Concurrency: The Works of Leslie Lamport."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357033"},{"key":"e_1_3_2_1_23_1","unstructured":"Biruk Wendimagegn Mammo. 2017. Reining in the functional verification of complex processor designs with automation prioritization and approximation. Ph.D. Dissertation."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2024.3352114"},{"key":"e_1_3_2_1_25_1","unstructured":"Prabhat Mishra Nikil Dutt and Alex Nicolau. 2001. Specification of hazards stalls interrupts and exceptions in EXPRESSION. (2001)."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.482313"},{"key":"e_1_3_2_1_27_1","first-page":"1","article-title":"A SLOC counting standard. In Cocomo ii forum, Vol. 2007","author":"Nguyen Vu","year":"2007","unstructured":"Vu Nguyen, Sophia Deeds-Rubin, Thomas Tan, and Barry Boehm. 2007. A SLOC counting standard. In Cocomo ii forum, Vol. 2007. Citeseer, 1-16.","journal-title":"Citeseer"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings. Second ACM and IEEE Int'l Conf. on Formal Methods and Models for Co-Design, 2004. MEMOCODE'04., IEEE, 69-70","author":"Nikhil Rishiyur","year":"2004","unstructured":"Rishiyur Nikhil. 2004. Bluespec System Verilog: Efficient, correct RTL from high level specifications. In Proceedings. Second ACM and IEEE Int'l Conf. on Formal Methods and Models for Co-Design, 2004. MEMOCODE'04., IEEE, 69-70."},{"key":"e_1_3_2_1_29_1","volume-title":"Programming in Scala","author":"Odersky Martin","unstructured":"Martin Odersky, Lex Spoon, and Bill Venners. 2008. Programming in Scala. Artima Inc."},{"key":"e_1_3_2_1_30_1","volume-title":"Proc. 14th Int'l Symp. on Systems Synthesis. 75-80","author":"Panda Preeti Ranjan","year":"2001","unstructured":"Preeti Ranjan Panda. 2001. SystemC: A modeling platform supporting multiple design abstractions. In Proc. 14th Int'l Symp. on Systems Synthesis. 75-80."},{"key":"e_1_3_2_1_31_1","first-page":"1066","volume-title":"Proc. ACM on Programming Languages","volume":"8","author":"Pelton Blake","year":"2024","unstructured":"Blake Pelton, Adam Sapek, Ken Eguro, Daniel Lo, Alessandro Forin, Matt Humphrey, Jinwen Xi, David Cox, Rajas Karandikar, Johannes de Fine Licht, et al., 2024. Wavefront threading enables effective high-level synthesis. Proc. ACM on Programming Languages, Vol. 8, PLDI (2024), 1066-1090."},{"key":"e_1_3_2_1_32_1","volume-title":"Kintex-7, and Artix-7 devices. Xilinx White Paper","author":"Przybus Brent","year":"2010","unstructured":"Brent Przybus. 2010. Xilinx redefines power, performance, and design productivity with three new 28 nm FPGA families: Virtex-7, Kintex-7, and Artix-7 devices. Xilinx White Paper (2010)."},{"key":"e_1_3_2_1_33_1","first-page":"110","article-title":"Machsuite: Benchmarks for accelerator design and customized architectures. In 2014 IEEE Int'l Symp. on Workload Characterization (IISWC)","author":"Reagen Brandon","year":"2014","unstructured":"Brandon Reagen, Robert Adolf, Yakun Sophia Shao, Gu-Yeon Wei, and David Brooks. 2014. Machsuite: Benchmarks for accelerator design and customized architectures. In 2014 IEEE Int'l Symp. on Workload Characterization (IISWC). IEEE, 110-119.","journal-title":"IEEE"},{"key":"e_1_3_2_1_34_1","unstructured":"David Seal. 2001. ARM architecture reference manual. Pearson Education."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.877952"},{"key":"e_1_3_2_1_36_1","unstructured":"Ben Simner Alasdair Armstrong Thomas Bauereiss Brian Campbell Ohad Kammar Jean Pichon-Pharabod et al. 2024. Relaxed exception semantics for Arm-A (extended version). arXiv preprint arXiv:2412.15140 (2024)."},{"key":"e_1_3_2_1_37_1","volume-title":"Proc. 46th Int'l Symp. on Computer Architecture. 318-331","author":"Skarlatos Dimitrios","unstructured":"Dimitrios Skarlatos, Mengjia Yan, Bhargava Gopireddy, Read Sprabery, Josep Torrellas, and Christopher W. Fletcher. 2019. Microscope: Enabling microarchitectural replay attacks. In Proc. 46th Int'l Symp. on Computer Architecture. 318-331."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/327070.327125"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSE.2007.44"},{"key":"e_1_3_2_1_40_1","volume-title":"Proc. 30th Asia and South Pacific Design Automation Conf., 1104-1111","author":"Teng Paul","year":"2025","unstructured":"Paul Teng and Christophe Dubach. 2025. Hardware synthesizable exceptions using continuations. In Proc. 30th Asia and South Pacific Design Automation Conf., 1104-1111."},{"key":"e_1_3_2_1_41_1","volume-title":"The Verilog\u00ae hardware description language","author":"Thomas Donald","unstructured":"Donald Thomas and Philip Moorby. 2008. The Verilog\u00ae hardware description language. Springer Science & Business Media."},{"key":"e_1_3_2_1_42_1","volume-title":"An efficient algorithm for exploiting multiple arithmetic units. IBM Journal of research and Development","author":"Tomasulo Robert M.","year":"1967","unstructured":"Robert M. Tomasulo. 1967. An efficient algorithm for exploiting multiple arithmetic units. IBM Journal of research and Development, Vol. 11, 1 (1967), 25-33."},{"key":"e_1_3_2_1_43_1","unstructured":"Zynq UltraScale. 2020. Device technical reference manual. (2020)."},{"key":"e_1_3_2_1_44_1","volume-title":"User-level ISA, version 2.0. EECS Department","author":"Waterman Andrew","year":"2014","unstructured":"Andrew Waterman, Yunsup Lee, David A. Patterson, and Krste Asanovic. 2014. The RISC-V instruction set manual, volume I: User-level ISA, version 2.0. EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS-2014-54 (2014), 4."},{"key":"e_1_3_2_1_45_1","first-page":"3","article-title":"Icarus Verilog: Open-source Verilog more than a year later","volume":"99","author":"Williams Stephen","year":"2002","unstructured":"Stephen Williams and Michael Baxter. 2002. Icarus Verilog: Open-source Verilog more than a year later. Linux Journal, 99 (2002), 3.","journal-title":"Linux Journal"},{"key":"e_1_3_2_1_46_1","volume-title":"Proc. 31st ACM SIGPLAN Conf. on Programming Language Design and Implementation. 99-110","author":"Yang Jean","year":"2010","unstructured":"Jean Yang and Chris Hawblitzel. 2010. Safe to the last instruction: Automated verification of a type-safe operating system. In Proc. 31st ACM SIGPLAN Conf. on Programming Language Design and Implementation. 99-110."},{"key":"e_1_3_2_1_47_1","volume-title":"Proc. 43rd ACM SIGPLAN Int'l Conf. on Programming Language Design and Implementation. 719-732","author":"Zagieboylo Drew","unstructured":"Drew Zagieboylo, Charles Sherk, G. Edward Suh, and Andrew C. Myers. 2022b. PDL: a high-level hardware design language for pipelined processors. In Proc. 43rd ACM SIGPLAN Int'l Conf. on Programming Language Design and Implementation. 719-732."},{"key":"e_1_3_2_1_48_1","unstructured":"Drew Zagieboylo Charles Sherk and Kevin Zhang. 2022a. PDL: a hardware pipeline description language. Github repository at https:\/\/github.com\/apl-cornell\/PDL."}],"event":{"name":"ASPLOS '26:31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Pittsburgh PA USA","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3760250.3762233","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T15:09:06Z","timestamp":1765465746000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3760250.3762233"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12,11]]},"references-count":48,"alternative-id":["10.1145\/3760250.3762233","10.1145\/3760250"],"URL":"https:\/\/doi.org\/10.1145\/3760250.3762233","relation":{},"subject":[],"published":{"date-parts":[[2025,12,11]]},"assertion":[{"value":"2025-12-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}