{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:05:28Z","timestamp":1762459528603,"version":"3.41.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["291389"],"award-info":[{"award-number":["291389"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A number of high-level languages and libraries have been proposed that offer novel and simple to use abstractions for concurrent, asynchronous, and distributed programming. The execution models that realise them, however, often change over time\u2014whether to improve performance, or to extend them to new language features\u2014potentially affecting behavioural and safety properties of existing programs. This is exemplified by<jats:sc>Scoop<\/jats:sc>, a message-passing approach to concurrent object-oriented programming that has seen multiple changes proposed and implemented, with demonstrable consequences for an idiomatic usage of its core abstraction. We propose a<jats:italic>semantics comparison workbench<\/jats:italic>for<jats:sc>Scoop<\/jats:sc>with fully and semi-automatic tools for analysing and comparing the state spaces of programs with respect to different execution models or semantics. We demonstrate its use in checking the consistency of properties across semantics by applying it to a set of representative programs, and highlighting a deadlock-related discrepancy between the principal execution models of<jats:sc>Scoop<\/jats:sc>. Furthermore, we demonstrate the extensibility of the workbench by generalising the formalisation of an execution model to support recently proposed extensions for distributed programming. Our workbench is based on a modular and parameterisable graph transformation semantics implemented in the<jats:sc>Groove<\/jats:sc>tool. We discuss how graph transformations are leveraged to atomically model intricate language abstractions, how the visual yet\u00a0algebraic nature of the model can be used to ascertain soundness, and highlight how the approach could be applied to similar languages.<\/jats:p>","DOI":"10.1007\/s00165-017-0443-1","type":"journal-article","created":{"date-parts":[[2017,11,13]],"date-time":"2017-11-13T11:28:51Z","timestamp":1510572531000},"page":"163-192","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A semantics comparison workbench for a concurrent, asynchronous, distributed programming language"],"prefix":"10.1145","volume":"30","author":[{"given":"Claudio","family":"Corrodi","sequence":"first","affiliation":[{"name":"Software Composition Group, University of Bern, Bern, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Heu\u00dfner","sequence":"additional","affiliation":[{"name":"Software Technologies Research Group, University of Bamberg, Bamberg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9376-2471","authenticated-orcid":false,"given":"Christopher M.","family":"Poskitt","sequence":"additional","affiliation":[{"name":"Singapore University of Technology and Design, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.5555\/7929"},{"key":"e_1_2_1_2_2_2","unstructured":"Armstrong J Virding R Williams M (1996) Concurrent Programming in ERLANG 2nd edn. Prentice Hall Upper Saddle River"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0033-8"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Backes P Reineke J (2015) Analysis of infinite-state graph transformation systems by cluster abstraction. In: Proceedings of VMCAI 2015 LNCS vol 8931. Springer pp. 135\u2013152","DOI":"10.1007\/978-3-662-46081-8_8"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bogdanas D Rosu G (2015) K-Java: A complete semantics of Java. In: Proceeding of POPL 2015. ACM pp 445\u2013456","DOI":"10.1145\/2775051.2676982"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Corradini A. Dotti F.L. Foss L Ribeiro L (2004) Translating Java code to graph transformation systems. In: Proceedings of ICGT 2004. LNCS vol 3256. Springer pp. 383\u2013398","DOI":"10.1007\/978-3-540-30203-2_27"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Corrodi C Heu\u00dfner A Poskitt CM (2016) A graph-based semantics workbench for concurrent asynchronous programs. In: Proceedings of FASE 2016. LNCS vol 9633. Springer pp 31\u201348","DOI":"10.1007\/978-3-662-49665-7_3"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.08.005"},{"key":"e_1_2_1_2_10_2","unstructured":"Code Contracts. https:\/\/www.microsoft.com\/en-us\/research\/project\/code-contracts\/ accessed: Oct 2017."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Christakis M Sagonas K (2010) Static detection of race conditions in Erlang. In: Proceedings of PADL 2010. Springer pp 119\u2013133","DOI":"10.1007\/978-3-642-11503-5_11"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Dotti FL Duarte LM Foss L Ribeiro L Russi D dos Santos OM (2005) An environment for the development of concurrent object-based applications. In: Proceedings of GraBaTs 2004. ENTCS vol 127. Elsevier pp 3\u201313","DOI":"10.1016\/j.entcs.2004.12.026"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Desai A Garg P Madhusudan P (2014) Natural proofs for asynchronous programs using almost-synchronous reductions. In: Proceedings of OOPLA 2014. ACM pp 709\u2013725","DOI":"10.1145\/2660193.2660211"},{"key":"e_1_2_1_2_14_2","unstructured":"Downey Allen B (October 2017) The Little Book of Semaphores. http:\/\/greenteapress.com\/semaphores\/. Accessed: Oct 2017"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Delzanno G Sangnier A Zavattaro G (2012) Verification of ad hoc networks with node and communication failures. In: Proceedings of FMOODS\/FORTE 2012. LNCS vol 7273. Springer pp 235\u2013250","DOI":"10.1007\/978-3-642-30793-5_15"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1121741"},{"key":"e_1_2_1_2_17_2","unstructured":"Eiffel Documentation: Concurrent Eiffel with SCOOP. https:\/\/www.eiffel.org\/doc\/solutions\/Concurrent%20programming%20with%20SCOOP. Accessed.: Oct 2017."},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Ferreira APL Foss L Ribeiro L (2007) Formal verification of object-oriented graph grammars specifications. In: Proceedings of GT-VC 2006. ENTCS vol 175. Elsevier pp 101\u2013114","DOI":"10.1016\/j.entcs.2007.04.020"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Ferreira APL Ribeiro L (2005) A graph-based semantics for object-oriented programming constructs. In: Proceedings of CTCS 2004. ENTCS vol 122. Elsevier pp 89\u2013104","DOI":"10.1016\/j.entcs.2004.06.053"},{"key":"e_1_2_1_2_20_2","unstructured":"Grand Central Dispatch (GCD) Reference. https:\/\/developer.apple.com\/reference\/dispatch. Accessed: Oct 2017."},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0186-x"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2700072"},{"key":"e_1_2_1_2_23_2","unstructured":"Higham L Kawash J Verwaal N (1997) Defining and comparing memory consistency models. In: Proceedings of PDCS 1997. pp 349\u2013356"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/1552068.1552070"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Heu\u00dfner A Poskitt CM Corrodi C Morandi B (2015) Towards practical graph-based verification for an object-oriented concurrency model. In: Proceeding of GaM 2015. EPTCS vol 181. pp 32\u201347","DOI":"10.4204\/EPTCS.181.3"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Johnsen EB Owe O Axelsen EW (2005) A run-time environment for concurrent objects with asynchronous method calls. In: Proceedings of WRLA 2004. ENTCS vol 117. Elsevier pp 375\u2013392","DOI":"10.1016\/j.entcs.2004.06.012"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.031"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Kitchin D Quark A Cook WR Misra J (2009) The Orc programming language. In: Proceedings of FMOODS\/FORTE 2009. LNCS vol 5522. Springer pp 1\u201325","DOI":"10.1007\/978-3-642-02138-1_1"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Lucanu D Serbanuta T-F Rosu G (2012) K framework distilled. In: Proceedings of WRLA 2012. LNCS vol 7571. Springer pp 31\u201353","DOI":"10.1007\/978-3-642-34005-5_3"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Mador-Haim S Alur R Martin MMK (2010) Generating litmus tests for contrasting memory consistency models. In: Proceedings of CAV 2010. LNCS vol 6174. Springer pp 273\u2013287","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/162685.162705"},{"key":"e_1_2_1_2_34_2","unstructured":"Meyer Bertrand (1997) Object-Oriented Software Construction . Prentice Hall 2nd edition"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Mador-Haim S Maranget L Sarkar S Memarian K Alglave J Owens S Alur R Martin MMK Sewell P Williams D (2012) An axiomatic memory model for power multiprocessors. In: Proceedings of CAV 2012. LNCS vol 7385. Springer pp 495\u2013512","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Morandi B Nanz S Meyer B (2012) Who is accountable for asynchronous exceptions? In: Proceedings of APSEC 2012. IEEE pp 462\u2013471","DOI":"10.1109\/APSEC.2012.48"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Morandi B Nanz S Meyer B (2014) Safe and efficient data sharing for message-passing concurrency. In: Proceedings of COORDINATION 2014. LNCS vol 8459. Springer pp 99\u2013114","DOI":"10.1007\/978-3-662-43376-8_7"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Morandi B Schill M Nanz S Meyer B (2013) Prototyping a concurrency model. In: Proceedings of ACSD 2013. IEEE pp 170\u2013179","DOI":"10.1109\/ACSD.2013.21"},{"key":"e_1_2_1_2_39_2","unstructured":"Nienaltowski P (2007) Practical framework for contract-based concurrent object-oriented programming. Doctoral dissertation ETH Z\u00fcrich"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Nienhuis K Memarian K Sewell P (2016) An operational semantics for C\/C++11 concurrency. In: Proceedings of OOPSLA 2016. ACM pp 111\u2013128","DOI":"10.1145\/2983990.2983997"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0073-8"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Park D \u015etef\u0103nescu A Ro\u015fu G (2015) KJS: A complete formal semantics of JavaScript. In Proceedings of PLDI 2015. ACM pp 346\u2013356","DOI":"10.1145\/2813885.2737991"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Plump D (2012) The design of GP 2. In: Proceedings of WRS 2011 Electronic Proceedings in Theoretical Computer Science vol 82. pp 1\u201316","DOI":"10.4204\/EPTCS.82.1"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/2385016.2385022"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Poskitt CM Plump D (2014) Verifying monadic second-order properties of graph programs. In: Proceedings of ICGT 2014. LNCS vol 8571. Springer pp 33\u201348","DOI":"10.1007\/978-3-319-09108-2_3"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Rensink A (2010) The edge of graph transformation\u2014graphs for behavioural specification. In: Graph transformations and model-driven engineering LNCS vol 5765. Springer Berlin pp 6\u201332","DOI":"10.1007\/978-3-642-17322-6_2"},{"key":"e_1_2_1_2_47_2","unstructured":"Source code repository. https:\/\/bitbucket.org\/ccorrodi\/scoopworkbench."},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Rozenberg G (eds) (1997) Handbook of graph grammars and computing by graph transformation: volume I. Foundations. World Scientific Singapore","DOI":"10.1142\/3303"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Rensink A Zambon E (2009) A type graph model for Java programs. In: Proceedings of FMOODS 2009. LNCS vol 5522. Springer pp 237\u2013242","DOI":"10.1007\/978-3-642-02138-1_18"},{"key":"e_1_2_1_2_51_2","unstructured":"Schill M (2016) Unified interference-free parallel concurrent and distributed programming Dissertation ETH Z\u00fcrich No. 24002."},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Svensson H Fredlund L-\u00c5 Benac Earle C (2010) A unified semantics for future Erlang. In: Proceedings of the 9th ACM SIGPLAN Workshop on Erlang Erlang \u201910. ACM pp 23\u201332","DOI":"10.1145\/1863509.1863514"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Summers AJ M\u00fcller P (2016) Actor services. In: Proceedings of ESOP 2016. LNCS vol 9632. Springer pp 699\u2013726","DOI":"10.1007\/978-3-662-49498-1_27"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Schill M Poskitt CM Meyer B (2016) An interference-free programming model for network objects. In: Proceedings of COORDINATION 2016. LNCS vol 9686. Springer pp 227\u2013244","DOI":"10.1007\/978-3-319-39519-7_14"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Serbanuta Traian-Florin Rosu Grigore (2012) A truly concurrent semantics for the K framework based on graph transformations. In Proc. ICGT 2012 volume 7562 of LNCS pages 294\u2013310. Springer","DOI":"10.1007\/978-3-642-33654-6_20"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Tschannen J Furia CA Nordio M Meyer B (2011) Usable verification of object-oriented programs by combining static and dynamic techniques. In: Proceedings of SEFM 2011. LNCS vol 7041. Springer pp 382\u2013398","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Torshizi F A Ostroff J S Paige R F Chechik M (2009) The SCOOP concurrency model in Java-like languages. In: Proceedings of CPA 2009. Concurrent systems engineering series vol 67. IOS Press pp 7\u201327","DOI":"10.3233\/978-1-60750-065-0-7"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Wickerson J Batty M Sorensen T Constantinides GA (2017) Automatically comparing memory consistency models. In: Proceedings of POPL 2017. ACM pp 190\u2013204","DOI":"10.1145\/3093333.3009838"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"West S Nanz S Meyer B (2010) A modular scheme for deadlock prevention in an object-oriented programming model. In: Proceedings of ICFEM 2010. LNCS vol 6447. Springer pp 597\u2013612","DOI":"10.1007\/978-3-642-16901-4_39"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"West S Nanz S Meyer B (2015) Efficient and reasonable object-oriented concurrency. In: Proceedings of ESEC\/FSE 2015. ACM pp 734\u2013744","DOI":"10.1145\/2786805.2786822"},{"key":"e_1_2_1_2_61_2","unstructured":"Companion website. https:\/\/ccorrodi.bitbucket.io\/scoopgraphs\/."},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Zambon E Rensink A (2011) Using graph transformations and graph abstractions for software verification. In: Proceedings of ICGT-DS 2010. ECEASST vol 38","DOI":"10.1007\/978-3-642-15928-2_37"},{"key":"e_1_2_1_2_63_2","unstructured":"Zambon E Rensink A (2014) Solving the N-Queens problem with GROOVE\u2014towards a compendium of best practices. In: Proceedings of GT-VMT 2014. ECEASST vol 67"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0443-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0443-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0443-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0443-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T00:20:21Z","timestamp":1750983621000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0443-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1]]},"references-count":63,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1007\/s00165-017-0443-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0443-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2018,1]]}}}