基于多线程监控器的运行时验证

来源：计算机技术与发展杂志2019年第02期北京时间：

作者：陈韬;王明明

摘要：运行时验证是一种轻量级的新型自动化验证技术。运用了该技术的验证软件由两部分组成:一部分是被监控的目标程序;另一部分是监控器。对于基于形式化语言的运行时验证方法主要思想就是输入表示描述事件和性质的形式化规约语法，目标程序。输出插桩好的新程序。插桩好的新程序在遇到需要监控的切点时，就会执行相应的函数去判断是否满足形式化规约语法。然而传统的单线程运行时验证监控器在目标程序需要监控的规约性质比较多的时候，重新生成的程序可能会因为要验证比较多的规约性质，造成程序的性能变慢。文中利用多核并行技术，对原型工具 Movec 进行优化。通过使用串行程序中多个监控器分配到多线程的方法，Clang 编译器的插桩技术和多核任务分配方法，实现了 Movec原型工具的优化。并将优化之后的 Movec 与没有改进之前的进行实验数据对比，实验结果表明采用多线程的运行方法具有很好的效果。

关键词：运行时验证;多线程;源代码插桩;编程语言