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

摘要:并发错误难触发、难调试、难检测.为应对这一挑战，已有动态程序分析技术通过观测或控制并发程序执行实现其质量保障.由于并发程序不确定性主要来自共享内存，实现其动态分析的基本问题即是获取线程访问共享内存的顺序，即获取访存依赖.提出访存依赖获取技术的综述框架，包含4个评价指标（即时性、准确性、高效性、简化性）、两种方法（在线追踪、离线合成）、两类应用（轨迹分析、并发控制）.通过对已有技术的总结和分析框架中的空白，对未来可能的研究方向予以展望.

摘要:异构众核架构具有超高的性能功耗比，已成为超级计算机体系结构的重要发展方向.但众核系统更为复杂的并行层次和存储层次，给编程和优化带来了极大的挑战.因此，研究面向众核系统的并行编程技术，对于降低国产众核系统并行应用的编程难度、提升并行程序的性能都具有重要的意义.提出统一架构的多模式并行编程模型，包括异构融合的加速运算模型和按同构方式编程的自主运算模型，根据编程模型设计了Parallel C语言，能够有效地描述国产众核系统的异构并行性.与其他众核系统上MPI+X的使用模式相比，编程和系统优化都具有全局视角，在多级局部性描述、单边消息、兼容已有多核应用等方面具有特色；基于Open64构建了Parallel C编译系统，全面支持加速运算模型和自主运算模型，提出并实现了数据布局与自动DMA、编译指导的线程代理和拓扑位置感知的集合通信等优化.Micro Benchmark和实际应用在神威太湖之光计算机系统上的测试数据结果表明：Parallel C语言和编译系统具有良好的性能和可扩展性，能够有效支撑大型应用.

摘要:描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构（ADTs），如set，list，map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系、抽象程序程序点和具体程序程序点的对应关系.基于对应关系，抽象程序和具体程序一致性证明可以分解，从而容易并可能自动证明.

摘要:由于多栈的模型图灵等价，因此，通用的异步通信程序模型的验证问题不可判定.为此，基于Petri网，提出了一个新的模型通信——通信Petri网，对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象，通过将这样限制下的模型编码到数据Petri网，证明了限制下的新模型可覆盖性可判定.

摘要:形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性，这种验证方式表达力强，可以证明复杂系统，但是自动化程度低、验证代价比较高；而使用程序验证器接受经过规范标注的源代码生成验证条件，并将验证条件交给约束求解器自动求解，这种方式自动化程度高，缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点，在定理证明工具Coq中实现了一个自动证明策略smt4coq，它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题，提高了自动化验证的程度，减少了用户手动验证程序的开销.

摘要:内存泄漏是C/C++程序的一种常见的、难以发现的缺陷，一直困扰着软件开发者，尤其是针对长时间运行的程序或者系统软件，内存泄漏的后果十分严重.针对内存泄漏的检测，目前主要有静态分析和动态测试两种方法.动态测试实际运行程序具有较大开销，同时依赖测试用例的质量；静态分析技术及自动化工具已被学术界和工业界广泛运用于内存泄漏缺陷检测中，然而由于静态分析采取了保守的策略，其结果往往包含数量巨大的误报，需要通过进一步的人工确认来甄别误报.但人工确认静态分析的结果耗时且容易出错，严重限制了静态分析技术的实用性.提出一种基于混合执行测试的静态内存泄漏警报的自动化确认方法：首先，针对静态分析报告的目标程序中内存泄漏的静态警报，对目标程序进行控制流分析，并计算警报的可达性，形成制导信息；其次，基于警报制导信息对目标程序进行混合执行测试；最后，在混合执行测试过程中，监控追踪内存对象的状态，判定内存泄漏是否发生，对静态警报进行动态确认并分类.实验结果表明：该方法可对静态内存泄漏警报进行有效的分类，显著降低了人工确认的工作量.

