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

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

基于新型掺钪氮化铝的级联马赫-曾德尔结构(解)复用器

在新型掺钪(Sc)氮化铝(Al1-xScxN)集成光学平台上设计了插入损耗低、传输通道谱线平坦的O波段四通道波分(解)复用器,并提出了优化方法。所设计的器件结构基于级联马赫-曾德尔干涉仪(MZI)滤波器,结合弯曲波导结构的定向耦合器改善波长敏感度。针对粗波分复用(CWDM)应用的特性,文章使用粒子群算法(PSO)提升器件性能优化的效率,通过调整器件结构的设计参数对四路通道的传输谱线质量进行优化。针对0%,9%,23%的掺Sc浓度,设计的解复用器表现出宽达约15.6nm的1-dB带宽和小于0.1dB的插入损耗,传输谱线呈“盒状”响应,各通道间串扰均优于-30.6dB。     

高均匀性1×4多模干涉耦合器的研究与设计

针对多输出端口输出光功率的不均匀性问题,文章设计了一种基于绝缘体上硅(SOI)的1×4多模干涉(MMI)耦合器,提出了一种优化其均匀性的新方法。耦合器输入/输出端采用锥形波导,为提升MMI耦合器的均匀性,对输出端锥形波导采用不等宽设计,通过优化,四路输出端口均匀性高达0.007 4 dB,而总的插损仅有0.058 dB。依据该方法最终使得输出端波导的传输常数失配,避免了波导之间的串扰,实现了对MMI耦合器输出端口均匀性的提升。     

蓝光LD抽运Pr~(3+):YLF直接获得橙红光的实验研究

对蓝光二极管(LD)泵浦Pr:YLF晶体输出橙红光进行了实验研究,分析了不同偏振方向的晶体和不同透过率的输出镜对橙红光输出功率的影响。在a切Pr~(3+):YLF晶体吸收功率为4.5W时最高输出639.7nm激光功率为491m W。c切Pr~(3+):YLF晶体在吸收功率为3.3W时最高输出607.3nm激光功率为177m W。     

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

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

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

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

固体热容激光器热管理系统中线性阀体的设计

提出了一种新型的、可用于固体热容激光器热管理系统中的线性可控流量阀体的设计方案.通过建立数学模型和用Matlab软件仿真,得出了设计方案.并根据具体的实例,通过理论计算设计出线性工作区间占总的工作区间的80.82%,最大过流面积占外筒圆孔的总面积90.95%的线性可控流量阀体,证明了方案的可行性.     

Cr4+:YAG被动调Q小型无水冷激光器

从被动调Q速率方程出发,分析了被动调Q条件下激光输出能量、脉冲宽度、饱和吸收体初始透过率、输出镜反射率与参数Z的关系.在此基础上,采用尺寸为φ4×48 mm、掺杂浓度为l atm%Nd:YAG激光晶体作激光工作物质,初始透过率为30%的Cr4+:YAG作为被动调Q晶体,透过率为50%的平面镜作为输出镜.以脉冲氙灯为泵浦光源,在注入电压为650 V条件下,激光器单脉冲能量输出为35 mJ,脉冲宽度为6.8 ns,能量不稳定度＜5%.     

基于Linux的通用加密文件系统Waycryptic的设计与实现

近年来,保护个人敏感数据成为人们关注的热点问题.使用加密技术是一种比较成功的保护方法.本文提出一种通用的加密文件系统—Waycryptic,将加密技术集成到文件系统层,应用程序完全不用任何修改就可以获得透明、动态、高效和安全的加密功能,加密文件可以不受限制地存放于任何物理文件系统,同时允许加密文件方便地在多个用户间共享以及指定账号恢复加密文件.Iozone和Bonnie测试程序的结果显示Waycryptic的性能令人满意,适合于具有安全要求的个人或多用户系统.     

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

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