A criterion for atomicity

Most proof methods for reasoning about concurrent programs are based upon theinterleaving semantics of concurrent computation: a concurrent program is executed in a stepwise fashion, with only one enabled action being executed at each step. Interleaving semantics, in effect, requires that a concurrent program be executed as a nondeterministic sequential program. This is clearly an abstraction of the way in which concurrent programs are actually executed. To ensure that this is a reasonable abstraction, interleaving semantics should only be used to reason about programs with simple actions; we call such programs atomic. In this paper, we formally characterise the class of atomic programs. We adopt the criterion that a program isatomic if it can be implemented in a wait-free, serialisable manner by a primitive program. A program isprimitive if each of its actions has at most one occurrence of a shared bit, and each shared bit is read by at most one process and written by at most one process. It follows from our results that the traditionally accepted atomicity criterion, which allows each action to have at most one occurrence of a shared variable, can be relaxed, allowing programs to have more powerful actions. For example, according to our criterion, an action can read any finite number of shared variables, provided it writes no shared variable.Work supported, in part, at the University of Texas at Austin by Office of Naval Research Contract N00014-89-J-1913, and at the University of Maryland by an award from the University of Maryland General Research Board.Work supported, in part, by Office of Naval Research Contract N00014-89-J-1913.     

An assertional criterion for atomicity

A criterion is presented to prove atomicity of read-write objects by means of ghost variables and invariants. The criterion is applied to Bloom's construction of a two-writer atomic register from two one-writer atomic registers and to the algorithm of Vitanyi and Awerbuch for the construction of a read-write object with readers and writers, based on read-write objects for one reader and one writer. In both cases, the proof comes down to the verification of a number of invariants. The hand-written proofs of these invariants have been verified with a mechanical theorem prover. Received: 10 May 2001 / 6 December 2001     

A challenge for atomicity verification

An unpublished algorithm of Haldar and Vidyasankar implements an atomic variable of an arbitrary type T for one writer and one reader by means of 4 unsafe variables of type T, three two-valued safe variables, and one three-valued regular variable. We present this algorithm, and prove its correctness by means of a refinement towards a known specification of an atomic variable. The refinement is a composition of refinement functions and a forward simulation. The correctness proof requires many nontrivial invariants. In its construction, we relied on the proof assistant PVS for the administration of invariants and proofs and the preservation of consistency.     

A two-stage information criterion for stochastic systems revisited

Two-stage information criteria for model selection are constructed by properly penalizing the maximized likelihood. A well known criterion is due to Hannan and Quinn (HQ). The applicability of HQ to multivariable, non-Gaussian, linear stochastic systems has been established by Hannan and Deistler deriving an asymptotic result for the maximized quasi-likelihood function. The objective of the paper is to provide a new, transparent and structured proof of the latter result, based on explicitly stated known techniques, under conditions only slightly stronger than those used by Hannan and Deistler. The advantage of our approach is that it naturally lends itself to the analysis of other models, such as Markov or Hidden Markov Models.     

Exploiting purity for atomicity

Multithreaded programs often exhibit erroneous behavior because of unintended interactions between concurrent threads. This paper focuses on the noninterference property of atomicity. A procedure is atomic if, for every execution, there is an equivalent serial execution in which the actions of the atomic procedure are not interleaved with actions of other threads. This key property makes atomic procedures amenable to sequential reasoning techniques, which significantly facilitates subsequent validation activities such as code inspection and testing. Several existing tools verify atomicity by using commutativity of actions to show that every execution reduces to a corresponding serial execution. However, experiments with these tools have highlighted a number of interesting procedures that, while intuitively atomic, are not reducible. In this paper, we exploit the notion of pure code blocks to verify the atomicity of such irreducible procedures. If a pure block terminates normally, then its evaluation does not change the program state and, hence, these evaluation steps can be removed from the program trace before reduction. We develop a static typed-based analysis for atomicity based on this insight, and we illustrate this analysis on a number of interesting examples that could not be verified using earlier tools based purely on reduction.     

Atomizer: A dynamic atomicity checker for multithreaded programs

Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected interactions between concurrent threads. Much previous work has focused on detecting race conditions, but the absence of race conditions does not by itself prevent undesired interactions between threads.A more fundamental noninterference property is atomicity. A method is atomic if its execution is not affected by and does not interfere with concurrently-executing threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies both formal and informal correctness arguments.This paper presents a dynamic analysis for detecting atomicity violations. This analysis combines ideas from both Lipton’s theory of reduction and earlier dynamic race detectors. Experience with a prototype checker for multithreaded Java code demonstrates that this approach is effective for detecting errors due to unintended interactions between threads. In particular, our atomicity checker detects errors that would be missed by standard race detectors. Our experimental results also indicate that the majority of methods in our benchmarks are atomic, indicating that atomicity is a standard methodology in multithreaded programming.     

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.     

