{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:14:31Z","timestamp":1767928471838,"version":"3.49.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377020","type":"print"},{"value":"9783031377037","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modifications, model checking can be an effective tool for verifying race-freedom. We explore this technique on a suite of C programs parallelized with OpenMP.<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_13","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"265-287","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking Race-Freedom When \u201cSequential Consistency for\u00a0Data-Race-Free Programs\u201d is Guaranteed"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9087-4240","authenticated-orcid":false,"given":"Wenhao","family":"Wu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3479-6361","authenticated-orcid":false,"given":"Jan","family":"H\u00fcckelheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0907-2567","authenticated-orcid":false,"given":"Paul D.","family":"Hovland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6557-3692","authenticated-orcid":false,"given":"Ziqing","family":"Luo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9359-3332","authenticated-orcid":false,"given":"Stephen F.","family":"Siegel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"13_CR1","unstructured":"Andrews, G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley (2000). https:\/\/www.pearson.ch\/HigherEducation\/Pearson\/EAN\/9780201357523\/Foundations-of-Multithreaded-Parallel-and-Distributed-Programming"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Atzeni, S., et al.: ARCHER: Effectively spotting data races in large OpenMP applications. In: 2016 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 53\u201362 (2016). https:\/\/doi.org\/10.1109\/IPDPS.2016.68","DOI":"10.1109\/IPDPS.2016.68"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Atzeni, S., Gopalakrishnan, G., Rakamaric, Z., Laguna, I., Lee, G.L., Ahn, D.H.: SWORD: A bounded memory-overhead detector of OpenMP data races in production runs. In: 2018 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 845\u2013854 (2018). https:\/\/doi.org\/10.1109\/IPDPS.2018.00094","DOI":"10.1109\/IPDPS.2018.00094"},{"issue":"5","key":"13_CR4","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1109\/PGEC.1966.264565","volume":"15","author":"AJ Bernstein","year":"1966","unstructured":"Bernstein, A.J.: Analysis of programs for parallel processing. IEEE Trans. Electronic Comput. EC 15(5), 757\u2013763 (1966). https:\/\/doi.org\/10.1109\/PGEC.1966.264565","journal-title":"IEEE Trans. Electronic Comput. EC"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Betts, A., et al.: The design and implementation of a verification technique for GPU kernels. ACM Trans. Program. Lang. Syst. 37(3) (2015). https:\/\/doi.org\/10.1145\/2743017","DOI":"10.1145\/2743017"},{"issue":"5","key":"13_CR6","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1007\/s10009-020-00601-z","volume":"23","author":"S Blom","year":"2021","unstructured":"Blom, S., Darabi, S., Huisman, M., Safari, M.: Correct program parallelisations. Int. J. Softw. Tools Technol. Trans. 23(5), 741\u2013763 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00601-z","journal-title":"Int. J. Softw. Tools Technol. Trans."},{"key":"13_CR7","unstructured":"Boehm, H.J.: How to miscompile programs with \"benign\" data races. In: Proceedings of the 3rd USENIX Conference on Hot Topic in Parallelism, HotPar 2011, pp. 1\u20136. USENIX Association, Berkeley, CA, USA (2011). http:\/\/dl.acm.org\/citation.cfm?id=2001252.2001255"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 68\u201378. PLDI \u201908, Association for Computing Machinery, New York (2008). https:\/\/doi.org\/10.1145\/1375581.1375591","DOI":"10.1145\/1375581.1375591"},{"issue":"4","key":"13_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3418597","volume":"17","author":"U Bora","year":"2020","unstructured":"Bora, U., Das, S., Kukreja, P., Joshi, S., Upadrasta, R., Rajopadhye, S.: LLOV: A fast static data-race checker for OpenMP programs. ACM Trans. Archit. Code Optimiz. (TACO) 17(4), 1\u201326 (2020). https:\/\/doi.org\/10.1145\/3418597","journal-title":"ACM Trans. Archit. Code Optimiz. (TACO)"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Bora, U., Vaishay, S., Joshi, S., Upadrasta, R.: OpenMP aware MHP analysis for improved static data-race detection. In: 2021 IEEE\/ACM 7th Workshop on the LLVM Compiler Infrastructure in HPC (LLVM-HPC). pp. 1\u201311 (2021). https:\/\/doi.org\/10.1109\/LLVMHPC54804.2021.00006","DOI":"10.1109\/LLVMHPC54804.2021.00006"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-030-58144-2_10","volume-title":"OpenMP: Portable Multi-Level Parallelism on Modern Systems","author":"N Boushehrinejadmoradi","year":"2020","unstructured":"Boushehrinejadmoradi, N., Yoga, A., Nagarakatte, S.: On-the-fly data race detection with the enhanced openmp series-parallel graph. In: Milfeld, K., de Supinski, B.R., Koesterke, L., Klinkenberg, J. (eds.) IWOMP 2020. LNCS, vol. 12295, pp. 149\u2013164. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58144-2_10"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-52709-3_10","volume-title":"Languages and Compilers for Parallel Computing","author":"P Chatarasi","year":"2017","unstructured":"Chatarasi, P., Shirako, J., Kong, M., Sarkar, V.: An extended polyhedral model for spmd programs and its use in static data race detection. In: Ding, C., Criswell, J., Wu, P. (eds.) LCPC 2016. LNCS, vol. 10136, pp. 106\u2013120. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52709-3_10"},{"issue":"1","key":"13_CR13","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/99.660313","volume":"5","author":"L Dagum","year":"1998","unstructured":"Dagum, L., Menon, R.: OpenMP: an industry standard API for shared-memory programming. IEEE Comput. Sci. Eng. 5(1), 46\u201355 (1998). https:\/\/doi.org\/10.1109\/99.660313","journal-title":"IEEE Comput. Sci. Eng."},{"key":"13_CR14","unstructured":"Davis, M.J.: Dynamatic: An OpenMP Race Detection Tool Combining Static and Dynamic Analysis. Undergraduate research scholars thesis, Texas A &M University (2021). https:\/\/oaktrust.library.tamu.edu\/handle\/1969.1\/194411"},{"key":"13_CR15","unstructured":"Edmund M. Clarke, J., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking, 2 edn. MIT press, Cambridge, MA, USA (2018). https:\/\/mitpress.mit.edu\/books\/model-checking-second-edition"},{"key":"13_CR16","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Precise race detection and efficient model checking using locksets. Tech. Rep. MSR-TR-2005-118, Microsoft Research (2006). https:\/\/www.microsoft.com\/en-us\/research\/publication\/precise-race-detection-and-efficient-model-checking-using-locksets\/"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","year":"1996","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60761-7"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Gu, Y., Mellor-Crummey, J.: Dynamic data race detection for OpenMP programs. In: SC18: International Conference for High Performance Computing, Networking, Storage and Analysis (2018). https:\/\/doi.org\/10.1109\/SC.2018.00064","DOI":"10.1109\/SC.2018.00064"},{"key":"13_CR19","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-27207-3_47","volume-title":"Software Engineering, Business Continuity, and Education","author":"O-K Ha","year":"2011","unstructured":"Ha, O.-K., Jun, Y.-K.: Efficient thread labeling for on-the-fly race detection of programs with nested parallelism. In: Kim, T., Adeli, H., Kim, H., Kang, H., Kim, K.J., Kiumi, A., Kang, B.-H. (eds.) ASEA 2011. CCIS, vol. 257, pp. 424\u2013436. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-27207-3_47"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Ha, O.K., Kuh, I.B., Tchamgoue, G.M., Jun, Y.K.: On-the-fly detection of data races in OpenMP programs. In: Proceedings of the 2012 Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, pp. 1\u201310. PADTAD 2012, Association for Computing Machinery, New York (2012). https:\/\/doi.org\/10.1145\/2338967.2336808","DOI":"10.1145\/2338967.2336808"},{"key":"13_CR21","unstructured":"International Organization for Standardization: ISO\/IEC 9899:2018. Information technology \u2013 Programming languages \u2013 C (2018). https:\/\/www.iso.org\/standard\/74528.html"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C-28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 378\u2013391. POPL \u201905, Association for Computing Machinery, New York (2005). https:\/\/doi.org\/10.1145\/1040305.1040336","DOI":"10.1145\/1040305.1040336"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Mellor-Crummey, J.: On-the-fly detection of data races for programs with nested fork-join parallelism. In: Supercomputing 1991: Proceedings of the 1991 ACM\/IEEE Conference On Supercomputing, pp. 24\u201333. IEEE (1991). https:\/\/doi.org\/10.1145\/125826.125861","DOI":"10.1145\/125826.125861"},{"key":"13_CR25","unstructured":"Open Group: IEEE Std 1003.1: Standard for information technology\u2013Portable Operating System Interface (POSIX(R)) base specifications, issue 7: General concepts: Memory synchronization (2018). https:\/\/pubs.opengroup.org\/onlinepubs\/9699919799\/basedefs\/V1_chap04.html#tag_04_12"},{"key":"13_CR26","unstructured":"OpenMP Architecture Review Board: OpenMP Application Programming Interface (Nov 2021). https:\/\/www.openmp.org\/wp-content\/uploads\/OpenMP-API-Specification-5-2.pdf, version 5.2"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.: LOCKSMITH: Practical static race detection for C. ACM Trans. Program. Lang. Syst. 33, 3:1\u20133:55 (2011). https:\/\/doi.org\/10.1145\/1889997.1890000","DOI":"10.1145\/1889997.1890000"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-65578-9_17","volume-title":"Scaling OpenMP for Exascale Performance and Portability","author":"J Protze","year":"2017","unstructured":"Protze, J., Hahnfeld, J., Ahn, D.H., Schulz, M., M\u00fcller, M.S.: OpenMP tools interface: synchronization information for data race detection. In: de Supinski, B.R., Olivier, S.L., Terboven, C., Chapman, B.M., M\u00fcller, M.S. (eds.) IWOMP 2017. LNCS, vol. 10468, pp. 249\u2013265. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-65578-9_17"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-030-53288-8_18","volume-title":"Computer Aided Verification","author":"D Schemmel","year":"2020","unstructured":"Schemmel, D., B\u00fcning, J., Rodr\u00edguez, C., Laprell, D., Wehrle, K.: Symbolic partial-order execution for testing multi-threaded programs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 376\u2013400. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_18"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Serebryany, K., Iskhodzhanov, T.: ThreadSanitizer: Data race detection in practice. In: Proceedings of the Workshop on Binary Instrumentation and Applications, pp. 62\u201371. WBIA 2009. Association for Computing Machinery, New York (2009). https:\/\/doi.org\/10.1145\/1791194.1791203","DOI":"10.1145\/1791194.1791203"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Siegel, S.F., et al.: CIVL: The concurrency intermediate verification language. In: SC15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. ACM, New York (Nov 2015). https:\/\/doi.org\/10.1145\/2807591.2807635, article no. 61, pages 1-12","DOI":"10.1145\/2807591.2807635"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"Swain, B., Huang, J.: Towards incremental static race detection in OpenMP programs. In: 2018 IEEE\/ACM 2nd International Workshop on Software Correctness for HPC Applications (Correctness), pp. 33\u201341. IEEE (2018). https:\/\/doi.org\/10.1109\/Correctness.2018.00009","DOI":"10.1109\/Correctness.2018.00009"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Swain, B., Li, Y., Liu, P., Laguna, I., Georgakoudis, G., Huang, J.: OMPRacer: A scalable and precise static race detector for OpenMP programs. In: SC20: International Conference for High Performance Computing, Networking, Storage and Analysis, pp. 1\u201314. IEEE (2020). https:\/\/doi.org\/10.1109\/SC41405.2020.00058","DOI":"10.1109\/SC41405.2020.00058"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Swain, B., Liu, B., Liu, P., Li, Y., Crump, A., Khera, R., Huang, J.: OpenRace: An open source framework for statically detecting data races. In: 2021 IEEE\/ACM 5th International Workshop on Software Correctness for HPC Applications (Correctness), pp. 25\u201332. IEEE (2021). https:\/\/doi.org\/10.1109\/Correctness54621.2021.00009","DOI":"10.1109\/Correctness54621.2021.00009"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Verma, G., Shi, Y., Liao, C., Chapman, B., Yan, Y.: Enhancing DataRaceBench for evaluating data race detection tools. In: 2020 IEEE\/ACM 4th International Workshop on Software Correctness for HPC Applications (Correctness), pp. 20\u201330 (2020). https:\/\/doi.org\/10.1109\/Correctness51934.2020.00008","DOI":"10.1109\/Correctness51934.2020.00008"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Ye, F., Schordan, M., Liao, C., Lin, P.H., Karlin, I., Sarkar, V.: Using polyhedral analysis to verify OpenMP applications are data race free. In: 2018 IEEE\/ACM 2nd International Workshop on Software Correctness for HPC Applications (Correctness), pp. 42\u201350. IEEE (2018). https:\/\/doi.org\/10.1109\/Correctness.2018.00010","DOI":"10.1109\/Correctness.2018.00010"}],"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-031-37703-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:04:33Z","timestamp":1693047873000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"18 July 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","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":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"26% - 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":"11","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)"}}]}}