二进制翻译正确性及优化方法的形式化模型

傅立国; 庞建民; 王军; 张家豪; 岳峰

doi:10.7544/issn1000-1239.2019.20180513

二进制翻译正确性及优化方法的形式化模型

(数学工程与先进计算国家重点实验室(战略支援部队信息工程大学) 郑州 450002) (flg_njlg@163.com)

基金项目: 国家自然科学基金项目(61472447)

详细信息

中图分类号: TP314
计量
- 文章访问数: 954
- HTML全文浏览量: 5
- PDF下载量: 493
出版历程
- 发布日期: 2019-08-31

Formal Model of Correctness and Optimization on Binary Translation

(State Key Laboratory of Mathematical Engineering and Advanced Computing (Strategic Support Force Information Engineering University), Zhengzhou 450002)

Funds: This work was supported by the National Natural Science Foundation of China (61472447).

摘要

摘要: 二进制翻译在体系结构设计、程序性能优化、安全性分析以及软件移植等领域的研究中备受关注.不同应用场景对二进制翻译的需求各不相同，却总聚焦于翻译的正确性和翻译的效率2个方面.翻译的正确性用于评判翻译前后程序在逻辑功能上是否具有等价性，而等价的证明依赖于适当的形式化模型.为了满足研究二进制翻译正确性以及翻译优化方法对理论模型的需求，对已有理论模型进行了深入的剖析，并进一步构建了新的基于后继关系的映射模型.该模型既能够形式化地描述正确翻译的二进制翻译过程所具备的性质和构造方法，也可以在翻译过程形式化描述的基础上对翻译过程优化方法的特征和性质进行描述.通过构建翻译正确性及翻译过程优化方法的形式化模型，为二进制翻译技术中关于翻译过程的实现以及优化方法的策略组合等进一步研究提供了更强的理论支撑.
- 二进制翻译 /
- 翻译正确性 /
- 效率 /
- 翻译优化 /
- 形式化模型
Abstract: Binary translation has attracted more and more attention in the fields of architecture optimization, program performance optimization, security analysis, software transplantation and so on. Although there are totally different requirements on the application of binary translation techniques in these various fields, the researchers are always focusing their attention on two aspects: the correctness of translation and the efficiency of translation. The correctness of translation refers to the equivalent logical functions between the program before and after the translation, so an appropriate formal model for the translation needs to be built at first. According to the current research needs on correctness and optimization of binary translation technique, twice mapping model based on subsequent relations could have been constructed firstly; then the properties and construction methods of a correct process on translation should have been described formally; based on the formal description, the optimization methods of translation would be classified and analyzed on their diverse characteristics and various properties finally. This paper provides a more powerful theoretical support for the further research on the strategy pattern combination of translation methods and optimization methods in the binary translation technology by constructing a formal model of binary translation based on correctness and optimization.
- binary translation /
- translation correctness /
- efficiency /
- translation optimization /
- formal model

HTML全文

参考文献(0)

施引文献(7)

期刊类型引用(4)

1.	张文柱，余静华. 移动边缘计算中基于云边端协同的任务卸载策略. 计算机研究与发展. 2023(02): 371-385 . 本站查看
2.	雷雨，张璐. 基于SSH2框架的智慧建筑施工信息查询系统设计. 粉煤灰综合利用. 2023(03): 106-111 . 百度学术
3.	顾雯轩，高原，顾文杰，邹庆，董子奇. 适用于电网调控系统的轻量级容器技术实现. 计算机技术与发展. 2021(02): 116-121 . 百度学术
4.	虞保忠，郝继锋，周霆，任晓宇. 云计算应用中的嵌入式容器技术研究. 单片机与嵌入式系统应用. 2021(05): 9-11+21 . 百度学术