{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:13:20Z","timestamp":1750220000292,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T00:00:00Z","timestamp":1723593600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2024,9,30]]},"abstract":"<jats:p>\n            Traditional imperative synchronous programming languages heavily rely on a strict separation between data memory and communication signals. Signals can be shared between computational units but cannot be overwritten within a synchronous reaction cycle. Memory can be destructively updated but cannot be shared between concurrent threads. This incoherence makes traditional imperative synchronous languages cumbersome for the programmer. The recent definition of\n            <jats:italic>sequentially constructive<\/jats:italic>\n            synchronous languages offers an improvement. It removes the separation between data memory and communication signals and unifies both through the notion of\n            <jats:italic>clock synchronized shared memory<\/jats:italic>\n            . However, it still depends on global causality analyses, which precludes black-box procedural abstraction. This complicates reuse and composition of software components. This article shows how black-box procedural abstraction can be accommodated inside the sequentially constructive model of computation. We present the Sequentially Constructive Procedural Language (\n            <jats:sans-serif>SCoPL<\/jats:sans-serif>\n            ) and its semantic theory of\n            <jats:italic>policy-constructive<\/jats:italic>\n            synchronous processes.\n            <jats:sans-serif>SCoPL<\/jats:sans-serif>\n            supports black-box procedural abstractions using\n            <jats:italic>policy interfaces<\/jats:italic>\n            to ensure that procedure calls are memory-safe and wait-free and their scheduling is determinate and causal. At the same time, a policy interface constrains the level of freedom for the implementation and subsequent refactoring of a procedure. As a result, policies enable separate compilation and composition of procedures. We present our extensions abstractly as a formal semantics for\n            <jats:sans-serif>SCoPL<\/jats:sans-serif>\n            and motivate it concretely in the context of the open-source, embedded, real-time language\n            <jats:sans-serif>Blech<\/jats:sans-serif>\n            .\n          <\/jats:p>","DOI":"10.1145\/3571585","type":"journal-article","created":{"date-parts":[[2022,11,18]],"date-time":"2022-11-18T12:01:22Z","timestamp":1668772882000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Synchronized Shared Memory and Black-box Procedural Abstraction: Toward a Formal Semantics of Blech"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1072-833X","authenticated-orcid":false,"given":"Friedrich","family":"Gretz","sequence":"first","affiliation":[{"name":"Bosch Corporate Research, Renningen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6387-355X","authenticated-orcid":false,"given":"Franz-Josef","family":"Grosch","sequence":"additional","affiliation":[{"name":"Bosch Corporate Research, Renningen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9562-0576","authenticated-orcid":false,"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[{"name":"University of Bamberg, Bamberg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0787-3181","authenticated-orcid":false,"given":"Stephan","family":"Scheele","sequence":"additional","affiliation":[{"name":"University of Bamberg, Bamberg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,8,14]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/FDL50818.2020.9232942"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/345868.345908"},{"key":"e_1_3_3_4_2","volume-title":"The Synchronous Programming Language Quartz","author":"Schneider K.","year":"2009","unstructured":"K. Schneider. 2009. The Synchronous Programming Language Quartz. Internal Report 375. Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany."},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558636"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/MCSoC.2016.13"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2019.01.014"},{"key":"e_1_3_3_8_2","volume-title":"The Esterel v7 Reference Manual Version v7_30 \u2013 Initial IEEE Standardization Proposal","author":"Technologies Esterel","year":"2005","unstructured":"Esterel Technologies. 2005. The Esterel v7 Reference Manual Version v7_30 \u2013 Initial IEEE Standardization Proposal. Technical Report. Esterel Technologies."},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/1534411"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1811212.1811222"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594310"},{"key":"e_1_3_3_12_2","first-page":"1836","volume-title":"World Congress on Formal Methods","author":"Olivier H.","year":"1999","unstructured":"H. Olivier, P. Laurent, L. B. Yann, and N. Eric. 1999. Cronos: A separate compilation toolset for modular Esterel applications. In World Congress on Formal Methods. Springer, 1836\u20131853."},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0823-8_9"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80443-8"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375657.1375674"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2009.5090916"},{"issue":"2","key":"e_1_3_3_17_2","first-page":"33","article-title":"SCEst: Sequentially constructive Esterel","volume":"17","author":"Smyth Steven","year":"2017","unstructured":"Steven Smyth, Christian Motika, Karsten Rathlev, Reinhard von Hanxleden, and Michael Mendler. 2017. SCEst: Sequentially constructive Esterel. ACM TECS\u2014Special Issue on MEMOCODE 2015 17, 2, Article 33 (Dec.2017), 33:1\u201333:26 pages.","journal-title":"ACM TECS\u2014Special Issue on MEMOCODE 2015"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31585-6_9"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_4"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_13"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0144-6"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2018.00018"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-010-9053-3"},{"key":"e_1_3_3_24_2","first-page":"78","volume-title":"Proceedings of the 36th Annual Symposium on Principles of Programming Languages (POPL\u201909)","author":"Lublinerman R.","year":"2009","unstructured":"R. Lublinerman, C. Szegedy, and S. Tripakis. 2009. Modular code generation from synchronous block diagrams - Modularity vs. code size. In Proceedings of the 36th Annual Symposium on Principles of Programming Languages (POPL\u201909), 78\u201389."},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/646723.702721"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2017.8285623"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/FDL53530.2021.9568373"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.293952"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1542452.1542455"},{"key":"e_1_3_3_30_2","volume-title":"The Constructive Semantics of Pure Esterel","author":"Berry G.","year":"1999","unstructured":"G. Berry. 1999. The Constructive Semantics of Pure Esterel. Draft Book."},{"key":"e_1_3_3_31_2","first-page":"581","volume-title":"Design, Automation & Test in Europe Conference & Exhibition (DATE\u201913)","author":"Hanxleden R. von","year":"2013","unstructured":"R. von Hanxleden, M. Mendler, J. Aguado, B. Duderstadt, I. Fuhrmann, C. Motika, S. Mercer, and O. O\u2019Brien. 2013. Sequentially constructive concurrency\u2014A conservative extension of the synchronous model of computation. In Design, Automation & Test in Europe Conference & Exhibition (DATE\u201913). IEEE, Grenoble, France, 581\u2013586."},{"key":"e_1_3_3_32_2","article-title":"The synchronous hypothesis and synchronous languages","author":"Potop-Butucaru D.","year":"2005","unstructured":"D. Potop-Butucaru, R. Simone, and J.-P. Talpin. 2005. The synchronous hypothesis and synchronous languages. In Embedded Systems: Handbook.","journal-title":"Embedded Systems: Handbook"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-6254-4_2"},{"key":"e_1_3_3_34_2","volume-title":"A Co-iterative Characterization of Synchronous Stream Functions","author":"Caspi P.","year":"1997","unstructured":"P. Caspi and M. Pouzet. 1997. A Co-iterative Characterization of Synchronous Stream Functions. Technical Report Research Report 97-7. VERIMAG, Grenoble."},{"key":"e_1_3_3_35_2","volume-title":"Forum on Specification and Design Languages (FDL\u201920)","author":"Baudart G.","year":"2020","unstructured":"G. Baudart, J.-L. Cola\u00e7o, L. Mandel, M. Mendler, and M. Pouzet. 2020. WiP. A co-iterative synchronous interpreter. In Forum on Specification and Design Languages (FDL\u201920). IEEE."},{"key":"e_1_3_3_36_2","volume-title":"SugarCubes Implementation of Causality","author":"Boussinot Fr\u00e9d\u00e9ric","year":"1998","unstructured":"Fr\u00e9d\u00e9ric Boussinot. 1998. SugarCubes Implementation of Causality. Research Report RR-3487. INRIA."},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3126520"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/11599555_15"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426437"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_16"},{"key":"e_1_3_3_41_2","volume-title":"Foundations of Interface Technologies (FIT\u201905) (ENTCS)","author":"Lee E. A.","year":"2005","unstructured":"E. A. Lee, H. Zheng, and Y. Zhou. 2005. Causality interfaces and compositional causality analysis. In Foundations of Interface Technologies (FIT\u201905) (ENTCS). Elsevier."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1561\/1000000053"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571585","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571585","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:50:55Z","timestamp":1750182655000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571585"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,14]]},"references-count":41,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,9,30]]}},"alternative-id":["10.1145\/3571585"],"URL":"https:\/\/doi.org\/10.1145\/3571585","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2024,8,14]]},"assertion":[{"value":"2022-01-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-10-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}