{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:03:56Z","timestamp":1760058236212,"version":"build-2065373602"},"reference-count":43,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T00:00:00Z","timestamp":1742342400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computers"],"abstract":"<jats:p>Verifying sequential consistency (SC) in concurrent programs is computationally challenging due to the exponential growth of possible interleavings among read and write operations. Many of these interleavings produce identical outcomes, rendering exhaustive verification approaches inefficient and computationally expensive, especially as thread counts increase. To mitigate this challenge, this study introduces a novel approach that efficiently verifies SC by identifying a minimal subset of valid event orderings. The proposed method iteratively focuses on ordering write events and evaluates their compatibility with SC conditions, including program order, read-from (rf) relations, and SC semantics, thereby significantly reducing redundant computations. Corresponding read events are subsequently integrated according to program order once the validity of write events has been confirmed, enabling rapid identification of violations to SC criteria. Three algorithmic variants of this approach were developed and empirically evaluated. The final variant exhibited superior performance, achieving substantial improvements in execution time\u2014ranging from 31.919% to 99.992%\u2014compared to the optimal existing practical SC verification algorithms. Additionally, comparative experiments demonstrated that the proposed approach consistently outperforms other state-of-the-art methods in both efficiency and scalability.<\/jats:p>","DOI":"10.3390\/computers14030110","type":"journal-article","created":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:38:48Z","timestamp":1742380728000},"page":"110","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Novel Approach to Efficiently Verify Sequential Consistency in Concurrent Programs"],"prefix":"10.3390","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-2988-4620","authenticated-orcid":false,"given":"Mohammed H.","family":"Abdulwahhab","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Zakho, Zakho 42002, Iraq"}]},{"given":"Parosh Aziz","family":"Abdulla","sequence":"additional","affiliation":[{"name":"Department of Information Technology, Uppsala University, 752 37 Uppsala, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5220-5548","authenticated-orcid":false,"given":"Karwan","family":"Jacksi","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Zakho, Zakho 42002, Iraq"},{"name":"Semantic Web Lab, Research Center, University of Zakho, Zakho 42002, Iraq"}]}],"member":"1968","published-online":{"date-parts":[[2025,3,19]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Schneider, F.B., and Andrews, G.R. (1986). Concepts for Concurrent Programming. Current Trends in Concurrency. Overviews and Tutorials, Springer.","DOI":"10.1007\/BFb0027049"},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/MCSE.2012.111","article-title":"Concurrency in Modern Programming Languages [Guest Editors\u2019 Introduction]","volume":"14","author":"Skinner","year":"2012","journal-title":"Comput. Sci. Eng."},{"key":"ref_3","unstructured":"Arpaci-Dusseau, R.H., and Arpaci-Dusseau, A.C. (2018). Operating Systems: Three Easy Pieces, Arpaci-Dusseau Books, LLC. Erscheinungsort Nicht Ermittelbar."},{"key":"ref_4","unstructured":"Arlt, E. (2023). A Formally Verified Automatic Verifier for Concurrent Programs. [Master\u2019s Thesis, ETH Z\u00fcrich]."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"100","DOI":"10.52783\/cana.v32.1922","article-title":"A Comparative Analysis of Memory Models: SC, TSO, and ARM in Concurrent Programming","volume":"32","author":"Abdulwahhab","year":"2024","journal-title":"Commun. Appl. Nonlinear Anal."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/3458593.3458595","article-title":"What Is Decidable under the TSO Memory Model?","volume":"7","author":"Atig","year":"2020","journal-title":"ACM SIGLOG News"},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"(1979). Lamport. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Comput., C-28, 690\u2013691.","DOI":"10.1109\/TC.1979.1675439"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3458926","article-title":"Armed Cats: Formal Concurrency Modelling at Arm","volume":"43","author":"Alglave","year":"2021","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1134\/S0361768821060050","article-title":"A Survey of Programming Language Memory Models","volume":"47","author":"Moiseenko","year":"2021","journal-title":"Program. Comput. Softw."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Lahav, O., Giannarakis, N., and Vafeiadis, V. (2016, January 20\u201322). Taming Release-Acquire Consistency. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, FL, USA.","DOI":"10.1145\/2837614.2837643"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3276505","article-title":"Optimal Stateless Model Checking under the Release-Acquire Semantics","volume":"2","author":"Abdulla","year":"2018","journal-title":"Proc. ACM Program. Lang."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Zhang, N., Kusano, M., and Wang, C. (2015, January 13\u201317). Dynamic Partial Order Reduction for Relaxed Memory Models. Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA.","DOI":"10.1145\/2737924.2737956"},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Ta, T., Troendle, D., and Jang, B. (2017). Thread Communication and Synchronization on Massively Parallel GPUs. Advances in GPU Research and Practice, Morgan Kaufmann.","DOI":"10.1016\/B978-0-12-803738-6.00003-3"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3360576","article-title":"Optimal Stateless Model Checking for Reads-from Equivalence under Sequential Consistency","volume":"3","author":"Abdulla","year":"2019","journal-title":"Proc. ACM Program. Lang."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Lorch, J.R., Chen, Y., Kapritsos, M., Parno, B., Qadeer, S., Sharma, U., Wilcox, J.R., and Zhao, X. (2020, January 15\u201320). Armada: Low-Effort Verification of High-Performance Concurrent Programs. Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, London UK.","DOI":"10.1145\/3385412.3385971"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-3-030-81685-8_16","article-title":"Stateless Model Checking Under a Reads-Value-from Equivalence","volume":"Volume 12759","author":"Silva","year":"2021","journal-title":"Computer Aided Verification"},{"key":"ref_17","first-page":"41","article-title":"Litmus: Running Tests against Hardware","volume":"Volume 6605","author":"Abdulla","year":"2011","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Sorin, D.J., Hill, M.D., and Wood, D.A. (2011). A Primer on Memory Consistency and Cache Coherence, Synthesis Lectures on Computer Architecture; Morgan & Claypool Publishers.","DOI":"10.1007\/978-3-031-01733-9"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Naeem, A., Jantsch, A., and Lu, Z. (2012, January 5\u20138). Architecture Support and Comparison of Three Memory Consistency Models in NoC Based Systems. Proceedings of the 2012 15th Euromicro Conference on Digital System Design, Cesme, Turkey.","DOI":"10.1109\/DSD.2012.27"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1007\/978-3-030-59152-6_20","article-title":"Boosting Sequential Consistency Checking Using Saturation","volume":"Volume 12302","author":"Hung","year":"2020","journal-title":"Automated Technology for Verification and Analysis"},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Arora, J., Atig, M.F., and Krishna, S. (2019, January 22\u201326). Verification of Programs under the Release-Acquire Semantics. Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Phoenix, AZ, USA.","DOI":"10.1145\/3314221.3314649"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Naeem, A., Chen, X., Lu, Z., and Jantsch, A. (2011, January 25\u201328). Realization and Performance Comparison of Sequential and Weak Memory Consistency Models in Network-on-Chip Based Multi-Core Systems. Proceedings of the 16th Asia and South Pacific Design Automation Conference (ASP-DAC 2011), Yokohama, Japan.","DOI":"10.1109\/ASPDAC.2011.5722176"},{"key":"ref_23","first-page":"26","article-title":"What\u2019s Decidable about Weak Memory Models?","volume":"Volume 7211","author":"Seidl","year":"2012","journal-title":"Programming Languages and Systems"},{"key":"ref_24","unstructured":"Nardelli, F.Z., Sewell, P., Sevcik, J., Sarkar, S., Owens, S., Maranget, L., Batty, M., and Alglave, J. (2009). Relaxed Memory Models Must Be Rigorous. Exploiting Concurrency Efficiently and Correctly, CAV 2009 Workshop, University of Kent. Available online: https:\/\/kar.kent.ac.uk\/31904\/."},{"key":"ref_25","unstructured":"Aronis, S. (2018). Effective Techniques for Stateless Model Checking, Acta Universitatis Upsaliensis."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Boer, F.S.d., and Olderog, E.-R. (2009). Verification of Sequential and Concurrent Programs. Texts in Computer Science, Springer. [3rd ed.].","DOI":"10.1007\/978-1-84882-745-5"},{"key":"ref_27","unstructured":"Baier, C., and Katoen, J.-P. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-94-011-1793-7_4","article-title":"Assigning Meanings to Programs","volume":"Volume 14","author":"Colburn","year":"1993","journal-title":"Program Verification"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Gries, D. (1978). An Axiomatic Basis for Computer Programming. Programming Methodology, Springer.","DOI":"10.1007\/978-1-4612-6315-9"},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/S0022-0000(75)80018-3","article-title":"Proving Assertions about Parallel Programs","volume":"10","author":"Ashcroft","year":"1975","journal-title":"J. Comput. Syst. Sci."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s100090050035","article-title":"State Space Reduction Using Partial Order Techniques","volume":"2","author":"Clarke","year":"1999","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Godefroid, P. (1996). Partial-Order Methods for the Verification of Concurrent Systems, Springer. Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-60761-7"},{"key":"ref_33","first-page":"409","article-title":"All from One, One for All: On Model Checking Using Representatives","volume":"Volume 697","author":"Courcoubetis","year":"1993","journal-title":"Computer Aided Verification"},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., and Sagonas, K. (2014, January 22\u201324). Optimal Dynamic Partial Order Reduction. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA.","DOI":"10.1145\/2535838.2535845"},{"key":"ref_35","first-page":"278","article-title":"Trace Theory","volume":"Volume 255","author":"Brauer","year":"1987","journal-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency"},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"730","DOI":"10.1109\/TPDS.2003.1225053","article-title":"Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking","volume":"14","author":"Qadeer","year":"2003","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"ref_37","first-page":"267","article-title":"Gradual Consistency Checking","volume":"Volume 11562","author":"Dillig","year":"2019","journal-title":"Computer Aided Verification"},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Qian, X., Torrellas, J., Sahelices, B., and Qian, D. (2013, January 16\u201320). Volition: Scalable and Precise Sequential Consistency Violation Detection. Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, Houston, TX, USA.","DOI":"10.1145\/2451116.2451174"},{"key":"ref_39","doi-asserted-by":"crossref","unstructured":"Muzahid, A., Qi, S., and Torrellas, J. (2012, January 1\u20135). Vulcan: Hardware Support for Detecting Sequential Consistency Violations Dynamically. Proceedings of the 2012 45th Annual IEEE\/ACM International Symposium on Microarchitecture, Vancouver, BC, Canada.","DOI":"10.1109\/MICRO.2012.41"},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/1809028.1806636","article-title":"DRFX: A Simple and Efficient Memory Model for Concurrent Programming Languages","volume":"45","author":"Marino","year":"2010","journal-title":"ACM SIGPLAN Not."},{"key":"ref_41","unstructured":"(2024, November 15). POWER and ARM Litmus Tests. Available online: https:\/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/ppc451.html#toc25."},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2858651","article-title":"Concurrency Testing Using Controlled Schedulers: An Empirical Study","volume":"2","author":"Thomson","year":"2016","journal-title":"ACM Trans. Parallel Comput."},{"key":"ref_43","unstructured":"SV-COMP (2024, June 20). Competition on Software Verification. Available online: https:\/\/sv-comp.sosy-lab.org\/."}],"container-title":["Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-431X\/14\/3\/110\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T16:56:41Z","timestamp":1760029001000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-431X\/14\/3\/110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,19]]},"references-count":43,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2025,3]]}},"alternative-id":["computers14030110"],"URL":"https:\/\/doi.org\/10.3390\/computers14030110","relation":{},"ISSN":["2073-431X"],"issn-type":[{"type":"electronic","value":"2073-431X"}],"subject":[],"published":{"date-parts":[[2025,3,19]]}}}