{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T15:33:52Z","timestamp":1768404832582,"version":"3.49.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF Award CCF","award":["2124184"],"award-info":[{"award-number":["2124184"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>While serverless platforms substantially simplify the provisioning, configuration, and management of cloud applications, implementing correct services on top of these platforms can present significant challenges to programmers. For example, serverless infrastructures introduce a host of failure modes that are not present in traditional deployments. Individual serverless instances can fail while others continue to make progress, correct but slow instances can be killed by the cloud provider as part of resource management, and providers will often respond to such failures by re-executing requests. For functions with side-effects, these scenarios can create behaviors that are not observable in serverful deployments.<\/jats:p>\n          <jats:p>In this paper, we propose mu2sls, a framework for implementing microservice applications on serverless using standard Python code with two extra primitives: transactions and asynchronous calls. Our framework orchestrates user-written services to address several challenges, such as failures and re-executions, and provides formal guarantees that the generated serverless implementations are correct. To that end, we present a novel service specification abstraction and formalization of serverless implementations that facilitate reasoning about the correctness of a given application\u2019s serverless implementation. This formalization forms the basis of the mu2sls prototype, which we then use to develop a few real-world microservice applications and show that the performance of the generated serverless implementations achieves significant scalability (3-5\u00d7 the throughput of a sequential implementation) while providing correctness guarantees in the context of faults, re-execution, and concurrency.<\/jats:p>","DOI":"10.1145\/3571206","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"367-395","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Executing Microservice Applications on Serverless, Correctly"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8984-6648","authenticated-orcid":false,"given":"Konstantinos","family":"Kallas","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5759-5637","authenticated-orcid":false,"given":"Haoran","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1733-7083","authenticated-orcid":false,"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3798-5590","authenticated-orcid":false,"given":"Sebastian","family":"Angel","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA \/ Microsoft Research, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7683-208X","authenticated-orcid":false,"given":"Vincent","family":"Liu","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328449"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3472883.3486977"},{"key":"e_1_2_1_3_1","unstructured":"2020. AWS Step Functions. https:\/\/docs.aws.amazon.com\/step-functions\/latest\/dg\/welcome.html \t\t\t\t  2020. AWS Step Functions. https:\/\/docs.aws.amazon.com\/step-functions\/latest\/dg\/welcome.html"},{"key":"e_1_2_1_4_1","unstructured":"2022. FoundationDB. https:\/\/www.foundationdb.org\/ \t\t\t\t  2022. FoundationDB. https:\/\/www.foundationdb.org\/"},{"key":"e_1_2_1_5_1","first-page":"196","article-title":"The development of Erlang","volume":"97","author":"Armstrong Joe","year":"1997","unstructured":"Joe Armstrong . 1997 . The development of Erlang . In ICFP. 97 , 196 \u2013 203 . Joe Armstrong. 1997. The development of Erlang. In ICFP. 97, 196\u2013203.","journal-title":"ICFP."},{"key":"e_1_2_1_6_1","unstructured":"2022. AWS Lambda. https:\/\/aws.amazon.com\/lambda\/ \t\t\t\t  2022. AWS Lambda. https:\/\/aws.amazon.com\/lambda\/"},{"key":"e_1_2_1_7_1","unstructured":"Jonas Bon\u00e9r. 2020. Towards Stateful Serverless. https:\/\/www.youtube.com\/watch?v=DVTf5WQlgB8 \t\t\t\t  Jonas Bon\u00e9r. 2020. Towards Stateful Serverless. https:\/\/www.youtube.com\/watch?v=DVTf5WQlgB8"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485510"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038916.2038932"},{"key":"e_1_2_1_10_1","unstructured":"2020. Using Durable Objects Cloudflare Docs. https:\/\/developers.cloudflare.com\/workers\/learning\/using-durable-objects \t\t\t\t  2020. Using Durable Objects Cloudflare Docs. https:\/\/developers.cloudflare.com\/workers\/learning\/using-durable-objects"},{"key":"e_1_2_1_11_1","unstructured":"2020. Workers Durable Objects Beta: A New Approach to Stateful Serverless. https:\/\/blog.cloudflare.com\/introducing-workers-durable-objects\/ \t\t\t\t  2020. Workers Durable Objects Beta: A New Approach to Stateful Serverless. https:\/\/blog.cloudflare.com\/introducing-workers-durable-objects\/"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (ATC). 1\u201314","author":"Duplyakin Dmitry","year":"2019","unstructured":"Dmitry Duplyakin , Robert Ricci , Aleksander Maricq , Gary Wong , Jonathon Duerig , Eric Eide , Leigh Stoller , Mike Hibler , David Johnson , Kirk Webb , Aditya Akella , Kuangching Wang , Glenn Ricart , Larry Landweber , Chip Elliott , Michael Zink , Emmanuel Cecchet , Snigdhaswin Kar , and Prabodh Mishra . 2019 . The Design and Operation of CloudLab . In Proceedings of the USENIX Annual Technical Conference (ATC). 1\u201314 . https:\/\/www.flux.utah.edu\/paper\/duplyakin-atc19 Dmitry Duplyakin, Robert Ricci, Aleksander Maricq, Gary Wong, Jonathon Duerig, Eric Eide, Leigh Stoller, Mike Hibler, David Johnson, Kirk Webb, Aditya Akella, Kuangching Wang, Glenn Ricart, Larry Landweber, Chip Elliott, Michael Zink, Emmanuel Cecchet, Snigdhaswin Kar, and Prabodh Mishra. 2019. The Design and Operation of CloudLab. In Proceedings of the USENIX Annual Technical Conference (ATC). 1\u201314. https:\/\/www.flux.utah.edu\/paper\/duplyakin-atc19"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference (USENIX ATC \u201919)","author":"Fouladi Sadjad","year":"2019","unstructured":"Sadjad Fouladi , Francisco Romero , Dan Iter , Qian Li , Shuvo Chatterjee , Christos Kozyrakis , Matei Zaharia , and Keith Winstein . 2019 . From Laptop to Lambda: Outsourcing Everyday Jobs to Thousands of Transient Functional Containers . In Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference (USENIX ATC \u201919) . USENIX Association, USA. 475\u2013488. isbn:978 1939133038 https:\/\/dl.acm.org\/doi\/10.5555\/3358807.3358848 Sadjad Fouladi, Francisco Romero, Dan Iter, Qian Li, Shuvo Chatterjee, Christos Kozyrakis, Matei Zaharia, and Keith Winstein. 2019. From Laptop to Lambda: Outsourcing Everyday Jobs to Thousands of Transient Functional Containers. In Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference (USENIX ATC \u201919). USENIX Association, USA. 475\u2013488. isbn:9781939133038 https:\/\/dl.acm.org\/doi\/10.5555\/3358807.3358848"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 14th USENIX Conference on Networked Systems Design and Implementation (NSDI\u201917)","author":"Fouladi Sadjad","year":"2017","unstructured":"Sadjad Fouladi , Riad S. Wahby , Brennan Shacklett , Karthikeyan Vasuki Balasubramaniam , William Zeng , Rahul Bhalerao , Anirudh Sivaraman , George Porter , and Keith Winstein . 2017 . Encoding, Fast and Slow: Low-Latency Video Processing Using Thousands of Tiny Threads . In Proceedings of the 14th USENIX Conference on Networked Systems Design and Implementation (NSDI\u201917) . USENIX Association, USA. 363\u2013376. isbn:978 1931971379 https:\/\/dl.acm.org\/doi\/10.5555\/3154630.3154660 Sadjad Fouladi, Riad S. Wahby, Brennan Shacklett, Karthikeyan Vasuki Balasubramaniam, William Zeng, Rahul Bhalerao, Anirudh Sivaraman, George Porter, and Keith Winstein. 2017. Encoding, Fast and Slow: Low-Latency Video Processing Using Thousands of Tiny Threads. In Proceedings of the 14th USENIX Conference on Networked Systems Design and Implementation (NSDI\u201917). USENIX Association, USA. 363\u2013376. isbn:9781931971379 https:\/\/dl.acm.org\/doi\/10.5555\/3154630.3154660"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304013"},{"key":"e_1_2_1_16_1","unstructured":"2022. Google Cloud Functions. https:\/\/cloud.google.com\/functions \t\t\t\t  2022. Google Cloud Functions. https:\/\/cloud.google.com\/functions"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2414639.2414641"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_19_1","unstructured":"2022. Hypercorn. https:\/\/pgjones.gitlab.io\/hypercorn \t\t\t\t  2022. Hypercorn. https:\/\/pgjones.gitlab.io\/hypercorn"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.03.001"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360575"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483541"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446701"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127479.3128601"},{"key":"#cr-split#-e_1_2_1_25_1.1","unstructured":"Eric Jonas Johann Schleier-Smith Vikram Sreekanti Chia-Che Tsai Anurag Khandelwal Qifan Pu Vaishaal Shankar Joao Carreira Karl Krauth and Neeraja Yadwadkar. 2019. Cloud programming simplified: A berkeley view on serverless computing. arXiv preprint arXiv:1902.03383 https:\/\/doi.org\/10.48550\/arXiv.1902.03383 10.48550\/arXiv.1902.03383"},{"key":"#cr-split#-e_1_2_1_25_1.2","unstructured":"Eric Jonas Johann Schleier-Smith Vikram Sreekanti Chia-Che Tsai Anurag Khandelwal Qifan Pu Vaishaal Shankar Joao Carreira Karl Krauth and Neeraja Yadwadkar. 2019. Cloud programming simplified: A berkeley view on serverless computing. arXiv preprint arXiv:1902.03383 https:\/\/doi.org\/10.48550\/arXiv.1902.03383"},{"key":"e_1_2_1_26_1","volume-title":"13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18)","author":"Klimovic Ana","year":"2018","unstructured":"Ana Klimovic , Yawen Wang , Patrick Stuedi , Animesh Trivedi , Jonas Pfefferle , and Christos Kozyrakis . 2018 . Pocket: Elastic ephemeral storage for serverless analytics . In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18) . 427\u2013444. https:\/\/dl.acm.org\/doi\/10.5555\/3291168.3291200 Ana Klimovic, Yawen Wang, Patrick Stuedi, Animesh Trivedi, Jonas Pfefferle, and Christos Kozyrakis. 2018. Pocket: Elastic ephemeral storage for serverless analytics. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18). 427\u2013444. https:\/\/dl.acm.org\/doi\/10.5555\/3291168.3291200"},{"key":"e_1_2_1_27_1","unstructured":"2022. Knative. https:\/\/knative.dev \t\t\t\t  2022. Knative. https:\/\/knative.dev"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527324"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3401025.3401731"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3472883.3487005"},{"key":"e_1_2_1_31_1","unstructured":"2022. Azure Functions. https:\/\/learn.microsoft.com\/en-us\/azure\/azure-functions\/functions-overview \t\t\t\t  2022. Azure Functions. https:\/\/learn.microsoft.com\/en-us\/azure\/azure-functions\/functions-overview"},{"key":"e_1_2_1_32_1","unstructured":"2022. Minikube. https:\/\/minikube.sigs.k8s.io \t\t\t\t  2022. Minikube. https:\/\/minikube.sigs.k8s.io"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328448"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452520.1452527"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102980.3102986"},{"key":"e_1_2_1_36_1","unstructured":"Benjamin C Pierce Chris Casinghino Marco Gaboardi Michael Greenberg C\u0103t\u0103lin Hri\u0163cu Vilhelm Sj\u00f6berg and Brent Yorgey. 2010. Software foundations. Webpage: http:\/\/www.cis.upenn.edu\/bcpierce\/sf\/current\/index.html. \t\t\t\t  Benjamin C Pierce Chris Casinghino Marco Gaboardi Michael Greenberg C\u0103t\u0103lin Hri\u0163cu Vilhelm Sj\u00f6berg and Brent Yorgey. 2010. Software foundations. Webpage: http:\/\/www.cis.upenn.edu\/bcpierce\/sf\/current\/index.html."},{"key":"e_1_2_1_37_1","unstructured":"2022. Quart. https:\/\/pgjones.gitlab.io\/quart \t\t\t\t  2022. Quart. https:\/\/pgjones.gitlab.io\/quart"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429100"},{"key":"e_1_2_1_39_1","unstructured":"2022. Ray Core: A faster simpler approach to parallel Python. https:\/\/ray.io\/ray-core \t\t\t\t  2022. Ray Core: A faster simpler approach to parallel Python. https:\/\/ray.io\/ray-core"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3342195.3387535"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407836"},{"key":"e_1_2_1_42_1","unstructured":"2022. Temporal. https:\/\/temporal.io\/ \t\t\t\t  2022. Temporal. https:\/\/temporal.io\/"},{"key":"e_1_2_1_43_1","unstructured":"Gil Tene. 2022. wrk2. https:\/\/github.com\/giltene\/wrk2 \t\t\t\t  Gil Tene. 2022. wrk2. https:\/\/github.com\/giltene\/wrk2"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_18"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110280"},{"key":"e_1_2_1_46_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Zhang Haoran","year":"2020","unstructured":"Haoran Zhang , Adney Cardoza , Peter Baile Chen , Sebastian Angel , and Vincent Liu . 2020 . Fault-tolerant and transactional stateful serverless workflows . In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) . 1187\u20131204. https:\/\/dl.acm.org\/doi\/10.5555\/3488766.3488833 Haoran Zhang, Adney Cardoza, Peter Baile Chen, Sebastian Angel, and Vincent Liu. 2020. Fault-tolerant and transactional stateful serverless workflows. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). 1187\u20131204. https:\/\/dl.acm.org\/doi\/10.5555\/3488766.3488833"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419111.3421277"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571206","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571206","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571206"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571206"],"URL":"https:\/\/doi.org\/10.1145\/3571206","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}