{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T18:40:14Z","timestamp":1758566414220,"version":"3.44.0"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T00:00:00Z","timestamp":1754438400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T00:00:00Z","timestamp":1754438400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100006260","name":"Technion - Israel Institute of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100006260","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>When a concrete concurrent object <jats:italic>refines<\/jats:italic> another, more abstract object, the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This approach is sound for <jats:italic>trace properties<\/jats:italic> of the program, but not for <jats:italic>hyperproperties<\/jats:italic>, including many security properties and probability distributions of events. We define <jats:italic>strong observational refinement<\/jats:italic>, a strengthening of refinement that preserves hypersafety properties, and prove that it is <jats:italic>equivalent<\/jats:italic> to the existence of <jats:italic>forward simulations<\/jats:italic>. We show that strong observational refinement generalizes <jats:italic>strong linearizability<\/jats:italic>, a restriction of <jats:italic>linearizability<\/jats:italic>, the prevalent consistency condition for implementing concurrent objects. Our results imply that strong linearizability is also equivalent to existence of forward simulations, and show that strongly linearizable implementations can be composed both horizontally and vertically. This paper also investigates whether there are wait-free strongly-linearizable implementations from realistic primitives such as test&amp;set or fetch&amp;add, whose consensus number is 2. We show that many objects with consensus number 1 have wait-free strongly-linearizable implementations from fetch&amp;add. We also show that several objects with consensus number 2 have wait-free or lock-free implementations from other objects with consensus number 2. In contrast, we prove that even when fetch&amp;add, swap and test&amp;set primitives are used, some objects with consensus number 2 do not have lock-free strongly-linearizable implementations. This includes queues and stacks, and relaxed variants thereof.<\/jats:p>","DOI":"10.1007\/s00236-025-00500-3","type":"journal-article","created":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T07:12:37Z","timestamp":1754464357000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Preserving hyperproperties of programs using primitives with consensus number 2"],"prefix":"10.1007","volume":"62","author":[{"given":"Hagit","family":"Attiya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Casta\u00f1eda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,6]]},"reference":[{"key":"500_CR1","doi-asserted-by":"publisher","unstructured":"Afek, Y., Weisberger, E., Weisman, H.: A completeness theorem for a class of synchronization objects (extended abstract). In: Anderson, J., Toueg, S. (eds.) Proceedings of the Twelth Annual ACM Symposium on Principles of Distributed Computing, Ithaca, New York, USA, August 15-18, 1993, pp. 159\u2013170. ACM (1993). https:\/\/doi.org\/10.1145\/164051.164071","DOI":"10.1145\/164051.164071"},{"issue":"4","key":"500_CR2","doi-asserted-by":"publisher","first-page":"873","DOI":"10.1145\/153724.153741","volume":"40","author":"Y Afek","year":"1993","unstructured":"Afek, Y., Attiya, H., Dolev, D., Gafni, E., Merritt, M., Shavit, N.: Atomic snapshots of shared memory. J. ACM 40(4), 873\u2013890 (1993). https:\/\/doi.org\/10.1145\/153724.153741","journal-title":"J. ACM"},{"issue":"1","key":"500_CR3","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1006\/JAGM.1998.0969","volume":"30","author":"Y Afek","year":"1999","unstructured":"Afek, Y., Weisberger, E.: The instancy of snapshots and commuting objects. J. Algorithms 30(1), 68\u2013105 (1999). https:\/\/doi.org\/10.1006\/JAGM.1998.0969","journal-title":"J. Algorithms"},{"issue":"4","key":"500_CR4","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s00446-007-0023-3","volume":"20","author":"Y Afek","year":"2007","unstructured":"Afek, Y., Gafni, E., Morrison, A.: Common2 extended to stacks and unbounded concurrency. Distributed Comput. 20(4), 239\u2013252 (2007). https:\/\/doi.org\/10.1007\/s00446-007-0023-3","journal-title":"Distributed Comput."},{"key":"500_CR5","doi-asserted-by":"publisher","unstructured":"Afek, Y., Morrison, A., Wertheim, G.: From bounded to unbounded concurrency objects and back. In: Gavoille, C., Fraigniaud, P. (eds.) Proceedings of the 30th Annual ACM Symposium on Principles of Distributed Computing, PODC 2011, San Jose, CA, USA, June 6-8, 2011, pp. 119\u2013128. ACM (2011). https:\/\/doi.org\/10.1145\/1993806.1993823","DOI":"10.1145\/1993806.1993823"},{"key":"500_CR6","doi-asserted-by":"publisher","unstructured":"Alur, R., Cern\u00fd, P., Zdancewic, S.: Preserving secrecy under refinement. In: Automata, Languages and Programming, 33rd International Colloquium, ICALP, vol. 4052, pp. 107\u2013118. Springer (2006). https:\/\/doi.org\/10.1007\/11787006_10","DOI":"10.1007\/11787006_10"},{"issue":"2\u20133","key":"500_CR7","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/S00446-002-0081-5","volume":"16","author":"J Aspnes","year":"2003","unstructured":"Aspnes, J.: Randomized protocols for asynchronous consensus. Distributed Comput. 16(2\u20133), 165\u2013175 (2003). https:\/\/doi.org\/10.1007\/S00446-002-0081-5","journal-title":"Distributed Comput."},{"key":"500_CR8","doi-asserted-by":"publisher","unstructured":"Aspnes, J., Attiya, H., Censor, K.: Max registers, counters, and monotone circuits. In: Tirthapura, S., Alvisi, L. (eds.) Proceedings of the 28th Annual ACM Symposium on Principles of Distributed Computing, PODC 2009, Calgary, Alberta, Canada, August 10-12, 2009, pp. 36\u201345. ACM (2009). https:\/\/doi.org\/10.1145\/1582716.1582728","DOI":"10.1145\/1582716.1582728"},{"issue":"2\u20133","key":"500_CR9","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s00446-002-0081-5","volume":"16","author":"J Aspnes","year":"2003","unstructured":"Aspnes, J.: Randomized protocols for asynchronous consensus. Distrib. Comput. 16(2\u20133), 165\u2013175 (2003)","journal-title":"Distrib. Comput."},{"key":"500_CR10","doi-asserted-by":"publisher","unstructured":"Aspnes, J., Herlihy, M.: Wait-free data structures in the asynchronous PRAM model. In: Leighton, F.T. (ed.) Proceedings of the 2nd Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA \u201990, Island of Crete, Greece, July 2-6, 1990, pp. 340\u2013349. ACM (1990). https:\/\/doi.org\/10.1145\/97444.97701","DOI":"10.1145\/97444.97701"},{"key":"500_CR11","doi-asserted-by":"publisher","unstructured":"Attiya, H., Enea, C.: Putting strong linearizability in context: Preserving hyperproperties in programs that use concurrent objects. In: 33rd International Symposium on Distributed Computing, DISC, pp. 2\u20131217 (2019). https:\/\/doi.org\/10.4230\/LIPICS.DISC.2019.2","DOI":"10.4230\/LIPICS.DISC.2019.2"},{"key":"500_CR12","doi-asserted-by":"publisher","unstructured":"Attiya, H., Casta\u00f1eda, A., Hendler, D.: Nontrivial and universal helping for wait-free queues and stacks. J. Parallel Distributed Comput. 121, 1\u201314 (2018) https:\/\/doi.org\/10.1016\/J.JPDC.2018.06.004","DOI":"10.1016\/J.JPDC.2018.06.004"},{"key":"500_CR13","doi-asserted-by":"publisher","unstructured":"Attiya, H., Enea, C., Welch, J.L.: Impossibility of strongly-linearizable message-passing objects via simulation by single-writer registers. In: Gilbert, S. (ed.) 35th International Symposium on Distributed Computing, DISC 2021, October 4-8, 2021, Freiburg, Germany (Virtual Conference). LIPIcs, vol. 209, pp. 7\u20131718. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.DISC.2021.7","DOI":"10.4230\/LIPICS.DISC.2021.7"},{"key":"500_CR14","doi-asserted-by":"publisher","unstructured":"Attiya, H., Casta\u00f1eda, A., Enea, C.: Strong linearizability using primitives with consensus number 2. In: Gelles, R., Olivetti, D., Kuznetsov, P. (eds.) Proceedings of the 43rd ACM Symposium on Principles of Distributed Computing, PODC 2024, Nantes, France, June 17-21, 2024, pp. 432\u2013442. ACM (2024). https:\/\/doi.org\/10.1145\/3662158.3662790","DOI":"10.1145\/3662158.3662790"},{"key":"500_CR15","doi-asserted-by":"publisher","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pp. 14\u201325. ACM (2004). https:\/\/doi.org\/10.1145\/964001.964003","DOI":"10.1145\/964001.964003"},{"key":"500_CR16","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pp. 651\u2013662. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2677002","DOI":"10.1145\/2676726.2677002"},{"key":"500_CR17","unstructured":"Chan, D.Y.C., Hadzilacos, V., Hu, X., Toueg, S.: An impossibility result on strong linearizability in message-passing systems. CoRR abs\/2108.01651 (2021)"},{"issue":"2","key":"500_CR18","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/S00446-022-00440-Y","volume":"36","author":"A Casta\u00f1eda","year":"2023","unstructured":"Casta\u00f1eda, A., Rajsbaum, S., Raynal, M.: Set-linearizable implementations from read\/write operations: Sets, fetch & increment, stacks and queues with multiplicity. Distributed Comput. 36(2), 89\u2013106 (2023). https:\/\/doi.org\/10.1007\/S00446-022-00440-Y","journal-title":"Distributed Comput."},{"issue":"6","key":"500_CR19","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"500_CR20","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8414, pp. 265\u2013284. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"500_CR21","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785713","DOI":"10.1109\/LICS.2019.8785713"},{"key":"500_CR22","doi-asserted-by":"publisher","unstructured":"Casta\u00f1eda, A., Chockler, G.V., Dongol, B., Lahav, O.: What cannot be implemented on weak memory? In: Alistarh, D. (ed.) 38th International Symposium on Distributed Computing, DISC 2024, October 28 to November 1, 2024, Madrid, Spain. LIPIcs, vol. 319, pp. 11\u201311122. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.DISC.2024.11","DOI":"10.4230\/LIPICS.DISC.2024.11"},{"key":"500_CR23","doi-asserted-by":"publisher","unstructured":"Denysyuk, O., Woelfel, P.: Wait-freedom is harder than lock-freedom under strong linearizability. In: Moses, Y. (ed.) Distributed Computing - 29th International Symposium, DISC 2015, Tokyo, Japan, October 7-9, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9363, pp. 60\u201374. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48653-5_5","DOI":"10.1007\/978-3-662-48653-5_5"},{"key":"500_CR24","doi-asserted-by":"publisher","unstructured":"Dongol, B., Schellhorn, G., Wehrheim, H.: Weak progressive forward simulation is necessary and sufficient for strong observational refinement. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland. LIPIcs, vol. 243, pp. 31\u201313123. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2022.31","DOI":"10.4230\/LIPICS.CONCUR.2022.31"},{"key":"500_CR25","unstructured":"Ellen, F., Sela, G.: Strongly-linearizable bags (2024) arXiv:2411.19365 [cs.DC]"},{"key":"500_CR26","doi-asserted-by":"publisher","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press (1995). https:\/\/doi.org\/10.7551\/MITPRESS\/5803.001.0001","DOI":"10.7551\/MITPRESS\/5803.001.0001"},{"key":"500_CR27","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B.: Model checking algorithms for hyperproperties (invited paper). In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12597, pp. 3\u201316. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_1","DOI":"10.1007\/978-3-030-67067-2_1"},{"issue":"51\u201352","key":"500_CR28","doi-asserted-by":"publisher","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I Filipovic","year":"2010","unstructured":"Filipovic, I., O\u2019Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51\u201352), 4379\u20134398 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.09.021","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"500_CR29","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/S10703-019-00334-Z","volume":"54","author":"B Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. Formal Methods Syst. Des. 54(3), 336\u2013363 (2019). https:\/\/doi.org\/10.1007\/S10703-019-00334-Z","journal-title":"Monitoring hyperproperties. Formal Methods Syst. Des."},{"issue":"1\u20132","key":"500_CR30","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/S00236-019-00358-2","volume":"57","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesis from hyperproperties. Acta Informatica 57(1\u20132), 137\u2013163 (2020). https:\/\/doi.org\/10.1007\/S00236-019-00358-2","journal-title":"Acta Informatica"},{"key":"500_CR31","doi-asserted-by":"publisher","unstructured":"Golab, W.M., Higham, L., Woelfel, P.: Linearizable implementations do not suffice for randomized distributed computation. In: Fortnow, L., Vadhan, S.P. (eds.) Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011, pp. 373\u2013382. ACM (2011). https:\/\/doi.org\/10.1145\/1993636.1993687","DOI":"10.1145\/1993636.1993687"},{"key":"500_CR32","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982, pp. 11\u201320. IEEE Computer Society (1982). https:\/\/doi.org\/10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"issue":"3","key":"500_CR33","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990). https:\/\/doi.org\/10.1145\/78969.78972","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"500_CR34","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/114005.102808","volume":"13","author":"M Herlihy","year":"1991","unstructured":"Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 124\u2013149 (1991). https:\/\/doi.org\/10.1145\/114005.102808","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"500_CR35","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Kirsch, C.M., Payer, H., Sezgin, A., Sokolova, A.: Quantitative relaxation of concurrent data structures. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013, pp. 317\u2013328. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429109","DOI":"10.1145\/2429069.2429109"},{"key":"500_CR36","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (2008)"},{"key":"500_CR37","doi-asserted-by":"publisher","unstructured":"Herlihy, M., Rajsbaum, S.: Set consensus using arbitrary objects (preliminary version). In: Anderson, J.H., Peleg, D., Borowsky, E. (eds.) Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, Los Angeles, California, USA, August 14-17, 1994, pp. 324\u2013333. ACM (1994). https:\/\/doi.org\/10.1145\/197917.198119","DOI":"10.1145\/197917.198119"},{"key":"500_CR38","doi-asserted-by":"publisher","unstructured":"Helmi, M., Higham, L., Woelfel, P.: Strongly linearizable implementations: possibilities and impossibilities. In: Kowalski, D., Panconesi, A. (eds.) ACM Symposium on Principles of Distributed Computing, PODC \u201912, Funchal, Madeira, Portugal, July 16-18, 2012, pp. 385\u2013394. ACM (2012). https:\/\/doi.org\/10.1145\/2332432.2332508","DOI":"10.1145\/2332432.2332508"},{"key":"500_CR39","doi-asserted-by":"publisher","unstructured":"Hwang, S.M., Woelfel, P.: Strongly linearizable linked list and queue. In: Bramas, Q., Gramoli, V., Milani, A. (eds.) 25th International Conference on Principles of Distributed Systems, OPODIS 2021, December 13-15, 2021, Strasbourg, France. LIPIcs, vol. 217, pp. 28\u201312820. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.OPODIS.2021.28","DOI":"10.4230\/LIPICS.OPODIS.2021.28"},{"key":"500_CR40","unstructured":"Li, Z.: Non-blocking Implementations of Queues in Asynchronous Distributed Shared-memory Systems. Master Thesis. University of Toronto (2001). https:\/\/hdl.handle.net\/1807\/16583"},{"key":"500_CR41","doi-asserted-by":"publisher","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. untimed systems. Inf. Comput. 121(2), 214\u2013233 (1995) https:\/\/doi.org\/10.1006\/inco.1995.1134","DOI":"10.1006\/inco.1995.1134"},{"key":"500_CR42","doi-asserted-by":"publisher","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: 1994 IEEE Computer Society Symposium on Research in Security and Privacy, Oakland, CA, USA, May 16-18, 1994, pp. 79\u201393. IEEE Computer Society (1994). https:\/\/doi.org\/10.1109\/RISP.1994.296590","DOI":"10.1109\/RISP.1994.296590"},{"key":"500_CR43","doi-asserted-by":"publisher","unstructured":"Nahum, L., Attiya, H., Ben-Baruch, O., Hendler, D.: Recoverable and detectable fetch &add. In: Bramas, Q., Gramoli, V., Milani, A. (eds.) 25th International Conference on Principles of Distributed Systems, OPODIS 2021, December 13-15, 2021, Strasbourg, France. LIPIcs, vol. 217, pp. 29\u201312917. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.OPODIS.2021.29","DOI":"10.4230\/LIPICS.OPODIS.2021.29"},{"key":"500_CR44","doi-asserted-by":"publisher","unstructured":"Ovens, S., Woelfel, P.: Strongly linearizable implementations of snapshots and other types. In: Robinson, P., Ellen, F. (eds.) Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, Toronto, ON, Canada, July 29 - August 2, 2019, pp. 197\u2013206. ACM (2019). https:\/\/doi.org\/10.1145\/3293611.3331632","DOI":"10.1145\/3293611.3331632"},{"key":"500_CR45","unstructured":"Rady, A.S.: Characterizing Implementations that Preserve Properties of Concurrent Randomized Algorithms. Master\u2019s thesis, York University, Toronto, Canada (2017)"},{"key":"500_CR46","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Wehrheim, H., Derrick, J.: How to prove algorithms linearisable. In: Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science, vol. 7358, pp. 243\u2013259. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_21","DOI":"10.1007\/978-3-642-31424-7_21"},{"key":"500_CR47","doi-asserted-by":"publisher","unstructured":"Shimon, Y.B., Lahav, O., Shoham, S.: Hyperproperty-preserving register specifications. In: Alistarh, D. (ed.) 38th International Symposium on Distributed Computing (DISC). LIPIcs, vol. 319, pp. 8\u20131819. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.DISC.2024.8","DOI":"10.4230\/LIPICS.DISC.2024.8"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00500-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00500-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00500-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T18:02:37Z","timestamp":1758564157000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00500-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,6]]},"references-count":47,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["500"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00500-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2025,8,6]]},"assertion":[{"value":"30 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"29"}}