“编译原理”课程实验项目介绍

在"编译原理"课程的教学中,实验项目是十分关键的部分。Decaf/Mind项目是近几年清华大学计算机系本科生"编译原理"课程的主体实验项目,在该项目中,学生在实验框架基础上,针对一个简单面向对象语言的实现开展4～5个阶段的编程实验,对理解和巩固理论知识以及提高软件系统的开发能力有较大帮助。本文就Decaf/Mind项目的背景、内容以及实施情况进行简要介绍。

并发面向对象中的继承反常现象

如果不考虑继承性,并发性与对象技术的结合是很自然的.继承反常(又称继承异常)现象是继承性和并发性不相容的主要原因之一.现阶段人们对继承反常现象的认识有许多模糊之处,出发点不尽相同,形式化的工作也很少.对不同的subtyping关系考虑其特有的渐增式继承方法有利于把握继承反常现象的实质,也丰富了在并发面向对象语言中应将inheritance层次和subtyping层次区别对待这一认识的内涵.在阐述基本观点之后,采用范畴论的术语对相关的概念和定义做了形式化工作.一些观点和结论适用于区分和解释相关工作的出发点和贡献,并对并发面向对象技术中继承性的建模问题有所启示.

并发进程指称语义的几种基于Trace模型的定义方法

Ｔｒａｃｅ模型是定义并发进程指称语义的基本方法之一．在Ｔｒａｃｅ模型的基础上，为获得更广泛的表达能力，通过进程指称论域的各种变化，派生出了一系列的语义模型．并对于这些模型进行了综述．

并发事务的一种操作模型

本文定义了一种描述分布式数据库系统并发事务行为的操作模型．以此为基础讨论了并发事务的调度，共享模式的Ｌｏｃｋｉｎｇ机制，死锁等问题．

面向系统能力培养的计算机专业课程体系建设实践

系统能力培养是提高计算机专业本科教学质量和水平的一个重要方向。本文提出了系统能力培养的基本概念和内涵,介绍了清华大学计算机科学与技术系在计算机系统能力培养方面所做的工作和实践效果,讨论了课程体系建设和改革的关键内容,给出了一种加强计算机系统能力培养的教学方案。

同步数据流语言可信编译器的构造

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.

OpenMP任务调度开销及负载均衡分析

任务调度是OpenMP规范的重要内容。在考虑调度开销、负载均衡等多方面因素的基础上,OpenMP规范制定了静态调度、动态调度、指数动态调度和运行时调度等不同策略。详细分析了在单次循环时间相等情况下,不同的OpenMP调度策略对额外开销和负载均衡的影响;提出了选择不同任务调度策略的原则。

同步数据流语言高阶运算消去的可信翻译

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.

可信编译器L2C的核心翻译步骤及其设计与实现

同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.

动态编译技术研究

本文从动态编译的概念出发,着重讨论了运行时特定化技术和Just-in-time编译技术;比较全面地总结并评述了具有代表性的动态编译系统及其采用的Profiling技术、重编译技术;并探讨了动态编译技术研究中存在的一些问题及进一步的工作。

同步数据流语言时态消去的可信翻译

为解决实现同步数据流语言Lustre到串行命令式语言C语言可信编译器过程中碰到的时态运算翻译的困难,提出了将所有的时态运算翻译单独分层定义和证明的方法。在同步数据流语言的时态特性和C语言的循环特性分析的基础上,结合可信编译器实现框架上下层的语言结构,使用Coq证明工具,形式化的定义了两种中间语言的语法和语义,经过分析时态翻译过程特点,归纳定义了时态变量传递性质,实现了翻译工作严格的形式化验证,最终完成了时态消去翻译的等价性证明。

一个C语言安全子集的可信编译器

以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估。之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器。最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率。

基于指令聚类与指令调度的嵌入式软件功耗优化研究

