Type-Safe Dynamic Placement with First-Class Placed Values
Journal
Proceedings of the ACM on Programming Languages
Type
journal article
Date Issued
2023-10
Author(s)
Abstract
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.
Language
English
Keywords
Distributed Programming
Multitier Programming
Placement Types
Scala
Dynamic Placement
Union Types
Publisher
ACM
Publisher place
New York, NY, USA
Volume
7
Number
OOPSLA2
Start page
297:1
End page
297:29
Pages
29
Event Location
Cascais, Portugal
File(s)![Thumbnail Image]()
Name
2023_Type-Safe-Dynamic-Placement-with-First-Class-Placed-Values.pdf
Size
642.82 KB
Format
Adobe PDF
Checksum (MD5)
8a10fa5a1c527392520f8cc2e7d22ba9