基于CSP的多线程自动建模和死锁检测研究

龙源期刊网基于CSP的多线程自动死锁检测与建模研究: 高飞武术红姚力来源: 《现代电子技术》 2019年12月;若要: 并发模型主要用于业务流程分析逻辑验证不能很好地支持多线程程序建模. 当前的大多数研究都集中在Java程序的死锁检测上，关于使用POSIX线程库开发的C语言程序的研究也很少. 为了检测POSIX线程库开发的C语言程序是否存在死锁问题，提出了一种用于多线程程序自动建模和死锁检测的形式化验证方法. 首先多线程死锁的例子，根据C ++ CSP框架与源程序之间的联系，实现了从源程序到C ++ CSP框架的语义转换. 然后，为C ++ CSP框架建立了一个通信序列过程（CSP）模型，并对过程分析工具（PAT）对该建立的模型执行死锁检测. 最后通过实例验证了本文自动建模与死锁检测方法的可行性和有效性. 关键字: 多线程建模；死锁检测；语义转换；正式验证；通信顺序过程；过程分析图的分类号: TN911.23？ 34; TP311.5 ;;;;;文件识别码: A ;;;;;;;;;货号: 1004？ 373X（2019）12吗？ 0057？ 05摘要: 并发模型分析主要用于业务流程的逻辑验证多线程死锁的例子，但不能很好地支持多线程程序建模. 由于当前大多数研究主要针对Java程序的死锁检测，因此使用POSIX线程库开发的C语言程序的研究仍然很少. 因此，提出了一种用于多线程程序自动建模和死锁检测的形式化验证方法，以检测用POSIX线程库开发的C语言程序中是否存在死锁现象. 根据C ++ CSP框架与源程序之间的关系，实现了从源程序到C ++ CSP框架的语义转换. 为C ++ CSP框架建立了通信序列过程（CSP）模型. 通过使用过程分析工具（PAT）对已建立的模型进行死锁检测. 通过实例验证了本文提出的自动建模与死锁检测方法的可行性和有效性. 关键字: 多线程建模；死锁检测；语义转换；正式验证；通信顺序过程；流程分析0;介绍;随着多核和异构多处理器的广泛应用，计算机由于硬件支持而同时执行一个或多个线程的能力提高了整体处理性能.

如今，多线程已应用于各种复杂的系统[1？ 2]. 但是，由于争用线程资源或线程推进顺序不正确，多线程也会导致死锁[3]. 卢斯等. 对包括Longyuan Periodical Network MySQL，FireFox，Apache和OpenOffice在内的4种开源软件进行了统计，发现近30％的并行序列缺陷与死锁有关[4]. 死锁会导致系统不稳定. 对于高安全性行业，一旦软件系统陷入僵局，它将带来灾难性的后果. 对并发模型的分析主要用于业务流程系统，对多线程程序的形式验证的研究较少. 马力等. 进行了物联网系统的正式建模和验证[5]；李开宁等. 基于模型驱动框架（MDA）实现业务流程的面向对象建模（BPMN），并对模型进行死锁检测[6]；中国科学技术大学的黄丽提出了一种基于Petri网的多线程死锁检测方法[7]. 用于业务流程和多线程死锁形式验证的现有方法主要由Petri网建模. 因为Petri网适合于表示过程关系，所以它们不能很好地描述数据流，因此对于程序中的复杂过程不适合. 为了为源程序建立合适的模型并提高死锁检测的准确性，本文受到了肯特大学的Neil BROWN和Peter WELCH开发的C ++ CSP框架的启发[8？ [9]，以C ++ CSP框架语言为中介，提出了一种自动多线程建模和死锁检测方法，以实现对多线程程序的形式化验证. 多线程程序对CSP的建模和检测过程如图1所示. 多线程程序到C ++

本文来自电脑杂谈，转载请注明本文网址：
http://www.pc-fly.com/a/jisuanjixue/article-148436-1.html