机械化定理证明研究综述

随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.

通用图形处理器缓存子系统性能优化方法综述

随着工艺和制程技术的不断发展以及体系架构的日趋完善,通用图形处理器(general purpose graphics processing units,GPGPU)的并行计算能力得到了很大的提升,其在高性能、高吞吐量等通用计算应用场景的使用越来越广泛.GPGPU通过支持大量线程的并发执行,可以较好地隐藏长延时访存操作,从而获得高并行计算能力.然而,GPGPU在处理计算和访存不规则的应用时,其存储子系统的效率受到很大影响,尤其是片上缓存的争用情况尤为突出,难以及时提供计算操作所需的数据,使得GPGPU的高并行计算能力不能得到充分发挥.解决片上缓存的争用问题、优化缓存子系统的性能,是优化GPGPU性能的主要解决方案之一,也是目前研究GPGPU性能优化的主要热点之一.目前,针对GPGPU缓存子系统的性能优化研究主要集中在线程级并行度(thread level parallelism,TLP)调节、访存顺序调节、数据通量增强、最后一级缓存(last level cache,LLC)优化和基于非易失性存储(non-volatile memory,NVM)的GPGPU缓存新架构设计等5个方面.也从这5个方面重点分析讨论了目前主要的GPGPU缓存子系统性能优化方法,并在最后指出了未来GPGPU缓存子系统优化需要进一步探讨的问题,对GPGPU缓存子系统性能优化的研究有重要意义.

无线传感器网络中公钥机制研究综述

物联网是当前学术界和产业界的研究热点,作为物联网主要构成部分之一的无线传感器网络(Wireless Sensor Networks,WSNs),其安全与人们的生活安全及隐私息息相关.过去近二十年来WSNs安全得到了广泛深入的研究,其中公钥机制从最初的不可行认知到现今的广泛研究应用,在WSNs中的可行性正逐渐被认可.然而公钥机制是否可以在WSNs中全面展开、其被引入到WSNs后会带来哪些问题、还有哪些尚未解决,这些都有待进一步探究.本文梳理了WSNs中公钥机制研究的高质量文献并将其归结为原语类、密钥管理类、认证与访问控制类、其他应用类,对比分析了各类文献中的经典研究工作,总结了WSNs中引入公钥机制的必要性、可行性及相关问题与挑战,针对这些挑战分析了其现有解决情况,最后对研究方向及可能的解决方案进行了展望.

机械化验证一个高效的迭代数据流求解算法

迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的“验证编译器”不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL.