基于多线程监控器的运行时验证
|
摘要
运行时验证是一种轻量级的新型自动化验证技术。运用了该技术的验证软件由两部分组成:一部分是被监控的目标程序;另一部分是监控器。对于基于形式化语言的运行时验证方法主要思想就是输入表示描述事件和性质的形式化规约语法,目标程序。输出插桩好的新程序。插桩好的新程序在遇到需要监控的切点时,就会执行相应的函数去判断是否满足形式化规约语法。然而传统的单线程运行时验证监控器在目标程序需要监控的规约性质比较多的时候,重新生成的程序可能会因为要验证比较多的规约性质,造成程序的性能变慢。文中利用多核并行技术,对原型工具Movec进行优化。通过使用串行程序中多个监控器分配到多线程的方法,Clang编译器的插桩技术和多核任务分配方法,实现了Movec原型工具的优化。并将优化之后的Movec与没有改进之前的进行实验数据对比,实验结果表明采用多线程的运行方法具有很好的效果。
Runtime verification is a new lightweight automatic verification technique.The verification software used in this technology is composed of two parts:one part is the monitored target program;the other is the monitor.The main idea of the runtime verification method based on formalized language is to input a formal specification syntax that represents events and properties and target program,and output a new program.The new program with inserting pile will execute the corresponding function to judge whether it satisfies the formal specification grammar when it meets the point that needs to be monitored.However,when the traditional single thread runtime verification monitor has many properties that the target program needs to monitor,the regenerated program may slow down the performance of the program because of the more specified nature.In this paper,we optimize the prototype tool Movec by using multi-core parallel technology.Through the way of serial program monitor assigned to multithreading,Clang compiler's piling technology and multi-core task allocation method have realized the optimization of Movec prototype tools.The optimized Movec is compared with the experimental data without the improved tools,which shows that the multithread operation method has a better effect.
Runtime verification is a new lightweight automatic verification technique.The verification software used in this technology is composed of two parts:one part is the monitored target program;the other is the monitor.The main idea of the runtime verification method based on formalized language is to input a formal specification syntax that represents events and properties and target program,and output a new program.The new program with inserting pile will execute the corresponding function to judge whether it satisfies the formal specification grammar when it meets the point that needs to be monitored.However,when the traditional single thread runtime verification monitor has many properties that the target program needs to monitor,the regenerated program may slow down the performance of the program because of the more specified nature.In this paper,we optimize the prototype tool Movec by using multi-core parallel technology.Through the way of serial program monitor assigned to multithreading,Clang compiler's piling technology and multi-core task allocation method have realized the optimization of Movec prototype tools.The optimized Movec is compared with the experimental data without the improved tools,which shows that the multithread operation method has a better effect.
引文
[1]CHEN Zhe,WANG Zhemin,ZHU Yunlong,et al.Parametric runtime verification of c programs[C]//International conference on tools and algorithms for the construction and analysis of systems.Berlin:Springer,2016:299-315.
[2]MEREDITH P O N,JIN D,GRIFFITH D,et al.An overview of the MOP runtime verification framework[J].International Journal on Software Tools for Technology Transfer,2012,14(3):249-289.
[3]LEUCKER M,SCHALLHART C.A brief account of runtime verification[J].The Journal of Logic and Algebraic Programming,2009,78(5):293-303.
[4]王哲民,陈哲,朱云龙,等.参数化运行时验证研究和工具实现[J].小型微型计算机系统,2016,37(12):2667-2672.
[5]LATTNER C,ADVE V.LLVM:a compilation framework for lifelong program analysis&transformation[C]//International symposium on code generation and optimization.[s.l.]:IEEE,2004:75-86.
[6]HOPCROFT J E,ULLMAN J D.Introduction to automata theory,languages,and computation[M].2nd ed.[s.l.]:[s.n.],2001.
[7]SHIELDS M W.An introduction to automata theory[M].[s.l.]:Blackwell Scientific Publications,Ltd.,1987.
[8]ZHANG X,LEUCKER M,DONG W.Runtime verification with predictive semantics[M]//NASA formal methods.Berlin:Springer,2012:418-432.
[9]BAUER A,LEUCKER M,SCHALLHART C.Runtime verification for LTL and TLTL[J].ACM Transactions on Software Engineering and Methodology,2011,20(4):14.
[10]LEVINE J.Flex&Bison:text processing tools[M].[s.l.]:[s.n.],2009.
[11]MEREDITH P O,JIN D,CHEN F,et al.Efficient monitoring of parametric context-free patterns[J].Automated Software Engineering,2010,17(2):149-180.
[12]LUK C K,HONG S,KIM H.Qilin:exploiting parallelism on heterogeneous multiprocessors with adaptive mapping[C]//Proceedings of the 42nd annual IEEE/ACM international symposium on microarchitecture.New York,NY,USA:ACM,2009:45-55.
[13]GIACOMONI J,MOSELEY T,VACHHARAJANI M.Fastforward for efficient pipeline parallelism a cache-optimized concurrent lock-free queue[C]//Proceedings of the 13th ACM SIGPLAN symposium on principles and practice of parallel programming.Salt Lake City,UT,USA:ACM,2008:43-52.
[14]NAVABPOUR S,BONAKDARPOUR B,FISCHMEISTERS.Time-triggered runtime verification of component-based multi-core systems[M].Waterloo:University of Waterloo,2015.
[15]张林波.并行计算导论[M].北京:清华大学出版社,2006.
[16]王锋.面向千万亿次CPU-GPU异构系统的编程模型与性能优化关键技术研究[D].长沙:国防科技大学,2013.
[17]张剑,胡军,郭丽娟,等.多核处理器架构下面向监控的软件运行时验证方法研究[J].小型微型计算机系统,2012,33(1):102-109.
[2]MEREDITH P O N,JIN D,GRIFFITH D,et al.An overview of the MOP runtime verification framework[J].International Journal on Software Tools for Technology Transfer,2012,14(3):249-289.
[3]LEUCKER M,SCHALLHART C.A brief account of runtime verification[J].The Journal of Logic and Algebraic Programming,2009,78(5):293-303.
[4]王哲民,陈哲,朱云龙,等.参数化运行时验证研究和工具实现[J].小型微型计算机系统,2016,37(12):2667-2672.
[5]LATTNER C,ADVE V.LLVM:a compilation framework for lifelong program analysis&transformation[C]//International symposium on code generation and optimization.[s.l.]:IEEE,2004:75-86.
[6]HOPCROFT J E,ULLMAN J D.Introduction to automata theory,languages,and computation[M].2nd ed.[s.l.]:[s.n.],2001.
[7]SHIELDS M W.An introduction to automata theory[M].[s.l.]:Blackwell Scientific Publications,Ltd.,1987.
[8]ZHANG X,LEUCKER M,DONG W.Runtime verification with predictive semantics[M]//NASA formal methods.Berlin:Springer,2012:418-432.
[9]BAUER A,LEUCKER M,SCHALLHART C.Runtime verification for LTL and TLTL[J].ACM Transactions on Software Engineering and Methodology,2011,20(4):14.
[10]LEVINE J.Flex&Bison:text processing tools[M].[s.l.]:[s.n.],2009.
[11]MEREDITH P O,JIN D,CHEN F,et al.Efficient monitoring of parametric context-free patterns[J].Automated Software Engineering,2010,17(2):149-180.
[12]LUK C K,HONG S,KIM H.Qilin:exploiting parallelism on heterogeneous multiprocessors with adaptive mapping[C]//Proceedings of the 42nd annual IEEE/ACM international symposium on microarchitecture.New York,NY,USA:ACM,2009:45-55.
[13]GIACOMONI J,MOSELEY T,VACHHARAJANI M.Fastforward for efficient pipeline parallelism a cache-optimized concurrent lock-free queue[C]//Proceedings of the 13th ACM SIGPLAN symposium on principles and practice of parallel programming.Salt Lake City,UT,USA:ACM,2008:43-52.
[14]NAVABPOUR S,BONAKDARPOUR B,FISCHMEISTERS.Time-triggered runtime verification of component-based multi-core systems[M].Waterloo:University of Waterloo,2015.
[15]张林波.并行计算导论[M].北京:清华大学出版社,2006.
[16]王锋.面向千万亿次CPU-GPU异构系统的编程模型与性能优化关键技术研究[D].长沙:国防科技大学,2013.
[17]张剑,胡军,郭丽娟,等.多核处理器架构下面向监控的软件运行时验证方法研究[J].小型微型计算机系统,2012,33(1):102-109.