Monitoring Atomicity in Concurrent Programs
Monitoring Atomicity in Concurrent Programs
复制标题
监控并发程序中的原子性
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
P. Madhusudan
中科院分区：
文献类型：
--
作者：
Azadeh Farzan;P. Madhusudan
我们研究监测并发程序违反原子的问题。在数据库控制中调度算法背后的发现基本结果，我们构建了用于检查原子性的空间有效监视算法，该算法在活动线程和实体的数量中使用空间多项式，并且与监视的运行长度无关。其次，通过将监视算法解释为有限自动机，我们解决了有限状态并发模型原子的模型检查问题。这（这是第一次）模型，该模型检查有限态态模型的原子性是可以决定的，并且文献中发表的补救措施不正确。最后，我们展示了实验证据，表明我们的原子性监测算法为基准应用提供了大量时间和空间优势。
We study the problem of monitoring concurrent program runs for atomicity violations. Unearthing fundamental results behind scheduling algorithms in database control, we build space-efficient monitoring algorithms for checking atomicity that use space polynomial in the number of active threads and entities, and independent of the length of the run monitored. Second, by interpreting the monitoring algorithm as a finite automaton, we solve the model checking problem for atomicity of finite-state concurrent models. This establishes (for the first time) that model checking finite-state concurrent models for atomicity is decidable, and remedies incorrect proofs published in the literature. Finally, we exhibit experimental evidence that our atomicity monitoring algorithm gives substantial time and space benefits on benchmark applications.