一种基于无锁队列的运行时多线程并行验证方法  

Runtime Multi-thread Parallel Verification Method Based on Lock-free Queues

作　　者：李佳洁 陈哲[1] 陈龙腾 LI Jiajie;CHEN Zhe;CHEN Longteng(Collegeof Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106

出　　处：《小型微型计算机系统》2024年第5期1249-1256,共8页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(62172217)资助;国家自然科学基金委员会-中国民航局民航联合研究基金项目(U1533130)资助;中央高校基本科研业务费人工智能+专项项目(NZ2020019)资助。

摘　　要：运行时验证是一种动态的软件验证技术,主要包括使用形式化规约描述待验证性质、自动生成对应监控器以及监控器的插桩.然而现有的面向C语言程序的运行时验证技术存在一些局限性,主要体现在多监控器的情况下,现有的运行时验证工具只能使用串行的方式处理,这大大降低了验证效率.因此,本文在分析了形式化规约的基础上,提出了一种基于无锁队列的运行时多线程并行验证方法.方法在现有工具MOVEC上实现并在测试集mibench上插桩运行,并与相关工具ACC、AC++和串行机制下的MOVEC进行了对比实验.实验结果表明,本文所实现的基于无锁队列的运行时多线程并行算法可以在有多个监控器的情况下有效地对C语言程序进行并行的运行时验证,且并行验证算法的性能比串行验证算法提升了约83%.Runtime verification is a dynamic software verification technology,which mainly includes the use of formal regulations to describe the properties of the pending verification,the automatic generation of the corresponding monitor,and the monitor plug pile.However,the existing runtime verification technology for C language programs has some limitations,which is mainly reflected in the case of multiple monitors.The existing runtime verification tools can only use serial processing,which greatly reduces the verification efficiency.Therefore,based on the analysis of formal specification,this paper proposes a runtimemulti-threadparallel verification method based on lock-free queues.Method was implemented on the existing tool named MOVEC and run on the test set named mibench.After that,the implemented tool was compared with the related tools ACC,AC++and MOVEC under serial mechanism.The experimental results show that the runtime multi-thread parallel algorithm based on lock-free queues implemented in this paper can effectively perform parallel runtime verification for C language programs with multiple monitors,and the performance of the parallel verification algorithm is about 83%higher than that of the serial verification algorithm.

关 键 词：运行时验证 形式化规约 多线程 无锁队列 C语言程序 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]