Corpse reviver: sound and efficient gradual typing via contract verification
Corpse reviver: sound and efficient gradual typing via contract verification
复制标题
尸体复活者：通过合约验证健全高效的逐步打字
DOI：
10.1145/3434334
复制
发表时间：
2021
影响因子：
--
通讯作者：
Van Horn, David
中科院分区：
文献类型：
--
作者：
Moy, Cameron;Nguyễn, Phúc C.;Tobin-Hochstadt, Sam;Van Horn, David
渐进类型化编程语言允许在非类型化程序中增加静态类型。为了保持可靠性，语言在类型化和非类型化代码之间的边界处插入运行时检查。不幸的是，性能研究表明，这些检查的开销可能高得惊人，这让人们对声音渐进式输入的可行性产生了疑问。在本文中，我们表明，通过建立在现有的工作上的软合同验证，我们可以减少或消除这种overhead.Our关键的洞察力是，而非类型化的代码不能被信任的逐步类型系统，有没有必要只考虑最坏的情况下，优化逐步类型化的程序。相反，我们静态地分析了一个渐进类型化程序的非类型化部分，以证明几乎所有的渐进类型边界所隐含的动态检查都不会失败，并且可以在编译时消除。我们的分析是模块化的，可以应用到程序的任何部分。我们评估了十几个现有的逐渐类型的程序，以前显示有令人望而却步的性能开销，平均开销为2.5倍，最坏的情况下高达80.6倍，并消除在大多数情况下的所有开销，在最坏的情况下只有1.5倍的开销。
Gradually typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries between typed and untyped code. Unfortunately, performance studies have shown that the overhead of these checks can be disastrously high, calling into question the viability of sound gradual typing. In this paper, we show that by building on existing work on soft contract verification, we can reduce or eliminate this overhead.Our key insight is that while untyped code cannot be trusted by a gradual type system, there is no need to consider only the worst case when optimizing a gradually typed program. Instead, we statically analyze the untyped portions of a gradually typed program to prove that almost all of the dynamic checks implied by gradual type boundaries cannot fail, and can be eliminated at compile time. Our analysis is modular, and can be applied to any portion of a program.We evaluate this approach on a dozen existing gradually typed programs previously shown to have prohibitive performance overhead—with a median overhead of 2.5× and up to 80.6× in the worst case—and eliminate all overhead in most cases, suffering only 1.5× overhead in the worst case.
登录
查看更多内容
来自合约的模块化基于集合的分析
影响因子：
--
作者：
P. Meunier;R. Findler;M. Felleisen
通讯作者：
M. Felleisen
具有条件类型的软类型
DOI：
10.1145/174675.177847
发表时间：
1994
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
A. Aiken;E. Wimmers;T. K. Lakshman
通讯作者：
T. K. Lakshman
TypeScript 的具体类型
影响因子：
--
作者：
G. Richards;Francesco Zappa Nardelli;J. Vitek
通讯作者：
J. Vitek
特定功能的分析
影响因子：
1.3
作者：
Leif Andersen;Vincent St;J. Vitek;M. Felleisen
通讯作者：
M. Felleisen
DOI：
10.1007/978-3-540-73589-2_2
发表时间：
2007-07
期刊：
--
影响因子：
--
作者：
Jeremy G. Siek;Walid Taha
通讯作者：
Jeremy G. Siek;Walid Taha