Arnab Sinha (Princeton University),

Title: Using Concurrency to Check Concurrency: Checking Serializability in Software Transactional Memory

 

Abstract:

Software implementations of transactional memory systems (STM) are very complex, often making tradeoffs along several axes, e.g. strong/weak isolation, direct/deferred update, object granularity, concurrency control, conflict detection etc. Ensuring the correctness of such complex concurrent software implementations is a daunting task. Attempts have been made to formally verify STMs, but these are limited in the scale of systems they can handle and generally verify only a model of the system, and not the actual system. In this paper we present an alternate attack on checking the correctness of an STM implementation by verifying the execution runs of an STM using a checker that runs in parallel with the transaction memory system. With future many-core systems predicted to have hundreds and even thousands of cores, it is reasonable to utilize some of these cores for ensuring the correctness of the rest of the system. This will be needed anyway given the increasing likelihood of dynamic errors due to particle hits (soft errors) and increasing fragility of nanoscale devices. These errors can only be detected at runtime.

 

An important correctness criterion that is the subject of verification is the serializability of transactions. While checking transaction serializability is NP-complete, practically useful subclasses such as interchange-serializability (DSR) are efficiently computable. Checking DSR reduces to checking for cycles in a transaction ordering graph which captures the access order of objects shared between transaction instances. Doing this concurrent to the main transaction execution requires minimizing the overhead of capturing object accesses, and managing the size of the graph which can be as large as the total number of dynamic transactions and object accesses. We discuss techniques for minimizing the overhead of access logging which includes time-stamping, and present techniques for on-the-fly graph compression that drastically reduce the size of the graph that needs to be maintained to be no larger than the number of threads. We have implemented concurrent serializability checking in the Rochester Software Transactional Memory (RSTM) system. We present our practical experiences with this including results for the RSTM and synthetic benchmarks. The overhead of concurrent checking is a strong function of the transaction length. For long transactions this is negligible. Thus the use of the proposed method for continuous runtime checking is acceptable. For very short transactions this can be significant. In this case we see the applicability of the proposed method for debugging.

Franjo Ivancic (NEC Labs),

Title: Challenges of Software Verification in Industry

 

Abstract:

The recent rapid increase of software in embedded systems has caused system dependability issues. This talk focuses on our effort to utilize software verification inside NEC to improve the quality of software. First, we give a brief overview of the F-Soft software verification platform. Then, we address the practical challenges we face to utilize Varvel, an internal product based on F-Soft, on industry software. The talk concludes with a number of lessons that we have learned in this effort.

Dejan Jovanovic (New York University),

Title: Polite Theories Revisited

 

Abstract:

The classic method of Nelson and Oppen for combining decision procedures requires the theories to be stably-infinite. Unfortunately, some important theories do not fall into this category (e.g. the theory of bit-vectors). To remedy this problem, previous work introduced the notion of polite theories. Polite theories can be combined with any other theory using an extension of the Nelson-Oppen approach. In this paper we revisit the notion of polite theories, fixing a subtle flaw in the original definition. We give a new combination theorem which specifies the degree to which politeness is preserved when combining polite theories. We also give conditions under which politeness is preserved when instantiating theories by identifying two sorts. These results lead to a more general variant of the theorem for combining multiple polite theories.

Swarat Chaudhuri (Penn State University),

Title: Cauchy: Language Tools for Uncertain and Approximate Computation

 

Abstract:

I will speak about Cauchy, a long-term research project aiming to build formal methods, programming abstractions, and language implementations for uncertain and approximate computation (in the present talk, I restrict myself to the program analysis aspects). As we enter an era where computation is tightly intertwined with the physical world and deployed on resource-constrained devices, more and more programs operate in uncertain environments. As the costs of computational resources become more explicit and software with "soft" correctness requirements emerge, opportunities for approximate computing are also on the rise. These trends raise several questions of interest to formal methods: How do we verify the correctness of programs in the presence of uncertainty? How do we specify "soft" correctness requirements for programs, and how do we reason with respect to them? Can we compile programs into forms that consume fewer resources but are yet approximately correct? The Cauchy project addresses all these questions and more. From results so far, it raises the possibility of a foundationally deep marriage between program verification and mathematical analysis, and opens up new applications of numerical optimization and machine learning in program analysis.

Kedar Namjoshi (Bell Labs),

Title: Parallelizing a Compositional Model Checking Method

 

Abstract:

Compositional approaches to model checking are good candidates for parallelization. Each component is analyzed largely in isolation, with limited knowledge about the internal state of the other components. This talk is about a simple and fully automatic local reasoning method, and our experience with parallelizing a BDD implementation.

 

This is joint work with Ariel Cohen (NYU/IBM Haifa), Yaniv Sa'ar (Weizmann Institute), and Lenore Zuck (UIC/NSF).

Stan Rosenberg (Stevens Institute of Technology),

Title: Our Recent Adventures with Region Logic

 

Abstract:

In this talk, we introduce region logic (RL), which formalizes a style of using ghost state in procedure specifications including frame conditions. It provides 'local reasoning' similar to separation logic yet with standard first order assertions. We focus on our recent experience with specifying and (automatically) verifying a representative implementation of the Composite design pattern, regarded as a challenge problem. We describe how to encode RL specifications in BoogiePL and we describe how and when local reasoning facilitates automated verification.

 

Joint work with Anindya Banerjee (IMDEA Software) and David Naumann (Stevens).

Michael Theobald (D.E. Shaw Research),

Title: Formal Verification Challenges of a Supercomputer-Class Machine Designed for Molecular Dynamics

 

Abstract:

In this talk, I will describe the formal verification challenges encountered in the design of Anton, a massively parallel, special-purpose machine for molecular dynamics simulations. I will review approaches that have had the most impact on the design verification of the chip, such as bug hunting, root-cause analysis, coverage closure and deadlock detection. A particular outcome of the verification effort for Anton is a method that attempts to identify hard-to-verify logic early in the design cycle, based on model checking. This approach allows early modifications of the RTL code that enhance its verifiability for both formal and simulation methods, reducing the long tail of verification time and effort.

Sela Mador-Haim (University of Pennsylvania),

Title: Specifying Relaxed Memory Models for State Exploration Tools

 

Abstract:

Modern microprocessors implement many different memory consistency models, some of which have complex semantics. Although most system architects tend to specify memory models in an axiomatic style, executable specifications are useful for memory-model-aware verification of concurrent programs. In this talk we describe a modular approach for executable specifications of memory models. We identify five different components that capture commonly occurring features of memory models and show that these components can be combined together in different configurations in order to specify many existing memory models, including the three SPARC memory models, as well as non-storeatomic models that capture the essence of the x86 and PowerPC memory models.