形态感知计算：拓扑变化后编译器有序的程序状态更新
Morph-Aware Computing: Compiler-Ordered Updates of Program State after Topology Changes
浏览论文内容
中文总结 AI 辅助
针对动态拓扑下程序状态失效问题，提出形态感知计算模型，通过编译器有序插入修复分支，确保状态更新先于拓扑感知，并验证其健全性，显著提升发送目标有效性。
中文摘要 AI 辅助
在无线传感器网络、网状网络、模块化机器人和形状自适应计算机中，计算模块在连接、断开或被替换时，其他模块继续运行并保留其本地状态。在旧布局下计算出的值（如缓存的下一跳）仍留在内存中，但可能不再描述当前布局，因此程序可能向已离开的邻居发送数据而不会出现任何运行时错误。我们提出了形态感知计算，一种编程模型，其中应用程序指定对这种状态的纠正性更新，称为修复，并由编译器决定何时执行。在MorphLang中，修复是处理发送、接收和传感器采样的普通分支旁边的Reconfigure分支。MorphC将MorphLang编译为裸机RISC-V，并在每个普通分支前插入一个守卫，以便每个模块在任何其他分支看到新拓扑之前修复其状态。依赖于此顺序，MorphC还拒绝发送目标可能是字面量或修复不总是刷新的值的发送。对于MorphC生成的代码模型，我们在Rocq中证明了对于任意数量的角色和拓扑变化，修复先于每个后续普通分支。这表明发送目标检查对于核心语言是健全的。在从七个网络栈派生的19个MorphLang程序中，移除修复会使13个声明修复的程序中的10个的目的地有效性恶化，且从未改善。在复现已发布的Contiki-NG缺陷的简化版本中，基于回调的版本在384次变化中的60次后向已离开的父节点发送，而MorphLang版本从未发送。在微基准测试中，守卫每个循环花费12个周期，在FPGA上，从每次提交到向新邻居首次发送的延迟与RTL仿真匹配。
英文摘要
In wireless sensor and mesh networks, modular robots, and shape-adaptive computers, computing modules attach, detach, or are replaced while the others keep running with their local state. A value computed under the old arrangement, such as a cached next hop, stays in memory but may no longer describe the current one, so a program can send to a neighbor that has left without any runtime errors. We present morph-aware computing, a programming model in which the application specifies a corrective update of such state, called a repair, and the compiler decides when it runs. In MorphLang, the repair is a Reconfigure branch next to the ordinary branches that handle sends, receives, and sensor samples. MorphC compiles MorphLang to bare-metal RISC-V and inserts a guard before every ordinary branch, so that each module repairs its state before any other branch sees a new topology. Relying on this order, MorphC also rejects sends whose target may be a literal or a value the repair does not always refresh. For a model of the code MorphC generates, we prove in Rocq that the repair precedes every later ordinary branch for any number of roles and topology changes. This shows that send-target checking is sound for a core language. On 19 MorphLang programs derived from seven network stacks, removing the repair worsens destination validity in ten of the 13 programs that declare one and never improves it. In a reduced reproduction of a released Contiki-NG defect, a callback-based version sends to a departed parent after 60 of 384 changes and the MorphLang version after none. The guards cost 12 cycles per loop in a microbenchmark, and on an FPGA the delay from each commit to the first send to the new neighbor matches RTL simulation.
发表机构
- Tokyo Metropolitan University（东京都立大学）
- Heinrich-Heine-Universität Düsseldorf（杜塞尔多夫大学）
- The University of Tokyo（东京大学）
机构由 AI 辅助整理，请以论文原文为准。
