程序设计语言与系统前沿专题前言

冯新宇1, 2,  陈海波3
1(中国科学技术大学计算机科学与技术学院,合肥安徽230027)
2(中国科学技术大学苏州研究院,苏州江苏215123)
3(上海交通大学软件学院,上海200240)
通信作者: 冯新宇,E-mail: xyfeng@ustc.edu.cn

中文引用格式: 冯新宇,陈海波.程序设计语言与系统专题前言.软件学报,2017,28(4). http://www.jos.org.cn/1000-9825/ 5198.htm

程序设计语言和系统是计算机领域的奠基性学科之一.近年来随着计算机系统的广泛应用,本领域的研究形成一波新的高潮,其中新的研究热点包括面向大数据、云计算、移动计算、软件定义网络、机器人等特定领域的领域专用程序设计语言和系统、基于程序设计语言的安全理论和技术、多核和众核下的并行程序设计语言和系统、程序分析和验证等.

为及时反映我国在程序设计语言和系统方面的研究进展,“程序设计语言和系统”专题围绕上述新兴热点问题,同时也兼顾经典问题的最新突破,征集本领域近期取得的原创性研究成果,以期促进本领域的发展.专题的征文范围包括（但并不限于）面向特定领域（大数据、云计算、移动计算、软件定义网络、机器人等）的领域专用语言和系统,基于程序设计语言的安全理论和技术,多核和众核下的并发和并行程序设计语言和系统,程序测试、分析和验证技术,编译器、解释器和抽象机,程序开发工具和环境,函数式、逻辑式、概率、量子等程序设计语言,以及程序语义、程序逻辑、类型论等程序设计语言理论.

专题公开征文,共征得投稿18篇.特约编辑先后邀请了国内外在该领域的一些重要学者参与审稿工作,每篇投稿至少邀请2位专家进行初审.大部分稿件经过初审和复审两轮评审,部分稿件经过了两轮复审.通过初审的稿件还在NASAC 2016大会上进行了现场报告,作者现场回答了听众的问题,并听取了听众的修改建议.最终有9篇论文入选本专题.入选论文覆盖并发和并行编程、程序分析和验证、软件安全等领域.

随着多核、众核系统的日益广泛应用,可靠易用的并发/并行编程模型、并发/并行程序的正确性分析和验证等问题成为程序设计语言领域的热点问题.蒋炎岩等人的《获取访存依赖：并发程序动态分析基础技术综述》对并发程序动态分析技术中的访存依赖获取技术进行综述,提出了包含四个评价指标（即时性、准确性、高效性、简化性）、两种方法（在线追踪、离线合成）和两类应用（轨迹分析、并发控制）的综述框架,对已有技术进行了系统总结,并对未来可能的研究方向予以展望.何王全等人的《面向国产异构众核系统的Parallel C语言设计与实现》提出统一架构的多模式并行编程模型,包括异构融合的加速运算模型和按同构方式编程的自主运算模型,根据编程模型设计了Parallel C语言,并基于Open64构建了编译系统.Parallel C能有效描述国产众核系统的异构并行性,在Micro Benchmark和实际应用在神威太湖之光计算机系统上的测试数据表明,语言设计和编译实现能够有效支撑大型应用.

程序验证是保证程序正确性和安全性的重要理论和技术之一,也是一直是程序设计语言领域的重要研究方向.本专题收录了3篇程序验证方向的研究成果.李彬等人的《通过抽象程序证明复杂具体程序》给出了一种通过证明抽象程序和具体程序一致性来保证具体程序正确性的验证方法.抽象程序使用抽象数据结构和抽象操作,程序简单,其正确性往往显而易见,可以作为程序的规范.用户通过给出抽象变量和具体变量的关系以及抽象程序程序点和具体程序程序点的对应关系,可以建立具体程序与抽象程序的一致性证明.杨启哲等人的《基于通讯Petri网的异步通讯程序验证模型》采用通讯Petri网对异步通讯程序进行建模和验证.通过对输入通讯进行k-型限制,以及对每个栈进行基于正则语言泵引理的抽象,可以将这样限制下的模型编码到数据Petri网,从而证明该限制下的新模型的可覆盖性是可判定的.张恒若等人的《基于Z3的Coq自动证明策略的设计和实现》指出基于交互式定理证明的程序验证支持表达力强的逻辑断言,但自动化程度低；而基于约束求解器的验证自动化程度高,但验证能力有限,难以验证复杂系统的全部的功能正确性.文章提出将两者结合,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻了用户手动验证程序的开销.

