Interface-Based Specification and Verification of Concurrency Controllers

We present a modular approach to specification and verification of concurrency controllers by decoupling their behavior and interface specifications. The behavior specification of a concurrency controller defines how its shared variables change their values whereas the interface specification defines the order in which a client thread should call its methods. We show that the concurrency controllers can be designed modularly by composing their interfaces. We separate the verification of the concurrency controllers from the verification of the threads that use them. For the verification of the concurrency controllers we use infinite state verification techniques which enable us to verify controllers with parameterized constants and arbitrary number of user threads. We automatically generate Java monitors from the concurrency controller specifications which preserve the verified properties. For the thread verification we use finite state program verification tools which enable us to verify Java threads without any restrictions. We show that the user threads can be verified using stubs generated from the concurrency controller interfaces which improves the efficiency of the thread verification significantly.     

Highly dependable concurrent programming using design for verification

There has been significant progress in automated verification techniques based on model checking. However, scalable software model checking remains a challenging problem. We believe that this problem can be addressed using a design for verification approach based on design patterns that facilitate scalable automated verification. In this paper, we present a design for verification approach for highly dependable concurrent programming using a design pattern for concurrency controllers. A concurrency controller class consists of a set of guarded commands defining a synchronization policy, and a stateful interface describing the correct usage of the synchronization policy. We present an assume-guarantee style modular verification strategy which separates the verification of the controller behavior from the verification of the conformance to its interface. This allows us to execute the interface and behavior verification tasks separately using specialized verification techniques. We present a case study demonstrating the effectiveness of the presented approach.     

Heuristics for model checking Java programs

Model checking of software programs has two goals – the verification of correct software and the discovery of errors in faulty software. Some techniques for dealing with the most crucial problem in model checking, the state space explosion problem, concentrate on the first of these goals. In this paper we present an array of heuristic model checking techniques for combating the state space explosion when searching for errors. Previous work on this topic has mostly focused on property-specific heuristics closely related to particular kinds of errors. We present structural heuristics that attempt to explore the structure (branching structure, thread interdependency structure, abstraction structure) of a program in a manner intended to expose errors efficiently. Experimental results show the utility of this class of heuristics. In contrast to these very general heuristics, we also present very lightweight techniques for introducing program-specific heuristic guidance.     

The effect of uncontrolled concurrency on model checking

Correctness of concurrent software is usually checked by techniques such as peer code reviews or code walkthroughs and testing. These techniques, however, are subject to human error, and thus do not achieve an in‐depth verification of correctness. Model‐checking techniques, which can systematically identify and verify every state that a system can enter, are a powerful alternative method for verifying concurrent systems. However, the usefulness of model checking is limited because the number of states for concurrent models grows exponentially with the number of processes in the system. This is often referred to as the ‘state explosion problem.’ Some processes are a central part of the software operation and must be included in the model. However, we have found that some exponential complexity results due to uncontrolled concurrency introduced by the programmer rather than due to the intrinsic characteristics of the software being modeled. We have performed tests on multimedia synchronization to show the effect of abstraction as well as uncontrolled concurrency using the Promela/SPIN model checker. We begin with a sequential model not expected to have exponential complexity but that results in exponential complexity. In this paper, we provide alternative designs and explain how uncontrolled concurrency can be removed from the code. Copyright © 2007 John Wiley & Sons, Ltd.     

Compiler Techniques for the Superthreaded Architectures1, 2

Several useful compiler and program transformation techniques for the superthreaded architectures are presented in this paper. The superthreaded architecture adopts a thread pipelining execution model to facilitate runtime data dependence checking between threads, and to maximize thread overlap to enhance concurrency. In this paper, we present some important program transformation techniques to facilitate concurrent execution among threads, and to manage critical system resources such as the memory buffers effectively. We evaluate the effectiveness of those program transformation techniques by applying them manually on several benchmark programs, and using a trace-driven, cycle-by-cycle superthreaded processor simulator. The simulation results show that a superthreaded processor can achieve promising speedup for most of the benchmark programs.     

基于约束依赖图的并发程序模型检测工具

模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.     

On Automation in the Verification of Software Barriers: Experience Report

