基于上下文定界的递归队列并发程序可达性分析

基于无界FIFO消息队列的通信框架作为一种通用的并发系统模型,常用于事件驱动的并发程序或分布式程序建模.然而当模型包含递归过程调用时,即使仅考虑执行有限次上下文切换,其可达性问题仍是不可判定的.假定进程的消息队列约束为良序,即仅当进程的局部栈为空时才能从队列中读取消息,则其在上下文切换定界上的可达性为可判定.文中以基于队列通信的递归并发程序为对象,研究其可达性问题.首先构造能模拟递归队列并发程序执行的多栈下推系统,并提出转换方法;然后给出一种基于多栈下推系统的上下文切换定界可达算法,算法使用标准Post*操作描述下推系统的迭代,基于良序排队控制进程对队列的出队操作,穷尽地计算k次上下文切换之内的正向可达格局,并证明了构造多栈下推系统方法和上下文切换定界可达算法的正确性;最后对目标状态集合与可达格局状态集合的交集进行判空,确定目标状态是否可达,从而较好地解决此类并发程序的可达性问题.     

通信下推系统的一种有界可达算法

Qadeer首次针对并发下推系统提出一种有界可达算法,通过限定上下文切换的次数使得算法可终止,可有效地分析过程间并发程序。但是并发下推系统以全局变量模拟同步,不适应于当前广泛使用的基于事件驱动的并发程序。针对通信下推系统,提出一种基于双重调度的有界可达算法,通过限定同步调度的次数,结合线程间的同步调度和线程内的路径调度解决通信下推系统的可达性问题,从而为事件驱动的过程间并发程序分析提供了算法基础。     

面向Fork/Join框架的软件重构及性能分析

针对目前对于Fork/Join框架应用和性能分析的相关工作还不多的现状,以JGF基准测试程序套件为基础,对其中的series、crypt、sparsematmult和sor等程序使用Fork/Join框架进行重构,并以series程序为例,详细地说明了重构的过程.在实验中,首先,测试了每个程序在不同阈值下使用Fork/Join框架分别递归1、2、3次执行程序的时间,进而选择相对较好的阈值;然后,对每个程序使用Fork/Join框架和使用Thread的执行时间进行了对比;此外,测试了重构后的程序在执行过程中任务窃取的情况.实验结果表明,Fork/Join框架执行时间与多线程执行时间相比,平均降低了14.2%;对于series程序,当数据大小为sizeC且线程个数为2时,Fork/Join框架执行时间比多线程执行时间降低高达40%,可见,在多核处理器平台上应用Fork/Join框架比使用多线程将获得更好的性能.     

混合动态系统SPN的可达性分析

根据混合动态系统SPN(StochasticPetriNets)模型的运行规则,给出了几种典型结构(串行结构、并行结构、冲突结构)中变迁的可激发以及可激发成功概率的计算方法,在此基础上,计算出托肯沿几种基本路径(简单串行路径、简单并行路径、简单Fork/Join路径)从起始库所到达终止库所的可达概率,同时从宏观状态的角度构建了该SPN模型的状态可达树,通过可达树可以判断状态间的可达性并计算可达概率。     

混合动态系统SPN的可达性分析

根据混合动态系统SPN(Stochastic Petri Nets)模型的运行规则,给出了几种典型结构(串行结构、并行结构、冲突结构)中变迁的可激发以及可激发成功概率的计算方法,在此基础上,计算出托肯沿几种基本路径(简单串行路径、简单并行路径、简单Fork/Join路径)从起始库所到达终止库所的可达概率,同时从宏观状态的角度构建了该SPN模型的状态可达树,通过可达树可以判断状态间的可达性并计算可达概率.     

基于偏序约简程序可达图的并发程序切片方法

并发程序切片是一种重要的并发程序分析手段.基于程序可达图可构造以程序状态和语句二元组为节点的、依赖关系具有可传递性的并发程序依赖图,解决依赖关系的不可传递性问题,提高切片精度.程序可达图通过交织执行模拟并发活动,分析代价较高.偏序约简是一种十分有效的并发系统状态空间约简技术,约简的并发系统状态空间包含所有的并发程序执行代表.为提高效率,该文将偏序约简技术扩展到程序可达图的约简中,在偏序约简理论的基础上,证明了基于未约简和约简的并发程序可达图构造的并发程序依赖图在进行切片计算时是等价的.实验结果表明,采用偏序约简技术使基于程序可达图的并发程序切片方法在保证切片精度不受损失的前提下显著提高切片效率.与其它高精度切片方法相比,基于约简程序可达图的切片方法的精度更高,在大多数情况下,切片效率也有一定提高.     