程序分析技术,包括静态分析和动态分析,是自动化发现程序的可靠性和性能问题的轻量级方法.李筱等人的《C/C++程序静态内存泄漏警报自动确认方法》针对静态分析中的误报问题,提出了一种基于混合执行测试的静态内存泄漏警报的自动化确认方法.该方法针对静态分析提出的警报,对目标程序进行控制流分析,形成制导信息；然后基于制导信息对目标程序进行混合执行测试,监控追踪内存对象的状态,判定内存泄漏是否发生,对静态警报进行动态确认并分类.该方法可以对静态内存泄漏警报进行有效的分类,能够降低人工确认的工作量.李登辉等人的《数据中心中DVFS对程序性能影响模型的设计》针对数据中心中广泛使用的DVFS技术,考察其对程序性能的影响.文章根据运行时指令的完成是否需要访问主存将指令分为片上完成指令和片外完成指令两部分,并分别构建了其执行时间同处理器频率的理论模型,从而可以获得程序的执行时间同频率的关系,通过实验验证平均误差不超过1.34%.该工作对于数据中心在节能和满足服务质量方面的平衡有很好的参考基础和理论价值.

软件安全是人们日益重视的问题,程序设计语言和系统相关的理论和技术在发现软件漏洞、确保系统安全方面有着重要应用.王蕾等人的《污点分析技术的原理和实践应用》对近年来面向解决应用程序安全问题的污点分析技术进行综述,系统性的梳理了污点分析技术的基本原理和核心技术思路,介绍了相关一些经典工作的思路和问题,探讨了包括隐式流分析和显式流分析,动态分析与静态分析等相关技术思路,并且以当下流行的Web平台和移动平台为例,结合隐私泄露、漏洞分析等领域的污点分析技术的实践,介绍了相关领域的实践思路,对于程序语言分析、程序安全性研究等相关领域的研究具有较大的意义.仝青等人的《拟态防御web服务器设计与实现》针对web服务器面临的攻击问题,对现有的入侵隔离、入侵检测、入侵容忍和移动目标四种方法进行分析,指出了其中的不足,并进而提出基于“动态异构冗余”结构的拟态防御模型,通过部署多个异构同功能的模块,使用表决器对同一输入的多个输出进行判断,从而防御对某个模块特定缺陷的攻击.文章基于实际系统实现了拟态防御web服务器的原型系统,并进行了性能和安全性的评测.

本专题主要面向程序设计语言领域的研究人员,反映了我国学者在该领域的最新研究进展.在此,我们要特别感谢《软件学报》编委会对专题工作的指导和帮助,感谢编辑部各位老师从征稿启示发布、审稿专家邀请至评审意见汇总、论文定稿、修改及出版所付出的辛勤工作和汗水,感谢专题国内外评审专家及时、耐心、细致的评审工作.此外,我们还要感谢向本专题踊跃投稿的作者对《软件学报》的信任.最后,感谢专题的读者们,希望本专题能够对相关领域的研究工作有所促进.

冯新宇(1978－),男,中国科学技术大学计算机科学与技术学院和苏州研究院教授、博士生导师.CCF会员、CCF系统软件专委会委员.主要研究领域为程序验证、可信软件、程序设计语言理论等.
陈海波(1982－),男,博士,上海交通大学软件学院教授、博士生导师,CCF杰出会员、杰出演讲者,CCF青年科学奖获得者.主要研究领域为系统软件与系统结构.