Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Isla: tích hợp ngữ nghĩa ISA quy mô đầy đủ và các mô hình đồng thời định lý (phiên bản mở rộng)
Springer Science and Business Media LLC - Trang 1-24 - 2023
Tóm tắt
Các thông số kiến trúc như Armv8-A và RISC-V là nền tảng cuối cùng cho việc xác minh phần mềm và tiêu chí chính xác cho việc xác minh phần cứng. Chúng nên xác định hành vi đồng thời của các chương trình theo thứ tự và mô hình bộ nhớ thư giãn cho phép, nhưng cho đến nay chưa có sự tích hợp giữa ngữ nghĩa tập lệnh kiến trúc quy mô đầy đủ (ISA) với các mô hình đồng thời định lý, cả về mặt toán học lẫn công cụ. Những ngữ nghĩa ISA này có thể khá lớn và phức tạp, ví dụ như 100k dòng cho Armv8-A. Trong bài báo này, chúng tôi trình bày một công cụ, Isla, để tính toán các hành vi cho phép của các bài kiểm tra đồng thời liên quan đến các định nghĩa ISA quy mô đầy đủ, trong ngôn ngữ Sail, và các mô hình đồng thời định lý thư giãn tùy ý, trong ngôn ngữ Cat. Nó dựa trên một động cơ biểu tượng tổng quát cho các thông số ISA Sail. Chúng tôi trang bị cho công cụ một giao diện web để làm cho nó trở nên dễ tiếp cận, và minh họa cũng như đánh giá nó cho Armv8-A và RISC-V. Động cơ thực thi biểu tượng cũng rất có giá trị cho các tác vụ xác minh khác: nó đã được sử dụng trong việc tạo ra các bài kiểm tra ISA tự động cho kiến trúc mẫu Arm Morello, mở rộng Armv8-A với các khả năng CHERI, và cho lý luận chương trình Iris về mã nhị phân dựa trên các thông số ISA Armv8-A và RISC-V. Bằng cách sử dụng ngữ nghĩa ISA quy mô đầy đủ và có thẩm quyền, Isla cho phép đánh giá các bài kiểm tra lít mát với các lệnh người dùng tùy ý với độ tin cậy cao. Hơn nữa, vì những thông số ISA này cung cấp các định nghĩa chi tiết và đã được xác thực về các khía cạnh tuần tự của chức năng hệ thống, như được sử dụng bởi các hypervisor và hệ điều hành, ví dụ như truy xuất lệnh, ngoại lệ, và dịch địa chỉ, công cụ của chúng tôi cung cấp một cơ sở để phát triển ngữ nghĩa đồng thời cho những điều này. Chúng tôi chứng minh điều này đối với mô hình truy xuất lệnh và bộ nhớ ảo của Armv8-A và các ví dụ của Simner et al.
Từ khóa
Tài liệu tham khảo
Armstrong A, Bauereiss T, Campbell B, Reid A, Gray KE, Norton-Wright R, Mundkur P, Wassell M, French J, Pulte C, Flur S, Stark I, Krishnaswami N, Sewell P (2019) ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS 3:71:1–71:31
Gray KE, Kerneis G, Mulligan D, Pulte C, Sarkar S, Sewell P (2015) An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In: Proc. MICRO-48, the 48th annual IEEE/ACM international symposium on microarchitecture
Reid A (2016) Trustworthy specifications of ARM v8-A and v8-M system level architecture. FMCAD 2016:161–168
Pulte C, Flur S, Deacon W, French J, Sarkar S, Sewell P (2018) Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. In: POPL 2018: proceedings of the 45th ACM SIGPLAN symposium on principles of programming languages
Arm Ltd. (2017) ARM architecture reference manual (ARMv8, for ARMv8-A architecture profile). ARM DDI 0487B.a (ID033117). https://developer.arm.com/documentation/ddi0487/b/?lang=en
The RISC-V Instruction Set Manual (2020) Volume I: unprivileged ISA, Document Version 20191214-draft. https://riscv.org/technical/specifications/. Accessed 23 Sep 2020
Arm Ltd. Memory model tool (2020) https://developer.arm.com/architectures/cpu-architecture/a-profile/memory-model-tool. Accessed 26 Jan 2021
Flur S, Gray KE, Pulte C, Sarkar S, Sezgin A, Maranget L, Deacon W, Sewell P (2016) Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Proceedings of POPL: the 43rd ACM SIGPLAN-SIGACT symposium on principles of programming languages
Pulte C, Pichon-Pharabod J, Kang J, Lee S-H, Hur C-K (2019) Promising-ARM/RISC-V: a simpler and faster operational concurrency model. In: PLDI 2019: proceedings of the 40th ACM SIGPLAN conference on programming language design and implementation
Pulte C (2018) The Semantics of Multicopy Atomic ARMv8 and RISC-V. Thesis, University of Cambridge. https://www.repository.cam.ac.uk/handle/1810/292229
Flur S, French J, Gray K, Pulte C, Sarkar S, Sewell P (2020) RMEM. www.cl.cam.ac.uk/~pes20/rmem/. Accessed 28 Jan 2021
Zhang H, Trippel C, Manerkar YA, Gupta A, Martonosi M, Malik S (2018) ILA-MCM: integrating memory consistency models with instruction-level abstractions for heterogeneous system-on-chip verification. In: 2018 Formal methods in computer aided design (FMCAD), pp 1–10
Park S, Dill DL (1999) An executable specification and verifier for relaxed memory order. IEEE Trans Comput 48(2):227–235
Yang Y, Gopalakrishnan G, Lindstrom G, Slind K (2003) Analyzing the intel itanium memory ordering rules using logic programming and SAT. In: Daniel G and Enrico T (eds) Correct hardware design and verification methods, 12th IFIP WG 10.5 advanced research working conference, CHARME 2003, L’Aquila, Italy, October 21–24, 2003, proceedings, volume 2860 of lecture notes in computer science. Springer, pp 81–95
Yue Y, Ganesh G, Gary L, Konrad S (2004) Nemos: a framework for axiomatic and executable specifications of memory consistency models. In: 18th international parallel and distributed processing symposium (IPDPS) (2004) Santa Fe. New Mexico, USA, p 2004
Sarkar S, Sewell P, Nardelli FZ, Owens S, Ridge T, Braibant T, Myreen MO, Alglave J (2009) The semantics of x86-CC multiprocessor machine code. In: Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 379–391
Owens S, Sarkar S, Sewell P (2009) A better x86 memory model: x86-TSO. In: Proceedings of TPHOLs 2009: theorem proving in higher order logics, LNCS 5674, pp 391–407
Sarkar S, Sewell P, Alglave J, Maranget L, Williams D (2011) Understanding POWER multiprocessors. In: Proceedings of PLDI 2011: the 32nd ACM SIGPLAN conference on programming language design and implementation, pp 175–186
Mador-Haim S, Maranget L, Sarkar S, Memarian K, Alglave J, Owens S, Alur R, Martin M, Sewell P, Williams D (2012) An axiomatic memory model for POWER multiprocessors. In: Proceedings of the 24th international conference on computer aided verification, pp 495–512
Alglave J, Maranget L, Tautschnig M (2014) Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM TOPLAS 36(2):7:1-7:74
Alglave J, Maranget L (2021) The diy7 tool. http://diy.inria.fr/. Accessed 28 Jan 2021
Bornholt J, Torlak E (2017) Synthesizing memory models from framework sketches and litmus tests. In: Cohen A, Vechev MT (eds) Proceedings of the 38th ACM SIGPLAN conference on programming language design and implementation, PLDI 2017, Barcelona, Spain, June 18–23, 2017. ACM, pp 467–481
Wickerson J, Batty M, Sorensen T, Constantinides GA (2017) Automatically comparing memory consistency models. In: Castagna G, Gordon AD (eds) Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages, POPL 2017, Paris, France, January 18-20, 2017. ACM, pp 190–204
Trippel C, Manerkar YA, Lustig D, Pellauer M, Martonosi M (2018) Full-stack memory model verification with tricheck. IEEE Micro 38(3):58–68
Martonosi Research Group. Check research tools and papers. https://check.cs.princeton.edu/. Accessed 28 Jan 2021
Alglave J, Cousot P, Maranget L (2016) Syntax and semantics of the weak consistency model specification language cat. arXiv:1608.07531
Bauereiss T, Campbell B, Sewell T, Armstrong A, Esswood L, Stark I, Barnes G, Watson RNM, Sewell P (2022) Verified security for the Morello capability-enhanced prototype Arm architecture. In: Proceedings of the 31st European symposium on programming
Sammler M, Hammond A, Lepigre R, Campbell B, Pichon-Pharabod J, Dreyer D, Garg D, Sewell P (2022) Islaris: verification of machine code against authoritative ISA semantics. In: Jhala R, Dillig I (eds) PLDI ’22: 43rd ACM SIGPLAN international conference on programming language design and implementation, San Diego, CA, USA, June 13–17, 2022. ACM, pp 825–840
Simner B, Flur S, Pulte C, Armstrong A, Pichon-Pharabod J, Maranget L, Sewell P (2020) ARMv8-A system semantics: instruction fetch in relaxed architectures. In: ESOP 2020: proceedings of the 29th European symposium on programming. http://www.cl.cam.ac.uk/~pes20/iflat/top-extended.pdf
Simner B, Armstrong A, Pichon-Pharabod J, Pulte C, Grisenthwaite R, Sewell P (2022) Relaxed virtual memory in Armv8-A. In: Proceedings of the 31st European symposium on programming
Armstrong A, Campbell B, Simner B, Pulte C, Sewell P (2021) Isla: integrating full-scale ISA semantics and axiomatic concurrency models. In: Silva A, Rustan K, Leino M (eds) Computer aided verification–33rd international conference, CAV 2021, virtual event, July 20–23, 2021, proceedings, part I, volume 12759 of LNCS. Springer, pp 303–316
Alglave J, Kroening D, Tautschnig M (2013) Partial orders for efficient bounded model checking of concurrent software. In: Computer aided verification—25th international conference, CAV, pp 141–157
Alglave J, Maranget L, Sarkar S, Sewell P (2011) Litmus: running tests against hardware. In: Proceedings of TACAS 2011: the 17th international conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, Heidelberg, pp 41–44
Lau S, Gomes V, Memarian K, Pichon-Pharabod J, Sewell P (2019) Cerberus-BMC: a principled reference semantics and exploration tool for concurrent and sequential C. In: Dillig I, Tasiran S (eds) Computer aided verification. Springer, pp 387–397
Deacon W (2016) The ARMv8 application level memory model. https://github.com/herd/herdtools7/blob/master/herd/libdir/aarch64.cat