第４ ３ 卷第１ １ 期２ ０ ２ ０ 年１ １ 月计算机学报ＣＨ Ｉ Ｎ Ｅ ＳＥＪ Ｏ ＵＲ Ｎ ＡＬＯＦ ＣＯ ＭＰ Ｕ ＴＥ ＲＳＶｏ ｌ ．４ ３Ｎ ｏ． １ １Ｎｏ ｖ． ２ ０ ２ ０同步语言多线程代码生成的语义保持证明方法袁胜浩ｎ杨志斌°’２）张博林＂周勇Ｄ薛ｆＢＯ ＤＥ Ｌ Ｅ ＩＸＪ ｅ ａ ｎ－ Ｐ ａｕ ｌＪ ，Ｆ Ｉ ＬＡ Ｌ ＩＭ ａｍｏ ｕ ｎ＇ １＂（ 南京航空航天大学计箅机科学与技术学院南京２ １ １ １ ０ ６ ）＆ （ 高安全系统的软件开发与验证技术工信部重点实验室南京２ １ １ １ ０ ６ ）（ 上海航天电子技术研究所上海２ ０ １ １ ０ ９ ）＂（ Ｉ ＲＩ Ｔ－ Ｕ ｎ ｉ ｖ ｅｒ ｓ ｉｔ ｙ  ｏ ｆＴｏ ｕ ｌ ｏ ｕ ｓｅ ， Ｔ ｏ ｕ ｌ ｏ ｕ ｓ ｅ３ １ ０ ６ ２Ｆｒ ａ ｎ ｃ ｅ ）摘要同步语言具有确定性并行和精确时间语义等特性， 因此被广泛用于设计和验证安全关键软件． 随着安全关键领域应用多核处理器逐渐成为趋势， 同步语言的多线程代码生成及其语义保持证明研究成为研究热点． 目前，已有同步语言代码生成方法还较少考虑多线程代码生成的语义保持证明． 因此， 本文提出一种同步语言ＳＩ ＧＮ Ａ Ｌ多线程代码生成的语义保持证明方法： 首先形式化定义编译过程中源、目标、中间语言的结构化操作语义； 其次形式化定义多线程代码生成过程； 最后基于互模拟等价思想证明编译前后的语义一致性．关键词同步语言； 安全关键软件； 多任务代码生成； 语义保持证明； Ｃ ｏｑ中图法分类号 ＴＰ３ １ １ＤＯＩ号１ ０． １ １ ８ ９ ７ ／ ＳＰ． Ｊ ． １ ０ １ ６．  ２ ０ ２ ０ ． ０ ２ ２ １ ６ＡＳｅｍａ ｎｔ ｉｃＰｒｅｓｅｒｖａｔｉｏｎＰ ｒｏ ｖｉｎ ｇＭｅ ｔｈ ｏｄｏｆＭｕｌ ｔｉ－Ｔｈ ｒｅａｄｅｄＣｏｄｅＧｅｎ ｅｒ ａｔｉ ｏｎ ｆｏｒＳｙｎｃ ｈｒｏｎ ｏｕｓＬ ａｎ ｇ ｕａｇ ｅＹＵＡＮ Ｓｈ ｅ ｎ ｇ－ Ｈａ ｏｕＹ ＡＮ Ｇ Ｚｈ ｉ－ Ｂ ｉ ｎ１ Ｋ ２ ）ＺＨ Ａ Ｎ ＧＢｏ－ Ｌ ｉ ｎ１ ）Ｚ ＨＯ ＵＹｏｎｇ１ １Ｘ ＵＥＬｅ ｉ３ ）Ｂ ＯＤ ＥＶ ＥＩＸＪ ｅａ ｎ－ Ｐａ ｕ ｌ４ ）Ｆ Ｉ ＬＡ ＬＩＭａ ｍｏ ｕｎ４ １］）｛ Ｃｏ ｌ ｌｅｇ ｅｏｆ Ｃｏ ｍ ｐｕ ｔ ｅｒ Ｓ ｃｉ ｅｎ ｃｅ ａ ｎ ｄ Ｔｅｃｈ ｎｏ ｌ ｏｇ ｙ＊ Ｎａ ｎ ｊｉｎｇＵｎ ｉｖｅｒｓ ｉ ｔｙ  ｏｆＡ ｅｒ ｏｎ ａ ｕ ｔｉ ｃｓ ａ ｎ ｄＡｓ ｔ ｒｏ ｎ ａ ｕ ｔ ｉｃｓ  ， Ｎａ ｎｊｉｎ ｇ２ １ １ １ ０ ６ ）２ ）（ Ｋ ｅｙ Ｌａ ｂｏ ｒａ ｔ ｏ ｒｙ ｏ ｆＳａ ｆｅｔ ｙ－Ｃ ｒｉ ｔ ｉｃ ａ ｌＳｏｆｔｗａ ｒｅ ＾ Ｍｉｎ ｉｓ ｔｒｙ ｏｆ Ｉ ｎ ｄｕ ｓ ｔｒ ｙ ａ ｎｄ Ｉ ｎ ｆｏ ｒ ｍａ ｔｉ ｏ ｎＴ ｅｃ ｈ ｎ ｏ ｌｏ ｇｙ  ｉＮａ ｎｊｉ ｎｇ２ １ １ １ ０ ６ ）（． Ｓ ｈａ ｎ ｇｈ ａ ｉＡ ｅ ｒｏ ｓ ｐａ ｃｅＥｌ ｅ ｃｔ ｒｏｎ ｉ ｃ Ｔｅ ｃｈ ｎ ｏｌ ｏ ｇｙ Ｉｎ ｓ ｔ ｉ ｔ ｕ ｔ ｅ －，Ｓｈ ａ ｎｇｈ ａ ｉ２ ０ １ １ ０ ９ ）” （ ＩＲ Ｉ Ｔ－ Ｕｎ ｉｖｅ ｒｓ ｉ ｔ ｙ ｏ ｆＴ ｏｕ ｌ ｏ ｕ ｓ ｅ ， Ｔｏ ｕ ｌｏ ｕ ｓ ｅ３ １ ０ ６ ２ ， Ｆｒａ ｎ ｃｅ ）Ａｂｓ ｔ ｒａｃｔＳａ ｆ ｅ ｔｙ－ｃ ｒ ｉ ｔｉ ｃａ ｌ ｓｏ ｆ ｔ ｗ ａ ｒ ｅｉ ｓ ｗ ｉｄ ｅ ｌ ｙｕｓ ｅｄｉ ｎｔ ｈ ｅｆｉ ｅ ｌ ｄｓｏ ｆａ ｖ ｉｏ ｎｉ ｃ ｓ ， ｓｐ ａ ｃｅｓ ｙｓ ｔｅ ｍｓ ？ａ ｎ ｄｎ ｕ ｃ ｌ ｅ ａｒ ｐｏ ｗｅ ｒｐｌ ａ ｎ ｔ ｓ ：Ｍａ ｌ ｆ ｕｎ ｃ ｔｉ ｏｎ ｓｏｆ ｓ ａ ｆｅ ｔ ｙ－ｃ ｒ ｉ ｔ ｉｃ ａ ｌｓｏ ｆ ｔｗａ ｒ ｅ ｃ ａ ｎｌ ｅ ａｄ ｔｏ ａ ｃｃ ｉ ｄｅ ｎｔ ｓｔ ｈａ ｔｃ ａ ｎｐｏ ｔｅ ｎｔ ｉａ ｌ ｌ ｙｐｕ ｔｐ ｅｏｐｌ ｅ ，ｅ ｎ ｖｉ ｒｏ ｎｍ ｅｎｔ ，ｐｒ ｏｐ ｅｒ ｔｙ ，ａ ｎｄｍ ｉ ｓ ｓｉｏ ｎｉ ｎｓ ｅｒ ｉ ｏｕｓ ｒ ｉｓｋ ｓｓｕｃｈ ａ ｓｅ ｎ ｖｉｒ ｏｎｍｅ ｎｔ ａ ｌｃａ ｔａ ｓ ｔｒ ｏ ｐｈ ｅｓ  ａｎ ｄ ｌｏｓ ｓ ｏｆ ｌｉ ｖｅｓ．Ｓ ｙｎ ｃｈｒｏｎ ｏｕｓ Ｌａ ｎｇ ｕ ａｇ ｅｓ ａ ｒ ｅ ａｄ ｏｐｔ ｅｄ ｆｏｒ ｔ ｈｅ ｄｅｓ ｉｇｎ ａ ｎｄ ｔｈ ｅｖｅ ｒｉ ｆｉ ｃ ａ ｔｉ ｏ ｎｏｆ ｓ ａ ｆ ｅｔ ｙ－ ｃｒ ｉ ｔ ｉ ｃａ ｌ ｓ ｏｆｔ ｗ ａ ｒ ｅ ，ｄｕ ｅｔ ｏｔ ｈｅ ｉ ｒｃｈ ａ ｒ ａ ｃ ｔ ｅ ｒ ｉ ｓ ｔ ｉ ｃ ｆ ｅａ ｔ ｕ ｒ ｅｓ ，ｆ ｏｒ ｉ ｎ ｓ ｔ ａ ｎｃ ｅｔ ｈ ｅｄｅ ｓ ｃ ｒ ｉ ｐｔ ｉｏ ｎｏ ｆｄ ｅｔｅ ｒｍｉ ｎｉ ｓ ｔｉ ｃ ｃｏｎｃ ｕｒ ｒ ｅ ｎｃｙ ｂｅｈ ａｖｉ ｏｒ ｓａ ｎｄｐｒ ｅ ｃｉ ｓ ｅｔ ｉｍ ｉｎ ｇｓ ｅ ｍａ ｎｔ ｉｃ ｓ．Ｒｅｃ ｅｎ ｔ ｌ ｙ ，ｓ ａ ｆｅ ｔｙ－ ｃｒ ｉ ｔｉ ｃ ａｌ ｄ ｏｍａ ｉ ｎｓｈ ａ ｖｅｅ ｖ ｏｌ ｖｅ ｄｔ ｏ ｕｓ ｅｈｉ ｇ ｈｃｏ ｍｐｕ ｔ ａ ｔ ｉ ｏｎ ｐｅ ｒ ｆｏ ｒｍａ ｎｃ ｅｐ ｒｏ ｖｉ ｄｅ ｄｂ ｙｍｕ ｌ ｔ ｉ ｃｏ ｒ ｅｐ ｌ ａ ｔｆ ｏｒｍｓ  ｔｏ ｉ ｍｐ ｌ ｅｍ ｅｎ ｔｍｏｒ ｅ ｃ ｏｍ ｐｌ ｅ ｘｆ ｕｎ ｃｔｉ ｏｎａ ｌｉｔ ｙ．Ｔｈ ｅ ｒ ｅｆｏｒ ｅ ｔ ｈｅ ｍ ｕｌ ｔｉ－ｔ ｈｒ ｅ ａｄ ｅｄｃｏｄｅｇ ｅｎ ｅｒ ａ ｔｉｏ ｎａ ｐｐ ｒｏａｃ ｈｆｏｒ  ｓｙｎ ｃｈｒｏｎ ｏｕｓｌ ａ ｎｇ ｕａ ｇ ｅｓ ａ ｎ ｄｒ ｅ ｌ ａ ｔｅ ｄｓ ｅｍａ ｎ ｔ ｉ ｃｐ ｒｅ ｓ ｅ ｒｖ ａｔ ｉ ｏｎｐ ｒｏ ｏｆ ｈ ａ ｖｅ ｂｅ ｅ ｎｒ ｅ ｓ ｅ ａ ｒ ｃｈｈ ｏｔ ｓ ｐｏｔ ｓ ．Ｈ ｏｗ ｅｖｅ ｒ ， ｔ ｈ ｅ收稿日期： ２ ０ １９ － ｌ ｌ － ２４； 在线发布日期：２ ０ ２ ０ － ０ ８－ ｌ ｌ ■ 本课题得到国家自然科学基金（ ６ １ ５ ０２ ２ ３ １ ） 、航空科学基金（ ２ ０ １ ９ １ ９０ ５２ ００ ２ ）、Ｇ Ｆ 基础科研重点项目（ Ｊ ＣＫ Ｙ ２０ １ ６ ２０ ３Ｂ０ １ １ ）、中央高校基本科研业务费专项资金资助（ Ｎ Ｐ ２ ０ １ ７ ２ ０ ５ ） 、南京航空航天大学研究生创新基地（ 实验室） 开放基金（ ｋ扭２ ０ １ ８ １ ６０ ３ ） 资助． 袁胜浩， 硕士研究生， 中国计算机学会（ ＣＣＦ） 学生会员， 主要研究方向为彤式化方法、定理证明． Ｅ－ ｍａｉ ｌ ：ｓ ｈ ｙ－ｕａ ｎ＠ ｍｉ ａａ ． ｅ ｄ ｕ ． ｃｎ ． 杨志斌（ 通信作者） ， 博士， 副教授， 中国计算机学会（ ＣＯＦ ） 会员， 主要研究方向为安全关键软件、形式化验证． Ｅ－ ｍａ ｉｌ：ｙ ａｎｇｚ ｈ ｉ ｂ ｉ ｎ ｌ ６ ８ ＠ １ ６ ３ ． ｃｏｍ． 张博林， 硕士研究生， 中国计算机学会（ ＣＣ Ｆ） 学生会员， 主要研究方向为模型验证、软件工程． 周勇， 博士， 副教授， 中国计算机学会（ ＣＣＦ） 会员， 研究方向为软件工程、形式化方法等． 薛垒， 硕士， 髙级工程师， 研究方向力嵌入式软件验证、嵌人式软件系统设计． ＢＯＤ ＥＶＥＩＸＪ ｅａ ｎ￣Ｐａｕｌ ， 博士， 教授， 研究领域为实时系统、形式方法． ＦＩＬ ＡＬＩ Ｍａｍｏ ｕ ｎ ， 博士， 高级研究员， 研究领域为实时系统、形式方法．１ １ 期袁胜浩等： 同步语言多线程代码生成的语义保持证明方法２ ２ １ ７ｅ ｘ ｉｓ ｔ ｉ ｎｇｓ ｔｕ ｄｉ ｅ ｓｏ ｎ ｓｙｎ ｃｈ ｒｏｎ ｏ ｕｓ ｌ ａ ｎｇ ｕａ ｇｅ ｓ ｍａ ｉ ｎ ｌ ｙｃ ｏｎｃ ｅ ｒｎ ｔ ｈ ｅ ｓ ｅ ｍａ ｎ ｔ ｉ ｃｐｒ ｅ ｓ ｅｒ ｖａ ｔ ｉｏ ｎｏｆ ｓ ｅ ｑ ｕｅ ｎ ｔ ｉ ａ ｌｃｏ ｄｅｇ ｅ ｎｅ ｒａ ｔ ｉｏｎ ｆ ｒ ｏｍｓｙｎ ｃｈ ｒｏ ｎｏ ｕｓ ｌ ａｎ ｇｕ ａ ｇｅ ｓ ． Ｓｕｃ ｈａ ｓ ｔ ｈ ｅｖ ｅｒ ｉ ｆ ｉ ｅ ｄｓｙ ｎｃ ｈ ｒｏｎ ｏｕ ｓｌ ａ ｎ ｇｕ ａ ｇｅ Ｌｕ ｓ ｔ ｒ ｅｃｏ ｍｐ ｉ ｌｅ ｒ Ｖ ｅｌ ｕ ｓ ｓｕ ｐｐ ｏｒ ｔ ｓｓ ｅｑ ｕｅ ｎｔ ｉ ａ ｌ Ｃ ｃｏｄ ｅｇ ｅｎ ｅ ｒ ａ ｔ ｉｏ ｎ ， ｔｈ ｅ ｖｅ ｒ ｉ ｆｉ ｅ ｄＬｕ ｓ ｔ ｒ ｅ ｃｏｍ ｐｉ ｌ ｅ ｒ Ｌ ２Ｃｔ ｒ ａ ｎ ｓｌ ａ ｔ ｅｓＬ ｕｓ ｔ ｒ ｅｍｏ ｄｅ ｌ ｓ ｔ ｏ Ｃｌ ｉ ｇｈ ｔｐ ｒｏ ｇｒａ ｍ ｓ ｗ ｈ ｉ ｃｈ ｃ ａｎ ｂ ｅ ｃｏｎ ｓ ｉｄ ｅ ｒｅ ｄ ａ ｓ  ｔ ｈｅ ｉ ｎ ｐｕ ｔｏｆ ｔ ｈｅ Ｃｏｍ ｐＣｅ ｒ ｔ ｃ ｏｍ ｐｉ ｌ ｅ ｒａ ｎ ｄ ｔｈ ｅｔｒ ａ ｎｓ ｌ ａ ｔ ｉｏｎ ｖａ ｌｉ ｄａ ｔ ｉ ｏｎ ａｐ ｐ ｒ ｏａ ｃｈｉ ｓｕｓ ｅ ｄｔｏｖｅ ｒ ｉ ｆ ｙｔｈ ｅ ｔ ｒ ａ ｎｓ ｆｏ ｒｍａ ｔ ｉｏ ｎｓ ｔ ｅ ｐｓｆ ｒｏｍｔｈ ｅｓｙ ｎ ｃｈ ｒｏ ｎｏ ｕ ｓｌ ａ ｎ ｇ ｕａ ｇｅ ＳＩ Ｇ Ｎ ＡＬ ｔ ｏ ｓｅ ｑｕ ｅｎ ｔ ｉ ａ ｌＣｃｏｄ ｅ ．Ｔｈ ｅ ｙｐａ ｙａ ｌ ｉ ｔ ｔｌ ｅａ ｔ ｔ ｅｎ ｔ ｉｏ ｎｔ ｏｔ ｈ ｅ ｓｅ ｍａ ｎ ｔ ｉｃｐｒ ｅｓ ｅｒ ｖ ａ ｔｉ ｏｎ ｏｆ ｍ ｕｌ ｔｉ－ｔ ｈ ｒ ｅ ａｄ ｅ ｄｃｏ ｄｅ ｇｅ ｎ ｅｒ ａ ｔ ｉ ｏｎ ．Ａ ｓ ｍ ｕ ｌ ｔｉ－ ｃｏ ｒ ｅｐ ｒｏｃ ｅ ｓ ｓｏｒ ｓ ｇｒ ａ ｄｕ ａ ｌ ｌ ｙｂ ｅ ｃｏｍ ｅ ｗｉ ｄ ｅｌ ｙｕｓ ｅ ｄｉ ｎｓａ ｆ ｅ ｔｙ－ ｃ ｒ ｉ ｔ ｉ ｃ ａ ｌｓ ｙ ｓ ｔ ｅ ｍｓ ，ｉ ｔ ｉ ｓｎ ｅ ｃｅ ｓ ｓ ａ ｒｙｔ ｏｃｏ ｎ ｓ ｉ ｄ ｅｒ ｔｈ ｅｓ ｅ ｍａ ｎ ｔ ｉｃ ｐｒ ｅ ｓ ｅｒ ｖａ ｔｉ ｏ ｎｏ ｆｍ ｕ ｌ ｔｉ？ｔ ｈｒ ｅ ａ ｄｅ ｄｃｏ ｄｅｇｅ ｎｅ ｒ ａ ｔｉ ｏｎ ａ ｐｐ ｒｏａ ｃ ｈ ｆｏｒ ｓｙｎ ｃ ｈｒｏ ｎｏ ｕｓｌ ａ ｎｇ ｕ ａｇ ｅ ｓ ．Ｔ ｈ ｅｒ ｅ ｆ ｏｒ ｅ ，ｔ ｈ ｉ ｓｐａ ｐｅ ｒ ｐ ｒ ｅ ｓ ｅ ｎ ｔ ｓ ａｖ ｅ ｒ ｉ ｆｉ ｅｄ ｍ ｕｌ ｔ ｉ－ｔ ｈ ｒｅ ａ ｄｅ ｄｃｏ ｄｅｇ ｅｎ ｅｒ ａｔ ｉ ｏｎ ｍｅ ｔ ｈｏ ｄｆ ｏｒ ｔ ｈ ｅｓ ｙｎ ｃ ｈ ｒｏ ｎｏ ｕｓ  ｌ ａ ｎｇ ｕａ ｇ ｅＳＩ Ｇ Ｎ Ａ Ｌ．Ｆ ｉ ｒ ｓｔ ｌ ｙ ，ａｃ ｏｍ ｍｏｎＳＩ Ｇ Ｎ ＡＬ ｓ ｕｂｓ ｅ ｔｗ ｈｉ ｃ ｈｉ ｓｃ ｏｍｐ ａ ｔｉ ｂ ｌ ｅｗ ｉ ｔｈ ｔｗ ｏｅ ｘｉ ｓ ｔｉ ｎ ｇＳＩ Ｇ Ｎ Ａ Ｌｃｏ ｍｐ ｉ ｌ ｅ ｒ ｓＰｏ ｌ ｙｃｈ ｒｏ ｎｙａ ｎ ｄＭｉ ｎ ｉ ＳＩＧ Ｎ ＡＬ ， ｉ ｓｓ ｅ ｌ ｅ ｃ ｔ ｅｄ ａ ｓ ｔ ｈ ｅｓ ｔ ａｒｔｐ ｏｉ ｎ ｔｔ ｏ ｃｏｎ ｓ ｉ ｄ ｅｒ ｔ ｈ ｅｐｒｏ ｏｆ ｏｆ  ｓ ｅ ｍａ ｎｔ ｉ ｃｐ ｒｅ ｓ ｅｒｖ ａ ｔｉ ｏｎ ｏｆｔ ｈ ｅｍ ｕ ｌ ｔｉ－ｔ ｈｒ ｅ ａ ｄ ｅｄｃｏｄ ｅｇ ｅｎ ｅ ｒａ ｔ ｉｏ ｎｐ ｒｏｃ ｅｓ ｓａ ｎ ｄｉ ｔ ｓｆｏｒ ｍａ ｌｓ ｙｎ ｔａ ｘ ａｎｄ ｓ ｔｒ ｕｃ ｔ ｕｒ ａ ｌｏ ｐｅ ｒａ ｔ ｉ ｏｎ ａｌｓ ｅ ｍａ ｎｔ ｉ ｃｓ （ ｂ ａｓ ｅ ｄ ｏｎ ｔ ｒａ ｎ ｓ ｉ ｔ ｉｏ ｎ ｓｙ ｓ ｔ ｅｍ ｓ ）ｉ ｓｐｒｏ ｐｏｓ ｅ ｄ ；Ｓ ｅ ｃｏ ｎｄ ｌ ｙ ？ｔ ｈｅ ｃ ｌ ｏｃｋ  ｃ ａ ｌ ｃｕ ｌ ｕ ｓｐｒｏ ｃｅ ｄｕ ｒｅ ｉ ｓｆ ｏｒｍａ ｌｌ ｙ ｄｅｆ ｉ ｎｅｄｔ ｏｇ ｅｎｅ ｒ ａ ｔｅ ｃ ｌｏｃ ｋｅ ｄＳ ＩＧ Ｎ Ａ Ｌｐｒｏｇ ｒａｍ ｓ ｆ ｒｏｍ  ｓｏｕｒ ｃ ｅＳ Ｉ ＧＮ ＡＬｍ ｏｄｅ ｌｓ ， ｔ ｈｅｐｒｏ ｃｅｄ ｕｒ ｅｃ ｏｎ ｓ ｉ ｓ ｔ ｓ ｏｆ ｔ ｈ ｅｆｏｒｍ ａ ｌ ｄｅ ｆｉ ｎ ｉｔ ｉｏｎ ｏｆ ｔ ｈ ｅｅ ｘ ｔ ｒ ａｃ ｔ ｉｏ ｎ ｆｕ ｎｃ ｔ ｉ ｏｎ ｏｆｃ ｌ ｏｃ ｋ ｒｅ ｌ ａｔ ｉ ｏｎ ｓａ ｎ ｄｃｏｎ ｓ ｔ ｒ ｕｃ ｔ ｉｏ ｎｆ ｕ ｎｃ ｔｉ ｏ ｎ ｏ ｆ ｃ ｌａ ｕ ｓ ｅｓ ｅｔ ｓ ，ｔ ｈｅ ｆｏ ｒｍａ ｌ ｄ ｅｓ ｃｒ ｉ ｐ ｔｉ ｏ ｎｏ ｆｓ ｏｌ ｖｉ ｎ ｇｃ ｌ ｏ ｃｋ ｅｑ ｕａ ｔ ｉ ｏｎｓ ｓ ｙｓｔ ｅ ｍａ ｎ ｄｔ ｈ ｅ ｄｅ ｆ ｉｎ ｉ ｔ ｉｏ ｎｏｆ ｔ ｈｅｃ ｌ ｏｃ ｋｄ ｅ ｐｅ ｎ ｄｅ ｎｃ ｙｇｒ ａｐ ｈ ，ｔ ｈｅ ｏ ｐ ｅｒ ａ ｔ ｉ ｏｎ ａ ｌ ｓ ｅ ｍａ ｎ ｔｉ ｃ ｓｏ ｆｃ ｌｏ ｃｋ ｅ ｄＳＩ ＧＮ Ａ Ｌｓ ｔ ｒｕｃ ｔ ｕｒ ｅ ｉｓａ ｌ ｓｏｃｏ ｎ ｓ ｔ ｒｕｃ ｔ ｅｄ ａ ｃｃ ｏｒ ｄｉ ｎｇ ｔ ｏｔ ｈ ｅ ｔｒ ａｎ ｓ ｉｔ ｉ ｏｎ ｓｙ ｓ ｔ ｅ ｍｓ ｏｆ ｓｏ ｕｒ ｃ ｅ ＳＩＧ Ｎ Ａ Ｌｍｏ ｄｅ ｌ ｓ ａ ｎｄｔ ｈ ｅｒ ｅ ｓｕ ｌ ｔｏｆ ｔ ｈ ｅｃ ｌｏ ｃｋ  ｃａｌ ｃｕ ｌ ｕ ｓ ｐ ｒ ｏｃｅ ｄｕ ｒ ｅ ；Ｔｈ ｉ ｒｄｌ ｙ ， ａ ｎａ ｂ ｓ ｔ ｒ ａｃ ｔＣ－ｌｉ ｋ ｅ ｓ ｕ ｂｓ ｅ ｔｓ ｔ ｒｕ ｃｔ ｕ ｒ ｅ ｉｓ ｃ ｏｎ ｓｉ ｄ ｅｒ ｅｄａｓｔ ｈ ｅｔ ａ ｒｇ ｅｔｌ ａｎｇ ｕａｇｅ ａｎｄｉ ｔｓ ｆ ｏｒｍａ ｌｄｅｆ ｉｎｉ ｔｉ ｏｎ ａ ｓ ｗｅｌ ｌａ ｓ ｔｈ ｅｏｐｅｒ ａ ｔｉｏ ｎａ ｌ ｓｅｍａ ｎｔ ｉ ｃｓ ａ ｒ ｅｐ ｒｏｐ ｏｓ ｅｄ ，ｔ ｈ ｅｔ ｒａｎ ｓｆ ｏｒ ｍａｔ ｉ ｏ ｎｓ ｔ ｅｐｆｒｏｍ ｃ ｌｏｃ ｋｅ ｄＳ ＩＧＮ ＡＬ ｐｒｏ ｇｒ ａｍ ｓ ｔｏｔ ａｒｇ ｅｔ Ｃ－ｌ ｉｋ ｅｓ ｕｂｓ ｅｔ ｃｏｄｅ ｃｏｎ ｔａ ｉｎ ｓｔ ｗｏｉ ｍｐｏ ｒｔａ ｎｔ ｆ ｕｎｃ ｔｉ ｏｎｓ ：ｔ ｈ ｅｃ ｏｍｐ ｕｔ ａ ｔ ｉｏ ｎ ｆ ｕｎ ｃｔ ｉｏ ｎａ ｎｄｔ ｈｅ ｍｅ ｍｏｒ ｙｕｐ ｄａ ｔ ｅ ｆｕ ｎｃ ｔ ｉ ｏｎ ． Ｔ ｈｅ ｓ ｅｍ ａｎ ｔ ｉ ｃｓｃｏ ｎｓ ｉ ｓ ｔ ｅ ｎ ｃｙ ｏｆ ｔ ｈｅｔ ｒａ ｎ ｓ ｆｏｒ ｍａ ｔ ｉｏ ｎｓ ｔ ｅｐ（ ｎ ａ ｍｅ ｄｃ ｌ ｏｃｋ ｅ ｄＳ Ｉ Ｇ Ｎ ＡＬ ２ Ｃ ）ｉ ｎ ｃ ｌ ｕ ｄ ｅｓｔｈ ｅｐｒｏｏ ｆｏ ｆｔ ｗ ｏｄ ｉ ｒ ｅｃ ｔ ｉ ｏｎ ｓ ：ｆｒｏ ｍｃｌ ｏ ｃｋ ｅｄ ＳＩＧ Ｎ Ａ Ｌ ｔ ｏＣｌｉ ｋｅ ａ ｎ ｄ ｆ ｒｏｍＣ－ｌ ｉ ｋ ｅｔ ｏ ｃｌ ｏ ｃｋ ｅｄ ＳＩ Ｇ Ｎ Ａ Ｌｗ ｈ ｉ ｃｈ ｃｏ ｒ ｒ ｅ ｓｐｏ ｎｄ ｔｏ ｔ ｗｏｌ ｅ ｍｍａ ｓ ．Ｃｏ ｎ ｓｉ ｄｅ ｒ ｉ ｎｇ ｔｈ ｅｐ ｒｏｏｆｐ ｒ ｏｃ ｅ ｓ ｓ ｅｓｏｆ ｔ ｗ ｏｌ ｅｍ ｍａ ｓ ａ ｒ ｅ ｓ ｉ ｍ ｉｌａ ｒ ，ｔ ｈ ｉ ｓ ｐ ａ ｐｅ ｒ ｍ ａ ｉ ｎｌ ｙｉ ｎ ｔｒ ｏｄ ｕｃ ｅ ｓ ｔｈ ｅ ｆ ｉ ｒ ｓ ｔｌ ｅｍ ｍａ ， ｉ． ｅ ．ｃ ｌ ｏｃ ｋ ｅｄ ＳＩ Ｇ Ｎ ＡＬ２ Ｃｓ ａ ｔ ｉｓ ｆ ｉｅ ｓｔ ｈ ｅｕ ｎｉ ｄｉ ｒ ｅｃ ｔ ｉ ｏｎａ ｌ ｂ ｉｓ ｉ ｍｕ ｌ ａ ｔｉ ｏｎｅｑ ｕｉ ｖａ ｌｅ ｎ ｔｒ ｅ ｌ ａｔ ｉ ｏｎ ．Ｆｉ ｎ ａ ｌ ｌ ｙ ，ａ ｔｈ ｅｏ ｒ ｅ ｍａ ｂｏ ｕｔ ｔ ｈ ｅｓｅ ｍａ ｎ ｔｉ ｃ ｓｃ ｏｎ ｓ ｉ ｓ ｔ ｅ ｎ ｃｙｏｆ ｔ ｈｅ ｔ ｒａ ｎｓ ｆｏｒ ｍａ ｔ ｉ ｏｎｓ ｔｅ ｐｉ ｓ ｐｒ ｏｖｅ ｄｔ ｏｇ ｕ ａ ｒａｎ ｔ ｅ ｅ ｔ ｈｅｓ ｅｍａ ｎ ｔｉ ｃｃｏ ｎ ｓ ｉ ｓｔ ｅ ｎｃ ｙｂｅ ｔ ｗｅｅ ｎ ｔ ｈ ｅＳＩ Ｇ Ｎ ＡＬｐｒｏｇ ｒａ ｍａｆ ｔ ｅ ｒｃｌ ｏ ｃｋｃ ａ ｌ ｃｕ ｌ ｕ ｓａ ｎ ｄｔ ｈｅｔ ａ ｒｇ ｅ ｔＣｐ ｒｏｇｒ ａ ｍ ａ ｆ ｔ ｅｒ  ｔ ｒ ａ ｎｓ ｌ ａｔ ｉｏ ｎ ｂａ ｓ ｅｄｏｎ ｔ ｈｅ ｂｉ ｓ ｉｍ ｕｌ ａ ｔ ｉ ｏｎ ｅｑｕ ｉ ｖａ ｌ ｅ ｎｔ ｒ ｅ ｌ ａｔ ｉ ｏｎ ．Ｋｅ ｙｗｏｒｄ ｓｓ ｙｎ ｃｈ ｒｏ ｎｏ ｕｓｌ ａ ｎｇ ｕａ ｇ ｅ ； ｓ ａ ｆｅ ｔ ｙ－ ｃｒ ｉｔ ｉ ｃａ ｌ ｓｏ ｆｔ ｗａ ｒ ｅ ；ｍ ｕｌ ｔ ｉ－ｔ ｈ ｒ ｅａ ｄｅ ｄｃ ｏｄ ｅｇ ｅ ｎ ｅｒａ ｔ ｉ ｏｎ ；ｓ ｅｍ ａ ｎｔ ｉ ｃｐ ｒ ｅ ｓ ｅｒ ｖａ ｔ ｉｏ ｎ ；Ｃｏｑｉ 引言安全关键软件（ Ｓａｆ ｅ ｔ ｙ－ Ｃｒｉ ｔ ｉ ｃａ ｌＳｏｆ ｔｗａ ｒ ｅ ）［１］ 是指应用于航空、航天、交通、能源等领域的安全关键系统中， 且其运行情况可能引起系统处于危险状态，从而导致财产损失、环境破坏或者人员伤害的一类软件． 近年来， 模型驱动（ Ｍｏｄ ｅｌ－ Ｄｒｉ ｖｅｎ ） 尤其是采用形式化模型驱动的安全关键软件设计与开发方法逐渐受到重视， 并被工业界认为是切实可行的重要手段． 其中， 同步语言是一种被广泛用于设计和验证安全关键软件的形式化语言． 例如， 空客使用ＳＣＡＤ Ｅ？（ 即同步语言ＬＵ ＳＴ ＲＥ［３］ 的工业界版本） 对Ａ ３ ８ ０ 的飞控子系统进行建模和代码生成．目前主流的同步语言有ＥＳＴＥＲＥＬＷ、ＬＵＳＴ ＲＥ、ＳＩＧＮ ＡＬ［５］、（３１＾＼１＾＇２［ ６ ］ 等？ 其中ＥＳＴＥＲＥＬ 、ＬＵＳＴＲＥ以及ＱＵＡＲＴＺ 采用纯同步模式（ Ｐｅ ｒｆｅ ｃｔ Ｓｙ ｎｃｈ ｒｏｎｙ ） ，即存在一个全局时钟（ 单时钟） ， 而ＳＩＧＮ ＡＬ 采用多态同步模式（ Ｐｏｌ ｙｃｈ ｒｏ ｎｙ ） ， 即多时钟， 能够更自然更方便地表达分布式系统． 随着多核处理器的不断发展， 嵌人式系统设计人员更多关注多态同步模式．２ ２ １ ８ 计算机学报 ２ ０ ２ ０年现有Ｓ ＩＧ ＮＡ Ｌ 编译器Ｐ 〇ｌ ｙ Ｃ ｈｒ〇ｎｙ［７－ ８］ 主要支持串行代码生成和仿真分析， 较少考虑在多核处理器上的多任务代码生成． 在文献［９ －１ １］ 中， 我们提出了一个面向多核平台的多线程代码生成工具Ｍ ｉ ｎｉ Ｓ Ｉ Ｇ Ｎ Ａ Ｌ ，同时支持生成串行、多线程程序．诸多安全关键领域标准（ 如ＤＯ － ３ ３ ０ ） 规定安全关键软件的开发工具本身必须经过验证， 但目前Ｐｏ ｌ ｙｃ ｈ ｒｏｎ ｙ 和Ｍｉ ｎ ｉＳ Ｉ Ｇ Ｎ Ａ Ｌ 的多线程代码生成过程中较少考虑语义一致性（ 即语义保持） 的形式化证明． 在前期研究［９ １ １ ］ 的基础上， 本文进一步研究并提出一种同步语言Ｓ ＩＧ Ｎ ＡＬ 多线程代码生成的语义保持证明方法． 该方法主要包括：（ １ ） 形式化定义编译过程中多种语言的结构化操作语义；（ ２ ） 形式化定义多线程代码生成各个阶段的翻译函数；（ ３ ） 基于互模拟等价思想证明编译前后的语义一致性．本文第２ 节介绍Ｍｉ ｎ ｉＳＩＧ ＮＡＬ 代码生成工具；第３ 节给出ＳＩ ＧＮ ＡＬ 多线程代码生成核心编译过程的语义保持证明方法； 第４ 节介绍相关工作； 第５节是本文的总结和展望．２Ｍｉｎ ｉ ＳＩ ＧＮＡＬ简介本节首先介绍Ｍ ｉ ｎｉ Ｓ ＩＧ Ｎ Ａ Ｌ 的模块化编译过程， 然后介绍ＳＩ Ｇ Ｎ Ａ Ｌ 多线程代码生成核心步骤的语义保持证明框架．２． １Ｍｉ ｎ ｉＳ ＩＧＮＡＬ 模块化编译过程Ｍ ｉ ｎｉ Ｓ ＩＧ Ｎ Ａ Ｌ 是一个同步语言Ｓ Ｉ Ｇ Ｎ Ａ Ｌ 的多任务代码生成工具， 整个工具使用函数式编程语言Ｏ Ｃａ ｍｌ 实现． 本文简要给出Ｍ ｉ ｎｉ Ｓ ＩＧ Ｎ Ａ Ｌ 多线程代码生成的基本步骤（ 见图１ ） ． 详细见文献［ １ ０］ ．（ １ ） 词法语法分析． 支持对用户输人的ｕ Ｓ ＩＧＮ ＡＬ程序进行词法语法分析；（ ２ ） 程序标准化． 将ｕＳＩ Ｇ Ｎ Ａ Ｌ 程序中扩展结构转换为基本结构， 以及将复合结构转换为基本结构．标准化后的程序只包括基本结构（ 称为ｋＳ Ｉ Ｇ Ｎ Ａ Ｌ程序） ；（ ３ ）Ｓ － ＣＧ Ａ 生成． 基于转换规则将ｋＳＩ Ｇ Ｎ Ａ Ｌ程序中基本结构所表达的功能／ 时钟关系转换为Ｓ － ＣＧ Ａ 中对应的卫式动作（ 也称为守卫条件（ ４ ） 时钟演算． 从Ｓ－ ＣＧ Ａ 程序中提取时钟关系等式， 并进行消解． 基于Ｂ ＤＤ／ ＳＭ Ｔ 计算时钟等价类并优化Ｓ － ＣＧＡ 程序；（ ５ ） 依赖分析． 分析卫式动作间的读写依赖关系， 生成数据依赖图ＣＤＤＧ ；（ ６ ） 任务划分． 基于划分算法对依赖图进行划分， 生成的划分结果ｐ ａｒ ｔｉ ｔ ｉ ｏｎ 表明了Ｓ － ＣＧ Ａ 程序中的并行信息；（ ７ ） 虚拟多线程代码生成． 基于划分结果， 将Ｓ － ＣＧ Ａ 程序转换为虚拟多线程代码ｖｍｔ ；（ ８ ） 多线程代码生成． 根据虚拟多线程代码进一步生成多线程Ａ ｄａ ／ Ｃ／Ｊ ａｖａ 程序．图１Ｍ ｉｎｉＳＩＧ Ｎ ＡＬ 多线程代码生成模块化编译步骤其中， 中间语言Ｓ － ＣＧ Ａ 和虚拟多线程结构等的形式语法语义分别基于定理证明工具Ｃｏｑ 进行形式化表示． 而程序标准化到Ｓ－ ＣＧＡ 的转换过程中的语义一致性也在定理证明器Ｃｏ ｑ 中证明［ １ ２］．和Ｐｏｌ ｙｃｈ ｒｏｎ ｙ 的编译步骤相比， Ｍｉ ｎ ｉＳ Ｉ Ｇ ＮＡ Ｌ中新增Ｓ － ＣＧＡ 生成和虚拟多线程结构： 前者用于支持Ｍ ｉ ｎｉ ＳＩ ＧＮ Ａ Ｌ 集成其它同步语言； 后者用于生成平台无关的多线程代码． 同时， 在任务划分阶段，Ｍ ｉ ｎ ｉＳ Ｉ ＧＮ Ａ Ｌ 支持引入多种划分算法例如基于拓扑排序划分、基于流水线方式［ １ ° ］ 和基于ＲＰＤＭＡ算法［ １ ３］等计算并行执行信息． 除代码生成外， Ｍｉ ｎｉ ＳＩ Ｇ Ｎ ＡＬ还将进一步支持仿真实验（ 如Ｓ ｉｍ ｕｌ ｉ ｎ ｋ 程序） ． 和形式化验证（ 如ＵＰＰ Ａ Ａ Ｌ 模型） 等．２ ． ２Ｓ ＩＧＮＡ Ｌ 多线程代码生成语义保持证明框架由于Ｐ ｏｌ ｙｃ ｈ ｒｏ ｎ ｙ 和Ｍｉ ｎ ｉＳ Ｉ Ｇ Ｎ Ａ Ｌ 的编译步骤有所差异， 因此本文在语义保持证明过程中， 选择了两者的公共子集（ 如图２ 所示） ， 即时钟演算和（ 多线程） 代码生成． 本文选择的源语言为ＳＩ ＧＮ Ａ Ｌ 语言核心子集ｋ Ｓ Ｉ ＧＮ Ａ Ｌ ， 该子集包括ＳＩ Ｇ ＮＡ Ｌ 语言中的基本结构、组合、局部声明等． 经时钟演算后生成的程序记为ｃ ｌ ｏｃ ｋｅ ｄＳ Ｉ ＧＮ Ａ Ｌ 程序． 本文选择的目标语言为Ｃ 语言子集．图２ＳＩＧ ＮＡＬ 多线程代码生成语义保持证明袁胜浩等： 同步语言多线程代１ １ 期 码生成的语 义保持 证明 方法 ２ ２１ ９ＳＩＧ Ｎ Ａ Ｌ 多线程代码生成语义保持证明框架包括如下步骤： 首先定义代码生成过程中间语言的操作语义（ 基于标记变迁系统） ， 具体包括ｋＳＩ Ｇ Ｎ Ａ Ｌ 、ｃ ｌ ｏ ｃｋ ｅｄ Ｓ ＩＧ Ｎ Ａ Ｌ 和目标Ｃ 语言子集； 其次形式化定义ｋＳ Ｉ Ｇ Ｎ Ａ Ｌ 到目标程序的翻译过程， 包括时钟演算和ｃ ｌ 〇Ｃ ｋｅ ｄＳ Ｉ Ｇ Ｎ Ａ Ｌ２ Ｃ 翻译函数； 最后基于互模拟等价关系证明翻译函数ｃ ｌ ｏｃ ｋｅ ｄＳＩ Ｇ ＮＡ Ｌ２ Ｃ 保持ｃ ｌ ｏｃ ｋ ｅｄ Ｓ ＩＧ Ｎ Ａ Ｌ 和目标Ｃ 子集的语义一致性．需要注意的是， 选择ｋＳ Ｉ Ｇ Ｎ ＡＬ 的主要原因在于该子集包括了 ＳＩ Ｇ Ｎ Ａ Ｌ 语言的基本表达能力， 便于后续验证编译器工作的开展， 但我们计划逐步增加该子集的规模， 直到覆盖完整的ＳＩ Ｇ Ｎ ＡＬ 语言．而选择Ｃ 子集作为目标语言的主要原因在于计划将生成的多线程Ｃ 程序进一步经过可信编译器Ｃ ｏｍ ｐｏｓ ｉ ｔｉ ｏ ｎａ ｌＣｏｍ ｐＣｅ ｒ ｔ［ １ ４］ 编译生成机器指令． 此外， 本文将依赖分析、任务划分和代码生成阶段抽象为ｃ ｌ ｏｃ ｋｅ ｄ Ｓ Ｉ Ｇ Ｎ Ａ Ｌ２ Ｃ翻译函数．３ 多线程代码生成语义保持证明方法本节首先给出ｋＳ Ｉ ＧＮ Ａ Ｌ 的形式语法和形式语义； 其次给出时钟演算的形式化描述并构造ｃｌ ｏｃ ｋｅｄＳＩ ＧＮ Ａ Ｌ 形式语义； 然后形式化定义ｃ ｌｏ ｃｋ ｅ ｄ－Ｓ ＩＧ ＮＡ Ｌ２ Ｃ 编译过程和Ｃ 子集的形式语义； 最后基于互模拟等价思想证明ｃｌ ｏ ｃｋ ｅ ｄＳ Ｉ ＮＧ Ａ Ｌ ２ Ｃ 过程的语义一致性．３． １ｋＳ ＩＧＮＡＬ３ ．１ ． １ｋＳ Ｉ Ｇ Ｎ Ａ Ｌ 形式语法ＳＩ ＧＮ ＡＬ 是一种声明式数据流同步语言． ＳＩＧＮＡＬ语言中定义了一种带类型的无限长的值序列， 称为信号（ ｓ ｉｇ ｎａ ｌ ） ． 在给定逻辑时刻下， 信号可以是“存在”状态并携带对应的数值， 或者是“ 缺失” 状态， 记为丄．信号ｘ 的逻辑时钟（ ｉ ） 为信号存在状态对应逻辑时刻组成的集合． 在Ｓ ＩＧ Ｎ Ａ Ｌ 中， 两个信号同步当且仅当其逻辑时钟相同．Ｓ ＩＧ Ｎ ＡＬ 的核心子集ｋ Ｓ ＩＧ Ｎ Ａ Ｌ 包括四类基本数据流结构、组合和局部声明， 其抽象语法定义为Ｐ： ：＝ｘ ■＝ｆ（ ｘ ｉ ， — ， ｘ ？ ）｜ｘ ：＝ Ｘ ｉ ￥ｉ ｎ ｉｔ  ｃ｜ ｘ ：＝Ｘ ｉｗｈ ｅｎ ｘｔ｜ ｊ： ：＝Ｘ ｉｄｅ ｆ ａ ｕｌ ｔ ｘ２＼ Ｐ ＼ Ｐ＇＼Ｐ／ ｘ在语义保持证明过程中， 局部声明Ｐ ／ｘ 可以作为一类特殊的输出进行处理， 因此后续语义保持证明中将不考虑局部声明．３ ． １ ．  ２ｋＳ Ｉ ＧＮ Ａ Ｌ 形式语义ＳＩ Ｇ Ｎ Ａ Ｌ 语言具有多种形式语义， 如踪迹语义和标签模型语义［１ ５］ 等． 本文遵循Ｐｌ ｏｔ ｋｉ ｎ 关于结构化操作语义的原则［１ ６］， 将ｋＳ Ｉ ＧＮ Ａ Ｌ 的操作语义定义为一个标签变迁系统＜ Ｓ ， Ａ ，—＞ ， 其中状态集Ｓ 中状态为进程Ｐ 所有可能状态， 标签Ａ 对应进程Ｐ和外界环境的交互，—：Ｓ Ｘ Ａ Ｘ Ｓ 为变迁规则． 约定变迁规则的记号为ＣＳ ｌ＞ Ｐ －＾Ｓ，＞ ｐ＇其中， Ｓ 〇Ｐ 和Ｓ＇ 分别表示进程Ｐ 的两个状态；〇： ６｛ ？Ｒ ｅ ｃｅ ｚＸ Ｊ ， ｕａＺ Ｍ ｅ ） ， Ｓ ｅ”ｃ ？ （ ０ ） ， ｒ ｝ 表亦进程Ｐ的动作； Ｃ 是与Ｓ＞ Ｐ、Ｓ＇和〇有关的前置条件． 该记号表示在前置条件满足时， 进程Ｐ 可以在状态Ｓ下完成动作ａ 并变迁到Ｙ 状态．首先， 进程Ｐ 的状态定义如下．定义１ ． 状态． 进程Ｐ 的状态定义为逻辑时钟、信号变量、端口和基本进程执行标记的取值组成：Ｓ ： Ｔ ＋ Ｐ Ｖｌｉ ｒ ＋ ｛ ｐｏ ｒ ｔ ， ｆｌａ ｇｐ｝－＞？Ｓ ｉ ｒｔｗｏ －＾ Ｖａ ｌ ｕｅ＾ｌＢｏ ｏ ｌｅａ ｎ ，其中， Ｔ 表示Ｐ 当前的逻辑时钟取值， 信号变量集合Ｐｖ ｗ 表示在不同时钟下取值可能不同（ 包括丄） ，／ｗ ｒ ｆ 和／ｔｏｇ ，， 分别表示端口状态和进程Ｐ 中基本数据流等式的执行状态． Ｐ 的初始状态为Ｓ。厶｛ ０ ｝Ｕ｛ 切［ 了］ ： 丄Ｉ功６｝ Ｕ ｛Ｐ〇＂ ：Ｔ ｒｕ ｅ ｝Ｕ｛ ｆｌａ ｇｉ ：Ｆ ａ ｌ ｓ ｅ｜  ｉＧＰｓ？｝ ■其次， 定义谓词前提．定义２ ． 前提ｐ ｒｅＣ． 在给定逻辑时刻丁下， 基本数据流等式的前提归纳定义为：（ １ ） ｐｒｅＣＵＡ（ （ ｘ， ［ Ｔ ］ ＾ｌ ＜ ／￡ｎ丄） ） ） 八（－１ｆ ｏ ｒ ， ） Ａ ｙｖ ＜２ ｇｖ ： ＝ ／ （． ｒｉ；（ ２ ） ＾ｒ ｅＣ１ （ ｘ：＝ａ ￥ｉ ｎｉ ｔＯ Ａ Ｃ ａ ［ Ｔ ］ 关丄） 八（ 八［ ｚ．］＝ 丄） ） Ａ（－？／ Ｊ Ｏ ＂ ） Ａ ￥ｉ ？ ｉ ， ｃ ；（ ３ ） ／＾Ｃ２（ ｘ：＝ 々￥ｉ ｎｉ ｔ 。＾ （ 々［了］ 关丄） 八（ Ｖ （ ？ｒ １ ［ ｚ＇］ ＿ 丄） ） Ａ（－＞／ ＞ 〇＂ ）／ ＜ 丁１（ ４ ）：＝Ｘｉｗ ｈ ｅｎ ６ ） 会（ 々［ 了］ ＃ 丄） 八（ ６ ＝ Ｔ ｒ ｕ ｅ） ）Ａ （－＞ｐｏ ｒｔ ｝ｈｆｌ ａｇｘ ：＝ＸｉＶｉ ｈ ｃ ｎ ｈ ＼（ ５ ） ｐ ｒｅＣ１ （ ｘ：二：＊ ＾ｄｅｆａ ｕｌ ｔ ｘ２ ［了］ 古丄） 八（－１ｐｏ ｒ ｔ ）Ａｆｌ ａｇ＾ ：  ＝ Ｓ］Ｍａ ｕ Ｕ ｒ２；（ ６ ） ／＞ ｒｅＣ２（ ｘ：＝ ｊ：ｉ ｄｅｆａ ｕｌ ｔ ｘ２ ） 会（ ｘ ！［ 了］＾ 丄） 八２ ２ ２ ０ 计算机学报 ２ ０ ２ ０ 年（ ｘ ２ ［ Ｔ］ 尹丄） 八（，ｐｏ ｒｔ ） 八／ｔｅｇ，？ｉｄ ｅ ｆ ａ ｕｌ ｌ Ｊ＿２．最后， 依次定义四类基本结构、组合操作和与环境交互的变迁规则． 其中外部不可见动作ｒ 被忽略．基本结构设Ｐ 为瞬时函数： ｃ ：＝ ／ （ 々， ＆ ，…， ｘ，，） ， 则Ｐ的语义规则Ｒ ｌ ． １ 定义为Ｓ＾＝ｐ ｒｅ Ｃ（ Ｐ）Ｓ＞ Ｐ＾ Ｓ［ ／（ ｘ， ［ Ｔ］ ， ？ ？ ？ ， ａ－？ ［ Ｔ］ ） ／ ｘ ［ Ｔ］ ，．Ｆ ａ ｌ ｓ ｅ ／ ｆｌａ ｇｐ ＾＼ ＞ Ｐ设ｉ３ 为延迟操作ｉ ：＝ｘ，￥ｉｎ ｉ ｔ ｏ 则Ｐ 的语义规则Ｒ ｌ ．  ２ 和Ｒ ｌ ． ３ 分别定义为Ｓ ＼＾ ｐ ｒｅＣ ＇（ Ｐ ）Ｓ Ｄ＞ Ｐ －＾ Ｓ ［ ｃ ／ｘ［ Ｔ］ ， Ｆａ ｌ ｓ ｅ／ ／Ｚａ ｇ＇ｐ ］  ＞ Ｐ？Ｓ ＼＝ ｐ ｒｅＣ２（ Ｐ ）Ｓ ［＞ Ｐ－？－ Ｓ ［ｘ ｉ ＼＿ｉ￣＼ ｆ ｘ＼＿Ｔ￣＼ ， ￥ａ ． ＼ ｓ ｅｆ ｆｌａ ｇＰ￣＼ ｔ＞ Ｐ其中，丨ｊｃ，  ［ ｔ＇］ ￥丄｝ ？设Ｐ 为条件采样：ｃ  ：＝Ａｗ ｈｅ ｎ６ ， 则Ｐ 的语义规则Ｒ ｌ ． ４ 定义为Ｓ＾ ｐｒｅ Ｃ（ Ｐ ）Ｓ＞Ｐ＾ Ｓ［ ｘ， ［ Ｔ］ ／ ｘ ［ Ｔ］ ，  Ｆａ ｌ ｓ ｅ／ ｆｌａ ｇｐ  ］ｔ＞ Ｐ＇设Ｐ 为确定性并发ｉ：＝ｐｄ ｅｆ ａ ｕ ｌ ｔ ｘ２ ， 则Ｐ 的语义规则Ｒ ｌ ．  ５ 和Ｒ ｌ ．  ６ 分别定义为Ｓ ＼＝ ｐｒ ｅＣ ｌ（ Ｐ ）Ｓ ＞ Ｐ＾ Ｓ［ｘ， ［Ｔ］ ／ ｘ［ Ｔ］ ， Ｆａ ｌ ｓ ｅ／ ／Ｚａ ｇ－ｐ ］ ＞ Ｐ５Ｓ ＾ ｐｒ ｅＣ ２（Ｐ ）Ｓ ＞Ｐ＾ Ｓ［ ｘ２ ［ Ｔ ］ ／ ｘ ［ Ｔ］ ， Ｆａ ｌ ｓ ｅ ／ ｆｌａ ｇ，］ ＞Ｐ＇组合操作设Ｐ 为组合操作朽Ｉ Ｐ２ ， 则Ｐ 的语义规则Ｒｌ ． ７和Ｒ ｌ． ８ 分别定义为Ｓ ＞ Ｐ，＾ Ｓ，＞ Ｐ，Ｓ Ｄ＞（ Ｐ ，｜Ｐ２ ）—丨 ｜Ｐ２ ）’Ｓ ｔ ＞ Ｐ２— Ｓ， ＞ Ｐ２｜Ｐ２ ）—环境交互设ｐ 的输出和输出变量集合分别为ｉ■和６ ， 进程Ｐ 和外部环境交互的语义规则Ｒ １ ． ９ 和Ｒ １ ．１ ０ 分别定义为Ｓ （＝／ ＞ ｏ ｒ？Ｓ ＞ ＰＲｅｃ ｅｉ ｖｅ ｄ Ｉ ｒ ｖａ ｌ ｕ ｅ）Ｆａ ｌ ｓ ｅ／ ｐ ｏ ｒｔ ］ ＼＞ ＰＳ＼＿ｖａ ｌｕ ｅ／ １ ， Ｔ ｒｕｅ ／ｆｌａ ｇＰ ，Ｓ ｜＝ （ＡＣ ｆｌ ａ ｇｐ－＊（￣ｉ ｐ ｒｅＣ Ｃ ｐ ） ） ）＇） Ａ （—＇ ｐ ｏ ｒｔ ）ｐ ＾ ｐｓ ，Ｓｅ ｎ ｄ （ Ｏ＇）Ｓ＞ Ｐ＞ －Ｓ ［Ｔ ｒｕ ｅ／ ｐ ｏ ｒ ｔ ， Ｓ ｕｃ ｃ （ Ｔ） ／ Ｔ＾＼ ＞ Ｐ以Ｒ ｌ． １ 规则为例解释对应变迁规则的具体含义： 瞬时函数的语义规则表明当等式右侧所有变量在状态Ｓ 中都有值， 且该瞬时函数未被执行， 即对应标志位为Ｔｍｅ ， 则将〇： 的值赋为运算符／作用下的取值， 且置对应／ｔｅ ｇ 为Ｆａｌ ｓ ｅ．３ ． ２ｃｌ ｏｃｋｅｄ ＳＩＧＮＡＬ３ ． ２ ． １ 时钟演算ｃ ｌ ｏｃ ｋ ｅ ｄＳＩ ＧＮ Ａ Ｌ 程序是ｋ ＳＩ Ｇ Ｎ Ａ Ｌ 经过时钟演算后生成的， 因此本节在构造ｃ ｌ ｏ ｃｋ ｅ ｄＳ Ｉ Ｇ ＮＡ Ｌ 操作语义之前， 需要形式化定义时钟演算． 时钟演算的形式化描述具体包括：（ １ ） 形式化定义时钟关系抽取函数和子句集构造函数；（ ２ ） 形式化表示求解时钟等式系统算法；（ ３ ） 基于时钟等式系统Ｅｇ 定义时钟依赖图．ｋＳ Ｉ ＧＮ ＡＬ 的基本结构冋时包括功能关系和时钟关系， 时钟关系抽取函数０ （ Ｐ ） 用于计算出ｋＳ ＩＧ Ｎ Ａ Ｌ 模型中的时钟关系． ＃（ Ｐ ） 可根据进程Ｐ的结构归纳定义如下：（ １ ） 当尸＝＾： ＾ ／ （ ：＾ ，…， ｘ？ ） 时： 必（ ｘｔ ／ Ｏｉ ，…， 工？ ） ） 会｛？￡？＝？￡？，■  ｜ ｌ ＜ ｚ＜ ｗ ｝ ；（ ２ ） 当Ｐ＝ ：ｃ  ：＝而￥ｉ ｎ ｉ ｔ ｃ时： 必０：＝ ｘ ，￥ｉ ｎ ｉ ｔｃ ） Ａ｛ ｘ ＝ ｉ ｔ ｝ ；（ ３ ） 当＿Ｐ＝ ：ｒ  ：＝ ｊ： ｉ ｗｈ ｅ ｎ６ 时： 必（ ｘ：＝？！！ ｗｈ ｅ ｎＡ Ｍ ；（ ４ ） 由Ｐ二：＝ＪＴｉｄ ｅｆ ａ ｕｌ ｔ工２时： 必（ 工：＝工１ｄ ｅ ｆａ ｕ ｌ ｔｘ ２＝Ｖ ｉ＂２ ｝ ；（ ５ ） 当Ｐ ＝ Ｐｌ  丨朽时： ＾ 巧 ｜Ｐ２ ） 蠱＃子句集构造函数用于将时钟关系等式进一步转换为对应子句集， 以便后续进行时钟演算．Ｃｌａ ｕ ｓ ｅ （ Ｐ ）＾ （Ｕ｛ ｛—＇ｘ ， ｘ ｔ ｝ ，｛—＞ｉ ；，  ｉ－｝｝ ）Ｕ＜．ｆ ＝ｊ ．  ） ６ ＾（ ／＞）（ ． Ｔ ＝ ：－， Ａ ４） ６  ＾ （ ／＞）（Ｕ｛ ｛－１ ｉ－， Ｘ！ ， ｉ ２ ｝ ？｛－ｌｉ ｉ  ， ｉ ｝ ， ｛－＞ ｉ２ ， ｉ－｝ ｝ ）．＜ ． ７ ＝ ．ｒ｜ Ｖ ．ｒ＾ ）＾ Ｉ＊）形成的子句集记为同时， 后续时钟演算中涉及到子句集操作定义如下：函数ＰＯ Ｓ ⑴ ， 表示变量在子句集Ｄ 中正出现的子句集； 同理ｉＶ￡Ｇ（ ｆ ２ ，ｘ／） Ａ ｛ ｃＺ｜■ ｕ Ｇ ｃＺ Ａ￡■／ £ ■？０ ｝ 表７Ｋ ｔ／ 在中负出现的子句集．集合｛１；｝ ｜ “ ６ 尸〇５ （仏１ ； ） ｝ 表示将ｗ 正出现的子句集中减去Ｗ ， ＪＶＥ Ｇ，， 会｛ ｃＺ—｛－Ｉｗ ｝丨袁胜浩等： 同步语言多线程代１ １ 期 码生成 的语义保持证 明方法 ２ ２２ １ｃ ／ ｅ ｉＶＥＧ Ｃ Ｄ ｄ ） ｝ 表示将ｔ； 负出现的子句集中减去Ｈ．求解时钟等式系统算法描述了时钟演算的核心步骤， 根据输人的ｋ ＳＩ Ｇ Ｎ Ａ Ｌ 程序Ｐ 中的时钟关系，计算出所有有定义的时钟等式， 形成时钟等式方程Ｅｇ 并输出． 算法首先计算出子句集Ｘ２ 并初始化有关变量（ 第１ 行） ， 然后进入循环， 依次计算出所有有定义的时钟等式（ 第３ ？１ ２ 行） ： 如果子句集中存在空子句（ 记为丨｝ 或０ ） ， 则表示时钟关系中存在矛盾，报错并终止算法（ 第３ 行）； 否则任选一个未定义变量Ｉ； （ 第５ 行）， 计算其对应的Ｐ〇Ｓ．ＪＪＶＥ Ｇ ，， 形成的新子句集， 新生成的子句集中永真子句被忽略（ 第７行） ， 其余子句添加到Ｄ 中（ 第８ 行） ； 最后将ｔ ； 对应的时钟等式加人到中， 并在中删去与ｒ 有关的子集． 当子句集为空时， 循环结束（ 第２ 行） ， 并返回时钟等式方程Ｅｇ （ 第１ ３ 行） ．算法１． 求解时钟等式系统算法．输人： ｋ ＳＩ ＧＮＡ Ｌ 进程Ｐ输出： 时钟等式方程Ｅｇ１． Ｑ ＾ Ｃｌａ ｕ ｓ ｅ Ｃ Ｐ ）０ ＼ Ｅｑ？＝０２ ． ＷＨ ＩＬ Ｅ Ｓ ７＾ ０Ｄ Ｏ３．Ｉ Ｆ｜＝（ Ａ （ Ｖ ｅ ） ） Ｔ ＨＥ ＮＥＲ Ｒ ＯＲｃ ｅ ｎ４ ．ＥＬ Ｓ Ｅ５ ．ｓ ｅ ｌ ｅ ｃｔ ａ －ｙ ＧＰ＼ Ｕ ｒ ＿ Ｄｅｆｉ Ｅｑ ）６ ．ＦＯＲ ＥＡＣ Ｈ〈ｈ Ｗ ｅ ｍＳ ｐ Ｘ ／ ＶＥＧ，ＤＯ７ ．Ｉ Ｆ＾Ｍ ｅＴ Ｈ ＥＮ ＳＫ Ｉ Ｐｅ ＾ ｐ ｖ  ｓ８ ．ＥＬ ＳＥａ— ａ Ｕ （ Ｐ Ｕ ｉＶ ）９ ．Ｅ ＮＤＦＯ Ｒ１ ０ ．Ｅｑ：＝ Ｅ ｑ ［ ｊ ｛ ｖ ＾ （Ａ（ ＼Ｍ ） ｝ｃ ｅＳＥＧ ，，＊＞ ｅ ｃｎ ．ａ■■＝ ａ〇（ｊ （ 〇－ ｐ〇ｓ ｉ ａ ， ｖ ）－ ＮＥＧｉ ａ ， ｖ ） ）１ ２ ．  ＥＮＤＷ ＨＩＬ Ｅ１ ３ ． Ｒ Ｅ ＴＵＲＮＥｑ根据时钟等式系统ｅ９ ， 可按如下方式定义时钟依赖图〈Ｖ ， ￡＞ ：ａ ） Ｖ＾Ｄ ｅｆ（ Ｅｑ）  ｕ ｛ Ｐｖ． ｒ－ Ｄ ｅｆ （ Ｅｑ ） ｝ ；（ ２ ） ￡ＧＶ Ｘ Ｖ ， 其中Ｕ ， 巧〉Ｅ Ｅ 当且仅当至少以下条件之一成立：① 》丨， ｔ；２ ＧＤｅ／（ ￡ｇ０ 并且存在叫６Ｅｇ  （ ｉ丨６ｒｉ ｇｈ ｔ （ ｅｑ ）／＼ ｖ２ ＝ ｌ ｅｆｔ （ ｅ ｑ＇）＇）；② 巧６—〇ｅ／（Ｅｇ） ， 巧６Ｄ ｅ／（） 并且存在ｅ ｑ ＆ Ｅｑ ， ｋ ＾： ｒ ｉ ｇｈ ｔＸ ｅｑ＇） Ｕｚ ＾： ｖｉｌ ＼ ｖｉ＝ｌｅ ｆｔ ｉ ｅｑ ）＇） ．其中｛Ｐｖ．，， ｒ— Ｄｅ ／（ ｆ：９）｝ 记为根节点ｒｏｏ ｆ ， 函数Ｚ ｅ／ｉ （ ｒ ｆ ｇ／ｉ Ｚ ） 用于计算时钟等式ｅｇ 左侧变量（ 右侧变量集合） ．易证上述定义方式形成时钟依赖图为有向无环图， 以及具有根时钟．３ ．  ２ ． ２ｃｌ ｏ ｃｋ ｅ ｄＳ Ｉ ＧＮ Ａ Ｌ 形式语义基于ｋＳ ＩＧ ＮＡ Ｌ 语义对应的变迁系统〈Ｓ ， Ａ ，— ＞，ｃ ｌ ｏｃｋｅ ｄＳＩ ＧＮＡＬ 语义对应的变迁系统〈Ｓ＇， Ａ ，—＇＞ 定义为： Ｓ＇ ４ ｛ ＼ Ｕ，６ Ｓａ ｎ ｄ ＼ ｔ＝ ｆ＾ａ ｎ ｄ．？；｜＝ ｒ ｏｃ ＾ ｝ 以及—， 会ｓ， ２ｎ —．其中叫 ｆｏｒ  ａ ｌ ｌ 叫６ ￡？ ．ｃ ｌｏ ｃｋ ｅ ｄＳ Ｉ ＧＮ Ａ Ｌ 语义定义表明， 只有当消解后的程序同时满足根节点存在且时钟等式方程约束时， 程序执行才有意义．３ ． ３Ｃ 子集本节介绍一个包含源语言特性的Ｃ 语言子集作为目标语言， 并形式化定义ｃ ｌｏ ｃｋ ｅ ｄＳ ＩＧ ＮＡＬ 到Ｃ之间翻译函数， 最后基于标签变迁系统定义所选Ｃ子集的形式语义．３ ． ３ ． １Ｃ 子集形式语法首先， 选择的Ｃ 子集由三类条件语句和并发语句组成， 其抽象语法如下所示：Ｐｃ Ｉ ；＝ ｉ ｆ ｂ ｉ ｔｈ ｅｎ ｊ：ｉ ：＝ｅ Ｙ｜ ｉ ｆ ｂ ＼ ｔ ｈｅ ｎ ＸｊＳ＼  ； ｊ ｔ ？ｅ ｌ ｓ ｅｉ ｆ ｂｚ ｔ ｈ ｅ ｎｘ３：＝ｅ３｜ ｉ ｆ ｂｉ ｔ ｈｅ ｎＸ ！ ：＝ｅ ｌ ｓ ｅｉ ｆ ｂ２ ｔｈ ｅ ｎｘ －ｉ＇■＝ ｅ ２Ｉ ｅｑ ｜ ｜ ｅｑ其中，？ 为变量， ｅ，？ 为表达式， ６，？ 为布尔表达式．３ ． ３ ． ２ｃ ｌ ｏｃｋ ｅ ｄＳ Ｉ Ｇ ＮＡ Ｌ２ Ｃ编译过程其次， 本文选择基本的任务划分算法［ １ °］， 其基本原则是每个基本结构对应于一个划分， 并转换为对应的目标线程． 这里本文将其抽象为ｃ ｌ ｏｃ ｋ ｅｄ－Ｓ Ｉ Ｇ Ｎ Ａ Ｌ ２ Ｃ 翻译函数， 该翻译函数由计算函数ｐ （ Ｐ ）和内存更新函数０ （ Ｐ ） 组成．根据ｃ ｌｏ ｃｋ ｅ ｄ Ｓ Ｉ ＧＮ Ａ Ｌ 程序Ｐ 的结构， ＜ｐ （Ｐ） 归纳定义为：（ １  ） 当时：：＝／（ 而，…，Ａｘ，ｔ ｈｅ ｎ Ｘ：＝ ／（ ｘｉ  ， ？ ？ ？，） ；ｌ ＜ｉ＜ ｎ（ ２ ） 当 ｊＰ＝ｘ￥ｉ ｎｉ ｔ ｃ 时： ｐ （ ：ｒ￥ｉ ｎｉ ｔｒ ）Ａ ｉ ｆＸ， 八／ ７ａ ｇｖｔｈ ｅ ｎＭｅ ｍ． ｒ：＝ ｃ ；＿ ／７ ａ ｇ ＿ｒ  ：＝ｆ ａ ｌ ｓ ｅｅ ｌ ｓ ｅｉ ｆｔ ｈｅ ｎＭｅｍ＾ ■＝ｘ ｊ ；（ ３ ） 当Ｐ＝ｘｗ ｈ ｅｎ ６时：９５ （ ＿ ｒ：＝■！■！ｗ ｈ ｅｎｆｅ ） Ａ ｉｆ ｉｊ 八６ ｔｈ ｅ ｎｘ：＝工１ ；（ ４ ） 当Ｐ ＝ｘ：＝；！：！ ｄｅｆａ ｕ ｌ ｔ ＿ｒ２ 时：９５ （ ｘｄｅ ｆａ ｕ ｌｔ－ｉ ｉ ｔｈ ｅｎ ｊ：：＝Ｘ！ ｅｌ ｓ ｅｉ ｆ （—＇ ｉ－！  ） Ａｉｔ ｈｅｎｘ－＝ｘ ＞－，２ ２ ２ ２ 计算机学报 ２ ０ ２ ０ 年（ ５ ） 当时： ９＾ （ ｅ ９ ） ＾ ｅ９ ；（ ６ ） 当１３＝ 巧｜ 朽时： ９ ３（ 巧 ｜Ｐ２ ） Ａ？３ （ Ｐ１ ）｜ ｜ ｆ （ 朽） ？内存更新函数０（ Ｐ ） 与延迟动作相关， 负责更新内存变量． 因此＃ ？？ ） 定义为：（ １ ） 当■？ ＝；！ ：：＝＿ｒｉ ￥ｉ ｎｉ ｔｃ ： 必（ ｊ：：＝ ｘ ！ ￥ ｉｎ ｉ ｔ ｃ ） ４ｉ ｆ ｉ：ｉ ｔ ｈｅ ｎｘ ＾ Ｍｅｍ＾ ；（ ２ ） 当Ｐ＝ Ｐ， ｜Ｐ２ ：０（ Ｐ， ｜Ｐ２ ） 么＃ 巧）Ｉ Ｉ ＃ Ｐ２ ） ．对于一个ｃ ｌｏ ｃ ｋｅ ｄＳＩ Ｇ Ｎ Ａ Ｌ 进程Ｐ ， 其生成的命令式程序为Ｐｒ＝ Ｐ （ Ｐ ） ＋ ０ （ Ｐ ） ， 其执行顺序为每次计算函数结束后， 执行一次内存更新函数．３ ． ３ ． ３Ｃ 子集形式语义最后， Ｃ 子集的操作语义定义为变迁系统〈及，Ａ ，—＞ ， 状态沒民包括时钟、变量、内存变量和内存标志：ｓ：Ｔ ＋ ｛Ｐ Ｖａ ｒ ， Ｐ Ｍ＞ ｍ ｝ ＋ ｛ ｆｌ ａ ｇＭｒ ｍ，ｆｌａ ｇＰ ， ｐｏ ｒｔ ｝ｔ ｙ〇 ＋ Ｖｉ２ ＺＭ ｅ丄＋ Ｂ ｏ ｏＺ ｅａ ｗ．特别地， ｃ Ｉ ｏｃｋ ＳＩ Ｇ ＮＡ Ｌ 中变量是时钟到变量取值的函数映射空间， 而Ｃ 程序中变量直接取为当前时钟下的变量取值， 因此需要额外定义内存变量和内存标志用于记录历史数据． Ｓｊ初始状态ｕ ｎ ： 丄卜ｅ Ｐｗ Ｕ ＪＶＪ Ｕ｛ ｖ －．Ｔ ｒｕｅ ＼ ｖ Ｅ ｆｌａ ｇＭｒ ｍ＼Ｊ ｆｌａｇ Ｐ ＼Ｊ ｛ ｐｏ ｒ ｔ ｝ ｝ ．类似地， 在定义Ｃ 子集变迁规则之前， 需归纳定义对应的谓词／＞ ｒｅ ｃ Ｃ ：（ １ ） ｐｒ ｅ ｃ Ｃ（ ｉ ｆｂ ｊ ｔｈ ｅ ｎｘ ｉ－＝ｅ ＼ ） ＾ｐｏ ｒ ｔ ）Ａ ｂｙ Ａｆｌａ ｇ ；（ ２ ）ｐｒ ｅｃＣ １ （ ｉｆ ｂ ｉｔ ｈｅ ｎ ？３＾ １＊＝£ ＼ ； Ｘ －ｚ６ ２ｅ ｌ ｓ ｅ ｉ ｆ ｂ ｔｔ ｈｅ ｎ ｘ３ ：＝ｅ３ ） ＾ （—ｉｐｏ ｒｔ ） ｆ＼ｂ＼ｆ＼Ｓ＼＝＾ｐｒｅ ｃＣ ｛ ＼｛ ｂ＼ ｔ ｈｅ ｎＸ ＼ －＝ｅｉ）Ｓ ＞ ｉ ｆｂ ｘｔ ｈ ｅ ｎｉ＝ ｅ＼＾ Ｓ ＼＾ｅ／ ｘ ，？Ｆａｌ ｓ ｅ ／／Ｚ ａ＾ ｉ （ ｉ ｔ ｈ ｅｎ ｊ ！＝ｆ｜］＞ ｉ ｆ ６， ｔ ｈｅ ｎ ｊ：， ：＝ ｅ，设Ｃ程序为＿ Ｐｃ＝ｉ ｆ ６丨ｔ ｈ ｅｎａ ：＝ 心； ｘ２ ：＝〇ｅｌ ｓ ｅ ｉ ｆ６２ｔ ｈ ｅｎ ｘ３  ：＝ｅ ３ ， 则对应语义规则Ｒ２． ２ 和Ｒ２ ．  ３ 分别定义为Ｓ＼＾ｐｒ ｅｃＣ ｌ （ ｉｆ ｂ ｉ ｔ ｈｅ ｎ Ｘ＼￣ ｅｊ ； ｘ ２？＝ ｅ２ｅ ｌ ｓ ｅ ｉ ｆ ｂ ２ ｔ ｈｅ ｎｘ ３：＝ ｅ３ ）Ｓ＞ｉ ｆ６ｉｔ ｈ ｅ ｎｘ＼ ：＝ｅｘ ； ｘ２ ＊＝ｅ２’ｅ ｌｓ ｅ ｉ ｆ ｈ－ｉ ｔｈ ｅ ｎｘ ３ ｅ３－＾ Ｓ［ ｅｉ ／ ｊ：ｉ ， ｅ２ ／ ｘ ２＞ｉ ｆｔ ｈｅ ｎ  ｊ－ｊ ＊＝Ｃｊ ｊ＾２１ －１＊２ ｅ＾ ｓ ｅ ＾＾＊ ＾ ｅｎ  ＾３！＝＜，ｉ＾＾ｉ ｆｂ＼ｔ ｈ ｅｎ Ｘ ＼ ，＞：＝ £＼ ； ｘ ？６ ２ｅ ｌ ｓ ｅｉ ｆ ｂ２ ｔ ｈｅ ｎ：＝ｅ ３Ｓｊ＝ｐｒｅ ｃＣ２ （ ｉ ｆ ｂ ｘ ｔ ｈｅ ｎ ｘ ｘ：＝ｅ ｘ  ； ｘ ２：＝ｅ ２ｅｌ ｓ ｅ ｉ ｆｂｔ ｔ ｈ ｅｎ ｘ３ ？ ＝ｅ３ ）ＳＤ ＞  ｉ ｆｂ＼ ｔ ｈ ｅｎ ｘ ｘ ：＝ｅ ｘ ； ｘ２ ：＝ｅ２ｅ ｌ ｓ ｅ  ｉｆ ｂ ｔ ｔ ｈ ｅｎ ｘ３＇＝ｅ３＾－Ｓ ［ｅ３ ／ ｘ３ ， Ｆａ ｌｓ ｅ ／ ／＇＾＾ ｉ ｆ ６ｉｌｉ ｉｅ ｎ Ｘ！ｉ ＝ｔ，ｉ［ Ｘ２．＝＾ ｅ ］ｓｅ ｉ ｆ ６７ ｔ ｈ ｅｎ ｊ．： ｊ， ＝ｔ．３］ｉｆ ｂ ＼ｔ ｈ ｅｎ Ｘ ＼ ？：＝ｅ ＼ ｊ Ｘ２ｅｌ ｓ ｅ ｉ ｆ ｂ２ｔ ｈ ｅ ｎｘ ３－＝ｅ３设Ｃ程序为Ｐ ｃ ＝ｉ ｆ ６ １ｔ ｈ ｅｎ Ｘ 〗：＝合丨ｅ ｌ ｓ ｅ ｉｆ ＆２ｔ ｈ ｅｎ ｘ ２：＝， 则对应语义规则Ｒ２ ． ４ 和Ｒ２ ． ５ 分别定义为Ｓｐ ｒｅ ｃＣ １ （ ｉ ｆ ｂ ＼ ｔｈ ｅ ｎｘ ｘ ：＝ｅｌ ｓ ｅ ｉ ｆ ｂ２ ｔ ｈ ｅｎ ｘ ｔｅ ２ ）Ｓ＞ｉ ｆｂｘｔ ｈ ｅｎ Ｘ ＼ｅｘ’ｅ ｌ ｓ ｅｉ ｆｔｈ ｅ ｎ ｘ２／ ：＾ ，Ｆ ａｌ ｓ ｅ ／ｔｈ ｅ ｎ：＝ｔ＊ｉ ｅ ｌ ｓｅ  ｉｆ ／，２ ｔ ｈ ｅｎ  ｊ＊， ： ＝（＊２］ 〉ｉ ｆｂ ＼ ｔ ｈ ｅｎ ｘ ｉｅｘｅｌ ｓ ｅ ｉ ｆ ｂ２ ｔ ｈ ｅｎ ｘ ２：— ｅ２ｉｆｔｈ ｅｎ  ｊ－ｊ＞ ＝ ｃｊｊ Ｊｇ１ ＝ ，＊ｏ ｅｌ ｓ ｔ＇＾２Ｘ３１ ＝ｆ３＊（ ３ ）ｐｒ ｅ ｃＣ ２ （ ｉ ｆ ｂｘ ｔ ｈｅ ｎ ｘ ｘ：＝ｅｘ ； ｘ２ ：＝ｅ ２  ｅｌ ｓ ｅｉ ｆｂ ２ ｔｈ ｅ ｎｘ ｚ：＝ ｅ３ ） ＾ （－＞ｐｏｒ ｔ ） Ａ（￣＊ ＾１ ）Ａ心２八■／＇，“ 尽 ｉ ｆ ＼ｔ ｈ ｅ ｎ ｊ＊ｉ ：ｉ ＿ ｒ９ ＊＝ｆ２ ｔ＇ｌ ｓｅ  ｉ ｆ  ６２ ｔ ｈ ｅ ｎ ｊ：３：，（ ４ ） ｐｒ ｅｃＣ １（ ｉ ｆ ６１ ｔ ｈｅ ｎ ｘ＼：＝ｅ＼ ｅｌ ｓ ｅｉ ｆ ｂ２ ｔ ｈｅ ｎ工ｐｏ ｒ ｔ ） ｆ＼ ｂ＼ ｆ＼ｉ ｆｔｈ ｅ ｎ！ ＝（＊ｊｅ ｌ ｓｅ ｉ ｆｔ ｈｅ ｎ ． ｔ９ｉＪ（ ５ ）ｐｒ ｅ ｃＣ ２ （ ｉ ｆ ｂ ＼ ｔ ｈｅ ｎ ｘ ｘ：＝ｅ ｘ ｅｌ ｓ ｅ ｉ ｆ ｂ２  ｔｈ ｅ ｎ工ｔ＇＝Ｋ ， ｐｏ ｒ ｔ 、ｔ＼ｂ ＇ 、［ ＼Ａ ／／ａｇ ｉ ｆ６ｉ， ｈ ｅｎ Ｊｉ！ ＝ ＜＊｜ｅｌ ｓｅ  ｉ ｆ ｂ０ｔ ｈ ｅ ｎｉ ＝ｅ９＊ｃ 子集对应操作语义规则按如下方式定义：设Ｃ 程序为＝匕ｔ ｈ ｅ ｎＸ ， ：＝Ａ ， 则对应语义规则Ｒ２ ．  １ 为Ｓｐ ｒｅｃ Ｃ １ （ ｉ ｆｂ ｉｔ ｈ ｅｎ Ｘ ｉ ：＝ ｅ＼ｅ ｌ ｓ ｅ ｉ ｆ ｂｚ ｔ ｈ ｅｎ ｘｚ＾＝ｅ｛）Ｓ＞ ｉ ｆｂｘｔ ｈ ｅｎ Ｘ ＼ ：＝ｅ＼？ｅ ｌ ｓ ｅｉ ｆ ｂ２  ｔｈ ｅ ｎ ｘｚ ：＝ ｅ ２＾ Ｓ ＼＾ ｅ ２ ／ ｘ ２？ Ｆ ａ ｌ ｓ ｅ ／ｆｌａ Ｓ ， ｕｘｔｈ ｅ ｎ ｊ－ｊ＊ｅ ｌ ｓｅ  ｉ ｆ ｂ９ｔ ｈ ｅｎ  ｊ－，： ￣ｅ＾＾ｉ ｆｂ＼ ｔ ｈ ｅｎ Ｘ ｉ：＝ ｅｘｅ ｌｓ ｅｉ ｆ ｂ２  ｔｈ ｅｎ ｘ ， ■＝ ｅ２对于并发结构， 设Ｃ 程序为ＰＣ ＝Ｐ Ｃ 。｜ ｜ＰＣｌ， 则对应语义规则Ｒ２ ． ６ 和Ｒ２ ． ７ 分别定义为Ｓ＞ Ｐ ｃｏ＾ Ｓ＇＞ Ｐ ｃ 〇Ｓ ＞ Ｐｃ 〇｜ ＩＰ ｃ＾Ｓ＇［＞ Ｐ ｃ ０ ｜ ｜Ｐｃ ，＇ＳＩ ＞Ｐ ｃ丨一＞？＿？ （：！Ｓ ＞ Ｐｃ０Ｉ Ｉ Ｐ ｃ＾Ｓ＾ Ｐ ｃ ｏ Ｉ Ｉ  Ｐｃ ，＇对于外部环境交互， 对应语义规则Ｒ ２ ．８ 和Ｒ ２ ． ９ 分别定义为１ １ 期 袁胜浩等： 同步语言多线程代码生成的语义保持证明方法 ２ ２ ２ ３Ｓ＼＝ ｐｏ ｒｔＫｖ ， ｖａ ｌ ｕ ｅ ）＿？一＞ － ，？＿Ｓ ＼＞ Ｐ＾ Ｓ ［＾ ｖａ ｌ ｕｅ ／ ｖ９ Ｔｒｕ ｅ／ ｆｌ ａｇＰ  ］＼＞ ＰＡ（ ｆｌａ ｇｆ＞＾（—ｔ ｐ ｒｅｃ Ｃ（ ｐ） ） ） ） Ａ Ｃ￣ｔ ｐ〇ｒ ｔ＇）＃ Ｐ５ｗ＿！ （ ｖ ｔ ｖａｌ ｕ ｅ），？Ｓ ＞ Ｐ＞ Ｓ ［ Ｊ＿／ Ｐ Ｖａｒ— Ｐ Ｍｆ ｍ？Ｔ ｒｕｅ ／ ｐｏ ｒ ｔ ， Ｓｕ ｃｃ Ｃ Ｔ） ／ Ｔ＾＼ Ｏ Ｐ注意ｃ ｌｏ ｃｋ ｅ ｄＳ ＩＧＮ Ａ Ｌ 中端口（ ｐ ｏｒｔ ） 等标记， 可以通过在实际物理设备上增加若干个从输出端口到输人端口的反馈信号来实现． 因此在语义保持证明过程中， 可以忽略ｃ ｌ ｏｃ ｋ ｅｄ Ｓ ＩＧ Ｎ Ａ Ｌ 语义中端口等标记对证明过程的影响．３ ． ４ 语义保持证明方法本节主要基于互模拟等价思想证明编译前后的语义一致性． 首先给出互模拟的定义， 其次介绍语义保持证明过程中的核心引理， 最后基于核心引理完成语义保持证明．定义３ ． 互模拟． 令Ｔ Ｓ ＝〈Ｓ ， Ａ ，—＞ 为一个标记转换系统． 互模拟定义为一种关系ｉ？ Ｑ Ｓ Ｘ Ｓ 使得， 如果〈…仏乂仏则对任意动作／＾ 八…下关系成立：（ １ ） ＼／ ｑ ［  （ ９１—＾ｇ ｌ＝＞３ｑ ｚ （ ｇ２＾－ｑ ？ ａｎ ｄｑ ［ Ｒ９２ ） ）；（ ２ ） Ｍｑ ｚ  ｉ ｑｚ－ Ｍ ＊－ｑ ２ ＝＞３ｑ ［ （ ｇｉ — ａ ｎ ｄｑ ［ Ｒ ９２ ） ） ．如果上述关系有且只有一个被满足， 则称为单向模拟关系．由于ｃｌ ｏｃｋｅｄ ＳＩＧＮＡＬ 操作语义是基于ｋＳ ＩＧＮＡＬ操作语义构造而成， 易证时钟演算过程只存在单向模拟关系． 因此， 本节主要讨论ｃｌ ｏｃ ｋｅ ｄＳ Ｉ Ｇ Ｎ ＡＬ ２ Ｃ编译过程的语义保持证明．该过程语义保持证明主要涉及两类引理：引理１ ．ｃ ｌ ｏｃｋ ｅ ｄＳ Ｉ Ｇ Ｎ Ａ Ｌ２ Ｃ 编译过程具有单向模拟关系（ １ ） ．引理２ ．ｃ ｌ ｏｃｋ ｅ ｄＳＩ Ｇ Ｎ Ａ Ｌ２ Ｃ 编译过程具有单向模拟关系（ ２ ） ．引理１ 和引理２ 证明思路相似， 这里仅介绍前者的主要证明过程．证明（ 引理１ ） ．设Ｐ 为ｃ ｌ ｏｃｋ ｅ ｄＳＩ ＧＮ Ａ Ｌ 程序， 对应操作语义为〈Ｓ ， Ａ ，—＞ ， Ｐｃ 为经过翻译程序生成的目标程序， 对应操作语义为〈Ｓ ｃ ， Ａ ，￣＊ ＞ ． 模拟关系ｒｇ ｓ ｘ ｓｃ 定义为〇， ｓ ｃ ＞ ｅ 尺当且仅当ｖ 〇ｅｈ ｔ； ） ． 这里我们考虑程序内部执行过程（ 不考虑和外部交互行为） ， 因此变迁动作仅包括不可见动作ｒ．假设〈９ １， ＜？２ 〉６ 尺， 且９ｉ—９’１ ：根据证明树的深度进行归纳证明， 按证明树上应用的最后一条规则进行分类讨论．情形１． 当应用语义规则Ｒｌ ．  １ 时：：． ｑｘ ＼＝ｐ ｒｅ Ｃ （ Ｐ ） ，ｑ＼ Ｎ＝ ｘ［ Ｔ ］＝／ （ ＾［ Ｔ ］ ，－，ｘ？ ［ Ｔ ］ ） 且｜＝ ｉｒ ．根据谓词可得Ａ（ Ｕ ［ Ｔ］ 乒丄） ．．？？ 仍Ａ （ ｕ ［ ：ｒ］ 关丄） ， 即八（三） ？ｌ ＜／＜ ｎｌ ＾ ｔ＜ ？根据函数ｐ 得到（ Ｐｃ ＝ｉ ｆＡ＾ｔｈ ｅ ｎｘ：＝ｉ ＾ ／ ＜ ？ｆ （ ｊ〇ｉ  ，？ ？ ？ ， ｘ？ ） ） ：二根据语义规则Ｒ ２ ． １ 可得：存在￥＝９２ ［／ （ 工〗，？ ？ ？， 工《） ／ ｌ ］ 使得￥？易证＾ （ ｑ ［ ， ｑ２） ｅ Ｒ．情形２ ． 当应用语义规则Ｒ１ ． ２ 时：？？？ ％， ｇ（ｈ：ｒ ［ ：ｒ ］＝ｃ且ｉ ｈｉ ．根据ｐｒｅ Ｃ 可得１１＝： ＾ ．？ ？ 仍［＾ 工丨， 即仍ｔ工１ ■根据 ｐ得到（ Ｐ ｃ ＝ｉ ｆｉ 丨Ａ ／／ ａｔｔ ｈ ｅ ｎＭｅｍ． ｒ：＝ｃ ＼ ｆｌａ ｇｘ＾＝ｆａ ｌ ｓ ｅ ｅｌ ｓ ｅｉ ｆ ｘ＼ｔｈ ｅ ｎＭｅｍ ｓ＼＝ｘ ｘ ） ｉ二由语义规则Ｒ ２ ． ２ 成立可得：存在＆＝ｇ２ ［ ｃ／ ｘ］ 使得的一‘易证？？？Ｗｉ ６ Ｒ ．情形３． 当应用语义规则Ｒ Ｌ ３ 时＼＝ ｐ ｒｅ Ｃ（ Ｐ ）２９ ｑ［ ｜＝ｘ ［ Ｔ］＝Ｘ ｉｌ＝ｉ根据／＞ｒ ｅＣ 可得ｗ ｜＝ 工１ ．？？％， 即仍？根据ｆ 的定义可知， Ａ 前一个有取值时刻不是０时刻．？？？ 根据Ｒ２ ．  ２可知， 仍［＝ －＞／Ｚ ａ＆ ．二语义规则Ｒ２ ． ３ 成立？？？ 存在９丨＝９ ２ ［工１ ／从側１ ］ 使得根据＃ 可得Ｗ＝ｇ２ Ｄｒｉ ／ ｘ］ 使得易证丨（＝ 工．Ｗ＼Ｇ Ｊ？ ．易证， 对于Ｒ １ ．  ４？ Ｒ１ ． ６ （ 情形３？ 情形６ ） ， 存在￥使得且情形４． 当应用语义规则Ｒ １．７ 时／． ｇｉ＞ Ｐ［ ．２ ２ ２ ４ 计算机学报 ２ ０ ２ ０ 年根据归纳假设， 存在对应的仍＂ 仍［＾ ＾＾ 且〈取， ｑ’２ ） ｄ？？？ 由语义规则Ｒ ２ ． ６ 可得：ｑ ２Ｅ＞ Ｐ ｃｉ｜ ｜ Ｐｃ ２＾ｑ／２ ＞ Ｐ ｃｉ ｜ ｜ Ｐｃ２ ．情形５ ． 当应用语义规则Ｒｌ ． ８ 时根据归纳假设， 存在对应的￥Ｉ ＞ ＪＶ２ 且（ ｑ？ ， （０ £ ：Ｒ ．／． 由语义规则Ｒ ２ ． ７ 可得：ｑ２ ＞ Ｐ ｃｌ｜ ｜Ｐｃ ２￣＾ｑ２ ＞ Ｐｃｉ ｜ ｜Ｐｃ ｉ．综上所述， 因此可得Ｖ ｄ （ ｇｉ— ３ａ ｎ ｄｑ＾Ｒｑｉ ） ）．证毕．最后， 利用定理１ 完成语义保持证明．定理１ ．Ｃ ｌｏｃｋ ｅｄＳＩＧＮＡＬ２ Ｃ 编译前后语义保持．证明？ 根据引理１ 可知， Ｖｇ（ （ ＜？ ｉ— 一ｑ ［ ａ ｎ ｄ ｑ［Ｒ ＜ ？ ２ ） ） ．根据引理２ 可知， Ｖ Ｗ（ ｇ ２（ ９丨ａ ｎ ｄｑ ［Ｒ ｑ＇２ ） ）？？？ 即证明ｃｌ ｏｃ ｋ ｅｄ ＳＩＧ Ｎ Ａ Ｌ 程序和翻译后的目标Ｃ 程序两者语义互模拟等价．证毕．４ 相关工作在设计实现安全关键系统时， 代码自动生成技术是一种提高系统安全性的重要手段． 代码自动生成方法本身的正确性需要经过形式化的证明， 即证明翻译前后保持程序正确性等性质， 以确保不会出现误编译的情况（ 即一个错误的编译器可能在编译过程中插人错误） ．本文将已有编译器验证工作按照接收源程序不同划分为语言层面和模型层面：４ ． １ 语言层面Ｃ〇ｍｐ Ｃｅｒ ｔ［ １ ７］ 是经过形式化验证的可信编译器． 该编译器将Ｃ 的一个核心子集翻译为机器代码， 生成的代码性能在Ｐ ｏｗ ｅｒ ＰＣ 上可达到ＧＣＣ ４－ １性能的９ ０ ％ ． Ｃｏ ｍｐ Ｃｅ ｒ ｔ 基于数学的方式提出一种消除误编译的根本性解决方案（ 即携带证明编译Ｃｅｒｔ ｉ ｆ ｉ ｅｄＣｏｍ ｐｉ ｌ ｅ ｒ 方法） ： 通过辅助定理证明工具对编译器本身进行形式化证明， 在数学上证明编译器生成的可执行机器代码和Ｃ 源程序的语义上完全一致．在Ｃｏ ｍｐ Ｃｅｒ ｔ 的基础上， Ｇ ｏｒ ｄ ｏｎ 等人提出一种经过验证支持分离编译的编译器Ｃｏｍｐ ｏｓ ｉ ｔｉ ｏ ｎ ａ ｌＣｏｍｐ Ｃｅｒ ｔ． Ｃｏｍ ｐｏ ｓ ｉ ｔ ｉｏ ｎａ ｌ ＣｏｍｐＣｅ ｒ ｔ支持共享内存交互， 基于交互语义（ｉｎ ｔ ｅｒ ａｃ ｔ ｉ ｏｎ ｓ ｅ ｍａ ｎｔ ｉ ｃ ｓ ） 对模块和外部环境的交互进行建模， 并通过逻辑模拟关系证明与交互语义相关的编译步骤的正确性．４ ． ２ 模型层面基于Ｃｏｍ ｐＣｅ ｒ ｔ 编译器， 法国Ｉ ｎ ｒ ｉ ａＰａ ｒ ｉ ｓ 的ＰＡ Ｒ Ｋ ＡＳ 小组实现了经过验证的Ｌｕ ｓ ｔ ｒ ｅ 编译器Ｖ ６ ｌ ｕｓ［ １ ８ ］． Ｖ ６ ｌ ｕ ｓ 接收—ｔ＊Ｌ ｕ ｓｔ ｒ ｅ 语言子集， 经过若干编译步骤， 最终生成符合Ｃｏｍ ｐＣ ｅｒ ｔ 语法的Ｃ ｌｉｇ ｈ ｔ 程序， 并基于Ｃｏｍ ｐＣｅ ｒ ｔ 进一步编译生成可执行机器代码．类似于Ｖｄ ｕ ｓ ， 国内清华大学Ｌ ２ Ｃ 项目提出一个Ｌ２ Ｃ 编译器［ １ ９ ］ 支持将Ｌ ｕ ｓ ｔ ｒ ｅ 语言子集可信翻译到Ｃ 程序． Ｌ ２ Ｃ 编译器的编译过程中涉及到类型和时钟检查， 处理时序算子ｆｂ ｙ 和ｐ ｒ ｅ （ 类似于本文中的时钟演算） ， 并经过一系列翻译步骤， 生成符合Ｃｏ ｍｐ Ｃｅ ｒ ｔ 的 Ｃｌ ｉｇ ｈｔ 程序？此外， Ｐ ｎ ｕｅ ｌ ｉ 等人？ 提出了一种转换确认（ Ｔｒ ａｎ ｓｌ ａ ｔ ｉ ｏｎＶ ａｌｉ ｄａ ｔｉ ｏｎ） 的方法， 并验证从ＳＩＧ ＮＡＬ语言到Ｃ 程序的翻译过程． 该方法针对每一次具体的编译， 并且要求源程序和翻译后的目标程序具有共同的语义基础（ 基于变迁系统） ． 然后证明翻译前后是否语义保持， 采用的行为等价关系为单向模拟关系（ Ｓｉ ｍ ｕｌ ａ ｔ ｉ ｏｎ ） ．综上所示， 相比于转换确认方法， 本文采用了Ｃｏｍ ｐＣｅ ｒ ｔ 中提出的携带证明编译技术， 可以更加彻底地对编译器内部翻译步骤依次进行形式化证明， 并开展在定理证明器Ｃｏ ｑ 中完成证明过程的检查工作． 此外， 目前已有基于携带证明技术的同步语言语义保持证明研究主要侧重于串行代码生成的语义保持证明， 而本文主要关注多线程代码生成的语义保持证明．５ 总结与展望随着多核处理器逐渐被用于在安全关键领域，同步语言的多线程代码生成方法及其语义保持证明方法成为学术界和工业界共同关注的重要问题． 在前期研究中， 我们提出了基于Ｏ Ｃ ａｍ ｌ 的同步语言ＳＩ Ｇ Ｎ ＡＬ 多线程代码生成工具Ｍ ｉｎ ｉ Ｓ ＩＧ Ｎ Ａ Ｌ． 本文则进一步提出一种ＳＩ Ｇ Ｎ ＡＬ 核心编译过程的语义保持证明方法， 通过形式化定义编译过程中多种语言的操作语义和抽象代码生成过程， 并基于互模拟等价思想证明了多线程代码生成核心步骤的语义一致性．１ １ 期 袁胜浩等： 同步语言多线程代码生成的语义保持证明方法 ２ ２ ２ ５Ｍ ｉｎ ｉ Ｓ ＩＧ Ｎ Ａ Ｌ 的最终目标是生成一个新的ＳＩＧ Ｎ Ａ Ｌ验证编译器（ Ｖｅ ｒ ｉ ｆｉ ｅ ｄＣｏ ｍｐ ｉｌｅ ｒ  ） ， 即在Ｃｏｑ 中规约并证明编译规则的语义保持， 然后从Ｃｏｑ 证明中自动抽取编译器的实现． 本文目前主要考虑Ｍ ｉ ｎｉ ＳＩ ＧＮ Ａ Ｌ 核心编译步骤的语义保持证明，并选择Ｃ 子集作为目标语言． 为生成最终的ＳＩ ＧＮＡＬ验证编译器， 我们正在Ｃｏｑ 中开展对Ｍ ｉ ｎｉ ＳＩ Ｇ Ｎ Ａ Ｌ中其余编译过程如标准化、任务划分（ 涉及多种划分算法） 、虚拟多任务结构和多线程代码生成（ 涉及Ａ ｄａ 和Ｊ ａ ｖ ａ 等多种目标语言） 等阶段的语义一致性进行证明． 前期研究中我们主要关注Ｓ ＩＧ Ｎ Ａ Ｌ 多线程代码生成方法， 在未来的工作中， 我们将进一步考虑在执行平台机制方面的优化工作［２ １］ 及负载均衡等问题． ＳＩＧ Ｎ ＡＬ 主要用于描述系统的同步数据流行为， 难以对复杂信息物理系统进行建模． 因此我们还将研究基于架构描述语言八八０ １／２ ２］ 和Ｓ ＩＧ Ｎ Ａ Ｌ的异构建模方法．参考文献［ １ ］Ｌ ｅｖ ｅ ｓｏｎ Ｎ． Ｅｎ ｇ ｉ ｎｅｅ ｒ ｉ ｎｇ  Ａ Ｓａ ｆ ｅｒ Ｗ ｏ ｒ ｌ ｄ ：Ｓ ｙ ｓ ｔ ｅｍｓ  Ｔｈ ｉ ｎ ｋ ｉｎ ｇＡｐ ｐ ｌ ｉ ｅｄ  ｔ ｏ Ｓａ ｆ ｅｔ ｙ ．Ｃａ ｍｂ ｒｉｄ ｇｅ， Ｕ ＳＡ ： Ｍ Ｉ ＴＰ ｒ ｅｓ ｓ ，  ２ ０ １ １［ ２］ Ｃｏ ｌ ａｃｏ  ＪＬ ，Ｐ ａ ｇａｎ ｏ Ｂ ， Ｐａｓ ｔｅ ｕ ｒ  Ｃ ，ｅｔ ａ ｌ． Ｓｃａ ｄ ｅ ６ ：Ｆ ｒｏ ｍ ａＫａ ｈｎ  ｓ ｅｍ ａｎｔｉ ｃｓ ｔｏ ａ Ｋ ａｈｎ  ｉ ｍｐ ｌ ｅ ｍｅｎ ｔ ａ ｔｉ ｏ ｎ ｆｏ ｒ ｍ ｕ ｌ ｔｉ ｃｏ ｒ ｅ／ ／Ｐｒ ｏ ｃｅｅ ｄｉｎｇ ｓ ｏ ｆ ｔ ｈ ｅ Ｆｏ ｒｕ ｍ ｏ ｎ Ｓ ｐ ｅｃｉｆｉｃａ ｔｉｏ ｎＤｅ ｓｉ ｇ ｎ Ｌａｎ ｇ ｕ ａｇｅｓ（ Ｆ Ｄ Ｌ ） ． Ｍｕ ｎｉ ｃｈ ， Ｇｅ ｒｍａ ｎｙ ， ２ ０ １ ８ ： ５－１ ６［３ ］ Ｈａ ｌ ｂｗａ ｃｈｓ Ｎ，  Ｃａ ｓｐｉ Ｐ ？ Ｒａｙｍｏ ｎｄ Ｐ ， Ｐｉ ｌ ａ ｕ ｄ Ｄ． Ｔ ｈｅ ｓｙ ｎ ｃｈ ｒｏ ｎ ｏ ｕｓｄａ ｔ ａ－ｆｌ ｏｗ ｐ ｒｏ ｇｒａｍ ｍｉ ｎ ｇ ｌ ａ ｎｇｕ ａ ｇ ｅ Ｌ ｕ ｓｔ ｒｅ． Ｐｒ ｏ ｃｅ ｅｄ ｉ ｎｇ ｓ ｏ ｆ ｔ ｈ ｅＩＥＥＥ ， １ ９ ９ １ ， ７９ （ ９ ） ： １ ３ ０ ５－１ ３ ２ ０［ ４ ］ Ｂｏｕ ｓｓｉ ｎ ｏｔ Ｆ ？ ｄ ｅＳｉ ｍｏｎ ｅ Ｒ． Ｔ ｈｅ Ｅｓｔ ｅｒ ｅｌ  ｌ ａｎｇ ｕ ａｇ ｅ． Ｐ ｒｏ ｃｅｅｄｉ ｎｇ ｓ ｏｆｔ ｈｅ Ｉ ＥＥＥ ， １ ９ ９ １ ， ７ ９ （ ９ ） ； １ ２ ９ ３－１ ３ ０ ４［ ５ ］Ｂｅｎ ｖ ｅｎ ｉ ｓ ｔｅ Ａ ， Ｌｅ Ｇｕ ｅ ｒ ｎ ｉ ｃ Ｐ ， Ｊ ａｃ ｑ ｕ ｅｍｏ ｔ Ｃ．Ｓｙ ｎｃ ｈｒ ｏ ｎ ｏ ｕ ｓｐｒｏ ｇ ｒ ａ ｍｍｉ ｎｇｗｉｔ ｈ ｅｖ ｅｎ ｔｓ ａ ｎｄ ｒ ｅ ｌ ａｔ ｉ ｏ ｎ ｓ ： Ｔ ｈ ｅ ｓｉ ｇ ｎ ａ ｌ ｌ ａ ｎ ｇｕ ａ ｇ ｅａｎ ｄ ｉ ｔｓ ｓ ｅｍａ ｎｔｉｃｓ． Ｓｃｉｅ ｎ ｃｅ ｏ ｆ Ｃｏ ｍｐ ｕ ｔ ｅ ｒ Ｐ ｒ ｏ ｇ ｒ ａ ｍｍｉ ｎ ｇ ， １ ９９ １ ，１ ６ ： １ ０ ３ －１ ４ ９［ ６ ］ Ｓｃ ｈｎｅ ｉｄ ｅ ｒＫ．Ｔ ｈｅ ｓｙ ｎ ｃ ｈｒｏ ｎ ｏ ｕ ｓ ｐ ｒｏ ｇ ｒ ａｍｍ ｉ ｎｇｌ ａ ｎ ｇ ｕ ａｇ ｅＱＵＡＲ 丁Ｚ ．Ｄｅｐ ａ ｒｔ ｍｅ ｎ ｔ ｏ ｆ Ｃｏｍ ｐ ｕ ｔ ｅ ｒ Ｓｃｉ ｅ ｎ ｃｅ，Ｕｎ ｉ ｖ ｅｒｓｉ ｔ ｙ ｏ ｆＫａｉ ｓｅｒｓ ｌ ａ ｕ ｔｅ ｒｎ ， Ｇ ｅ ｒｍａ ｎ ｙ ：Ｉ ｎｔ ｅ ｒ ｎ ａ ｌ Ｒｅｐ ｏ ｒ ｔ ： ３ ７ ５ ， ２ ０ １ ０［ ７ ］Ｂｅｓ ｎａｒ ｄ Ｌ ， Ｇａ ｕ ｔｉ ｅｒ Ｔ ， ＬｅＧｕ ｅ ｒ ｎ ｉ ｃＰ ， ｅ ｔ ａｌ． Ｃｏｍｐ ｉ ｌ ａ ｔｉｏ ｎｏ ｆｐｏ ｌｙｃｈｒｏｎｏ ｕｓ ｄ ａｔ ａ ｆｌｏｗ ｅｑ ｕａｔｉ ｏ ｎｓ ／ ／ Ｐｒ ｏｃｅｅｄ ｉｎ ｇｓｏ ｆ ｔ ｈｅ Ｓｙ ｎｔｈ ｅｓｉ ｓｏ ｆ Ｅｍｂ ｅ ｄ ｄ ｅｄ  Ｓｏ ｆ ｔｗａ ｒ ｅ． Ｂｏ ｓｔ ｏ ｎ ， ＵＳＡ ？ ２ ０ １ ０： １－ ４０［ ８ ］Ｂｅ ｓｎａ ｒｄＬ ？ Ｇａ ｕ ｔｉ ｅ ｒ Ｔ ，Ｔ ａ ｌｐ ｉ ｎＪ Ｐ． Ｃｏ ｄ ｅ ｇｅ ｎ ｅｒ ａ ｔ ｉ ｏ ｎ ｓ ｔｒａ ｔｅ ｇ ｉｅ ｓｉ ｎｔ ｈｅＰ ｏ ｌ ｙｃ ｈｒｏ ｎｙ ｅｎ ｖ ｉ ｒ ｏ ｎｍｅ ｎ ｔ．Ｆ ｒ ａｎ ｃ ｅ ： Ｉ Ｎ ＲＩ Ａ ， Ｒ ｅｓｅ ａ ｒｃ ｈＲ ｅ ｐｏ ｒｔ： Ｒ Ｒ－ ６ ８ ９４ ，  ２ ０ ０ ９［ ９ ］Ｙａ ｎ ｇ Ｚｈ ｉ－ Ｂｉ ｎ ， Ｚ ｈａ ｏ Ｙ ｏ ｎ ｇ－Ｗａ ｎ ｇ ＊ Ｈ ｕ ａ ｎ ｇＺ ｈ ｉ－ Ｑｉ ｕ ｔｅｔａ ｌ．Ｔｉ ｍｅ － ｐ ｒ ｅ ｄｉ ｃ ｔａ ｂ ｌｅｍｕ ｌ ｔｉ－ ｔ ｈ ｒ ｅ ａｄ ｅ ｄｃｏ ｄ ｅｇ ｅ ｎ ｅ ｒ ａｔｉ ｏ ｎｗ ｉｔ ｈｓ ｙ ｎｃｈ ｒｏ ｎ ｏ ｕ ｓ ｌ ａｎｇ ｕ ａｇ ｅ ｓ ． Ｊｏ ｕ ｒ ｎ ａｌ  ｏ ｆＳｏ ｆ ｔ ｗａ ｒ ｅ ， ２ ０ １ ６ ， ２ ７ （ ３ ） ：６ １ １－６ ３ ２ （ ｉ ｎ Ｃｈ ｉ ｎ ｅ ｓ ｅ ）（ 杨志斌， 赵永望， 黄志球等． 同步语言的时间可预测多线程代码生成方法． 软件学报，２ ０ １ ６，２ ７ （ ３ ） ： ６ １ １－ ６ ３２ ）［ １ ０］ Ｙａ ｎ ｇ  Ｚｈ ｉ－ Ｂｉ ｎ ？Ｙ ｕａ ｎＳｈ ｅ ｎ ｇ－Ｈ ａｏ ， Ｘｉ ｅ Ｊ ｉ ａ ｎ ，ｅｔ ａＬ Ｍｕ ｌ ｔｉ？ｔ ｈ ｒ ｅａｄ ｅｄ ｃｏ ｄ ｅｇｅ ｎ ｅ ｒａ ｔｉ ｏ ｎｔ ｏ ｏ ｌ ｆ ｏ ｒｓ ｙ ｎ ｃｈｒ ｏｎ ｏ ｕｓ ｌａ ｎ ｇｕ ａｇｅ ．Ｊ ｏ ｕ ｒ ｎ ａｌ  ｏ ｆ Ｓ ｏ ｆｔ ｗ ａｒ ｅ ， ２ ０ １ ９ ， ３ ０ （ ７ ） ： １ ９ ８ ０－ ２ ０ ０ ２ （ ｉ ｎ Ｃｈ ｉ ｎｅｓ ｅ ）（ 杨志斌， 袁胜浩， 谢健等．一种同步语言多线程代码自动生成工具． 软件学报， ２ ０ １ ９ ， ３ ０ （ ７ ） ：１ ９ ８ ０ － ２ ０ ０ ２ ）［ １ １ ］Ｙ ａ ｎ ｇ Ｚ ， Ｂｏ ｄｅ ｖｅｉ ｘ Ｊ Ｐ ， Ｆ ｉｌ ａｌ ｉＭ ， ｅｔ ａ ｌ ． Ｔｏｗ ａ ｒ ｄ ｓａ ｖ ｅｒｉ ｆ ｉ ｅｄｃｏ ｍｐ ｉｌ ｅｒ ｐ ｒ ｏｔ ｏ ｔ ｙ ｐ ｅ ｆｏ ｒ  ｔ ｈｅ ｓｙ ｎ ｃｈｒ ｏ ｎ ｏ ｕ ｓ ｌ ａｎｇ ｕ ａｇｅ ＳＩ Ｇ Ｎ ＡＬ．Ｆｒ ｏ ｎ ｔｉ ｅｒ ｓ ｏ ｆ Ｃ ｏｍｐ ｕ ｔ ｅｒ  Ｓｃｉ ｅｎ ｃｅ ， ２ ０ １ ６， １ ０ （ １ ） ：  ３ ７ －５ ３［ １ ２ ］Ｙ ａｎ ｇ Ｚ ？Ｂｏ ｄ ｅ ｖ ｅｉ ｘ Ｊ  Ｐ ？ Ｆ ｉ ｌ ａ ｌ ｉ Ｍ． Ｔ ｏｗａ ｒｄ ｓ ａｓ ｉ ｍ ｐ ｌ ｅａ ｎ ｄ ｓ ａｆ ｅＯ ｂｊｅ ｃｔｉ ｖｅ Ｃａ ｍ！ ｃｏ ｍｐ ｉｌｉ ｎ ｇｆｒ ａ ｍｅ ｗｏ ｒｋ ｆｏ ｒｔ ｈ ｅ ｓ ｙ ｎ ｃｈ ｒ ｏ ｎ ｏ ｕ ｓｌ ａｎ ｇ ｕ ａｇ ｅＳ ＩＧ Ｎ ＡＬ． Ｆｒ ｏｎ ｔｉ ｅｒ ｓ ｏ ｆ Ｃｏｍｐ ｕ ｔｅ ｒ Ｓｃｉ ｅｎ ｃｅ ＊  ２ ０ １ ９，  １ ３ （ ４ ） ：７ １ ５ － ７３ ４［ １ ３ ］Ｊ ｉａ ｎ ｇＷ ｅｎ － Ｙ ｉ ， Ｐ ａ ｎ ｇＬ ｉ－ Ｐｉ ｎｇ ， Ｇ ａｏ  Ｌａｎ？ ｅｔ  ａｌ ．Ｓｅ ｒ ｉａｌ  ｐ ｒ ｏ ｇ ｒａ ｍｐ ａｒ ａｌ ｌ ｅｌ ｉ ｓｍ ａｌ ｇ ｏ ｒ ｉｔ ｈｍ ．Ｊ ｏ ｕ ｒｎａ ｌｏ ｆＨ ｕａ ｚ ｈ ｏ ｎｇＵｎ ｉｖ ｅｒ ｓｉ ｔ ｙｏ ｆＳｃｉ ｅ ｎ ｃｅ ａ ｎ ｄＴ ｅ ｃｈｎ ｏ ｌ ｏ ｇｙ（ Ｎａ ｔｕ ｒａｌ Ｓｃｉ ｅｎｃ ｅ Ｅｄｉｔｉ ｏ ｎ ） ，２ ０ ０ ０ ，２ ８ （ １ ２ ） ： ３ ０ － ３ ２ （ ｉ ｎＣ ｈｉ ｎ ｅｓ ｅ ）（ 江文毅， 庞丽萍， 高兰． 串行程序的并行划分算法研究． 华中科技大学学报（ 自然科学版），２ ０ ００，  ２ ８ （ １ ２ ） ： ３ ０－３ ２ ）［ １ ４ ］Ｓ ｔ ｅｗ ａ ｒ ｔＧ ， Ｂｅｒｉｎｇ ｅ ｒ Ｌ ， Ｃ ｕ ｅｌ ｌ ａ ｒＳ ， ｅ ｔａ ｌ ．Ｃｏｍｐ ｏ ｓｉｔｉｏ ｎ ａ ｌｃ ｏｍｐ ｃｅ ｒ ｔ ／ ／ Ｐｒ ｏ ｃ ｅｅ ｄｉｎ ｇｓ ｏ ｆ ｔ ｈｅ ４ ２ ｎ ｄ Ａ ｎ ｎ ｕ ａ ｌ ＡＣＭＳ ＩＧＰＬＡＮ －ＳＩ Ｇ ＡＣＴ Ｓｙｍｐ ｏ ｓｉ ｕｍ ｏ ｎ Ｐ ｒｉｎｃｉ ｐ ｌ ｅｓ  ｏ ｆＰ ｒｏｇｒａｍｍｉ ｎ ｇＬａ ｎｇｕ ａｇｅ ｓ（ Ｐ ＯＰＬ） ．Ｍｕ ｍｂ ａ ｉ， Ｉ ｎ ｄｉ ａ ， ２ ０ １ ５ ， ５ ０ （ １ ） ： ２ ７ ５－２ ８ ７［ １ ５］ Ｇａ ｍａ ｔｉ ｅ Ａ． Ｄ ｅｓｉ ｇ ｎｉ ｎ ｇ Ｅｍ ｂ ｅｄｄ ｅｄ  Ｓ ｙ ｓｔ ｅｍ ｓ ｗｉｔ ｈｔ ｈｅ Ｓ ＩＧＮ ＡＬＰ ｒｏｇｒａｍｍｉ ｎ ｇＬａ ｎｇｕａｇ ｅ ： Ｓｙｎｃ ｈｒｏ ｎ ｏ ｕ ｓ ＊Ｒｅ ａｃｔ ｉｖｅＳｐ ｅｃｉ ｆｉｃａ ｔｉ ｏ ｎ，Ｂｅ ｒ ｌ ｉ ｎ ， Ｇｅｒｍａ ｎｙ ：  Ｓｐ ｒ ｉ ｎ ｇｅ ｒ Ｓｃｉ ｅ ｎ ｃｅＢｕｓ ｉ ｎｅ ｓｓ Ｍｅｄ ｉ ａ ， ２ ０ ０ ９［ １ ６ ］Ｐ ｌ ｏ ｔ ｋｉ ｎ  Ｇ Ｄ．  Ａ ｓｔ ｒ ｕ ｃ ｔｕ ｒａ ｌ  ａｐ ｐ ｒｏ ａ ｃｈ  ｔ ｏ ｏ ｐ ｅ ｒａ ｔｉ ｏ ｎ ａ ｌ ｓｅ ｍａ ｎｔｉｃｓ ．Ｃｏ ｍ ｐ ｕ ｔｅ ｒ  Ｓｃｉ ｅ ｎｃｅ Ｄｅ ｐ ａ ｒｔ ｍｅｎｔ ， Ａ ａｒ ｈ ｕ ｓ Ｕｎ ｉ ｖ ｅ ｒｓ ｉ ｔ ｙ Ｄｅ ｎｍａ ｒｋ，Ａａ ｒｈ ｕ ｓ ， Ｄ ｅｎｍ ａｒ ｋ ， １ ９ ８ １［ １ ７］Ｌｅ ｒｏ ｙＸ ．Ｆ ｏ ｒ ｍａ ｌ ｖ ｅ ｒ ｉ ｆｉ ｃ ａ ｔｉ ｏ ｎ  ｏ ｆａ  ｒ ｅａ ｌ ｉ ｓ ｔｉ ｃ ｃｏｍ ｐｉ ｌ ｅｒ ． Ｃ ｏｍｍｕ ？ｎｉｃａ ｔｉｏ ｎ ｓ ｏｆ  ｔｈ ｅＡＣ Ｍ， ２ ０ ０ ９，  ５ ２ （ ７ ） ： １ ０ ７－１ １ ５［ １ ８ ］Ｂｏ ｕ ｒ ｋ ｅ Ｔ ． Ｂｒ ｕ ｎ Ｌ ， Ｄａ ｇ ａ ｎｄ Ｐ Ｅ ，  ｅｔ ａ ｌ ． Ａ ｆｏ ｒ ｍａ ｌ ｌ ｙ  ｖ ｅｒｉｆｉ ｅｄｃｏｍｐ ｉｌ ｅｒ  ｆｏ ｒ Ｌｕ ｓｔ ｒｅ ／／ Ｐ ｒ ｏｃ ｅｅ ｄｉ ｎｇｓ ｏ ｆ ｔｈｅ ３ ８ ｔ ｈＡＣＭＳＩ ＧＰＬＡＮＣｏ ｎ ｆ ｅｒ ｅｎ ｃｅ  ｏ ｎ Ｐｒ ｏｇ ｒａ ｍ ｍｉ ｎ ｇＬａ ｎｇｕａ ｇｅＤｅ ｓｉ ｇｎａ ｎｄ Ｉ ｍｐ ｌ ｅｍｅ ｎ－ｔ ａ ｔｉ ｏ ｎ （ Ｐ ＬＤ Ｉ ） ．Ｂａ ｒｃｅ ｌｏ ｎ ａ ， Ｓｐ ａ ｉ ｎ ，  ２ ０ １ ７ ， ５ ２ （ ６ ） ：  ５ ８ ６ －６ ０ １［ １ ９ ］Ｋ ａｎｇＹ ｕ ｅ－ Ｘｉ ｎ ？ Ｇ ａｎＹｕ ａ ｎ－ Ｋ ｅ ， Ｗ ａｎｇ Ｓｈ ｅｎｇ－Ｙｕ ａｎ． Ｃｏｍｐ ａｒｉ ｓｏｎｏ ｆ ｔ ｗ ｏ ｔ ｒ ｕ ｓ ｔｗ ｏ ｒ ｔ ｈ ｙ ｃｏｍ ｐ ｉｌ ｅ ｒｓＶｅ ｌ ｕ ｓ ａ ｎ ｄ Ｌ２ Ｃ ｆｏ ｒ  ｓ ｙ ｎｃｈ ｒｏｎｏ ｕｓｌ ａ ｎ ｇｕ ａ ｇｅｓ ．Ｊ ｏ ｕ ｒ ｎａｌ  ｏ ｆ Ｓｏ ｆｔ ｗａｒ ｅ ，  ２０ １ ９ ，３ ０ （ ７ ） ：  ２ ０ ０ ３ － ２０ １ ７ （ ｉ ｎＣｈ ｉ ｎ ｅｓｅ ）（ 康跃馨， 甘元科， 王生原． 同步数据流语言可信编译器ＶＭ ｕ ｓ与Ｌ２ Ｃ的比较． 软件学报， ２ ０ １ ９ ，  ３ ０ （ ７ ） ：２ ０ ０ ３－２ ０ １ ７ ）［ ２ ０ ］Ｐ ｎ ｕ ｅ ｌ ｉ Ａ ， Ｓ ｉ ｅｇ ｅ ｌ Ｍ ， Ｓ ｉｎ ｇｅｒｒａａ ｎ Ｅ． Ｔｒ ａｎ ｓｌ ａ ｔｉ ｏｎ  ｖａｌ ｉ ｄ ａ ｔｉ ｏ ｎ／ ／Ｐ ｒ ｏ ｃｅｅ ｄｉｎ ｇｓ ｏ ｆ ｔ ｈ ｅ Ｉ ｎ ｔ ｅ ｒ ｎａ ｔ ｉ ｏ ｎａ ｌ Ｃｏ ｎ ｆｅ ｒｅ ｎｃｅ ｏ ｎＴｏ ｏ ｌ ｓａ ｎｄＡｌ ｇ ｏ ｒｉｔ ｈｍ ｓｆｏ ｒ ｔ ｈ ｅＣｏ ｎ ｓ ｔｒ ｕ ｃ ｔｉｏ ｎａｎ ｄ Ａ ｎ ａｌ ｙｓ ｉ ｓ ｏ ｆ Ｓ ｙ ｓｔ ｅ ｍｓ．Ｂｅｒ ｌ ｉ ｎ＊Ｇ ｅ ｒｍａ ｎ ｙ ， １ ９ ９ ８ ： １ ５ １－１ ６６［ ２ １］Ｔ ｒａ ｎＨＮ ， Ｈ ｏ ｎｏ ｒａｔ  Ａ ，Ｔ ａｌ ｐ ｉ ｎ Ｊ Ｐ ＊ ｅｔ  ａｌ ．  Ｅｆｆ ｉｃｉ ｅｎ ｔ  ｃｏ ｎｔ ｅｎ ｔ ｉｏ ｎ－ａ ｗａ ｒ ｅ ｓ ｃｈ ｅｄ ｕ ｌｉ ｎｇ〇￡Ｓ ＤＦｇ ｒａ ｐｈ ｓｏ ｎ ｓｈａ ｒｅｄｍ ｕ ｌ ｔｉ－ｂ ａｎ ｋｍｅ ｍｏ ｒｙ ／ ／ Ｐｒ ｏ ｃｅ ｅｄ ｉ ｎ ｇ ｓ ｏ ｆｔ ｈ ｅ ２ ４ ｔ ｈ Ｉ ｎｔ ｅ ｒｎ ａｔ ｉ ｏ ｎａ ｌ Ｃｏ ｎｆ ｅｒ ｅｎｃｅｏ ｎ Ｅｎ ｇ ｉ ｎ ｅ ｅｒ ｉ ｎｇ  ｏ ｆ Ｃｏｍｐ ｌ ｅ ｘ Ｃｏｍ ｐ ｕｔ ｅｒ  Ｓｙ ｓ ｔ ｅ ｍｓ ．Ｈｏ ｎ ｇ  Ｋｏ ｎｇ ，Ｃｈ ｉ ｎａ，２ ０ １ ９： １ １ ４ －１ ２ ３［ ２ ２ ］Ｆｅ ｉ ｌ ｅｒ ＰＧ ｌ ｕｃ ｈ ＤＰ ， Ｈｕ ｄａ ｋ ＪＪ ． Ｔｈｅ ａｒｃｈｉ ｔ ｅｃｔ ｕｒｅ ａ ｎａ ｌｙ ｓｉｓ ＆－ｄｅｓ ｉ ｇ ｎ  ｌ ａｎ ｇｕ ａ ｇｅ （ ＡＡＤＬ） ：Ａｎ ｉｎｔ ｒｏ ｄ ｕｃ ｔｉｏ ｎ ． Ｃａｒｎ ｅｇｉ ｅ－Ｍｅ ｌ ｌｏ ｎＵｎ ｉ ｖ ｅ ｒｓｉｔ ｙ Ｐｉｔ ｔ ｓｂ ｕ ｒ ｇｈＰ ＡＳｏ ｆ ｔ ｗａｒ ｅＥｎｇ ｉ ｎｅ ｅ ｒｉ ｎ ｇＩ ｎｓ ｔｉ ｔ ｕ ｔ ｅ，ＵＳＡ ：Ｔ ｅｃ ｈｎ ｉ ｃａ ｌ Ｒｅｐ ｏ ｒ ｔ： ＣＭＵ ／Ｓ ＥＩ－ ２０ ０ ６－Ｔ Ｎ－０ １ １ ， ２ ０ ０ ６２ ２ ２ ６ 计算机学报 ２ ０ ２ ０ 年Ｙ ＵＡＮＳ ｈｅ ｎｇ－Ｈａ ｏ ．Ｍ． Ｓ． ｃ ａ ｎｄ ｉ ｄ ａｔ ｅ ．Ｈ ｉ ｓｒｅ ｓ ｅ ａ ｒ ｃ ｈｉ ｎ ｔ ｅ ｒｅ ｓ ｔ ｓ ｉ ｎ ｃ ｌ ｕ ｄｅ ｆｏ ｒｍａ ｌｍｅ ｔ ｈ ｏ ｄａ ｎｄ ｔ ｈ ｅ ｏｒ ｅｍ ｐ ｒｏ ｖ ｉ ｎｇ ．Ｙ Ａ Ｎ ＧＺｈ ｉ－ Ｂ ｉ ｎ．Ｐ ｈ． Ｄ．， ａ ｓ ｓｏ ｃ ｉ ａ ｔ ｅｐ ｒｏ ｆ ｅｓ ｓ ｏ ｒ．Ｈ ｉ ｓｒｅ ｓ ｅａ ｒ ｃ ｈ  ｉ ｎ ｔ ｅ ｒ ｅ ｓｔ ｓｉ ｎ ｃｌｕ ｄｅ  ｓａ ｆｅ ｔ ｙ－ ｃ ｒ ｉ ｔ ｉ ｃ ａｌ ｓ ｏ ｆｔ ｗａ ｒｅ  ａ ｎ ｄ ｆｏ ｒｍａｌｖ ｅ ｒｉ ｆ ｉ ｃ ａ ｔ ｉ ｏ ｎ ．ｉ ｎ ｃｌｕ ｄｅ  ｆｏ ｒｍａ ｌ ｖ ｅ ｒｉ ｆ ｉ ｃａ ｔ ｉ ｏｎ ａ ｎ ｄ ｓｏ ｆ ｔ ｗａ ｒｅ ｅ ｎｇ ｉ ｎ ｅ ｅ ｒｉ ｎｇ ．ＺＨ ＯＵＹ ｏｎｇ ， Ｐ ｈ． Ｄ． ， ａ ｓ ｓｏ ｃ ｉ ａ ｔ ｅ ｐ ｒｏｆ ｅｓ ｓ ｏｒ ．Ｈｉ ｓｒｅ ｓ ｅ ａ ｒｃ ｈｉ ｎ ｔ ｅ ｒｅ ｓ ｔ ｓ ｉ ｎ ｃｌ ｕ ｄｅ ｓ ｏｆ ｔｗａ ｒｅ ｅ ｎ ｇ ｉ ｎ ｅｅ ｒｉ ｎ ｇ ，ｆ ｏｒ ｍａｌ ｍｅ ｔ ｈｏ ｄｓ．ＸＵ ＥＬｅ ｉ ，Ｍ．Ｓ．， ｓ ｅ ｎｉ ｏ ｒ ｅ ｎｇ ｉ ｎｅ ｅ ｒ．Ｈ ｉ ｓ ｒｅ ｓ ｅａｒｃ ｈｉ ｎｔ ｅ ｒｅ ｓｔ ｓｉ ｎｃ ｌ ｕｄｅ ｅｍｂ ｅ ｄｄ ｅｄ ｓ ｏ ｆ ｔ ｗａ ｒ ｅｖｅ ｒｉ ｆｉ ｃａ ｔ ｉ ｏｎ ， ｅｍｂ ｅ ｄ ｄｅ ｄ ｓｏ ｆ ｔ ｗａ ｒ ｅｓｙ ｓ ｔ ｅｍｄｅ ｓ ｉ ｇｎ ．ＢＯ ＤＥ ＶＥＩ Ｘ Ｊ ｅ ａ ｎ －Ｐ ａ ｕ ｌ ，Ｐ ｈ． Ｄ． ， ｐｒ ｏｆ ｅ ｓ ｓｏ ｒ．Ｈ ｉ ｓ ｒ ｅ ｓ ｅａ ｒｃ ｈｉ ｎ ｔｅ ｒ ｅ ｓ ｔ ｓ ｉ ｎ ｃ ｌ ｕ ｄｅ ｒｅ ａ ｌ－ｔ ｉｍｅ ｓ ｙｓ ｔｅｍａ ｎｄ ｆｏ ｒ ｍａ ｌｍｅ ｔ ｈ ｏｄ ．ＦＩＬ ＡＬ Ｉ Ｍ ａ ｍｏ ｕ ｎ ． Ｐｈ ．Ｄ．  ，ｓ ｅ ｎ ｉ ｏ ｒ ｒｅ ｓ ｅａ ｒｃ ｈ ｆｅｌ ｌｏｗ．Ｈ ｉ ｓｒｅ ｓ ｅａ ｒ ｃ ｈ ｉ ｎ ｔ ｅ ｒｅ ｓ ｔ ｓｉ ｎ ｃ ｌ ｕ ｄｅｒ ｅａ ｌ－ｔ ｉ ｍｅｓ ｙｓ ｔ ｅ ｍａ ｎ ｄ ｆｏ ｒｍａ ｌ／ＨＡ Ｎ Ｇ Ｂｏ－ Ｌｉ ｎ ．Ｍ ． Ｓ．ｃ ａ ｎｄ ｉ ｄ ａ ｔ ｅ．Ｈ ｉ ｓ ｒ ｅｓ ｅ ａ ｒ ｃ ｈ ｉ ｎ ｔ ｅ ｒｅ ｓ ｔ ｓｍｅ ｔ ｈ ｏｄ ．Ｂ ａ ｃ ｋｇｒ ｏｕｎ ｄＣ ｏ ｍｐ ｉ ｌｅ ｒｖｅ ｒｉ ｆｉ ｃ ａ ｔ ｉ ｏｎｉ ｓ ａｆ ｕｎ ｄａｍｅ ｎ ｔ ａ ｌｐ ｒｏ ｂ ｌｅｍｏ ｆｃ ｏｍｐｕ ｔ ｅ ｒ ｓ ｃｉ ｅｎｃ ｅ ，ｅ ｓ ｐ ｅ ｃ ｉ ａ ｌ ｌ ｙ ｉ ｎ ｔ ｈ ｅ ｃ ｏｍｐ ｕ ｔ ｅ ｒｓ ｙ ｓ ｔｅｍ ．Ｉ ｔ ａ ｌ ｓｏｐ ｌ ａ ｙ ｓ ａ ｖｉ ｔ ａ ｌｒ ｏｌ ｅｉ ｎ ｔ ｈｅ ｄ ｅ ｓｉ ｇ ｎｏ ｆ ｓａ ｆｅ ｔ ｙ－ ｃ ｒｉ ｔ ｉ ｃ ａ ｌｓ ｏ ｆ ｔ ｗａ ｒｅ ｉ ｎｏ ｒｄｅ ｒ ｔ ｏｇ ｕ ａ ｒａ ｎ ｔ ｅ ｅｔ ｈ ｅ ｃｏ ｒｒ ｅ ｃ ｔ ｎｅ ｓ ｓ ｏｆ ａ ｌ ｌ ｋｉ ｎ ｄｓ ｏｆ  ｔ ｒａ ｎｓ ｆｏ ｒｍａｔ ｉ ｏ ｎｐ ｒｏ ｃ ｅ ｓｓ ｅ ｓ ， ｉ ｎ ｃｌ ｕｄ ｉ ｎ ｇ ｃｏ ｄｅ ｇ ｅ ｎ ｅ ｒａ ｔ ｉ ｏｎ ． Ｆｏｒ ｉ ｎｓ ｔ ａ ｎ ｃｅ ， Ｃ ｏｍｐ－Ｃ ｅ ｒ ｔｉ ｓ ｏｎ ｅ ｏ ｆ ｔ ｈ ｅ ｍｏ ｓ ｔ ｃ ｌ ａ ｓ ｓ ｉｃ ａ ｌｖ ｅ ｒ ｉ ｆ ｉ ｅ ｄ ｃ ｏｍ ｐｉ ｌｅ ｒ ｓ， ｗｈ ｉ ｃ ｈｃ ｏｍｅ ｓ ｗ ｉ ｔ ｈ ａ ｍａ ｔ ｈ ｅｍａ ｔ ｉ ｃ ａ ｌ， ｍ ａ ｃ ｈｉ ｎｅ － ｃ ｈ ｅ ｃｋ ｅ ｄｐ ｒｏ ｏｆ ｔ ｈ ａ ｔ ｔ ｈ ｅｇ ｅ ｎｅ ｒ ａ ｔ ｅ ｄｅ ｘ ｅ ｃ ｕｔ ａ ｂｌ ｅ ｃｏ ｄ ｅｂ ｅｈ ａ ｖ ｅ ｓｅ ｘａ ｃ ｔ ｌｙ ａ ｓ ｐ ｒｅ ｓ ｃ ｒ ｉ ｂ ｅ ｄｂｙｔ ｈ ｅ ｓ ｅｍａ ｎｔ ｉ ｃ ｓ ｏｆ ｔ ｈｅ ｓｏ ｕｒｃ ｅ ｐ ｒｏｇ ｒａｍ． Ｒｅ ｃ ｅｎ ｔｌ ｙ ， ｍａ ｎ ｙｒｅ ｓｅ ａ ｒｃ ｈｅ ｒｓｆ ｏｃ ｕ ｓｏ ｎ ｔ ｈ ｅ ｃｏ ｍｐ ｉ ｌ ａ ｔ ｉ ｏｎ  ｖ ｅ ｒｉ ｆ ｉ ｃ ａ ｔ ｉ ｏｎ ｏ ｆ ｓｙ ｎ ｃｈ ｒｏｎ ｏｕ ｓ ｌ ａ ｎｇ ｕ ａ ｇ ｅｓ，ｓ ｕ ｃｈ ａ ｓＶｅｌ ｕｓ ａ ｎｄ Ｌ２ Ｃ ．Ｈ ｏｗ ｅ ｖｅ ｒ， ｔ ｈｅ ｅ ｘｉｓ ｔ ｉ ｎ ｇｓ ｔ ｕｄ ｉ ｅ ｓｍａ ｉ ｎｌ ｙｃ ｏｎ ｃｅ ｒ ｎ ｔｈ ｅ ｓ ｅｍａ ｎｔ ｉ ｃ ｐｒｅ ｓ ｅ ｒｖａ ｔ ｉ ｏ ｎ ｏｆ  ｓ ｅｑｕｅ ｎ ｔ ｉａ ｌ ｃｏｄ ｅｇ ｅ ｎ ｅ ｒ ａ ｔ ｉ ｏｎｆ ｒｏ ｍｓ ｙｎ ｃ ｈ ｒｏ ｎｏ ｕ ｓｌａ ｎ ｇ ｕ ａ ｇ ｅ ｓ， ｔ ｈ ｅ ｙ ｐａ ｙａ ｌｉ ｔ ｔｌｅ  ａ ｔｔ ｅ ｎ ｔ ｉ ｏ ｎｔ ｏｔ ｈ ｅｓ ｅｍａ ｎ ｔ ｉ ｃ ｐ ｒｅ ｓ ｅ ｒｖ ａ ｔ ｉ ｏ ｎｏ ｆ ｍｕ ｌ ｔ ｉ－ｔ ｈ ｒｅ ａ ｄｅ ｄ ｃ ｏｄｅｇ ｅ ｎ ｅ ｒａ ｔ ｉｏ ｎ ．Ｉ ｎ ｔ ｈ ｉ ｓｐ ａ ｐ ｅ ｒ， ｗｅ ｐ ｒ ｅ ｓｅ ｎ ｔ ａ  ｖ ｅ ｒ ｉ ｆ ｉ ｅ ｄｍ ｕｌｔ ｉ－ｔ ｈ ｒｅ ａｄ ｅ ｄ ｃｏ ｄ ｅｇｅ ｎ ｅ ｒ ａ ｔ ｉ ｏｎ ｍｅ ｔｈ ｏｄｆ ｏ ｒｔ ｈｅ ｓ ｙｎｃ ｈ ｒｏ ｎ ｏｕ ｓｌ ａ ｎ ｇ ｕａ ｇ ｅＳＩ Ｇ Ｎ ＡＬ ．Ｔｈ ｅ ｍａ ｉ ｎ ａ ｄｖ ａ ｎｔ ａ ｇｅ ｏ ｆ  ｔｈ ｅｍｅ ｔ ｈ ｏｄｉｓ  ｔｏ ｓ ｕｐｐｏ ｒ ｔｍｕ ｌｔ ｉ－ｔ ｈ ｒｅ ａ ｄｅ ｄｃｏ ｄ ｅｇ ｅ ｎ ｅ ｒａ ｔ ｉｏ ｎ ，ｃｏ ｍｐ ａ ｒｅ ｄｗｉ ｔ ｈｔ ｈ ｅｅｘ ｉ ｓ ｔ ｉ ｎｇ ｒｅ ｌ ａ ｔ ｅ ｄｗｏ ｒ ｋｓ ．Ｆｉ ｒｓ ｔｌ ｙ ， ｔｈ ｅｍｅ ｔ ｈｏ ｄｄ ｅ ｆ ｉ ｎ ｅ ｓｔ ｈｅｓ ｔ ｒｕ ｃ ｔ ｕ ｒｅ ｄｏｐｅ ｒ ａ ｔ ｉｏｎ ａｌｓ ｅ ｍａ ｎｔ ｉ ｃ ｓｏ ｆｍｕ ｌ ｔ ｉｐ ｌ ｅ ｉ ｎ ｔ ｅ ｒｍ ｅｄ ｉ ａ ｔ ｅ  ｌ ａ ｎｇｕａ ｇ ｅｓ  ｉ ｎ ｃ ｏｄ ｅｇ ｅ ｎ ｅｒ ａ ？ｔ ｉ ｏ ｎ； ｓ ｅｃ ｏｎ ｄ ｌｙ ， ｉｔｆ ｏ ｒｍａ ｌｉ ｚｅ ｓ ｔ ｈｅ  ａ ｌｇｏ ｒ ｉ ｔ ｈｍｓａｎ ｄｍａ ｐｐ ｉ ｎ ｇｒ ｕ ｌ ｅ ｓ ｉｎｔ ｈｅ ｃ ｏｄ ｅｇ ｅ ｎ ｅ ｒａ ｔ ｉ ｏ ｎ ｐｒ ｏｃ ｅ ｓ ｓ ； ｔ ｈ ｉ ｒ ｄｌ ｙ ＊ｉ ｔｐ ｒｏ ｖｅ ｓ ｔ ｈｅｓ ｅｍ ａ ｎｔ ｉ ｃｃ ｏｎ ｓ ｉ ｓ ｔ ｅ ｎ ｃｙ ｂ ｅ ｔ ｗ ｅｅ ｎ ｔ ｈｅ ＳＩＧＮＡ Ｌｐ ｒ ｏｇ ｒ ａｍａ ｆ ｔ ｅ ｒｃ ｌ ｏｃ ｋ ｃ ａ ｌｃ ｕ ｌ ｕ ｓ ａ ｎｄｔ ｈ ｅｔ ａ ｒ ｇｅ ｔ Ｃｐｒ ｏ ｇ ｒａｍａ ｆ ｔ ｅ ｒｔ ｒａ ｎ ｓｌ ａ ｔ ｉ ｏ ｎｂａ ｓｅ ｄ ｏｎ ｔｈ ｅ ｂ ｉ ｓ ｉｍｕｌ ａ ｔ ｉ ｏ ｎ ｅｑｕ ｉ ｖａ ｌ ｅ ｎｔ  ｒｅ ｌａ ｔ ｉ ｏ ｎ．Ｔｈｅ ｒ ｅ ｓ ｅａ ｒｃ ｈｉ ｎ ｔ ｈ ｅ ｐ ａ ｐｅ ｒ ｉ ｓ ａ ｐａ ｒ ｔ ｏｆ ｔ ｈ ｅＮ ａ ｔ ｉｏｎ ａ ｌＮ ａｔ ｕ ｒ ａ ｌ Ｓｃｉ ｅ ｎｃ ｅ Ｆｏ ｕ ｎ ｄａ ｔ ｉ ｏ ｎｏ ｆ Ｃ ｈ ｉ ｎ ａ （ ６ １ ５ ０ ２ ２ ３ １ ） ， ｔ ｈ ｅ Ａｖ ｉ ａ ？ｔ ｉ ｏ ｎＳ ｃ ｉ ｅｎｃ ｅ Ｆ ｕ ｎ ｄ ｏｆ Ｃ ｈ ｉ ｎ ａ （ ２ ０ １ ９ １ ９ ０ ５ ２ ０ ０ ２ ） ，ｔ ｈｅ Ｎａ ｔ ｉ ｏｎ ａ ｌＤｅ ｆ ｅ ｎｓ ｅ Ｂａ ｓ ｉ ｃ Ｓ ｃ ｉ ｅ ｎｔ ｉ ｆ ｉ ｃＲ ｅ ｓｅ ａｒｃ ｈＰ ｒｏｊｅ ｃ ｔ ｕ ｎ ｄｅ ｒＧｒ ａ ｎｔ  ｏｆ Ｃ ｈ ｉ ｎａ（ Ｊ Ｃ Ｋ Ｙ２ ０ １ ６ ２ ０ ３ Ｂ０ １ １ ） ？ ｔ ｈ ｅ Ｆｕ ｎｄ ａ ｍｅ ｎ ｔａ ｌＲｅ ｓ ｅ ａ ｒｃ ｈ Ｆ ｕ ｎｄ ｓ ｆｏ ｒｔ ｈｅ Ｃ ｅ ｎ ｔ ｒ ａｌＵｎ ｉ ｖ ｅ ｒｓｉｔｉｅｓ （ Ｎ Ｐ２ ０ １ ７ ２ ０ ５ ） ，ｔ ｈｅ Ｆｏ ｕ ｎ ｄ ａ ｔ ｉ ｏｎ ｏｆＧ ｒａ ｄ ｕ ａ ｔ ｅ Ｉ ｎ ｎｏ ｖａ ｔ ｉｏ ｎ Ｃｅ ｎ ｔ ｅ ｒ ｉ ｎ ＮＵＡＡ （ ｋｆｊ ｊ２ ０ １ ８ １ ６ ０ ３ ）．