Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous Programs

Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous Programs
复制标题

Diamont:分布式异步程序不确定性的动态监控

DOI:
10.1007/978-3-030-88494-9_10
复制
发表时间:
2021
期刊:
2021 in Runtime Verification
影响因子:
--
通讯作者:
Misailovic, Sasa
Misailovic, Sasa
中科院分区:
--
文献类型:
--
作者:
Fernando, Vimuth;Joshi, Keyur;Laurel, Jacob;Misailovic, Sasa

文献摘要

相似文献

包括图形分析、物联网、精准农业和媒体处理在内的许多应用领域都对噪声数据进行操作和/或产生近似结果。这些应用程序可以将计算分布在多个(通常是资源受限的)处理单元上。分析这些应用程序的可靠性和准确性是具有挑战性的,因为大多数现有的技术操作特定的固定错误模型,检查个别属性,或只能应用于顺序programmes. Diamont,动态监测系统的不确定性属性在分布式programmes。Diamont程序由通过异步消息传递进行通信的分布式进程组成。Diamont包括动态监视数据中的不确定性的数据库,并提供在运行时对监视的不确定性检查谓词的支持。我们还提出了一个通用的方法来验证运行时系统的可靠性和使用规范序列化的优化。我们实现了Diamont的Go语言的一个子集,并评估了八个程序,从精准农业,图形分析,和媒体处理。我们表明,Diamont可以证明程序输出的重要端到端属性,与以前的工作相比,输入明显更大,执行时间开销适中:对于我们的主要评估输入集,平均为3%(最大为16.3%),对于8倍大的输入,平均为15%。
Many application domains including graph analytics, the Internet-of-Things, precision agriculture, and media processing operate on noisy data and/or produce approximate results. These applications can distribute computation across multiple (often resource-constrained) processing units. Analyzing the reliability and accuracy of such applications is challenging, since most existing techniques operate on specific fixed-error models, check for individual properties, or can only be applied to sequential programs.We present Diamont, a system for dynamic monitoring of uncertainty properties in distributed programs. Diamont programs consist of distributed processes that communicate via asynchronous message passing. Diamont includes datatypes that dynamically monitor uncertainty in data and provides support for checking predicates over the monitored uncertainty at runtime. We also present a general methodology for verifying the soundness of the runtime system and optimizations using canonical sequentialization.We implemented Diamont for a subset of the Go language and evaluated eight programs from precision agriculture, graph analytics, and media processing. We show that Diamont can prove important end-to-end properties of program outputs for significantly larger inputs compared to prior work, with modest execution time overhead: 3% on average (max 16.3%) for our main evaluation input set and 15% on average for 8x larger inputs.