一句话：提出支持输入/输出操作的多元宇宙调试方法，并证明其只探索常规执行可达的程序状态。
在微控制器上调试非确定性程序十分困难，尤其当缺陷依赖输入且执行路径不可预测时。现有多元宇宙调试器虽可前后遍历或跳转至任意已访问状态，但遇到输入/输出操作时可能暴露常规执行中不可达的程序状态，误导开发者。本文提出一种支持广泛 I/O 操作的多元宇宙调试新方法，给出其形式语义并证明调试器正确性：即使支持多种 I/O，也只探索常规执行可达的状态。作者基于 WARDuino WebAssembly 虚拟机实现原型 MIO，并用 Lego Mindstorms 电机与颜色传感器构建颜色转盘，在 STM32 微控制器上展示了可行性与效率。
Debugging non-deterministic programs on microcontrollers is notoriously challenging, especially when bugs manifest in unpredictable, input-dependent execution paths. A recent approach, called multiverse debugging, makes it easier to debug non-deterministic programs by allowing programmers to explore all potential execution paths. Current multiverse debuggers enable both forward and backward traversal of program paths, and some facilitate jumping to any previously visited states, potentially branching into alternative execution paths within the state space. Unfortunately, debugging programs that involve input/output operations using existing multiverse debuggers can reveal inaccessible program states, i.e. states which are not encountered during regular execution. This can significantly hinder the debugging process, as the programmer may spend substantial time exploring and examining inaccessible program states, or worse, may mistakenly assume a bug is present in the code, when in fact, the issue is caused by the debugger. This paper presents a novel approach to multiverse debugging, which can accommodate a broad spectrum of input/output operations. We provide the semantics of our approach and prove the correctness of our debugger, ensuring that despite having support for a wide range of input/output operations the debugger will only explore those program states which can be reached during regular execution. We have developed a prototype, called MIO, leveraging the WARDuino WebAssembly virtual machine to demonstrate the feasibility and efficiency of our techniques. As a demonstration of the approach we highlight a color dial built with a Lego Mindstorms motor, and color sensor, providing a tangible example of how our approach enables multiverse debugging for programs running on an STM32 microcontroller.
@article{paperbot2973,
title = {MIO: Multiverse Debugging in the Face of Input/Output},
author = {Tom Lauwaerts and Maarten Steevens and Christophe Scholliers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763136}
}