A theorem on atomicity in distributed algorithms

Reasoning about a distributed algorithm is simplified if we can ignore the time needed to send and deliver messages and can instead pretend that a process sends a collection of messages as a single atomic action, with the messages delivered instantaneously as part of the action. A theorem is derived that proves the validity of such reasoning for a large class of algorithms. It generalizes and corrects a well-known folk theorem about when an operation in a multiprocess program can be considered atomic.List of notations A The set of program actions - A The algorithm under consideration - A The reduced version of algorithmA - A The action obtained by executing the operationA as an atomic action - C The set of state components - d[i] A variable of the Distance-Finding Algorithm - L An operation ofA, as in C2 - The operation obtained by adding toL the actions that deliver messages sent byL - N _p(S) The set of possible next actions of processp from states - P The correctness property - R An operation ofA, as in C2 - S The set of states - S ₀ The set of initial states - S _c The range of values of state componentc - X An action ofA, as in C2 - Usually denotes an execution ofA - The execution ofA that corresponds to an execution ofA When snow conditions are poor,Dr. L. Lamport works at Digital Equipment Corporation's Systems Research Center. As an undergraduate, he took a course in atomic physics.     

A decision procedure for detecting atomicity violations for communicating processes with locks

The problem of interest is to verify data consistency of a concurrent Java program. In particular, we present a new decision procedure for verifying that a class of data races caused by inconsistent accesses on multiple fields of an object cannot occur (so-called atomic-set serializability). Atomic-set serializability generalizes the ordinary notion of a data race (i.e., inconsistent coordination of accesses on a single memory location) to a broader class of races that involve accesses on multiple memory locations. Previous work by some of the authors presented a technique to abstract a concurrent Java program into an EML program, a modeling language based on pushdown systems and a finite set of reentrant locks. Our previous work used only a semi-decision procedure, and hence provides a definite answer only some of the time. In this paper, we rectify this shortcoming by developing a decision procedure for verifying data consistency, i.e., atomic-set serializability, of an EML program. When coupled with the previous work, it provides a decision procedure for verifying data consistency of a concurrent Java program. We implemented the decision procedure, and applied it to detect both single-location and multi-location data races in models of concurrent Java programs. Compared with the prior method based on a semi-decision procedure, not only was the decision procedure 34 times faster overall, but the semi-decision procedure timed out on about 50% of the queries, whereas the decision procedure timed out on none of the queries.     

A formal model of atomicity in asynchronous systems

Summary We propose a generalisation of occurrence graphs as a formal model of computational structure. The model is used to define the atomic occurrence of a program, to characterise interference freeness between programs, and to model error recovery in a decentralised system.     

Weak atomicity for the x86 memory consistency model

We consider the interaction of weakly atomic Software Transactional Memory (STM) providing single global lock atomicity with the x86 memory consistency model. We show that a practical design for such an STM requires that some program behaviour be disallowed, due to the strictness of the x86 memory consistency model in comparison to the language level memory models hitherto considered in weakly atomic STM designs. We present the design and construction of such an STM that disallows races between a transactional read and a non-transactional write. We also report on a practical application of this STM to elide legacy locks in x86 binaries. This allows software transactional memory to be applied without requiring software to be a priori written with awareness of transactional memory and without any restriction on source language or compiler. As an example, we show how a mainstream multiplayer game can use transactional memory with zero changes and 11% overhead over language level transactional memory, which requires over 700 annotations and severely restricts software development.     

Alternators in read/write atomicity

The alternator problem requires that in legitimate states no two neighboring processes are enabled and between two executions of a process, its neighbors execute at least once. In this paper, we present a solution for the alternator problem that has the following properties: (1) If the underlying topology is arbitrary and the program is executed in read/write atomicity then it is stabilizing fault-tolerant, i.e., starting from an arbitrary state, it recovers to states from where its specification is satisfied, (2) If the underlying topology is bipartite and the program is executed in the concurrent execution model then it provides stabilizing fault-tolerance and maximal concurrency, (3) If the underlying topology is linear or tree then the program provides both these properties, and (4) The program uses bounded state if the network size is known. To our knowledge, this is the first alternator program that achieves these properties.     

Standards and verification for fair-exchange and atomicity in e-commerce transactions

