分享的三大优化
Three Optimisations for Sharing
摘要:
为了提高精度和效率,共享分析应同时跟踪自由度和线性。这些组合域的抽象统一算法是次优的,因此有提高精度的余地。本文结合自由度和线性度提出了跟踪共享的三种优化方法。方程和共享抽象之间的一种新的连接被用来建立这些优化的正确性,即使在理性树的存在。提出了一种修剪中间共享抽象以提高效率的方法。优化是轻量级的,因此这些优化中的一些(如果不是全部)将对实现者感兴趣。
英文摘要:
In order to improve precision and efficiency sharing analysis should track both freeness and linearity. The abstract unification algorithms for these combined domains are suboptimal, hence there is scope for improving precision. This paper proposes three optimisations for tracing sharing in combination with freeness and linearity. A novel connection between equations and sharing abstractions is used to establish correctness of these optimisations even in the presence of rational trees. A method for pruning intermediate sharing abstractions to improve efficiency is also proposed. The optimisations are lightweight and therefore some, if not all, of these optimisations will be of interest to the implementor.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。