摘要:数据中心以可接受的成本，承载着超大规模的互联网应用.数据中心的能源消耗直接影响着数据中心的一次性建造成本和长期维护成本，是数据中心总体持有成本的重要组成部分.现代的数据中心普遍采用动态电压频率调节（dynamic voltage frequency scaling，简称DVFS）来提升单节点的能耗表现.但是，DVFS这一类机制同时影响到应用的能源消耗和性能，而这一问题尚未被深入探索.专注于DVFS机制对应用程序性能的影响，提出了一个分析模型用来量化地刻画应用程序的性能与处理器频率之间的关系，可以预测程序在任意频率下的性能.具体来说，依据执行时访问内存子系统资源的不同，把程序的指令分为两部分——片上指令和片外指令，并分别独立建模.片上指令是指仅需访问片上资源就可以完成执行的指令，其执行时间与处理器频率呈线性关系；片外指令是指需要访问主存的指令，其执行时间与处理器频率无关.通过上述划分和对每一部分执行时间的分别建模，可以获得应用程序的执行时间与处理器频率之间的量化模型.使用两个不同的平台和SPEC 2006中的所有标准程序验证该模型，平均误差不超过1.34%.

摘要:信息流分析可以有效保证计算机系统中信息的保密性和完整性，污点分析作为其实践，被广泛用于软件系统的安全保障技术领域.对近些年来面向解决应用程序安全问题的污点分析技术进行综述：首先，总结了污点分析的基本原理以及在应用中的通用技术，即，使用动态和静态的方法解决污点传播；随后，分析该技术在移动终端、互联网平台上的应用过程中遇到的问题和解决方案，包括解决Android应用隐私泄露与检测Web系统安全漏洞的污点分析技术；最后，展望该技术的研究前景和发展趋势.

摘要:Web服务器系统作为重要的服务承载和提供平台，面临的安全问题日益严重.已有的防御技术主要基于已知攻击方法或漏洞信息进行防御，导致难以很好地应对未知攻击的威胁，从而难以全面防护Web服务器系统的安全.首先提出了攻击链模型，对已有技术的问题和不足进行了深入的分析.在此基础上，提出了基于“动态异构冗余”结构的拟态防御模型，并描述了拟态防御模型的防御原理和特点.基于拟态防御模型构建了拟态防御Web服务器，介绍了其架构，分析了拟态原理在Web服务器上的实现.安全性和性能测试结果显示，拟态防御Web服务器能够在较小开销的前提下防御测试中的全部攻击类型.说明拟态防御Web服务器能够有效地提升系统安全性，验证了拟态防御技术的有效性和可行性.最后讨论了拟态防御技术今后的研究前景和挑战.

摘要:线性μ演算（linear time μ-calculus，简称νTL）语法简单，表达能力强，可用于验证并发程序的多种性质.然而，不动点操作符的嵌套使其判定问题难以有效解决.针对这一问题，开发了工具NuTL2PFG，用以判定νTL公式的可满足性.利用νTL公式的当前-未来范式（present future form，简称PF式），该工具能够为一个给定公式构造其当前-未来范式图（present future form graph，简称PFG），用以描述满足该公式的模型.通过在所得PFG中寻找一条ν-路径，即，不涉及最小不动点公式的无穷展开的路径，该工具便可判断出给定公式的可满足性.实验结果表明，NuTL2PFG的执行效率优于已有工具.

摘要:模型转换是模型驱动开发的核心技术.当要把模型转换用于工业生产时，其性能成为影响这一技术成败的关键因素之一.为了测试模型转换程序的性能，需要能够快速地生成一组具有较大规模的模型数据用于作为测试的输入数据.提出一种随机化的模型生成方法，该方法能够根据元模型的定义以及用户输入的约束条件随机且正确地生成模型文件.实验结果表明：该方法与其他方法相比，具有更好的生成效率，从而更适合支持模型转换的性能测试.

摘要:SIMD扩展部件是集成到通用处理器中的加速部件，旨在发掘多媒体和科学计算等领域程序的数据级并行.当前，两种基本的向量发掘方法分别是发掘迭代间并行的Loop-based方法和发掘迭代内并行的SLP方法.Loop-aware方法是对SLP方法的改进，其思想是：首先，通过循环展开将迭代间并行转换为迭代内并行，使循环体内的同构语句条数足够多；再利用SLP方法进行向量发掘.但当循环展开不合法或者并行度低于向量化因子时，Loop-aware方法无法实现程序向量并行性的发掘.因此提出了向量并行度指导的循环向量化方法，依据迭代间并行度、迭代内并行度和向量化因子构建循环向量化方法选择方案，同时提出了不充分向量化方法发掘并行度低于向量化因子的循环向量并行性，最后，依据向量并行度对生成的向量循环进行展开.经过标准测试集测试，向量并行度指导的循环SIMD向量化方法比Loop-aware方法的识别率提升了107.5%，性能提升了12.1%.

