We present a compilation framework in which dimensional type annotations persist through multi-stage MLIR lowering, enabling the compiler to jointly resolve numeric representation selection and deterministic memory management as coeffect properties of a single program semantic graph (PSG). Dimensional inference determines value ranges; value ranges determine representation selection; representation selection determines word width and memory footprint; and memory footprint, combined with escape classification, determines allocation strategy and cross-target transfer fidelity. The Dimensional Type System (DTS) extends Hindley-Milner unification with constraints drawn from finitely generated abelian groups, yielding inference that is decidable in polynomial time, complete, and principal. Where conventional systems erase dimensional annotations before code generation, DTS carries them as compilation metadata through each lowering stage, making them available where representation and memory placement decisions occur. Deterministic Memory Management (DMM), formalized as a coeffect discipline within the same graph, unifies escape analysis and memory placement with the dimensional framework. Escape analysis classifies value lifetimes into four categories (stack-scoped, closure-captured, return-escaping, byref-escaping), each mapping to a verified allocation strategy. We identify implications for auto-differentiation: the dimensional algebra is closed under the chain rule, and forward-mode gradient computation exhibits a coeffect signature that the framework can verify. The practical consequence is a development environment where escape diagnostics, allocation strategy, representation fidelity, and cache locality estimation are design-time views over the compilation graph.


翻译:我们提出一种编译框架,其中维度类型标注在多层次MLIR降级过程中持续存在,使编译器能够将数值表示选择与确定性内存管理作为单一程序语义图(PSG)的协同效应属性联合求解。维度推断确定值域范围;值域范围决定表示选择;表示选择决定字宽与内存占用;内存占用结合逃逸分类决定分配策略与跨目标传输保真度。维度类型系统(DTS)通过有限生成阿贝尔群约束扩展了Hindley-Milner合一算法,实现了多项式时间内可判定、完备且具主体性的推断。传统系统在代码生成前擦除维度标注,而DTS将其作为编译元数据贯穿各降级阶段,使其在表示与内存放置决策点保持可用。确定性内存管理(DMM)在同一图中形式化为协效应规范,将逃逸分析与内存放置统一于维度框架内。逃逸分析将值生命周期分为四类(栈作用域、闭包捕获、返回逃逸、按引用逃逸),每类映射至经验证的分配策略。我们揭示了自动微分的相关启示:维度代数在链式法则下封闭,前向模式梯度计算呈现框架可验证的协效应特征。实际意义在于,逃逸诊断、分配策略、表示保真度与缓存局部性估计成为编译图上的设计时视图,由此构建开发环境。

0
下载
关闭预览

相关内容

【深度语义匹配模型】原理篇二:交互篇
AINLP
16+阅读 · 2020年5月18日
基于模型系统的系统设计
科技导报
10+阅读 · 2019年4月25日
深度学习中Attention Mechanism详细介绍:原理、分类及应用
深度学习与NLP
10+阅读 · 2019年2月18日
推荐系统算法合集,满满都是干货(建议收藏)
七月在线实验室
17+阅读 · 2018年7月23日
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
VIP会员
相关主题
最新内容
网状网络及其在军事领域的运用
专知会员服务
1+阅读 · 今天6:18
无美国参与的欧洲战争方式(万字长文)
专知会员服务
2+阅读 · 今天5:54
《国防领域敏感性分析白皮书》
专知会员服务
1+阅读 · 今天3:42
综述 | 从问答到任务完成:Agent系统与Harness设计
Agentic RL:框架、实践与长程智能体训练
专知会员服务
3+阅读 · 6月24日
重新思考无人机时代的生存能力
专知会员服务
7+阅读 · 6月24日
装甲突击旅:现代战争思考、战斗与组织
专知会员服务
5+阅读 · 6月24日
在人工智能加速决策环境中拓展OODA循环
专知会员服务
7+阅读 · 6月24日
军事欺骗:供作战战术指挥官使用的工具
专知会员服务
5+阅读 · 6月24日
相关VIP内容
相关基金
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员