A general lock-free algorithm using compare-and-swap

The compare-and-swap register (CAS) is a synchronization primitive for lock-free algorithms. Most uses of it, however, suffer from the so-called ABA problem. The simplest and most efficient solution to the ABA problem is to include a tag with the memory location such that the tag is incremented with each update of the target location. This solution, however, is theoretically unsound and has limited applicability. This paper presents a general lock-free pattern that is based on the synchronization primitive CAS without causing ABA problem or problems with wrap around. It can be used to provide lock-free functionality for any data type. Our algorithm is a CAS variation of Herlihy’s LL/SC methodology for lock-free transformation. The basis of our techniques is to poll different locations on reading and writing objects in such a way that the consistency of an object can be checked by its location instead of its tag. It consists of simple code that can be easily implemented using C-like languages. A true problem of lock-free algorithms is that they are hard to design correctly, which even holds for apparently straightforward algorithms. We therefore develop a reduction theorem that enables us to reason about the general lock-free algorithm to be designed on a higher level than the synchronization primitives. The reduction theorem is based on Lamport’s refinement mappings, and has been verified with the higher-order interactive theorem prover PVS. Using the reduction theorem, fewer invariants are required and some invariants are easier to discover and formulate without considering the internal structure of the final implementation.     

Using refinement calculus techniques to prove linearizability

Stepwise refinement is a method for systematically transforming a high-level program into an efficiently executable one. A sequence of successively refined programs can also serve as a correctness proof, which makes different mechanisms in the program explicit. We present rules for refinement of multi-threaded shared-variable concurrent programs. We apply our rules to the problem of verifying linearizability of concurrent objects, that are accessed by an unbounded number of concurrent threads. Linearizability is an established correctness criterion for concurrent objects, which states that the effect of each method execution can be considered to occur atomically at some point in time between its invocation and response. We show how linearizability can be expressed in terms of our refinement relation, and present rules for establishing this refinement relation between programs by a sequence of local transformations of method bodies. Contributions include strengthenings of previous techniques for atomicity refinement, as well as an absorption rule, which is particularly suitable for reasoning about concurrent algorithms that implement atomic operations. We illustrate the application of the refinement rules by proving linearizability of Treiber’s concurrent stack algorithm and Michael and Scott’s concurrent queue algorithm.     

Verifying Concurrent Data Structures by Simulation

We describe an approach to verifying concurrent data structures based on simulation between two Input/Output Automata (IOAs), modelling the specification and the implementation. We explain how we used this approach in mechanically verifying a simple lock-free stack implementation using forward simulation, and briefly discuss our experience in verifying three other lock-free algorithms which all required the use of backward simulation.     

A scalable lock-free stack algorithm

The literature describes two high performance concurrent stack algorithms based on combining funnels and elimination trees. Unfortunately, the funnels are linearizable but blocking, and the elimination trees are non-blocking but not linearizable. Neither is used in practice since they perform well only at exceptionally high loads. The literature also describes a simple lock-free linearizable stack algorithm that works at low loads but does not scale as the load increases. The question of designing a stack algorithm that is non-blocking, linearizable, and scales well throughout the concurrency range, has thus remained open.     

Transactional execution: toward reliable, high-performance multithreading

Although lock-based critical sections are the synchronization method of choice, they have significant performance limitations and lack certain properties, such as failure atomicity and stability. Addressing both these limitations requires considerable software overhead. Transactional lock removal can dynamically eliminate synchronization operations and achieve transparent transactional execution by treating lock-based critical sections as lock-free optimistic transactions.     

A method for detecting obfuscated calls in malicious binaries

