Runtime analysis of atomicity for multithreaded programs

Atomicity is a correctness condition for concurrent systems. Informally, atomicity is the property that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. In multithreaded programs, executions of procedures (or methods) can be regarded as transactions. Correctness in the presence of concurrency typically requires atomicity of these transactions. Tools that automatically detect atomicity violations can uncover subtle errors that are hard to find with traditional debugging and testing techniques. This paper describes two algorithms for runtime detection of atomicity violations and compares their cost and effectiveness. The reduction-based algorithm checks atomicity based on commutativity properties of events in a trace; the block-based algorithm efficiently represents the relevant information about a trace as a set of blocks (i.e., pairs of events plus associated synchronizations) and checks atomicity by comparing each block with other blocks. To improve the efficiency and accuracy of both algorithms, we incorporate a multilockset algorithm for checking data races, dynamic escape analysis, and happen-before analysis. Experiments show that both algorithms are effective in finding atomicity violations. The block-based algorithm is more accurate but more expensive than the reduction-based algorithm.     

Synchronizing concurrent model updates based on bidirectional transformation

Model-driven software development often involves several related models. When models are updated, the updates need to be propagated across all models to make them consistent. A bidirectional model transformation keeps two models consistent by updating one model in accordance with the other. However, it does not work when the two models are modified at the same time. In this paper we first examine the requirements for synchronizing concurrent updates. We view a synchronizer for concurrent updates as a function taking the two original models and the two updated models as input, and producing two new models where the updates are synchronized. We argue that the synchronizer should satisfy three properties that we define to ensure a reasonable synchronization behavior. We then propose a new algorithm to wrap any bidirectional transformation into a synchronizer with the help of model difference approaches. We show that synchronizers produced by our algorithm are ensured to satisfy the three properties if the bidirectional transformation satisfies the correctness property and the hippocraticness property. We also show that the history ignorance property contributes to the symmetry of our algorithm. An implementation of our algorithm shows that it worked well in a practical runtime management framework.     

一种新的Statechart模型验证方法

在传统的基于时序逻辑的模型检查框架下验证Statcchart模型面临三大挑战:全状态空间搜索、多次重复搜索和复杂时序逻辑公式难写。基于上述问题和实践工作,提出一种新的Statechart模型验证方法。该方法的中心是一种强化了的属性描述语言—属性状态图,并利用属性状态图中存在的先后关系和并发关系,把各个属性状态图有机地结合成一个树结构—属性树。属性树涵盖了目标系统要求验证的属性空间,因此可自上而下的验证整棵属性树。在验证过程中系统Statechart模型对应状态空间是逐步展开的,每验证部分属性就展开相应的部分状态空间并对其进行验证,验证过程是基于属性树转换并以step为单位,验证step的初始status和结束status是否满足对应属性树节点公式对其的属性约束,这样既能够迅速找出错误又能屏蔽step内部系统Statcchart模型的状态变化,使得验证过程更简单快捷。为了说明属性状态图和基于其的验证算法是实用和易用的,通过一个例子说明了从模型设计到具体验证整个过程。     

基于主观逻辑的信任搜索算法

针对现有信任模型中信任搜索算法不能准确有效地对信任进行搜索与合成,利用主观逻辑理论对信任进行量化与计算,提出基于主观逻辑的信任搜索算法.算法由两个关键技术组成:信任路径提取算法与信任路径合成算法.仿真实例验证了该算法在信任合成时减少了信任网络中冗余信息对信任合成的影响,提高了信任搜索效率,使得合成结果更加准确.     

Component-wise incremental LTL model checking

