乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T22:10:05Z","timestamp":1729548605019,"version":"3.28.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"Region inference is a type-based program analysis that takes a non-annotated program as input and constructs a program that explicitly manages memory allocation and deallocation by dividing the heap into a stack of regions, each of which can grow and shrink independently from other regions, using constant-time operations.<\/jats:p>Whereas region-based memory management has shown useful in the contexts of explicit region-based memory management, and in particular, in combination with parallel execution of code, combining region inference with techniques for higher-order parallel programming has not been investigated.<\/jats:p>In this paper, we present an implementation of a fork-join parallel construct suitable for a compiler based on region inference. We present a minimal higher-order language incorporating the parallel construct, including typing rules and a dynamic semantics for the language, and demonstrate type soundness. We present a novel effect-based region-protection inference algorithm and discuss benefits and shortcomings of the approach. We also describe an efficient implementation embedded in the MLKit Standard ML compiler. Finally, we evaluate the approach and the implementation based on a number of parallel benchmarks, and thereby demonstrate that the technique effectively utilises multi-core architectures in a higher-order functional setting.<\/jats:p>","DOI":"10.1145\/3591256","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"884-906","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Parallelism in a Region Inference Context"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-6061-5993","authenticated-orcid":false,"given":"Martin","family":"Elsman","sequence":"first","affiliation":[{"name":"University of Copenhagen, Denmark"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-1195-9722","authenticated-orcid":false,"given":"Troels","family":"Henriksen","sequence":"additional","affiliation":[{"name":"University of Copenhagen, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207137"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582448"},{"volume-title":"Making Reliable Distributed Systems in the Presence of Software Errors. Ph. D. Dissertation","author":"Armstrong Joe","key":"e_1_2_2_3_1","unstructured":"Joe Armstrong . 2003. Making Reliable Distributed Systems in the Presence of Software Errors. Ph. D. Dissertation . The Royal Institute of Technology , Stockholm, Sweden . Joe Armstrong. 2003. Making Reliable Distributed Systems in the Presence of Software Errors. Ph. D. Dissertation. The Royal Institute of Technology, Stockholm, Sweden."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434299"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237771"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1086\/260062"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781168"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/42288.214372"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926354.1926358"},{"key":"e_1_2_2_10_1","unstructured":"E. Cooper and G. Morrisett. 1990. Adding Threads to Standard ML. Carnegie Mellon University Department of Computer Science. Technical report E. Cooper and G. Morrisett. 1990. Adding Threads to Standard ML. Carnegie Mellon University Department of Computer Science. Technical report"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492408.2492415"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2247684.2247695"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604190"},{"volume-title":"A Framework for Cut-Off Incremental Recompilation and Inter-Module Optimization","author":"Elsman Martin","key":"e_1_2_2_14_1","unstructured":"Martin Elsman . 2008. A Framework for Cut-Off Incremental Recompilation and Inter-Module Optimization . IT University of Copenhagen , Rued Langgaards Vej 7, DK-2300 Copenhagen S, Denmark. Martin Elsman. 2008. A Framework for Cut-Off Incremental Recompilation and Inter-Module Optimization. IT University of Copenhagen, Rued Langgaards Vej 7, DK-2300 Copenhagen S, Denmark."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591229"},{"volume-title":"An Optimizing Backend for the ML Kit Using a Stack of Regions. Student Project 95-7-8","author":"Elsman Martin","key":"e_1_2_2_16_1","unstructured":"Martin Elsman and Niels Hallenberg . 1995. An Optimizing Backend for the ML Kit Using a Stack of Regions. Student Project 95-7-8 , University of Copenhagen (DIKU) . Martin Elsman and Niels Hallenberg. 1995. An Optimizing Backend for the ML Kit Using a Stack of Regions. Student Project 95-7-8, University of Copenhagen (DIKU)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36388-2_7"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000010"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7810545"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24836-1_16"},{"key":"e_1_2_2_21_1","volume-title":"Proceedings of the ML Family Workshop (ML \u201918)","author":"Elsman Martin","year":"2018","unstructured":"Martin Elsman , Philip Munksgaard , and Ken Friis Larsen . 2018 . Experience Report: Type-Safe Multi-Tier Programming with Standard ML Modules . In Proceedings of the ML Family Workshop (ML \u201918) . Martin Elsman, Philip Munksgaard, and Ken Friis Larsen. 2018. Experience Report: Type-Safe Multi-Tier Programming with Standard ML Modules. In Proceedings of the ML Family Workshop (ML \u201918)."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385994"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411224"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378815"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708020"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1248648.1248654"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512547"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065944.1065952"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062354"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2930957.2930958"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375637"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034685"},{"volume-title":"Compiling with Types. Ph. D. Dissertation. School of Computer Science","author":"Morrisett Greg","key":"e_1_2_2_35_1","unstructured":"Greg Morrisett . 1995. Compiling with Types. Ph. D. Dissertation. School of Computer Science , Carnegie Mellon University , Pittsburgh, PA 15213. Greg Morrisett. 1995. Compiling with Types. Ph. D. Dissertation. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44471-9_10"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968867"},{"key":"e_1_2_2_38_1","volume-title":"Draft Proceedings of the ML family workshop (ML \u20192017)","author":"Ohori Atsushi","year":"2017","unstructured":"Atsushi Ohori , Kenjiro Taura , and Katsuhiro Ueno . 2017 . Making SML# a General-purpose High-performance Language . In Draft Proceedings of the ML family workshop (ML \u20192017) . Atsushi Ohori, Kenjiro Taura, and Katsuhiro Ueno. 2017. Making SML# a General-purpose High-performance Language. In Draft Proceedings of the ML family workshop (ML \u20192017)."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951935"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596588"},{"key":"e_1_2_2_41_1","volume-title":"Efficient Region-Based Memory Management for Resource-limited Real-Time Embedded Systems. In Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems.","author":"Salagnac Guillaume","year":"2006","unstructured":"Guillaume Salagnac , Chaker Nakhli , Christophe Rippert , and Sergio Yovine . 2006 . Efficient Region-Based Memory Management for Resource-limited Real-Time Embedded Systems. In Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems. Guillaume Salagnac, Chaker Nakhli, Christophe Rippert, and Sergio Yovine. 2006. Efficient Region-Based Memory Management for Resource-limited Real-Time Embedded Systems. In Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2017.2766062"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/224964.224987"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408995"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708046.1708059"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000161"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.02.003"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291894"},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","unstructured":"Mads Tofte and Lars Birkedal. 2000. Unification and Polymorphism in Region Inference. Proof Language and Interaction. Essays in Honour of Robin Milner May (25 pages) Mads Tofte and Lars Birkedal. 2000. Unification and Polymorphism in Region Inference. Proof Language and Interaction. Essays in Honour of Robin Milner May (25 pages)","DOI":"10.7551\/mitpress\/5641.003.0020"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:LISP.0000029446.78563.a4"},{"key":"e_1_2_2_51_1","volume-title":"Tommy H\u00f8jfeld Olesen, and Peter Sestoft","author":"Tofte Mads","year":"2022","unstructured":"Mads Tofte , Lars Birkedal , Martin Elsman , Niels Hallenberg , Tommy H\u00f8jfeld Olesen, and Peter Sestoft . 2022 . Programming with Regions in the MLKit (Revised for Version 4.7.2). IT University of Copenhagen , Denmark. Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy H\u00f8jfeld Olesen, and Peter Sestoft. 2022. Programming with Regions in the MLKit (Revised for Version 4.7.2). IT University of Copenhagen, Denmark."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018743.3018746"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159877"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547646"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371115"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591256","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T21:30:38Z","timestamp":1729546238000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591256"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":56,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591256"],"URL":"https:\/\/doi.org\/10.1145\/3591256","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}