We present an experience report on automating the verification of the software barrier synchronization primitive. The informal specification of the primitive is: when a thread calls the software barrier function, the thread halts until all other threads call their instances of the software barrier function. A successful software barrier call ensures that each thread has finished its portion of work before the threads start exchanging the results of these portions of work. While software barriers are widely used in parallel versions of major numerical algorithms and are indispensable in scientific computing, software barrier algorithms and their implementations scarcely have been verified. We improve the state of the art in proving the correctness of the major software barrier algorithms with off-the-shelf automatic verification systems such as Jahob, VCC, Boogie, Spin and Checkfence. We verify a central barrier, a C implementation of a barrier, a static tree barrier, a combining tree barrier, a dissemination barrier, a tournament barrier, a barrier with its client and a barrier on a weak memory model. In the process, we introduce a novel theorem proving method for proving validity of formulas containing cardinalities of comprehensions and improve the capabilities of one of the verification systems. Based on our experience, we propose new challenges in the verification of software barriers.     

JAC技术实现生产者-消费者问题

JAC技术通过扩展JAVA注释实现并发，具有并发表达层次高、并发逻辑与应用逻辑分离、软件复用进一步加强等优点。论文利用JAC技术解决生产者-消费者问题，阐述了JAC技术的使用及其线程同步能力。     

Interrupt Verification via Thread Verification

Most of the research effort towards verification of concurrent software has focused on multithreaded code. On the other hand, concurrency in low-end embedded systems is predominantly based on interrupts. Low-end embedded systems are ubiquitous in safety-critical applications such as those supporting transportation and medical automation; their verification is important. Although interrupts are superficially similar to threads, there are subtle semantic differences between the two abstractions. This paper compares and contrasts threads and interrupts from the point of view of verifying the absence of race conditions. We identify a small set of extensions that permit thread verification tools to also verify interrupt-driven software, and we present examples of source-to-source transformations that turn interrupt-driven code into semantically equivalent thread-based code that can be checked by a thread verifier. Finally, we demonstrate a proof-of-concept program transformation tool that converts interrupt-driven sensor network applications into multithreaded code, and we use an existing tool to find race conditions in these applications.     

Runtime verification of concurrency-specific correctness criteria

We give an overview of correctness criteria specific to concurrent shared-memory programs and runtime verification techniques for verifying these criteria. We cover a spectrum of criteria, from ones focusing on low-level thread interference such as races to higher-level ones such as linearizability. We contrast these criteria in the context of runtime verification. We present the key ideas underlying the runtime verification techniques for these criteria and summarize the state of the art. Finally, we discuss the issue of coverage for runtime verification for concurrency and present techniques that improve the set of covered thread interleavings.     

Experimenting with software testbeds for evaluating new technologies

The evolution of a new technology depends upon a good theoretical basis for developing the technology, as well as upon its experimental validation. In order to provide for this experimentation, we have investigated the creation of a software testbed and the feasibility of using the same testbed for experimenting with a broad set of technologies. The testbed is a set of programs, data, and supporting documentation that allows researchers to test their new technology on a standard software platform. An important component of this testbed is the Unified Model of Dependability (UMD), which was used to elicit dependability requirements for the testbed software. With a collection of seeded faults and known issues of the target system, we are able to determine if a new technology is adept at uncovering defects or providing other aids proposed by its developers. In this paper, we present the Tactical Separation Assisted Flight Environment (TSAFE) testbed environment for which we modeled and evaluated dependability requirements and defined faults to be seeded for experimentation. We describe two completed experiments that we conducted on the testbed. The first experiment studies a technology that identifies architectural violations and evaluates its ability to detect the violations. The second experiment studies model checking as part of design for verification. We conclude by describing ongoing experimental work studying testing, using the same testbed. Our conclusion is that even though these three experiments are very different in terms of the studied technology, using and re-using the same testbed is beneficial and cost effective.

飞行颤振数据处理软件多线程编程的有效实现

多线程编程提高了飞行颤振数据处理软件的灵活性和易操作性，但也增加了软件编程和维护的复杂程度。针对这一矛盾，本文引进新的设计思想，提出新的多线程编程框图实现方法（Diagram method for multiple thread programming,DM/MTP），从而简化多线程的设计思路，特别适合于大型工程软件的设计。文中详细介绍了DM／MTP在模态参数识别算法NLUP中的应用。     

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads

