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 lowering过程中持续存在,使编译器能够将数值表示选择与确定性内存管理作为单一程序语义图(PSG)的协效应属性共同解析。维度推理确定值域;值域确定表示选择;表示选择确定字宽与内存占用;内存占用结合逃逸分类确定分配策略及跨目标传输保真度。维度类型系统(DTS)将Hindley-Milner泛化与有限生成阿贝尔群约束相结合,实现多项式时间可判定、完备且主类型的推理。传统系统在代码生成前擦除维度注解,而DTS将其作为编译元数据贯穿每个lowering阶段,使其在表示与内存布局决策点可用。确定性内存管理(DMM)在同一图中形式化为协效应规约,将逃逸分析与内存布局统一到维度框架中。逃逸分析将值生命周期划分为四类(栈作用域、闭包捕获、返回逃逸、引用逃逸),每类对应已验证的分配策略。我们指出其对自动微分的意义:维度代数在链式法则下封闭,且前向模式梯度计算呈现框架可验证的协效应签名。实际结果是构建了一个开发环境,其中逃逸诊断、分配策略、表示保真度与缓存局部性估计成为编译图上的设计时视图。

0
下载
关闭预览

相关内容

基于模型系统的系统设计
科技导报
10+阅读 · 2019年4月25日
推荐系统算法合集,满满都是干货(建议收藏)
七月在线实验室
17+阅读 · 2018年7月23日
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
23+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
6+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
VIP会员
相关主题
最新内容
以色列-美国-伊朗战争中的无人机:关键要点
专知会员服务
1+阅读 · 47分钟前
《Palantir任务保障性软件安全标准(MA-S2)》
专知会员服务
4+阅读 · 今天13:49
基于声学的无人机检测技术综述
专知会员服务
3+阅读 · 今天13:37
《当代混合战争分析框架:俄乌战争经验教训》
专知会员服务
4+阅读 · 今天13:11
战略前沿人工智能的再思考(中文)
专知会员服务
7+阅读 · 5月29日
《量化地基防空系统间接效应的博弈论方法》
专知会员服务
5+阅读 · 5月29日
“史诗怒火行动”中美军损失的作战飞机
专知会员服务
6+阅读 · 5月29日
ICML 2026 | 理解上下文持续学习中的泛化与遗忘
专知会员服务
5+阅读 · 5月28日
相关VIP内容
相关基金
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
23+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
6+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员