多分支单变量循环程序的终止性分析

对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性问题是可判定的.     

有界闭区间并上的非线性循环程序的终止性验证

利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法.利用该算法可以验证一维有界闭区间上的非线性循环程序的终止性.最后,给出计算实例演示该算法的算法步骤.     

有界闭连通域上的非线性循环终止性分析

运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法. 该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.     

一类线性循环程序的终止性判定

提出一种判定这类线性循环程序是否终止的新方法,该方法通过分析循环变量每次迭代后的状态.最后得到循环条件的满足与否只是与变量的初始值和迭代的次数有关.从而判断该循环程序是否终止.根据该方法,不但能判断这一类程序是否终止.对于不是对所有输入都终止的程序,还能够给出程序终止的输入条件.     

单分支线性约束循环程序的终止性分析

秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.     

基于迭代轨迹划分的单分支循环程序终止性分析

秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念，将单分支循环分为双向迭代循环和非双向迭代循环。其次，针对双向迭代循环程序，建立了一种划分思路，提出了三段式秩函数的概念，并证明了若该双向迭代循环存在三段式秩函数，则其是终止的。而对非双向迭代循环，引用增函数的划分思路，即利用增函数将原程序空间划分为更小的空间，并通过计算更小空间上的秩函数来证明原程序的终止性。最后，将三段式秩函数的计算问题归结为SVM分类问题，并利用工具Z3或bottema对由SVM所得的候选秩函数进行验证。     

非线性循环的终止性分析

单重线性循环程序的终止性问题已被广泛研究,而有关非线性循环终止性判定的结果甚少.利用不动点理论研究了n维单重非线性循环的终止性问题,并建立了相应的符号判定算法,同时,对几类特殊循环的终止性进行了分析,得出了相应的结论.     

循环程序的界函数合成

作为循环程序终止性分析的主流方法,当前的秩函数方法大多局限于线性或多项式秩函数的求解。针对循环程序若不存在对应的线性或多项式秩函数,现有秩函数方法就无法证明其终止性的问题,提出一个新的方法来合成给定循环程序对应的界函数。对于给定的循环程序,倘若能找到其界函数,则表明该循环程序是可终止的。首先将界函数的求解问题转化为一个线性二分类问题,并在选定界函数模板后,根据模板建立映射关系以构建训练集;然后利用所得训练集通过支持向量机（SVM）获取分类超平面进而求解得到模板系数,从而得到候选的界函数;最后利用现有的符号验证工具Redlog对该候选界函数进行验证。实验结果表明,相较于现有的秩函数方法,所提方法不仅能够应用于更多的循环程序,而且所得界函数在形式上相较于秩函数更加简化。具体表现为,对于某些没有线性秩函数的循环,该方法可以得到其对应的线性界函数;同时,对于某些只有多阶段线性秩函数的循环,该方法可以求解得到全局的线性界函数。     

非线性循环的终止性分析?

单重线性循环程序的终止性问题已被广泛研究,而有关非线性循环终止性判定的结果甚少。利用不动点理论研究了n维单重非线性循环的终止性问题,并建立了相应的符号判定算法。同时,对几类特殊循环的终止性进行了分析,得出了相应的结论。     

基于k阶秩函数的线性赋值循环程序的终止性分析

循环程序的终止性是确保循环程序完全正确的必要条件。 如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Aⁿx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于 不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。     

A measurement study of persistent forwarding loops on the Internet

In this paper, we present a measurement study of persistent forwarding loops and a flooding attack that exploits persistent forwarding loops. Persistent forwarding loops may share one or more links with forwarding paths to some hosts. An attacker can exploit persistent forwarding loops to overload the shared links and disrupt Internet connectivity to those hosts.To understand the extent of this vulnerability, we perform extensive measurements to systematically study persistent forwarding loops. We find that persistent forwarding loops do exist in the Internet. At least 35 million addresses experience persistent forwarding loops, and at least 11 million addresses can be attacked by exploiting such persistent forwarding loops. In addition, 87.4% of persistent forwarding loops involve routers in destination domains, which can be observed from various locations. This makes it possible to launch attacks from multiple vantage points. We also find that most persistent forwarding loops are just two hops long, which enables an attacker to significantly amplify traffic to them.We further investigate the possible cause of persistent forwarding loops, and find that about 50% of them are caused by neglecting to configure pull-up routes. We show that even if the misconfiguration occurs in a stub network, it may cause persistent forwarding loops involving routers in large ISPs, and can potentially be exploited by attackers to flood links in a backbone network. To the best of our knowledge, this is the first study of exploiting routing misconfigurations to launch DDoS attacks and understanding the impact of such attacks.     

Graphically structured value-function compilation

Classical work on eliciting and representing preferences over multi-attribute alternatives has attempted to recognize conditions under which value functions take on particularly simple and compact form, making their elicitation much easier. In this paper we consider preferences over discrete domains, and show that for a certain class of simple and intuitive qualitative preference statements, one can always generate compact value functions consistent with these statements. These value functions maintain the independence structure implicit in the original statements. For discrete domains, these representation theorems are much more general than previous results. However, we also show that it is not always possible to maintain this compact structure if we add explicit ordering constraints among the available outcomes.     

