A Study of Shared-Memory Mutual Exclusion Protocols Using CADP
A Study of Shared-Memory Mutual Exclusion Protocols Using CADP
复制标题
基于CADP的共享内存互斥协议研究
DOI：
10.1007/978-3-642-15898-8_12
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Wendelin Serwe
中科院分区：
文献类型：
--
作者：
Radu Mateescu;Wendelin Serwe
互斥协议是并发系统的基本构建块：实际上，只要必须保护共享资源不受并发非原子访问的影响，就需要这样的协议。因此，共享内存设置中存在互斥协议的许多变体，例如Peterson或Dekker的著名协议。虽然这些协议的功能正确性已被广泛研究，但对它们的非功能方面，如它们的长期性能，相对较少关注。在这篇文章中，我们报告了使用交互马尔可夫链对互斥协议进行性能评估的实验。稳态分析为比较协议提供了一个额外的标准，这是对协议功能特性验证的补充。我们还仔细地重新检查了函数属性，其在基于动作的设置中作为时态逻辑公式的准确公式被证明是相当复杂的。
Mutual exclusion protocols are an essential building block of concurrent systems: indeed, such a protocol is required whenever a shared resource has to be protected against concurrent non-atomic accesses. Hence, many variants of mutual exclusion protocols exist in the shared-memory setting, such as Peterson's or Dekker's well-known protocols. Although the functional correctness of these protocols has been studied extensively, relatively little attention has been paid to their nonfunctional aspects, such as their performance in the long run. In this paper, we report on experiments with the performance evaluation of mutual exclusion protocols using Interactive Markov Chains. Steady-state analysis provides an additional criterion for comparing protocols, which complements the verification of their functional properties. We also carefully re-examined the functional properties, whose accurate formulation as temporal logic formulas in the action-based setting turns out to be quite involved.