Hardware interrupts are widely used in the world’s critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. Handling interrupts properly is an essential component of low-level system programming. Unfortunately, interrupts are also extremely hard to reason about: they dramatically alter the program control flow and complicate the invariants in low-level concurrent code (e.g., implementation of synchronization primitives). Existing formal verification techniques—including Hoare logic, typed assembly language, concurrent separation logic, and the assume-guarantee method—have consistently ignored the issues of interrupts; this severely limits the applicability and power of today’s program verification systems. In this paper we present a novel Hoare-logic-like framework for certifying low-level system programs involving both hardware interrupts and preemptive threads. We show that enabling and disabling interrupts can be formalized precisely using simple ownership-transfer semantics, and the same technique also extends to the concurrent setting. By carefully reasoning about the interaction among interrupt handlers, context switching, and synchronization libraries, we are able to—for the first time—successfully certify a preemptive thread implementation and a large number of common synchronization primitives. Our work provides a foundation for reasoning about interrupt-based kernel programs and makes an important advance toward building fully certified operating system kernels and hypervisors.     

Gauss: A Framework for Verifying Scientific Computing Software

High performance scientific computing software is of critical international importance as it supports scientific explorations and engineering. Software development in this area is highly challenging owing to the use of parallel/distributed programming methods and complex communication and synchronization libraries. There is very little use of formal methods to debug software in this area, given that the scientific computing community and the formal methods community have not traditionally worked together. The Utah Gauss project combines expertise from scientific computing and formal methods in addressing this problem. We currently focus on MPI programs which are the kind that run on over 60% of world's supercomputers. These are programs written in C / C++ / FORTRAN employing message passing concurrency supported by the Message Passing Interface (MPI) library. Large-scale MPI programs also employ shared memory threads to manage concurrency within smaller task sub-groups, capitalizing on the recent availability of small-scale (e.g. single-chip) shared memory multiprocessors; such mixed programming styles can result in additional bugs. MPI libraries themselves can be buggy as they strive to implement complex requirements employing aggressive techniques such as multi-threading. We have built a model extractor that extracts from MPI C programs a formal model consisting of communicating processes represented in Microsoft's Zing modeling language. MPI library functions are also being modeled in Zing. This allows us to run formal analysis on the models to detect bugs in the MPI programs being analyzed. Our preliminary results and future plans are described; in addition, our contribution is to expose the special needs of this area and suggest specific avenues for problem- driven advances in software model-checking applied to scientific computing software development and verification.     

JAC: declarative Java concurrency

The Java programming language has a low‐level concurrency model which is hard to use and does not blend well with inheritance. JAC is an extension of Java that introduces a higher level of concurrency, hiding threads and separating thread synchronization from application logic in a declarative fashion. The emphasis is on limiting the differences between sequential and concurrent code, thus furthering code reuse, and on avoiding inheritance anomalies. This is achieved by taking a middle road between concurrent code on the one hand and complete separation of sequential application logic from concurrency mechanisms on the other. An extensive comparison with related approaches is given for motivating our design decisions. Copyright © 2005 John Wiley & Sons, Ltd.     

多线程同步数据处理方法研究

线程处理使C#程序能够执行并发处理,以便可以同时执行多个操作。描述了线程状态,阐述了利用C#进行程序设计时线程同步数据处理的几种方式：使用监视器来同步变量的访问、使用事件来同步线程和使用Mutex同步多个对象并避免锁死,多线程同步数据处理方法能避免多线程数据处理时出现的线程同步错误．     

Parallel and distributed model checking in Eddy