Voice Loops as Coordination Aids in Space Shuttle Mission Control

Voice loops, an auditory groupware technology, are essential coordination support tools for experienced practitioners in domains such as air traffic management, aircraft carrier operations and space shuttle mission control. They support synchronous communication on multiple channels among groups of people who are spatially distributed. In this paper, we suggest reasons for why the voice loop system is a successful medium for supporting coordination in space shuttle mission control based on over 130 hours of direct observation. Voice loops allow practitioners to listen in on relevant communications without disrupting their own activities or the activities of others. In addition, the voice loop system is structured around the mission control organization, and therefore directly supports the demands of the domain. By understanding how voice loops meet the particular demands of the mission control environment, insight can be gained for the design of groupware tools to support cooperative activity in other event-driven domains.     

Optimal code parallelization using unimodular transformations

Lamport's parallelization algorithm (cf. [7]) is generalized to a broader class of loops, and the complexity of the transformation process has been estimated. It is shown that every loop can be parallelized using methods similar to those in [7]; moreover, they also have the property that all their inner loops are devoid of data dependencies, and so are fully parallelizable. Unfortunately, without restricting the nature of the loop to be parallelized, the negative solution to Hilbert's tenth problem (cf. [3]) can be applied to show that the parallelizing transformations are not computable. The class of affine loops was therefore introduced. This class is more general than that considered by Lamport, and it is shown that parallelizing transformations for affine loops are computable. In general, however, the complexity estimates for finding such loops suggest that the parallelization procedure will take longer than executing the original loop sequentially. It is further shown that, if the loop satisfies an additional, nondegeneracy condition, then the loop can be efficiently transformed.

Finally, although more generally applicable, these methods are best applied to vectorization problems.     

Termination of linear programs with nonlinear constraints

Tiwari (2004) proved that the termination problem of a class of linear programs (loops with linear loop conditions and updates) over the reals is decidable through Jordan forms and eigenvector computation. Braverman (2006) proved that it is also decidable over the integers. Following their work, we consider the termination problems of three more general classes of programs which are loops with linear updates and three kinds of polynomial loop conditions, i.e., strict constraints, non-strict constraints and both strict and non-strict constraints, respectively. First, we prove that the termination problems of such loops over the integers are all undecidable. Then, for each class we provide an algorithm to decide the termination of such programs over the reals. The algorithms are complete for those programs satisfying a property, Non-Zero Minimum.     

An empirical examination of the prevalence of inhibitors to the parallelizability of open source software systems

An empirical study is presented that examines the potential to parallelize general-purpose software systems. The study is conducted on 13 open source systems comprising over 14 MLOC. Each for-loop is statically analyzed to determine if it can be parallelized or not. A for-loop that can be parallelized is termed a free-loop. Free-loops can be easily parallelized using tools such as OpenMP. For the loops that cannot be parallelized, the various inhibitors to parallelization are determined and tabulated. The data shows that the most prevalent inhibitor by far, is functions called within for-loops that have side effects. This single inhibitor poses the greatest challenge in adapting and re-engineering systems to better utilize modern multi-core architectures. This fact is somewhat contradictory to the literature, which is primarily focused on the removal of data dependencies within loops. Results of this paper also show that function calls via function pointers and virtual methods have very little impact on the for-loop parallelization process. Historical data over a 10-year period of inhibitor counts for the set of systems studied is also presented. It shows that there is little change in the potential for parallelization of loops over time.     

Learning over subconcepts: Strategies for 1‐class classification

In machine learning research and application, multiclass classification algorithms reign supreme. Their fundamental property is the reliance on the availability of data from all known categories to induce effective classifiers. Unfortunately, data from so‐called real‐world domains sometimes do not satisfy this property, and researchers use methods such as sampling to make the data more conducive for classification. However, there are scenarios in which even such explicit methods to rectify distributions fail. In such cases, 1‐class classification algorithms become the practical alternative. Unfortunately, domain complexity severely impacts their ability to produce effective classifiers. The work in this article addresses this issue and develops a strategy that allows for 1‐class classification over complex domains. In particular, we introduce the notion of learning along the lines of underlying domain concepts; an important source of complexity in domains is the presence of subconcepts, and by learning over them explicitly rather than on the entire domain as a whole, we can produce powerful 1‐class classification systems. The level of knowledge regarding these subconcepts will naturally vary by domain, and thus, we develop 3 distinct methodologies that take the amount of domain knowledge available into account. We demonstrate these over 3 real‐world domains.     

Lur''e系统镇定问题的非线性控制器设计

本语文研究了用Ｌｕｒ‘ｅ多非线性系统描述的被控对象的镇定问题,把问题的可解笥归结到特殊的多线性矩阵不等式的的可解性,非线笥状态反馈和输出反馈控制器的设计分别依赖于一个双线性和三个三线性矩阵不等式的解,给出了基于线性矩阵不等式的交替寻优算法的设计步骤。