一句话：提出 Dyno 语言，用一等放置值和放置类型并集，在支持动态放置的同时保持类型安全与放置正确性。
分布式编程语言通常借助多层级编程、编排编程或行为类型在编译期静态保证数据与计算放置的安全性，但动态放置对性能优化、数据本地性、安全与合规等场景至关重要，却与静态推理相冲突。本文提出 Dyno 语言，其类型系统中值被显式放置，同时放置值又是一等值，可被传递并从其他位置引用；作者进一步将动态放置解释为放置类型的并集，并形式化了类型健全性、放置正确性（作为类型健全性的一部分）以及体系结构一致性。案例研究与基准测试表明，Dyno 能在存在动态放置时仍进行静态推理，且性能开销可忽略。作者用 Dyno 重新实现了一个约 7K 行代码的 Android 应用，发现了原实现中的缺陷，并证明该应用的动态放置方式在大型开源应用商店中超过 100 个应用中具有代表性。
Several distributed programming language solutions have been proposed to reason about the placement of data, computations, and peers interaction. Such solutions include, among the others, multitier programming, choreographic programming and various approaches based on behavioral types. These methods statically ensure safety properties thanks to a complete knowledge about placement of data and computation at compile time. In distributed systems, however, dynamic placement of computation and data is crucial to enable performance optimizations, e.g., driven by data locality or in presence of a number of other constraints such as security and compliance regarding data storage location. Unfortunately, in existing programming languages, dynamic placement conflicts with static reasoning about distributed programs: the flexibility required by dynamic placement hinders statically tracking the location of data and computation. In this paper we present Dyno, a programming language that enables static reasoning about dynamic placement. Dyno features a type system where values are explicitly placed, but in contrast to existing approaches, placed values are also first class, ensuring that they can be passed around and referred to from other locations. Building on top of this mechanism, we provide a novel interpretation of dynamic placement as unions of placement types. We formalize type soundness, placement correctness (as part of type soundness) and architecture conformance. In case studies and benchmarks, our evaluation shows that Dyno enables static reasoning about programs even in presence of dynamic placement, ensuring type safety and placement correctness of programs at negligible performance cost. We reimplement an Android app with ∼ 7 K LOC in Dyno, find a bug in the existing implementation, and show that the app's approach is representative of a common way to implement dynamic placement found in over 100 apps in a large open-source app store.
@article{paperbot1874,
title = {Type-Safe Dynamic Placement with First-Class Placed Values},
author = {George Zakhour and Pascal Weisenburger and Guido Salvaneschi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622873}
}