Information about calls to the operating system (or kernel libraries) made by a binary executable may be used to determine whether the binary is malicious. Being aware of this approach, malicious programmers hide this information by making such calls without using the call instruction. For instance, the call addr instruction may be replaced by two push instructions and a ret instruction, the first push pushes the address of instruction after the ret instruction, and the second push pushes the address addr. The code may be further obfuscated by spreading the three instructions and by splitting each instruction into multiple instructions. This work presents a method to statically detect obfuscated calls in binary code. The idea is to use abstract interpretation to detect where the normal call-ret convention is violated. These violations can be detected by what is called an abstract stack graph. An abstract stack graph is a concise representation of all potential abstract stacks at every point in a program. An abstract stack is used to associate each element in the stack to the instruction that pushes the element. An algorithm for constructing the abstract stack graph is also presented. Methods for using the abstract stack graph are shown to detect eight different obfuscations. The technique is demonstrated by implementing a prototype tool called DOC (detector for obfuscated calls).     

新区入栈的区域填充扫描线算法

针对传统区域填充存在的一些欠缺，提出了一种新的区域填充扫描线算法。该算法在处理同一条扫描线上的多个填充区域时，分成向上搜索和向下搜索两种情况进行，每种情况又都可能出现多个搜索新区；在填充过程中，考虑到当前扫描线区间的左右连续性和上下相关性，只需将出现的新搜索区压入堆栈，不需要将相邻的每根扫描线都压入堆栈，从而减少了像素的重复判读和回溯区的搜索时间，避免了不必要的进栈出栈处理，提高了填充效率。     

多重中断C程序中数据竞争及原子性检测

在多重中断C程序中,中断嵌套可能会导致一些非期望的交叠执行,从而造成错误的程序执行结果。典型的问题是共享变量引起的数据竞争破坏了程序的原子性。针对此类问题,对多重中断C程序的运行时语义进行建模,根据共享变量的访问给出了一种原子性的定义,提出了相应的数据竞争及原子性检测方法,并采用函数摘要技术缩减静态分析过程中所需遍历的程序状态。最后,设计并实现了一个数据竞争及原子性检测原型工具MIDAC(multiple interruption C program data race and atomicity checker),实验结果表明,该工具能够针对一定规模的实际程序得到很好的检测效果。     

Parsing as abstract interpretation of grammar semantics

Earley's parsing algorithm is shown to be an abstract interpretation of a refinement of the derivation semantics of context-free grammars.     

改进型锁无关双端队列的设计与实现

高性能实时系统对系统性能、确定性和容错性有着更高的要求。非阻塞同步在任务同步方面满足要求,实现方法之一就是设计锁无关数据结构。介绍了设计锁无关数据结构算法的关键技术,通过对已有算法不足的分析提出了一种改进型的锁无关双端队列算法,介绍了对该算法的实验分析和实际应用。实验结果表明,该算法提高了访问双端队列的执行速度,并避免了多任务间同步引发的死锁、优先级逆转、低容错性等缺点。     

Instruction-level security analysis for information flow in stack-based assembly languages

We propose a method to analyze secure information flow in stack-based assembly languages, communicating with the external environment by means of input and output channels. The method computes for each instruction a security level for each memory variable and stack element. Instruction-level security analysis is flow-sensitive and hence is more precise than other analyses, such as standard security typing. Instruction-level security analysis is specified in the framework of abstract interpretation. We define concrete operational semantics which handles, in addition to execution aspects, the flow of information of the program. The basis of the approach is that each value is annotated by a security level and that the abstract domain is obtained from the concrete one by keeping the security levels and forgetting the actual values. Operand stack are abstracted as fixed-length stacks of security levels. An abstract state is a map from instructions to abstract machine configurations, where values are substituted by security levels. The abstract semantics consists of a set of abstract rules manipulating abstract states. The instruction-level security typing can be performed by an efficient fixpoint iteration algorithm, similar to that used by bytecode verification.     

压入区段端点的区域填充扫描线算法

本文对通常的区域填充扫描线算法进行改进，用区段端点入栈替代种子点入栈。改进后的算法不增加入栈出栈操作的次数，却免除了原算法中为获取众多象颜色值所需要的大量重复操作，对矩形区域这样减少操作的次数等于该区域中含象素的数目。     

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.     

