RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
CoRR(2024)
摘要
Safe, shared-memory interoperability between languages with 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 WebAssembly and 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 L3, 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要