{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:56:23Z","timestamp":1774025783960,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816841","type":"print"},{"value":"9783030816858","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in\u00a0tools. These ISA semantics can be surprisingly large and intricate, e.g.\u00a0100k+ lines for Armv8-A.<\/jats:p><jats:p>\u00a0\u00a0\u00a0In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in Sail, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications, which should be valuable also for other verification tasks. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V.<\/jats:p><jats:p>\u00a0\u00a0\u00a0By using full-scale and authoritative ISA semantics, this lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of <jats:italic>systems<\/jats:italic> functionality, as used by hypervisors and operating systems, e.g.\u00a0instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch model and self-modifying code examples of Simner et al.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_14","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"303-316","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models"],"prefix":"10.1007","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[]},{"given":"Brian","family":"Campbell","sequence":"additional","affiliation":[]},{"given":"Ben","family":"Simner","sequence":"additional","affiliation":[]},{"given":"Christopher","family":"Pulte","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"14_CR1","unstructured":"The RISC-V Instruction Set Manual, Volume I: Unprivileged ISA, Document Version 20191214-draft, 238 pages (2020). https:\/\/riscv.org\/technical\/specifications\/ . Accessed 23 Sept 2020"},{"key":"14_CR2","unstructured":"Alglave, J., Cousot, P., Maranget, L.: Syntax and semantics of the weak consistency model specification language cat. CoRR abs\/1608.07531 (2016)"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Computer Aided Verification - 25th International Conference, CAV, pp. 141\u2013157 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"14_CR4","unstructured":"Alglave, J., Maranget, L.: The diy7 tool. http:\/\/diy.inria.fr\/. Accessed 28 Jan 2021"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-19835-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Litmus: running tests against hardware. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 41\u201344. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_5"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM TOPLAS 36(2), 7:1\u20137:74 (2014). https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"14_CR7","unstructured":"Arm: Arm Architecture Reference Manual: Armv8, for Armv8-A architecture profile, 8248 pages (2020). https:\/\/developer.arm.com\/documentation\/ddi0487\/fc. Accessed 23 Sept 2020"},{"key":"14_CR8","unstructured":"Arm: Memory model tool (2020). https:\/\/developer.arm.com\/architectures\/cpu-architecture\/a-profile\/memory-model-tool Accessed 26 Jan 2021"},{"key":"14_CR9","unstructured":"ARM Ltd.: ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) (2017). ARM DDI 0487B.a (ID033117). https:\/\/developer.arm.com\/documentation\/ddi0487\/b\/?lang=en"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Armstrong, A., et al.: ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS (2019). http:\/\/www.cl.cam.ac.uk\/~pes20\/sail\/","DOI":"10.1145\/3290384"},{"key":"14_CR11","unstructured":"Armstrong, A., Campbell, B., Simner, B., Pulte, C., Sewell, P.: Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version). In: Extended version of a paper in Proceedings of CAV 2021: 33rd International Conference on Computer-Aided Verification (2021). https:\/\/www.cl.cam.ac.uk\/~pes20\/isla\/"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Bornholt, J., Torlak, E.: Synthesizing memory models from framework sketches and litmus tests. In: Cohen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, 18\u201323 June, 2017, pp. 467\u2013481. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062353","DOI":"10.1145\/3062341.3062353"},{"key":"14_CR13","unstructured":"Deacon, W.: The ARMv8 application level memory model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/aarch64.cat (2016)"},{"key":"14_CR14","unstructured":"Flur, S., French, J., Gray, K., Pulte, C., Sarkar, S., Sewell, P.: RMEM (2020). www.cl.cam.ac.uk\/~pes20\/rmem\/. Accessed 28 Jan 2021"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Gray, K.E., Kerneis, G., Mulligan, D., Pulte, C., Sarkar, S., Sewell, P.: An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In: Proceedings of MICRO-48, the 48th Annual IEEE\/ACM International Symposium on Microarchitecture (2015). https:\/\/doi.org\/10.1145\/2830772.2830775","DOI":"10.1145\/2830772.2830775"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-030-25540-4_22","volume-title":"Computer Aided Verification","author":"S Lau","year":"2019","unstructured":"Lau, S., Gomes, V.B.F., Memarian, K., Pichon-Pharabod, J., Sewell, P.: Cerberus-BMC: a principled reference semantics and exploration tool for concurrent and sequential C. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification. LNCS, vol. 11561, pp. 387\u2013397. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_22"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Mador-Haim, S., et al.: An axiomatic memory model for POWER multiprocessors. In: Proceedings of the 24th International Conference on Computer Aided Verification, pp. 495\u2013512 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_36","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"14_CR18","unstructured":"Martonosi Research Group: Check research tools and papers. https:\/\/check.cs.princeton.edu\/. Accessed 28 Jan 2021"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, LNCS 5674, pp. 391\u2013407 (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: An executable specification and verifier for relaxed memory order. IEEE Trans. Comput. 48(2), 227\u2013235 (1999)","DOI":"10.1109\/12.752664"},{"key":"14_CR21","unstructured":"Pulte, C.: The semantics of multicopy atomic ARMv8 and RISC-V. Ph.D. thesis, University of Cambridge (2018). https:\/\/www.repository.cam.ac.uk\/handle\/1810\/292229"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: 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 (2018). https:\/\/doi.org\/10.1145\/3158107","DOI":"10.1145\/3158107"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Pulte, C., Pichon-Pharabod, J., Kang, J., Lee, S.H., Hur, C.K.: 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 (2019). https:\/\/doi.org\/10.1145\/3314221.3314624","DOI":"10.1145\/3314221.3314624"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Reid, A.: Trustworthy specifications of ARM v8-A and v8-M system level architecture. In: FMCAD 2016, pp. 161\u2013168 (2016). https:\/\/alastairreid.github.io\/papers\/fmcad2016-trustworthy.pdf","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proceedings of PLDI 2011: the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 175\u2013186 (2011). https:\/\/doi.org\/10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Sarkar, S., et al.: 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\u2013391 (2009). https:\/\/doi.org\/10.1145\/1594834.1480929","DOI":"10.1145\/1594834.1480929"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Simner, B., et al.: Armv8-a system semantics: instruction fetch in relaxed architectures. In: ESOP 2020: Proceedings of the 29th European Symposium on Programming (2020). http:\/\/www.cl.cam.ac.uk\/~pes20\/iflat\/top-extended.pdf","DOI":"10.1007\/978-3-030-44914-8_23"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Trippel, C., Manerkar, Y.A., Lustig, D., Pellauer, M., Martonosi, M.: Full-stack memory model verification with tricheck. IEEE Micro 38(3), 58\u201368 (2018)","DOI":"10.1109\/MM.2018.032271062"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 190\u2013204. ACM (2017). http:\/\/dl.acm.org\/citation.cfm?id=3009838","DOI":"10.1145\/3009837.3009838"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-540-39724-3_9","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yang","year":"2003","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Analyzing the intel Itanium memory ordering rules using logic programming and SAT. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 81\u201395. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39724-3_9"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: 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 (2004). https:\/\/doi.org\/10.1109\/IPDPS.2004.1302944","DOI":"10.1109\/IPDPS.2004.1302944"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Zhang, H., Trippel, C., Manerkar, Y.A., Gupta, A., Martonosi, M., Malik, S.: 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\u201310 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603015","DOI":"10.23919\/FMCAD.2018.8603015"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:07:18Z","timestamp":1626480438000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}