Morris' tree traversal algorithm reconsidered

In 1968, Knuth posed the problem of designing a stack-free, tag-free, non-recursive algorithm that traversed the tree in in-order while leaving it unaltered in the end. Since then, numerous solutions have appeared in the literature. The 1979 algorithm by Morris is one of the most elegant of these solutions. The algorithm is clearly non-recursive, and appears, at first glance, to use neither a stack, nor tag fields. We present an insightful derivation of this algorithm. We also show that a stack is indeed present and ‘time-shares’ the right-link fields of the tree nodes. Our proof comes in two parts: (a) We start with a traversal algorithm that explicitly uses a stack, and show that it is computationally equivalent to another that uses a non-standard implementation of a stack; (b) We then show that the later algorithm can be transformed to Morris' algorithm using only control structure transformations.     

良结构下推系统的可覆盖性问题的下界

良结构下推系统是下推系统和良结构迁移系统的结合,该系统允许状态和栈字符是向量的形式,因而它们是无限的.状态迁移的同时允许栈进行入栈出栈的操作.它“非常接近不可判定的边缘”.利用重置0操作,提出了一个模型可覆盖性问题复杂度下界的一般性证明方法,并且证明了状态是3维向量的子集和一般性的良结构下推系统的可覆盖性问题分别是Tower难和Hyper-Ackermann难的.     

Verifying Contextual Refinement with Ownership Transfer

Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.     

Verifying atomic data types

Atomic transactions are a widely-accepted technique for organizing computation in fault-tolerant distributed systems. In most languages and systems based on transactions, atomicity is implemented through atomic objects, typed data objects that provide their own synchronization and recovery. Hence, atomicity is the key correctness condition required of a data type implementation. This paper presents a technique for verifying the correctness of implementations of atomic data types. The significant aspect of this technique is the extension of Hoare's abstraction function to map to a set of sequences of abstract operations, not just to a single abstract value. We give an example of a proof for an atomic queue implemented in the programming language Avalon/C++.     

并行程序的原子性验证算法研究

原子性保证并行程序中的多线程以正确方式交互,大多主流的编程语言都没有提供确保原子性的内部机制.为了提高测试程序原子性的效率与准确性,提出了一种自动检测并行程序中违反原子性错误的算法.基于状态转换,建立了原子性的形式化定义.在此基础上,利用线程锁设计了具体的算法模型以及实现中需注意的细节,同时给出自动修正错误的设计思路和建议.结合常用的基准数据结构,对模型和算法进行了实验,实验结果表明了该算法的正确性和有效性.     

Invariant diagrams with data refinement

Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and post-conditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. Data refinement is a technique of building correct programs working on concrete data structures as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant based programs and we apply it to the construction of the classical Deutsch–Schorr–Waite graph marking algorithm. Our results are formalized and mechanically proved in the Isabelle/HOL theorem prover.     

Stabilization-Preserving Atomicity Refinement

Program refinements from an abstract to a concrete model empower designers to reason effectively in the abstract and architects to implement effectively in the concrete. For refinements to be useful, they must not only preserve functionality properties but also dependability properties. In this paper, we focus our attention on refinements that preserve the dependability property of stabilization. Specifically, we present a stabilization-preserving refinement of atomicity from an abstract model where a process can atomically access the state of all its neighbors and update its own state, to a concrete model where a process can only atomically access the state of any one of its neighbors or atomically update its own state. Our refinement is sound and complete with respect to the computations admitted by the abstract model, and induces linear step complexity and constant synchronization delay in the computations admitted by the concrete model. It is based on a bounded-space, stabilizing dining philosophers program in the concrete model. The program is readily extended to: (a) solve stabilization-preserving semantics refinement, (b) solve the stabilizing drinking philosophers problem, and (c) allow further refinement into a message-passing model.