一种基于并发错误模式的Java并发程序动态测试方法

并发程序中时序的不确定性导致的错误很难被检测.本文介绍了一种基于并发错误模式的多线程动态测试方法,通过在并发事件处插入线程时序改变探针,发现并发错误.本文首先介绍了出现在并发程序中的几种常见的错误模式,接着根据错误模式介绍插装策略.     

对Java并发程序进行模型检测

随着多核处理器的发展,多线程并发程序成为现代程序设计的趋势.但并发线程的执行存在不确定性,传统的测试方法很难发现这类错误.针时这个问题,提出了一种直接分析Java源代码,从中提取并发程序模型的方法;并以此方法为基础开发了工具JTS(Java to SPIN),实现了对Java并发程序的自动化分析和模型检测.实验表明JTS能够成功地检测出Java并发程序中存在的错误并给出相应的错误路径.这项工作给Java并发程序的测试与验证提供了新的途径.     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。     

基于MapReduce的内存并行Join算法研究

传统的并行Join算法缺少必要的容错能力,且数据划分不均往往导致单个线程的阻塞成为整个任务执行的瓶颈。针对以上问题,分析内存连接的各个阶段对Join算法性能的影响,提出一种可利用MapReduce的动态机制,避免了传统并行连接算法的数据任务分派不均和容错问题。算法使用MapReduce编程框架,并通过封装分块标记减少MapReduce Join执行过程中标记和排序的计算开销,使算法性能显著提高。实验结果表明,该算法在共享内存体系结构下,性能上相比已有算法有显著改进。     

Modular strategies for recursive game graphs

Many problems in formal verification and program analysis can be formalized as computing winning strategies for two-player games on graphs. In this paper, we focus on solving games in recursive game graphs which can model the control flow in sequential programs with recursive procedure calls. While such games can be viewed as the pushdown games studied in the literature, the natural notion of winning in our framework requires the strategies to be modular with only local memory; that is, resolution of choices within a module does not depend on the context in which the module is invoked, but only on the history within the current invocation of the module. While reachability in (global) pushdown games is known to be EXPTIME-complete, we show reachability in modular games to be NP-complete. We present a fixed-point computation algorithm for solving modular games such that in the worst case the number of iterations is exponential in the total number of returned values from the modules. If the strategy within a module does not depend on the global history, but can remember the history of the past invocations of this module, that is, if memory is local but persistent, we show that reachability becomes undecidable.     

基于下推系统可达性分析的程序机密消去机制

针对程序语言信息流安全领域的现有机密消去策略,提出了一种基于下推系统可达性分析的程序信息流安全验证机制.将存储-匹配操作内嵌于对抽象模型的紧凑自合成结果中,使得对抽象结果中标错状态的可达性分析可以作为不同机密消去策略下程序安全性的验证机制.实例研究说明,该方法比基于类型系统的方法具有更高的精确性,且比已有的自动验证方法更为高效.     

Verifying parallel programs with dynamic communication structures

We address the verification problem of networks of communicating pushdown systems modeling communicating parallel programs with procedure calls. Processes in such networks can read the control state of the other processes according to a given communication structure (specifying the observability rights between processes). The reachability problem of such models is undecidable in general. First, we define a class of networks that effectively preserves recognizability (hence, its reachability problem is decidable). Then, we consider networks where the communication structure can change dynamically during the execution according to a phase graph. The reachability problem for these dynamic networks being undecidable in general, we define a subclass for which it becomes decidable. Then, we consider reachability when the switches in the communication structures are bounded. We show that this problem is undecidable even for one switch. We define a natural class of models for which this problem is decidable. This class can be used in the definition of an efficient semi-decision procedure for the analysis of the general model of dynamic networks. Our techniques allowed to find bugs in two versions of a Windows NT Bluetooth driver.     

不确定线性系统的可达集估计

