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虚拟机实现了原型系统，在真实场景中验证了方法的可行性与效率。实验结果表明，与传统的多宇宙调试相比，我们的方法实现了显著的状态空间缩减。这使得多宇宙调试对处理微控制器上复杂非确定性程序的开发者而言更加便捷高效。