Model checking of safety properties can be scaled up by pooling the CPU and memory resources of multiple computers. As compute clusters containing 100s of nodes, with each node realized using multi-core (e.g., 2) CPUs will be widespread, a model checker based on the parallel (shared memory) and distributed (message passing) paradigms will more efficiently use the hardware resources. Such a model checker can be designed by having each node employ two shared memory threads that run on the (typically) two CPUs of a node, with one thread responsible for state generation, and the other for efficient communication, including (1) performing overlapped asynchronous message passing, and (2) aggregating the states to be sent into larger chunks in order to improve communication network utilization. We present the design details of such a novel model checking architecture called Eddy. We describe the design rationale, details of how the threads interact and yield control, exchange messages, as well as detect termination. We have realized an instance of this architecture for the Murphi modeling language. Called Eddy_Murphi, we report its performance over the number of nodes as well as communication parameters such as those controlling state aggregation. Nearly linear reduction of compute time with increasing number of nodes is observed. Our thread task partition is done in such a way that it is modular, easy to port across different modeling languages, and easy to tune across a variety of platforms. Supported in part by NSF award CNS-0509379 and SRC Contract 2005-TJ-1318.     

Model checking unbounded concurrent lists

We present a model checking-based method for verifying list-based concurrent set data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification community. These data structures are unbounded in two dimensions: the list size is unbounded and an unbounded number of threads access them. Thus, their model checking requires abstraction to a model bounded in both the dimensions. We first show how the unbounded number of threads can be model checked by reduction to a finite model, while assuming a bounded number of list nodes. In particular, we leverage the CMP (CoMPositional) method which abstracts the unbounded threads by keeping one thread as is (concrete) and abstracting all the other threads to a single environment thread. Next, the method proceeds as a series of iterations where in each iteration the abstraction is model checked and, if a spurious counterexample is observed, refined. This is accomplished by the user by inspecting the returned counterexamples. If the user determines the returned counterexample to be spurious, she adds constraints to the abstraction in the form of lemmas to refine it. Upon addition, these lemmas are also verified for correctness as part of the CMP method. Thus, since these lemmas are verified as well, we show how some of the lemmas required for refinement of this abstract model can be mined automatically using an assertion mining tool, Daikon. Next, we show how the CMP method approach can be extended to the list dimension as well, to fully verify the data structures in both the dimensions. While it is possible to show correctness of these data structures for an unbounded number of threads by keeping one concrete thread and abstracting others, this is not directly possible in the list dimension as the nodes pointed to by the threads change during list traversal. Our method addresses this challenge by constructing an abstraction for which the concrete nodes, i.e., the nodes pointed to by the threads, can change as the thread pointers move with program execution. Further, our method also allows for refinement of this abstraction to prove properties of interest. We show the soundness of our method and establish its utility by model checking challenging concurrent list-based data structure examples.     

Deadlock prevention for flexible manufacturing system

Deadlock must be prevented via the shop controller during the flexible manufacturing system （FMS） performing. Various models have been tried for the analysis and design of shop controller. Petri net is suitable to describe the dynamic behavior of the discrete event system, such as concurrency, conflict and deadlock, however, the verification of the .system behavior needs structure analysis with complex theoretical proof method. Temporal logic model checking has important advantages over traditional theorem prover. It is flatly automatic and can produce possible counter-example which is particularly important in finding subtle error in complex transition systems. In this paper, a new method for the deadlock prevention based on Petri net and Temporal Logic model checking is presented. The specification in the Temporal Logic is expressed according to some result of structure analysis of the Petri net. The model checking is employed to execute the formal verification, which will conduct an exhaustive exploration of all possible behaviors. Finally, an example is presented to demonstrate how the method works.     

Deadlock p revention f or flexible manufacturing system

Deadlock must be prevented via the shop controller during the flexible manufacturing system (FMS) performing. Various models have been tried for the analysis and design of shop controller. Petri net is suitable to describe the dynamic behavior of the discrete event system , such as concurrency , conflict and deadlock , however , the verification of the system behavior needs ructure analysis with complex theoretical proof method. Temporal logic model checking has important advantages over traditional theorem prover. It is fully automatic and can produce possible unter- example which is particularly important in finding subtle error in complex transition systems. In this paper ,a new method for the deadlock prevention based on Petri net and Temporal Logic model checking is presented. The specification in the Temporal Logic is expressed according to some result of structure analysis of the Petri net . The model checking is employed to execute the formal verification ,which will conduct an exhaustive exploration of all possible behaviors. Finally ,an example is presented to demonstrate how the method works.