MIO：在输入/输出问题面前实现的多宇宙调试

《Proceedings of the ACM on Programming Languages》：MIO: Multiverse Debugging in the Face of Input/Output

调试微控制器上的非确定性程序存在输入输出操作导致不可达状态难以追溯的问题。本文提出新型多宇宙调试方法，通过语义定义和正确性证明确保仅探索可达状态，并开发MIO原型验证其有效性，在STM32微控制器上实现乐高颜色传感器调试示例。

　　

摘要

在微控制器上调试非确定性程序一直是一个极具挑战性的任务，尤其是当错误出现在不可预测的、依赖于输入的执行路径中时。最近出现了一种称为“多宇宙调试”（multiverse debugging）的方法，它通过允许程序员探索所有可能的执行路径来简化非确定性程序的调试过程。当前的多宇宙调试器支持程序路径的正向和反向遍历，有些调试器甚至可以跳转到之前访问过的状态，并在这些状态空间内分支到其他执行路径。

不幸的是，使用现有的多宇宙调试器调试涉及输入/输出操作的程序时，可能会发现一些无法访问的程序状态，即那些在常规执行过程中不会出现的状态。这会严重阻碍调试过程，因为程序员可能需要花费大量时间来探索和检查这些无法访问的状态；更糟糕的是，程序员可能会错误地认为代码中存在错误，而实际上问题可能是由调试器本身引起的。

本文提出了一种新颖的多宇宙调试方法，该方法能够处理各种输入/输出操作。我们阐述了该方法的语义，并证明了调试器的正确性，确保即使在支持多种输入/输出操作的情况下，调试器也只会探索那些在常规执行过程中能够到达的程序状态。

我们开发了一个名为MIO的原型，利用WARDuino WebAssembly虚拟机来展示我们技术的可行性和效率。作为该方法的一个示例，我们展示了一个由Lego Mindstorms电机和颜色传感器组成的颜色调节器，这直观地展示了我们的方法如何实现对运行在STM32微控制器上的程序的多宇宙调试。