摘要:针对传统容错方法在融合网络环境下服务组合的低效性，提出了一种快速可靠的服务组合容错方法.该方法首先采用模糊逻辑对服务的临时性故障进行服务重试；然后采用多属性决策理论对服务的永久性故障进行服务复制；最后，通过改进的粒子群算法对永久性故障进行服务补偿.基于真实数据集的实验结果表明，所提方法在故障排除率、故障处理时间与组合最优度方面均优于其他方法.

摘要:大数据时代下，移动互联网发展与移动终端的普及形成了海量移动对象轨迹数据.轨迹数据含有丰富的时空特征信息，通过轨迹数据处理技术，可以挖掘人类活动规律与行为特征、城市车辆移动特征、大气环境变化规律等信息.海量的轨迹数据也潜在性地暴露出移动对象行为特征、兴趣爱好和社会习惯等隐私信息，攻击者可以根据轨迹数据挖掘出移动对象的活动场景、位置等属性信息.另外，量子计算因其强大的存储和计算能力成为大数据挖掘重要的理论研究方向，用量子计算技术处理轨迹大数据，可以使一些复杂的问题得到解决并实现更高的效率.对轨迹大数据中数据处理关键技术进行了综述.首先，介绍轨迹数据概念和特征，并且总结了轨迹数据预处理方法，包括噪声滤波、轨迹压缩等；其次，归纳轨迹索引与查询技术以及轨迹数据挖掘已有的研究成果，包括模式挖掘、轨迹分类等；总结了轨迹数据隐私保护技术基本原理和特点，介绍了轨迹大数据支撑技术，如处理框架、数据可视化；也讨论了轨迹数据处理中应用量子计算的可能方式，并且介绍了目前轨迹数据处理中所使用的核心算法所对应的量子算法实现；最后，对轨迹数据处理面临的挑战与未来研究方向进行了总结与展望.

摘要:团队形成问题作为一个出自于运筹学中的问题，已经得到了深入的研究.然而，随着各种社交平台的流行以及网络通信的迅速发展，社会化网络中的团队形成再次调动起了众多学者的研究热情.社会化网络中的团队形成问题与传统的团队形成有很大的不同，因此，它不能再简单地借助集合覆盖、任务分配或者最大化匹配等经典问题来解决.在充分调研和分析的基础上，对社会化网络下的团队形成问题的研究现状进行了阐述.综述了社会化网络下的团队形成问题的各种变形问题及其优化方法，同时还归纳介绍了该研究中使用的实验数据集和评价指标.最后，对该问题今后可以开展的方向进行了展望.

摘要:随着网络空间安全重要性的不断提高，网络安全态势感知（network security situation awareness，简称NSSA）的研究与应用正在得到更多的关注.NSSA实现对网络中各种活动的行为辨识、意图理解和影响评估，以支持合理的安全响应决策.它是对网络的安全性进行定量分析的一种手段，网络安全管理系统可以借助其宏观把握整个网络的安全状况，分析攻击者的意图，为管理决策提供重要的依据.讨论了NSSA的任务范围，并据此对网络安全态势感知的概念进行了重新定义.然后，分别从网络安全态势觉察、网络安全态势理解、网络安全态势投射这3个层面综述了网络安全态势感知的研究现状和存在的问题.

摘要:现代晶体管技术在单芯片上集成多个处理器已经成为现实.近年来，随着多核处理器集成核数的不断增加，高速缓存的一致性问题凸显出来，已成为多核处理器的性能瓶颈之一，亟待解决.介绍了片上多核处理器一致性问题的由来.总结了多核时代高速缓存一致性协议设计的关键问题，综述了近年来学术界对一致性的研究.从程序访存行为模式、目录组织结构、一致性粒度、一致性协议流量、目录协议的可扩展性等方面，阐述了近年来缓存一致性协议性能优化的方向.对目前片上多核处理器缓存一致性协议设计中存在的问题进行了讨论，并指出了未来进一步研究的方向.