计算机科学 ›› 2016, Vol. 43 ›› Issue (Z6): 461-466.doi: 10.11896/j.issn.1002-137X.2016.6A.109

• 软件工程与数据库技术 • 上一篇    下一篇

基于符号执行和人机交互的自动向量化方法

陈勇,徐超   

  1. 中国电子科技集团公司第十四研究所 南京210039,南京审计大学 南京210029
  • 出版日期:2018-11-14 发布日期:2018-11-14

Symbolic Execution and Human-Machine Interaction Based Auto Vectorization Method

CHEN Yong and XU Chao   

  • Online:2018-11-14 Published:2018-11-14

摘要: 自动向量化技术是一种针对单指令多数据(SIMD)向量化计算单元的并行编译优化技术,它能够自动将源程序中多个相同标量操作合并为一个向量操作,从而提升系统吞吐量。随着SIMD向量化计算单元的广泛应用,自动向量化技术已经成为学术界和商业界的研究热点。针对现有自动向量化技术可向量化模块识别难、向量化优化方案选择难、可移植性差等问题,提出了一种基于符号执行和人机交互的自动向量化方法。首先借助于符号执行技术,获得较好的可移植性和较高的可向量化模块识别率;然后利用人机交互技术选择出理想的向量化方案。应用示例及实验结果表明,该方法具有较好的可操作性,能够有效提升自动向量化技术的优化效果和可移植性。

关键词: 自动向量化,符号执行,人机交互,可移植性,单指令多数据

Abstract: Auto-vectorization is a parallel compiling optimization technology for SIMD vector computing units.It combines multiple same operations into one SIMD instruction which can significantly improve the output of the system.As SIMD vector computing units are used widely,auto-vectorization technology has become the hot topic in both academic and commerce world.Focusing on the shortcoming of current auto-vectorization technology such as the difficulty to get the code that can be vectorized,the difficulty to select the best optimization schema and poor portability,we proposed a new vectorizing method based on the symbolic execution and human-machine interaction.The method contains two phases.At first,based on the symbolic execution technology,it recognizes the vectorizable code as much as possible.Then,the human-machine interaction technology is used for determining the exactly code to be vectorized.At the same time,the method has portability that can be used for other architectures by only modifying the pattern file.Application example shows that our new technology is feasible and effective.

Key words: Auto-vectorization,Symbolic execution,Human-machine interaction,Portability,SIMD

[1] Lee Y,Avizienis R,Bishara A,et al.Exploring the Tradeoffs between Programmability and Efficiency in Data-Parallel Accelerators[C]∥Proceedings of Annual International Symposium on Computer Achitecture.2011:129-140
[2] Pujara C,Modi A,Sandeep G,et al.VC-1 video decoder optimization on ARM Cortex-A8 with NEON[C]∥2010 National Conference on Communications (NCC).IEEE,2010:1-5
[3] Lacassagne L,Etiemble D,Zahraee H,et al.High Level Transforms for SIMD and low-level computer vision algorithms[C]∥Proceedings of the 2014 Workshop on Programming Models for SIMD/Vector Processing.ACM,2014
[4] Trifunovic K,Nuzman D,Cohen A,et al.Polyhedral-ModelGuided Loop-Nest Auto-Vectorization.[C]∥Proceedings of PACT’09.Washington DC,USA,2009:327-337
[5] Wang Y,Pan L,Shao Z,et al.Loop Transforming for Reducing Data Alignment on Multi-Core SIMD Processors[J].Journal of Signal Processing Systems,2014,74(2):137-150
[6] Haine C,Aumage O,Enguerrand P.et al.Exploring and Evaluating Array Layout Restructuration for SIMDization[C]∥The 27th International Workshop on Languages and Compilers for Parallel Computing (LCPC 2014).Hillsboro,USA,2014
[7] Ramanarayanan R,Gupta M,Chakraborty S S,et al.Harnessing partial vectorization in Open64 compiler[C]∥2014 IEEE International on Advance Computing Conference (IACC).IEEE,2014:813-824
[8] Guelton S,Falcou J,Brunet P.Exploring the vectorization of Python constructs using Pythran and Boost SIMD[C]∥Procee-dings of the 2014 Workshop on Programming Models for SIMD/Vector Processing.ACM,2014:79-86
[9] 徐金龙,赵荣彩,丁锐.面向循环的混合向量化方法研究[J].小型微型计算机系统,2014,35(12):2764-2769
[10] Zhu Q S.Improving Program Performance via Auto-Vectorization of Loops with Conditional Statements with GCC Compiler Setting[J].Applied Mechanics and Materials,2014,433:1410-1414
[11] Ojha D K,Sikka G.A Study on Vectorization Methods for Multicore SIMD Architecture Provided by Compilers[C]∥ICT and Critical Infrastructure:Proceedings of the 48th Annual Convention of Computer Society of India-Vol I.Springer International Publishing,2014:723-728
[12] 李春江,黄娟娟,徐颖,等.典型编译器自动向量化效果评估与分析[J].计算机科学,2013,40(4):41-46
[13] King J.Symbolic execution and program testing[J].Communications of the ACM,1976,19(7):385-394
[14] Bardin S,Kosmatov N,Cheynier F.Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria[C]∥2014 IEEE Seventh International Conference on Software Testing,Verification and Validation (ICST).IEEE Computer Society,2014:173-182
[15] Ibing A.SMT-Constrained Symbolic Execution for Eclipse CDT/Codan[M]∥Software Engineering and Formal Methods.Springer.International Publishing.2013:113-124
[16] Reus B,Charlton N,Horsfall B.Symbolic Execution Proofs for Higher Order Store Programs[J].Journal of Automated Reasoning,2015,54(3):199-284
[17] Chen T,Zhang X S,Ji X L,et al.Test Generation for Embedded Executables via Concolic Execution in a Real Environment[J].IEEE Transactions on Reliability,2015,64(1):284-296

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!