Efficient symbolic and explicit-state model checking approaches have been developed for the verification of linear time temporal logic (LTL) properties. Several attempts have been made to combine the advantages of the various algorithms. Model checking LTL properties usually poses two challenges: one must compute the synchronous product of the state space and the automaton model of the desired property, then look for counterexamples that is reduced to finding strongly connected components (SCCs) in the state space of the product. In case of concurrent systems, where the phenomenon of state space explosion often prevents the successful verification, the so-called saturation algorithm has proved its efficiency in state space exploration. This paper proposes a new approach that leverages the saturation algorithm both as an iteration strategy constructing the product directly, as well as in a new fixed-point computation algorithm to find strongly connected components on-the-fly by incrementally processing the components of the model. Complementing the search for SCCs, explicit techniques and component-wise abstractions are used to prove the absence of counterexamples. The resulting on-the-fly, incremental LTL model checking algorithm proved to scale well with the size of models, as the evaluation on models of the Model Checking Contest suggests.     

Directed explicit-state model checking in the validation of communication protocols

The success of model checking is largely based on its ability to efficiently locate errors in software designs. If an error is found, a model checker produces a trail that shows how the error state can be reached, which greatly facilitates debugging. However, while current model checkers find error states efficiently, the counterexamples are often unnecessarily lengthy, which hampers error explanation. This is due to the use of naive search algorithms in the state space exploration.In this paper we present approaches to the use of heuristic search algorithms in explicit-state model checking. We present the class of A^* directed search algorithms and propose heuristics together with bitstate compression techniques for the search of safety property violations. We achieve great reductions in the length of the error trails, and in some instances render problems analyzable by exploring a much smaller number of states than standard depth-first search. We then suggest an improvement of the nested depth-first search algorithm and show how it can be used together with A^* to improve the search for liveness property violations. Our approach to directed explicit-state model checking has been implemented in a tool set called HSF-SPIN. We provide experimental results from the protocol validation domain using HSF-SPIN.     

Symbolic predictive analysis for concurrent programs

Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on the happens-before causality relations have been proposed for predictive analysis. However, these models often rely on only the observed runtime events and typically do not utilize the program source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted traces often suffer from the interleaving explosion problem. In this paper, we introduce a precise predictive model based on both the program source code and the observed execution events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events of the given trace. Rather than explicitly enumerating and checking the interleavings, our method conducts the search using a novel encoding and symbolic reasoning with a satisfiability modulo theory solver. We also propose a technique to bound the number of context switches allowed in the interleavings during the symbolic search, to further improve the scalability of the algorithm.     

并发程序原子图挖掘技术

针对当前并发程序的不确定性和复杂性,以及程序原子性质获取困难的问题,提出一种并发程序原子性质提取方法。将并发程序中的同步区域转化为与并发操作相关的并发操作图后,采用频繁子图挖掘算法自动提取程序中的原子图,使其能刻画并发程序的原子性质,包括并发操作以及操作之间的控制依赖关系。实验结果证明,该方法能以较低的误测率有效提取并发程序的原子性质。     

分组密码复杂线性层可分性传播的MILP刻画方法

混合整数线性规划(MILP)作为一种自动化搜索工具, 被广泛地应用于搜索分组密码的差分、线性、积分等密码性质. 提出一种基于动态选取策略构建MILP模型的新技术, 该技术在不同的条件下采用不同的约束不等式刻画密码性质的传播. 具体地, 从可分性出发根据输入可分性汉明重量的不同, 分别采用不同的方法构建线性层可分性传播的MILP模型. 最后, 将该技术应用于搜索uBlock和Saturnin算法的积分区分器. 实验结果表明: 对于uBlock128算法, 该技术可以搜索到比之前最优区分器多32个平衡比特的8轮积分区分器. 除此之外, 搜索到uBlock128和uBlock256算法比之前最优区分器更长一轮的9和10轮积分区分器. 对于Saturnin256算法, 同样搜索到比之前最优区分器更长一轮的9轮积分区分器.     

Exploring very large state spaces using genetic algorithms

We present a novel framework for exploring very large state spaces of concurrent reactive systems. Our framework exploits application-independent heuristics using genetic algorithms to guide a state-space search toward error states. We have implemented this framework in conjunction with VeriSoft, a tool for exploring the state spaces of software applications composed of several concurrent processes executing arbitrary code. We present experimental results obtained with several examples of programs, including a C implementation of a public-key authentication protocol. We discuss heuristics and properties of state spaces that help a genetic search detect deadlocks and assertion violations. For finding errors in very large state spaces, our experiments show that a genetic search using simple heuristics can significantly outperform random and systematic searches.     

