尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。
Safe, shared-memory interoperability between languageswith different type systems and memory-safety guarantees is an intricate problem as crossing language boundaries may result in memory-safety violations. In this paper, we present RichWasm, a novel richly typed intermediate language designed to serve as a compilation target for typed high-level languages with different memory-safety guarantees. RichWasm is based on WebAssemblyand enables safe shared-memory interoperability by incorporating a variety of type features that support fine-grained memory ownership and sharing. RichWasm is rich enough to serve as a typed compilation target for both typed garbage-collected languages and languages with an ownership-based type system and manually managed memory. We demonstrate this by providing compilers from core ML and L 3 , a type-safe language with strong updates, to RichWasm. RichWasm is compiled to regular Wasm, allowing for use in existing environments. We formalize RichWasm in Coq and prove type safety.
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{FitzgibbonsPMTMA24,
title = {RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly},
author = {Michael Fitzgibbons and Zoe Paraskevopoulou and Noble Mushtak and Michelle Thalakottur and Jose Sulaiman Manzur and Amal Ahmed},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656444}
}