From 653d6db69f84f23ca2175a9192d2e0f39e85b862 Mon Sep 17 00:00:00 2001 From: Gan Shen Date: Tue, 16 Apr 2024 09:31:37 -0700 Subject: [PATCH] update Dan's talk --- content/lsd-seminar/2024sp.md | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/content/lsd-seminar/2024sp.md b/content/lsd-seminar/2024sp.md index 54566a0..bf2aed7 100644 --- a/content/lsd-seminar/2024sp.md +++ b/content/lsd-seminar/2024sp.md @@ -17,10 +17,10 @@ For spring 2024, we will continue to host the LSD Seminar in a hybrid fashion. Talks will be advertised on the [ucsc-lsd-seminar-announce](https://groups.google.com/g/ucsc-lsd-seminar-announce) (for anyone) and [lsd-group](https://groups.google.com/a/ucsc.edu/g/lsd-group/members) (for UCSC-affiliated people) mailing lists. -| Date | Speaker | Title | -|------- |--------- |--------- | -| [April 5](#april-5) | Luke Geeson | Compiler Testing with Relaxed Memory Models | -| April 12 | Dan Plyukhin | _TBD_ | +| Date | Speaker | Title | +|------- |--------- |--------- | +| [April 5](#april-5) | Luke Geeson | Compiler Testing with Relaxed Memory Models | +| [April 12](#april-12) | Dan Plyukhin | Ozone: Fully Out-of-Order Choreographies | | April 19 | Kuru Ismail | _TBD_ | | April 26 | Jennifer Switzer | _TBD_ | | May 3 | Julian Haas | _TBD_ | @@ -54,6 +54,18 @@ https://lukegeeson.com/talks/2024-01-15-POPL24/ He is based in the compiler teams at Arm in Cambridge where he assists engineers with finding bugs and deploying automated concurrency testing as part of an EPSRC grant. Luke's opinions are his own and Arm does not endorse his work. +## April 12 + +**Speaker:** Dan Plyukhin + +**Title:** Ozone: Fully Out-of-Order Choreographies + +**Abstract:** Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order -- for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs). + +In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered or dropped messages as in the UDP transport protocol. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency by overlapping communication with computation. + +**Bio:** Dan works as a postdoc at the University of Southern Denmark and is receiving his PhD from the University of Illinois at Urbana-Champaign (UIUC). He is the author of the UIGC library for Akka, which provides fault-tolerant resource management for distributed actor systems. Dan’s research focuses on making distributed reactive applications easier to write and reason about. + --- [Archive](../)