【摘 要】
：
随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求,多核并行程序验证的重要性日益凸显。本文提出了一个完整的基于多核的并行程序验证框架,该验证框架包括抽象机器
【机 构】
：
清华大学计算机科学与技术系 北京 100084
【出 处】
：
2008全国软件与应用学术会议(NASAC'08)
论文部分内容阅读
随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求,多核并行程序验证的重要性日益凸显。本文提出了一个完整的基于多核的并行程序验证框架,该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及其证明。目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问。验证框架采用Hoare风格的推导方式,使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略。在该框架下,程序员可以对多核并行程序的部分正确性进行验证。
其他文献
SUSAN是低级图像处理中的一种边及角点检测方法,具有大量可挖掘的数据级并行.本文分析了SUSAN的主要程序模式,提取相应的流特征,提出了SUSAN的流式实现,并在流处理器MASA-I上
多核处理器已经成为高性能微处理器技术发展的重要方向,同时也对多核体系结构下的编译技术提出了更高的要求.本文以典型的NPB程序CG为例,分析了该程序在多核处理器上的实验结
网络式软件作为基于Internet这一开放环境运行的软件的一个典型代表,其全开放运行机制使得需求过程的自动调度尤为重要.为此,首先将网络式软件的需求状态(NRS)划分为6个状态,
事务存储系统是一种全新的多核体系结构,为并行编程提供了一个简洁高效的编程环境.基于Signature的冲突检测算法是事务存储系统中很有前景的一种冲突检测方法,其误判率直接影
预测性对象点(POPs)方法是一种面向对象软件度量方法。它从多个方面对软件进行度量,估算软件规模。POPs方法计算的核心是每类加权平均方法数。相对于传统的图表法,本文利用多
面向Agent的软件设计是一种新的软件设计方法,对目前谊方法在工程领域的应用进行分析,总结了阻碍谊方法广泛使用的基本原因,并于此提出了一种基于结构化P2P网络的多Agent框架
随着网络上Web服务的增多,如何从大量的Web服务中全面、准确的找到满足需求的Web服务变得越来越重要.目前的Web服务发现机制主要基于UDDI规范。然而,在UDDI机制中,服务的描述
服务器集群是提高系统QOS和可用性一种方法,但由于需要长期连续运行提供服务,集群系统仍然会存在软件老化现象,从而造成系统的处理能力随时间的增加而降低、失效率随时间的增
为了克服全球计算环境中计算节点的动态性的特征,引入了计算节点可信任度模型,该模型分别收集节点的历史任务完成情况和专门测试节点对计算节点的测试情况这两条独立的证据,