选用指令级能耗评估模型,提出和验证了一种基于指令聚类与指令调度的功耗优化方案.该方案采用深度优先算法搜索局部最优解,挑选出能耗较小的一种指令序列.又兼顾测试工作量与精确度,将能耗相似的指令归入同类,有效降低了获取相邻指令切换能耗参数的工作量过大这一问题.通过分析基于SimpleScalar/Wattch模拟器的实验结果,指出仅用指令调度技术进行指令级功耗优化,其效果有限,为了提高优化效率,必须进行更高级别的功耗评估与优化.

可信编译器构造的翻译确认方法简述

编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失。消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信。近年来,形式化验证方法被成功用于可信编译器的构造中。一种方法是对编译器本身进行形式化验证,经过严密的证明,可杜绝误编译的发生。然而,这种方法可能"冻结"编译器的设计,阻碍编译器未来可能的优化和完善。翻译确认是另外一种用于可信编译器构造的形式化方法,它避免了对编译器自身的验证,有很好的可重用性,近年来在编译器验证领域得到了广泛研究,已取得令人瞩目的成果。介绍了翻译确认方法的概念及研究进展。

字节码虚拟机的构造和验证

提出一种虚拟机构造和验证方案.给出字节码程序运行环境BVM(bytecode virtual machine)的形式化定义;采用X86机器语言构造虚拟机CertVM(certified virtual machine);并证明该虚拟机实现符合相应程序规范并和BVM之间具有模拟关系.利用辅助工具Coq给出证明,所有证明均可机器自动检查.CertVM确保在硬件环境满足其语义规范的情况下,已验证的字节码程序能够在给定虚拟机环境中正常运行.给出的方案不仅为虚拟机验证提供理论基础,而且为可信软件构造提供了一种有益的尝试.

一种用于字节码程序模块化验证的逻辑系统

字节码既是运行于虚拟机的解释指令,也是定义良好的中间表示,是当今网络软件和计算设备中广泛使用的重要技术.字节码验证可以提高相关软件的可信程度,同时为构造证明保持编译器提供中间表示支持,具有重要的实用价值和理论价值.虽然近年提出了一些用于字节码程序的逻辑系统,但由于字节码本身的特点,造成了抽象控制栈复杂、控制流结构信息不足,因而字节码程序的"模块化验证"依然是一个巨大的挑战,并没有得到有效解决.将FPCC(foundationalproof-carryingcode)方法引入中间表示字节码,借鉴汇编程序的验证方法.设计出一种逻辑系统,给出字节码程序运行环境BCM(ByteCodemachine)的逻辑系统CBP(certifyingbytecodeprogram)定义,完成系统的合理性证明和一组代表性实例程序的模块化证明,并实现机器自动检查.该工作为字节码验证提供一种良好的解决方案,同时也向着构造证明保持编译器环境迈出了坚实的一步,还可以为广泛使用的基于虚拟机复杂网络应用程序的深刻理解和深入分析提供理论帮助.

在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程

Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器的形式化验证,实现了开源L2C编译器前端语法分析器的两个选项之一。首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结。

转动机械故障诊断专家系统ROFD的实现

ROFD是我们为兰州炼油化工总厂开发的一个用于大型转机故障诊断的专家系统。本文介绍了ROFD的系统结构、知识表示及推理机制,并对其特点作了简要评论。

BSP用于分布式系统的协议规范

ＢＳＰ（ＢｒｏａｄｃａｓｔｉｎｇＳｅｑｕｅｎｔｉａｌＰｒｏｃｅｓｓｅｓ）是一种带有广播原语的分布式语言，能很好地支持分布式系统中的消息传递。本文强调了ＢＳＰ在分布式系统协议规范方面的应用，并完成了对ＯＳＩ参考模型的网络协议以及数据库并发控制的ｔｉｍｅｓｔａｍｐ协议的规范说明。

“编译原理专题训练”课程介绍

"编译原理专题训练"是清华大学为计算机科学与技术系本科生开设的实践类限选课,旨在提高学生的实践能力。课程首次将开放源代码软件GCC和Open64作为实验框架引入实践教学,引导学生参与大型开源软件开发和维护活动,基于具有工业水准的真实软件开展实践。本文重点介绍了该课程在我校开设的基本情况,以期给大家更多的启示。