An Adaptive Tradeoff Model for Constrained Evolutionary Optimization

In this paper, an adaptive tradeoff model (ATM) is proposed for constrained evolutionary optimization. In this model, three main issues are considered: (1) the evaluation of infeasible solutions when the population contains only infeasible individuals; (2) balancing feasible and infeasible solutions when the population consists of a combination of feasible and infeasible individuals; and (3) the selection of feasible solutions when the population is composed of feasible individuals only. These issues are addressed in this paper by designing different tradeoff schemes during different stages of a search process to obtain an appropriate tradeoff between objective function and constraint violations. In addition, a simple evolutionary strategy (ES) is used as the search engine. By integrating ATM with ES, a generic constrained optimization evolutionary algorithm (ATMES) is derived. The new method is tested on 13 well-known benchmark test functions, and the empirical results suggest that it outperforms or performs similarly to other state-of-the-art techniques referred to in this paper in terms of the quality of the resulting solutions.     

带时间窗的多车型需求可拆分揽收配送问题

研究了一种带时间窗的多车型需求可拆分揽收配送问题（Multi-Vehicle Split Pickup and Delivery Problem with Time Windows,MVSPDPTW）。针对这个问题以执行任务车辆行驶路径总长度最小为目标函数,建立了一个混合整数线性规划模型。提出了一种高效禁忌模拟退火（Tabu Simulated Annealing,TSA）算法,在算法中设计了两种新的邻域搜索算子,分别用于修复违反容量约束以及换车操作,多种算子配合的方式扩大了邻域搜索范围,避免算法陷入局部最优。此外在算法中加入了禁忌机制以及违反约束惩罚机制,实现了搜索空间的有效裁剪,提高了算法的全局寻优能力。最后基于Solomon数据集和构造的仿真数据集等对算法进行了大量仿真实验,实验验证了该算法的有效性。     

A new algorithm inspired in the behavior of the social-spider for constrained optimization

During the past decade, solving constrained optimization problems with swarm algorithms has received considerable attention among researchers and practitioners. In this paper, a novel swarm algorithm called the Social Spider Optimization (SSO-C) is proposed for solving constrained optimization tasks. The SSO-C algorithm is based on the simulation of cooperative behavior of social-spiders. In the proposed algorithm, individuals emulate a group of spiders which interact to each other based on the biological laws of the cooperative colony. The algorithm considers two different search agents (spiders): males and females. Depending on gender, each individual is conducted by a set of different evolutionary operators which mimic different cooperative behaviors that are typically found in the colony. For constraint handling, the proposed algorithm incorporates the combination of two different paradigms in order to direct the search towards feasible regions of the search space. In particular, it has been added: (1) a penalty function which introduces a tendency term into the original objective function to penalize constraint violations in order to solve a constrained problem as an unconstrained one; (2) a feasibility criterion to bias the generation of new individuals toward feasible regions increasing also their probability of getting better solutions. In order to illustrate the proficiency and robustness of the proposed approach, it is compared to other well-known evolutionary methods. Simulation and comparisons based on several well-studied benchmarks functions and real-world engineering problems demonstrate the effectiveness, efficiency and stability of the proposed method.     

一种求解作业车间调度的混合粒子群算法*

针对车间作业调度问题,提出了一种混合了知识进化算法和粒子群优化的算法。算法主要是结合知识进化算法的进化选择机制和粒子群优化的局部快速收敛性特性,首先让粒子替代知识进化算法中的进化个体,在群体空间中按粒子群优化规则寻找局部最优,然后根据知识进化算法的全局选择机制寻找全局最优,最后,将车间作业调度问题的特点融入到所提出的混合算法中求解问题。采用基准数据进行测试的仿真实验,并比对标准遗传算法,结果表明所提算法的有效性。     

Improving convergence of evolutionary multi-objective optimization with local search: a concurrent-hybrid algorithm

