摘要：本文引入描述传值并发系统的新模型“带赋值符号迁移图（STGA）”．STGA推广了Hen－nessy和Lin提出的“符号迁移图”的概念，允许迁移上带有赋值，从而能将更大的一类传值系统表示为有穷状态图．STGA的另一优点是在并行运算下封闭．文中给出了STGA的操作语义，在此基础上定义了STGA的互模拟等价关系．为了刻划STGA的互模拟，以谓词等式系的形式在一阶逻辑的正子集中扩充了最大和最小不动点，并设计了一个算法将STGA的互模拟归结为谓词等式系的最大不动点．

摘要：当今世界的主流超级计算机越来越多地使用带有加速器的异构系统.随着加速器的浮点性能不断提高,超级计算机内计算节点的CPU、内存、总线、网络以及系统架构都要与之相适应.HPL(high performance Linpack)是高性能计算机评测的传统基准测试程序,复杂异构系统给HPL评测带来很多机遇与挑战.针对带有GPU的异构超级计算机系统,提出一套新的CPU与加速器计算任务分配方式,提出平衡点理论指导HPL性能优化.为了优化HPL程序,提出了使用CPU与加速器协同工作的look-ahead算法和行交换连续流水算法,实现了加速器、CPU、网络等部件的高度并行.此外,为带有加速器的系统设计了新的panel分解和行交换的实现方法,提高了加速器的利用率.在每个节点带有4个GPU的系统上,单节点HPL效率达到了79.51%.

摘要：认证协议设计和实现的安全性分析是网络安全的重要课题，越来越多的人关注这个方向的发展。在此系统地讨论了认证协议形式验证研究的前沿课题和发展趋势，并介绍了基于时序逻辑的认证协议研究成果和基于时序逻辑的ModelChecking的构想。

摘要：利用模块化设计的思想 ,首先为分布式数据库系统中各事务的每一种操作 (读锁、写锁、解锁 )构造一个基本的加权 Petri网模型 ,并给出了加权 Petri网共享合成的概念 .然后利用共享合成技术 ,动态地构造各站点的加权 Petri网模型 ,以适应系统的动态变化 .此外 ,本文利用 Petri网的化简技术 ,极大地简化了各站点的 Petri网模型 ,之后利用同步合成技术构造出整个系统的 Petri网模型 ,较好地解决了 Petri网的可达性分析中可能出现的状态 "爆炸 "问题 .

摘要：虚拟现实（ＶＲ）系统对火焰的模拟，通常采用纹理映射（ＴｅｘｔｕｒｅＭａｐｐｉｎｇ）技术，即采用二维火焰图象作为纹理，将其映射到画面对应位置．由于纹理是二维的，所以无法从各个角度对火焰进行观察，从而大大影响了场景的真实感及用户的沉浸感．本文提出了一种在ＶＲ飞行模拟系统中生成导弹尾部火焰的算法，用该算法产生的三维尾焰，在形状、色彩、动画效果上均十分逼真，且计算开销较小．对于有图形硬件支持的ＶＲ系统来说，完全可以实现尾焰的实时生成．

摘要：根据申威26010众核处理器的特点提出了基于两层分解的一维FFT众核并行算法.该算法基于迭代的Stockham FFT计算框架和Cooley-Tukey FFT算法,将大规模FFT分解成一系列的小规模FFT来计算,并通过设计合理的任务划分方式、寄存器通信、双缓冲以及SIMD向量化等与计算平台相关的优化方法来提高FFT的计算性能.最后对所提出算法的性能进行了测试,相比于单主核上运行的FFTW3.3.4库,获得了平均44.53x的加速比,最高加速比可达56.33x,且其带宽利用率最高可达83.45%.

摘要：世界首台峰值性能超过100P的超级计算机——神威太湖之光已经研制完成,该超级计算机采用了国产申威异构众核处理器,该处理器不同于现有的纯CPU,CPU-MIC,CPU-GPU架构,采用了主-从核架构,单处理器峰值计算能力为3TFlops/s,访存带宽为130GB/s.稀疏矩阵向量乘SpMV(sparse matrix-vector multiplication)是科学与工程计算中的一个非常重要的核心函数,众所周知,其是带宽受限型的,且存在间接访存操作.国产申威处理器给稀疏矩阵向量乘的高效实现带来了很大的挑战.针对申威处理器提出了一种CSR格式SpMV操作的通用异构众核并行算法,该算法从任务划分、LDM空间划分方面进行精细设计,提出了一套动静态buffer的缓存机制以提升向量x的访存命中率,提出了一套动静态的任务调度方法以实现负载均衡.另外还分析了该算法中影响SpMV性能的几个关键因素,并开展了自适应优化,进一步提升了性能.采用Matrix Market矩阵集中具有代表性的16个稀疏矩阵进行了测试,相比主核版最高有10倍左右的加速,平均加速比为6.51.通过采用主核版CSR格式SpMV的访存量进行分析,测试矩阵最高可达该处理器实测带宽的86%,平均可达到47%.

摘要：大气动力学问题的数值模拟在气象预报等领域具有广泛的应用.相关数值模拟依赖超级计算机平台实现高精度高分辨率的气象预报,隐式求解不受稳定性条件限制,相比显式求解更有优势.面向新的超级计算机架构特征研究隐式大气动力学问题中一系列算子操作的并行和优化方法是非常有必要的.本文在规则递推关系的理论框架下对大气动力学问题预条件阶段的稀疏三角回代求解以及ILU矩阵分解操作的特征进行了总结,并结合申威26010Pro处理器的架构特点,对现有结构化稀疏三角线性方程组问题的并行算法进行了推广,设计了一套面向单向规则递推关系的算法框架,解决了预条件阶段各类算子的并行加速问题.本文还面向申威26010Pro处理器对大气动力学问题的模板计算等算子进行了移植和优化.实验结果显示,本文的算法框架对预条件阶段的算子能够实现26-33倍不等的加速效果,对模板计算等算子的优化相比串行计算有10-152倍的加速比.在新的神威超级计算机上最大测试到1700多万核心,浮点性能达到20.5PFlop/s.在大规模测试条件下的强(弱)可扩展性维持在56.81%(41.87%)以上.

摘要：程序信息流安全是信息安全的一个重要研究方向.基于类型的静态分析可以保证程序信息流安全.与单进程系统相比,移动计算系统中数据通讯的存在使得程序信息流安全保护更加困难.Cornell大学的Zdancewic对函数式语言λsec的单进程程序信息流安全进行了研究.本文在其工作的基础上,根据移动计算系统的结构特征,通过对函数式语言λsec进行扩充,加入通讯原语,将其扩展成移动计算语言MobileML,并针对一个简单的移动计算模型,给出了描述程序信息流安全的无干扰性定义,设计了相应的信息流类型系统,用以静态检查保证MobileML语言程序信息流安全.

摘要：网络隐蔽信道是在网络环境下违反通信限制规则进行隐蔽信息传输的信息通道,为网络信息安全带来了新的挑战,也为数据传输的安全性和隐私性带来了新的研究方向.首先介绍了网络隐蔽信道的定义、分类、能力维度等基本概念;进而从码元设计、信息编码和信道优化这3个方面归纳分析了存储型和时间型两类网络隐蔽信道的构建技术,从隐蔽性、鲁棒性和传输效率这3个方面总结了网络隐蔽信道评估方法,从消除、限制、检测这3个方面梳理了网络隐蔽信道的对抗技术;最后,对未来的研究方向进行了展望.