基于流分析与归纳不变式结合的German协议验证

来源 :计算机系统应用 | 被引量 : 0次 | 上传用户：yilongfengyue5656

【摘要】

：

German缓存一致性协议是用于共享内存的并发多处理器系统中的缓存一致性协议,对German协议进行形式化验证一直是学术界和工业界的热点.我们生成German协议的流图,对流程图的

【作者】

：

张瑜孙文辉

【机构】

：

北京交通大学计算机与信息技术学院

【出处】

：

计算机系统应用

【发表日期】

：

2017年10期

【关键词】

：

缓存一致性协议流分析归纳不变式形式化验证 cache coherence protocol flow analysis inductive invar

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

German缓存一致性协议是用于共享内存的并发多处理器系统中的缓存一致性协议,对German协议进行形式化验证一直是学术界和工业界的热点.我们生成German协议的流图,对流程图的各个步骤进行详细的描述,并提出了流分析与归纳不变式结合对协议验证的方法,通过辅助不变式与协议流图的对应关系,从而进一步分析和验证German协议的正确性.

其他文献

基于顶点法向量约束的Catmull-Clark细分插值方法

提出一种基于顶点法向量约束实现插值的两步Catmull-Clark细分方法.第一步,通过改造型CatmullClark细分生成新网格.第二步,通过顶点法向量约束对新网格进行调整.两步细分分别

期刊

CATMULL-CLARK细分插值法向量渐进迭代拉格朗日乘子Catmull-Clark subdivisioninterpolationnorma

基于补全矩阵的多标签相关性情感分类

目前,对新闻情感分类问题的研究大部分是从新闻作者的角度进行的,而对读者反馈的真实情感分析的较少.本文从读者角度入手进行情感分析研究.提出一种基于补全矩阵的多标签相关

期刊

社会新闻情感分析标签相关性补全矩阵-LDA(CM-LDA)多标签分类social news sentiment analysis label co

基于CRC的防污染网络编码方案

网络编码的直接应用容易遭受污染攻击,我们针对这一安全性问题,给出了一种基于CRC校验码的防污染网络编码方案.该方案首先通过引入快速的并行CRC校验码和消息时间戳的设计理

期刊

网络编码污染攻击并行CRC校验码时间戳network coding pollution attacks parallel CRC check cod

基于改进高斯核度量和KPCA的数据聚类新方法

大多数超椭球聚类（hyper-ellipsoidal clustering,HEC）算法都使用马氏距离作为距离度量,已经证明在该条件下划分聚类的代价函数是常量,导致HEC无法实现椭球聚类.本文说明了使用

期刊

数据聚类超椭球聚类最小体积椭球核主成分分析高斯核data clustering hyper-ellipsoidal clustering mini

面向高性能DSP的图像滤波库优化

滤波函数在图像处理领域起着至关重要的作用.传统的滤波实现方法以窗口为处理单位,但窗口尺寸较小导致指令流水线频繁中断.针对该问题,本文提出了算法切片的优化方法.首先,对滤波算法进行切片,使得每个切片处理滤波窗口中的一个像素点;接着,根据切片处理的像素点在滤波窗口中的位置计算出有效处理范围,去除图像边缘处理中复杂的条件判断;最后,按列方向进行多簇流水,让流水线重复执行大量相同的指令序列.结合BWDSP

期刊

数字信号处理器超流水线多簇图像滤波软件流水化中值滤波digital signal processor（DSP） superpipline mul

基于图像退化模型的图像去雾算法

在雾、霾之类的恶劣天气下拍摄的图像,由于存在大气的散射作用,使得物体特征难以辨认,严重影响了图像的视觉效果,同时还妨碍了图像的特征提取.因此,需要利用去雾技术对图像进行增强和修复,以改善视觉效果和方便后期处理.本文针对暗原色先验去雾算法耗时长和处理效果不佳等问题,提出了一种改进的自适应边界约束去雾算法.同时,引入了信息熵和平均梯度对其进行客观评价,对比实验结果表明该方法运算速度快,在细节处理上效果

期刊

去雾边界约束自适应defogging boundary constraints adaptive

基于自适应惯性权重的混沌粒子群优化无线传感器网络成簇算法

为了解决簇头选举过程中多因素冲突问题,以优化簇头选举和延长网络生命周期为目标,提出一种基于自适应惯性权重混沌粒子群优化（AWCPSO）的分簇算法.该算法在簇头竞选过程中,考虑

期刊

无线传感器网络分簇算法粒子群算法混沌理论网络生命周期wireless sensor networks clustering algorithm p

基于DBN的多特征融合音乐情感分类方法

本文在音乐情感分类中的两个重要的环节：特征选择和分类器上进行了探索.在特征选择方面基于传统算法中单一特征无法全面表达音乐情感的问题,本文提出了多特征融合的方法,具体

期刊

音乐情感分类深度学习深度置信网络音乐特征提取特征融合music mood classification deep learning deep be

数据整合中异常检测算法研究

传统的数据整合方案-（[1]）中存在结构上的不严谨性,在整合期间由于各种原因导致整合后的结果存在很多异常离群点,而且并没有有效的措施进行检测和避免.本文提出了基于角度的改

期刊

数据整合异常检测离群点检测基于角度生产事故data integration anomaly detection outlier detection

非平稳时序数据的分段辨识及其递推算法

在实际生活中,广泛地存在着一类在整体上属于非平稳但又可转化为数段局部平稳的时序数据,对该类非平稳时序数据的辨识问题进行了研究,并提出了一种具有递推机制的分段辨识算

期刊

非平稳时序数据局部平稳分段辨识递推分界点自回归模型non-stationary time series data local stationary

基于流分析与归纳不变式结合的German协议验证

与本文相关的学术论文