Debugging nondeterministic programs is inherently difficult, particularly in microcontroller environments where execution paths can diverge unpredictably due to external sensor inputs. Traditional debugging techniques often fail to capture or reproduce this nondeterministic behavior effectively. Multiverse debugging has emerged as a compelling technique to debug nondeterministic programs, allowing developers to systematically explore all possible execution paths. Unfortunately, current multiverse debuggers are snapshot-based and most operate over a model of the program, limiting their use for debugging resource-constrained microcontrollers. Additionally, current multiverse debuggers, even ones specifically designed for microcontrollers suffer from state explosion making the state space overwhelming during debugging. To address these challenges, we introduce a trace-based multiverse debugger with a novel state-space reduction technique based on concolic execution. Our approach interleaves concolic analysis with live debugging to identify input values that define unique program paths. This hybrid technique efficiently prunes redundant paths from the state space while ensuring full code coverage. Unlike MIO, a recently published multiverse debugger for microcontrollers that focuses on IO consistency, our approach directly targets state explosion by leveraging concolic execution and uses a trace-based approach, significantly reducing the memory and communication overhead. We implemented a prototype using the WARDuino WebAssembly VM, demonstrating the feasibility and efficiency of our approach in real-world scenarios. Our results highlight substantial reductions in the state space compared to traditional multiverse debugging. This makes multiverse debugging more accessible and efficient for developers working with complex, nondeterministic programs running on microcontrollers.

翻译：调试非确定性程序本质上十分困难，特别是在微控制器环境中，执行路径可能因外部传感器输入而不可预测地发散。传统调试技术往往难以有效捕获或复现这种非确定性行为。多宇宙调试已发展为一种引人注目的技术，用于调试非确定性程序，使开发者能够系统性地探索所有可能的执行路径。然而，当前的多宇宙调试器基于快照，且大多在程序模型上运行，限制了其在资源受限微控制器调试中的应用。此外，即便专门为微控制器设计的多宇宙调试器，也面临状态爆炸问题，导致调试时的状态空间过于庞大。为解决这些挑战，我们提出了一种基于轨迹的多宇宙调试器，并引入了一种基于共形执行的新型状态空间缩减技术。该方法将共形分析与实时调试相结合，以识别定义唯一程序路径的输入值。这种混合技术能够高效地从状态空间中剪枝冗余路径，同时确保代码全覆盖。与近期发布的专注于IO一致性的微控制器多宇宙调试器MIO不同，我们的方法直接通过利用共形执行来应对状态爆炸，并采用基于轨迹的方式，显著降低了内存与通信开销。我们使用WARDuino WebAssembly虚拟机实现了原型系统，验证了该方法在实际场景中的可行性与效率。结果表明，与传统的多宇宙调试相比，状态空间得到了显著缩减。这使得多宇宙调试对于在微控制器上运行复杂非确定性程序的开发者而言更加易用且高效。