Monitoring Partially Synchronous Distributed Systems Using SMT Solvers
Monitoring Partially Synchronous Distributed Systems Using SMT Solvers
复制标题
使用 SMT 求解器监控部分同步分布式系统
DOI：
10.1007/978-3-319-67531-2_17
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
M. Demirbas
中科院分区：
文献类型：
--
作者：
Vidhya Tekken Valapil;Sorrachai Yingchareonthawornchai;S. Kulkarni;E. Torng;M. Demirbas
在本文中，我们讨论了监视部分同步分布式系统以检测潜在错误的可行性，即是由并发过程中的并发和种族条件引起的错误。我们提出了一个监视框架，在该框架中，我们将系统约束和潜在错误建模为满足模式理论（SMT）公式，并使用SMT求解器检测到潜在错误的存在。我们使用两个综合应用程序都证明了我们的框架的可行性，在该应用程序中，潜在错误随机概率随机概率以及涉及对共享资源的独家访问具有微妙的时正时错误的应用。我们说明验证所需的时间如何受到参数（例如通信频率，延迟和时钟偏斜）的影响。我们的结果表明，我们的框架可用于现实生活中的应用程序，并且由于我们的框架使用SMT求解器，因此随着这些求解器随着时间的流逝而变得更加有效，适当的应用程序的范围将增加。
In this paper, we discuss the feasibility of monitoring partially synchronous distributed systems to detect latent bugs, i.e., errors caused by concurrency and race conditions among concurrent processes. We present a monitoring framework where we model both system constraints and latent bugs as Satisfiability Modulo Theories (SMT) formulas, and we detect the presence of latent bugs using an SMT solver. We demonstrate the feasibility of our framework using both synthetic applications where latent bugs occur at any time with random probability and an application involving exclusive access to a shared resource with a subtle timing bug. We illustrate how the time required for verification is affected by parameters such as communication frequency, latency, and clock skew. Our results show that our framework can be used for real-life applications, and because our framework uses SMT solvers, the range of appropriate applications will increase as these solvers become more efficient over time.