Computer Science ›› 2016, Vol. 43 ›› Issue (Z6): 461-466.doi: 10.11896/j.issn.1002-137X.2016.6A.109

Previous Articles     Next Articles

Symbolic Execution and Human-Machine Interaction Based Auto Vectorization Method

CHEN Yong and XU Chao   

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

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!