本文针对线性不确定系统,研究了系统状态可达集估计问题.在已知参考输入,未知扰动有界的条件下,提出了一种新的可达集估计方法,并把所提方法推广到系统不稳定的情况,分别估计出不稳定系统的闭环可达集和开环可达集.通过分析动态系统的李雅普诺夫函数,将求取系统可达集的问题转化为线性矩阵不等式优化问题,并将可达集范围用椭球集形式表述.最后分别通过数值仿真分析,验证了所提出方法对线性系统可达集估计的有效性.     

Reachability Analysis of Synchronized PA Systems

We present a generic approach for the analysis of concurrent programs with (unbounded) dynamic creation of threads and recursive procedure calls. We define a model for such programs based on a set of term rewrite rules where terms represent control configurations. The reachability problem for this model is undecidable. Therefore, we propose a method for analyzing such models based on computing abstractions of their sets of computation paths. Our approach allows to compute such abstractions as least solutions of a system of (path language) constraints. More precisely, given a program and two regular sets of configurations (process terms) T and T^′, we provide (1) a construction of a system of constraints which characterizes the set of computation paths leading from T to T^′, and (2) a generic framework, based on abstract interpretation, allowing to solve this system in various abstract domains leading to abstract analysis with different precision and cost.     

Bond computing systems: a biologically inspired and high-level dynamics model for pervasive computing

Targeting at modeling the high-level dynamics of pervasive computing systems, we introduce bond computing systems (BCS) consisting of objects, bonds and rules. Objects are typed but addressless representations of physical or logical (computing and communicating) entities. Bonds are typed multisets of objects. In a BCS, a configuration is specified by a multiset of bonds, called a collection. Rules specify how a collection evolves to a new one. A BCS is a variation of a P system introduced by Gheorghe Paun where, roughly, there is no maximal parallelism but with typed and unbounded number of membranes, and hence, our model is also biologically inspired. In this paper, we focus on regular bond computing systems (RBCS), where bond types are regular, and study their computation power and verification problems. Among other results, we show that the computing power of RBCS lies between linearly bounded automata (LBA) and LBC (a form of bounded multicounter machines) and hence, the regular bond-type reachability problem (given an RBCS, whether there is some initial collection that can reach some collection containing a bond of a given regular type) is undecidable. We also study a restricted model (namely, B-boundedness) of RBCS where the reachability problem becomes decidable.     

Hierarchical reachability graph of bounded Petri nets forconcurrent-software analysis

Petri nets have been proposed as a promising tool for modeling and analyzing concurrent-software systems such as Ada programs and communication protocol software. Among analysis techniques available for Petri nets, the most general approach is to generate all possible states (markings) of the system in a form of a so-called reachability graph. However, this conventional reachability graph approach is inefficient or intractable, even for a bounded Petri net, due to state explosion in many practical applications. To cope with this problem, this paper proposes a method for constructing a hierarchically organized state space called the hierarchical reachability graph (HRG). Using the HRG, we obtain necessary and sufficient conditions for reachability and deadlock, as well as algorithms to test whether a given state or marking is reachable from the initial state and whether there is a deadlock state (a state with no successor states)     

Property analysis of logic Petri nets by marking reachability graphs

Logic Petri nets (LPNs) are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method for analyzing LPNs is proposed based on marking reachability graphs in this paper. Enabled conditions of transitions are obtained and a marking reachability graph is constructed. All reachable markings can be obtained based on the graph; the fairness and reversibility of LPNs are analyzed. Moreover, the computing complexity of the enabled conditions and reachable markings can be reduced by this method. The advantages of the proposed method are illustrated by examples and analysis.     

基于下推系统可达性分析的输出信道信息流检测

提出了一种对含输出信道的命令式语言进行信息流安全性分析的方法。将程序抽象为下推系统,通过自合成将不千涉性转化为安全性属性,将两次相关执行中向输出信道的输出操作分别抽象为由下推规则表示的存储和匹配操作,通过对标错状态的可达性分析验证程序是否满足终止不敏感不干涉性。演化后的方法支持程序的发散执行,通过上界回退算法找到强制终止首次执行所需的最大输出信道上界。实验说明该方法与现有工作相比具有更高的精确性和验证效率。