Electronic commerce can be defined as the conduct of commerce in goods and services, with the assistance of telecommunications and telecommunications-based tools. The economic growth potential of e-commerce is extraordinary—but so are the challenges that lie on the path toward success. One of the more pressing challenges is how to ensure the integrity and reliability of the transaction process: key aspects being fair-exchange and atomicity assurance.This paper delineates an extended fair-exchange standard, which includes atomicity assurance, intended for a wide audience including e-commerce designers, managers, users, and auditors. We demonstrate how such a standard prevents or mitigates important e-commerce concerns. To bridge theory with practice, we illustrate how the application of model checking can be used to verify the correctness of the implementation of e-commerce protocols to prevent the failure of such protocols when unforeseen circumstances occur.     

Causality and atomicity in distributed computations

Summary. In a distributed system, high-level actions can be modeled by nonatomic events. This paper proposes causality relations between distributed nonatomic events and provides efficient testing conditions for the relations. The relations provide a fine-grained granularity to specify causality relations between distributed nonatomic events. The set of relations between nonatomic events is complete in first-order predicate logic, using only the causality relation between atomic events. For a pair of distributed nonatomic events X and Y, the evaluation of any of the causality relations requires integer comparisons, where and , respectively, are the number of nodes on which the two nonatomic events X and Y occur. In this paper, we show that this polynomial complexity of evaluation can by simplified to a linear complexity using properties of partial orders. Specifically, we show that most relations can be evaluated in integer comparisons, some in integer comparisons, and the others in integer comparisons. During the derivation of the efficient testing conditions, we also define special system execution prefixes associated with distributed nonatomic events and examine their knowledge-theoretic significance. Received: July 1997 / Accepted: May 1998     

工作流事务原子性研究

传统的工作流管理系统事务处理能力不足,使得系统在失败时不能尽快恢复流程的执行。实现事务工作流原型系统,通过扩充建模功能,在建模阶段指定失败处理模式,当任务执行失败时,系统自动调用事务处理算法保证工作流事务的放松的原子性及数据的一致性和正确性,减少人工参与决策的工作。实验表明,引入了事务处理功能的工作流系统具有任务执行失败后快速恢复的能力。     

A note on atomicity: Boosting Test&Set to solve consensus

This short note shows how a simple extension of object types with consensus number 2 boosts them to an infinite consensus number. This extension is a simple embedding of a shared memory write within the base operation defining the corresponding type with consensus number 2. The style of this note is voluntarily informal.     

Atomicity failure and the retrenchment atomicity pattern

The issues surrounding the question of atomicity, both in the past and nowadays, are briefly reviewed, and a picture of an ACID (atomic, consistent, isolated, durable) transaction as a refinement problem is presented. An example of a simple air traffic control system is introduced, and the discrepancies that can arise when read-only operations examine the state at atomic and finegrained levels are handled by retrenchment. Non-ACID timing aspects of the ATC example are also handled by retrenchment, and the treatment is generalised to yield the Retrenchment Atomicity Pattern. The utility of the pattern is confirmed against a number of different case studies. One is the Mondex Electronic Purse, its protocol treated as a conventional atomic transaction. Another is the recovery protocol of Mondex, viewed as a compensated transaction (leading to the view that compensated transactions in general fit the pattern). A final one comprises various unruly phenomena occurring in the implementations of software transactional memory systems, which can frequently display non-ACID behaviour. In all cases the Atomicity Pattern is seen to perform well.     

A stopping criterion for active learning

Active learning (AL) is a framework that attempts to reduce the cost of annotating training material for statistical learning methods. While a lot of papers have been presented on applying AL to natural language processing tasks reporting impressive savings, little work has been done on defining a stopping criterion. In this work, we present a stopping criterion for active learning based on the way instances are selected during uncertainty-based sampling and verify its applicability in a variety of settings. The statistical learning models used in our study are support vector machines (SVMs), maximum entropy models and Bayesian logistic regression and the tasks performed are text classification, named entity recognition and shallow parsing. In addition, we present a method for multiclass mutually exclusive SVM active learning.     

A stability criterion for general systems

The direct method of Liapunov characterizes stability properties of sets in dynamical systems in terms of the existence of corresponding real-valued Liapunov functions. The traditional limitation of Liapunov functions to real values has blocked the extension of this approach to more general systems. In this paper, a stability concept analogous to classical uniform stability is defined as a relationship between a quasiorder and a uniformity on the same set, and it is shown that stability in this sense occurs if and only if there exists a Liapunov function taking values in a certain partially ordered uniform space associated with the given uniformity and called its retracted scale. A few general properties of scales and retracted scales are discussed, and the continuity of the Liapunov functions is briefly considered.