A local search method is often introduced in an evolutionary optimization algorithm, to enhance its speed and accuracy of convergence to optimal solutions. In multi-objective optimization problems, the implementation of local search is a non-trivial task, as determining a goal for local search in presence of multiple conflicting objectives becomes a difficult task. In this paper, we borrow a multiple criteria decision making concept of employing a reference point based approach of minimizing an achievement scalarizing function and integrate it as a search operator with a concurrent approach in an evolutionary multi-objective algorithm. Simulation results of the new concurrent-hybrid algorithm on several two to four-objective problems compared to a serial approach, clearly show the importance of local search in aiding a computationally faster and accurate convergence to the Pareto optimal front.     

一种禁忌搜索算法在二维HP非格模型中的应用

禁忌搜索算法是一种启发式的全局优化算法,是局部搜索算法的一种推广,已被成功地应用于许多组合优化问题,本文探讨将一种记忆的禁忌搜索算法应用于求解蛋白质结构预测问题。文中首先介绍了一种二维HP非格模型,此模型最后可以归结为一个全局优化问题,然后介绍了记忆的禁忌搜索算法在其中的应用,通过与PERM（Pruned—Enriched—Rosenbluth Method）比较,发现禁忌算法能得到较好的实验结果,经分析发现虽然二维HP非格模型很简单,但却能反映蛋白质结构的一些简单的性质,即在蛋白质结构中,疏水性氨基酸形成束,总是被极性氨基酸包围。数值实验表明该算法对于蛋白质结构预测是可行有效的。     

Towards efficiently searching triple product property triples: Deterministic and randomized algorithms

The key objects in the group-theoretic approach to matrix multiplication are subsets of a group satisfying the so-called triple product property (TPP). In this paper, we focus on the problem of efficiently finding the triple product property triples. We deduce and present some new characteristics of the tripleproduct property. Using these new characteristics, we firstly propose an efficient deterministic algorithm in which a screening process based on historical information is designed to reduce the search space. In contrast to some of the recent heuristic search methods, the proposed deterministic algorithm can search all kinds of TPP triples in a highly efficient way with the help of a novel representation for subsets and a Moving 1 principle. In addition, we also propose an efficient randomized algorithm for finding TPP triples, which adopts a greedy randomized strategy to randomly generate possible TPP candidates. Experimental results demonstrate that our proposed deterministic algorithm can achieve a huge speed-up in terms of running time compared with the existing deterministic algorithm, and the proposed randomized algorithm outperforms other existing approaches for finding TPP triples.     

Assigning real-time tasks to heterogeneous processors by applying ant colony optimization

The problem of determining whether a set of periodic tasks can be assigned to a set of heterogeneous processors without deadline violations has been shown, in general, to be NP-hard. This paper presents a new algorithm based on ant colony optimization (ACO) metaheuristic for solving this problem. A local search heuristic that can be used by various metaheuristics to improve the assignment solution is proposed and its time and space complexity is analyzed. In addition to being able to search for a feasible assignment solution, our extended ACO algorithm can optimize the solution by lowering its energy consumption. Experimental results show that both the prototype and the extended version of our ACO algorithm outperform major existing methods; furthermore, the extended version achieves an average of 15.8% energy saving over its prototype.     

一种混合遗传算法及收敛性分析

为了改进遗传算法的局部搜索性能，通过在遗传算法中引入局部搜索技术，提出了一种新型混合算法。应用马尔克夫链理论证明了新算法的收敛性。实际应用结果表明了该算法的有效性。     

Combining partial order reductions with on-the-fly model-checking

Partial order model-checking is an approach to reduce time and memory in model-checking concurrent programs. On-the-fly model-checking is a technique to eliminate part of the search by intersecting an automaton representing the (negation of the) checked property with the state during its generation. We prove conditions under which these two methods can be combined in order to gain reduction from both. An extension of the model-checker SPIN, which implements this combination, is studied, showing substantial reduction over traditional search, not only in the number of reachable states, but directly in the amount of memory and time used. We also describe how to apply partial-order model-checking under given fairness assumptions.