TV on Monday, August 21st

Session 1: Experience Reports, Transactions I (08:30‑09:30)

08:30‑09:00

Robert Cook (Georgia Southern University) Thread Verification – an experience report The paper details the author’s thread verification experiences with three applications: Linux kernel code, the Red Hat Linux POSIX Thread library, and a portable PThread library, which was developed by the author for NASA, together with a HandyChecker prototype. Based on the author’s experiences, the paper concludes with a list of challenges for the verification community.

09:00‑09:30

Arndt Mühlenfeld (Graz University of Technology) Franz Wotawa (Graz University of Technology) Fault Detection in Multi-Threaded C++ Server Applications Due to increasing demands in processing power on the one hand, but the physical limit on CPU clock speed on the other hand, multi-threaded programming is becoming more important in current applications. Unfortunately, multi-threaded programs are prone to programming mistakes that result in hard to find defects, mainly race-conditions and deadlocks. The need for tools that help finding these faults is immanent, but currently available tools are either difficult to use because of the need for annotations, unable to cope with more than a few 10~kLOC, or issue too many false warnings. This paper describes experiments with the freely available tool Helgrind, results obtained by using it for debugging a server application comprising 500~kLOC. We present improvements to the runtime analysis of C++ programs that result in a dramatic reduction of false warnings.

Invited Talk (09:30‑10:30)

09:30‑10:30

Maurice Herlihy (Brown University) What Can We Prove about Transactional Memory? [ppt]

Break (10:30‑11:00)

Session 2: Abstraction Refinement, Typing I (11:00‑12:30)

11:00‑11:30	Alexander Malkis (Max-Planck Institut für Informatik) Andreas Podelski (MPI) Andrey Rybalchenko (Max-Planck Institut für Informatik) Thread-Modular Verification and Cartesian Abstraction Verification of multithreaded programs is difficult. It requires reasoning about state spaces that grow exponentially in the number of concurrent threads. Successful verification techniques based on modular composition of overapproximations of thread behaviors have been designed for this task. These techniques have been traditionally described in assume-guarantee style, which does not admit reasoning about the abstraction properties of the involved compositional argument. Flanagan and Qadeer thread-modular algorithm is a characteristic representative of such techniques. In this paper, we investigate the formalization of this algorithm in the framework of abstract interpretation. We identify the abstraction that the algorithm implements; its definition involves Cartesian products of sets. Our result provides a basis for the systematic study of similar abstractions for dealing with the state explosion problem. As a first step in this direction, we obtain polynomial-time algorithms based on Cartesian abstraction that enjoy increased precision with respect to the Flanagan-Qadeer method. We limit the design space for future polynomial-time algorithms by providing a characterization of minimal precision increase that leads to loss of polynomial-time complexity.
11:30‑12:00	Chiara Braghin (University of Lugano) Natasha Sharygina (UNISI) Modeling and Verification of Mobile Systems This paper describes an approach for modeling and verification of mobile systems. Mobile systems are multi-threaded programs that are characterized by 1) the explicit notion of locations (e.g., sites where they run), 2) the ability to create and execute (possibly infinite) threads at multiple locations (e.g., sites), and 3) the capability to withstand network failures. We give formal semantics to mobile systems as Labeled Kripke Structures (LKSs), which encapsulate the notion of location and unbounded thread creation. This notation allows for the modeling of both data and communication structures of the multi-threaded systems and, thus, outperforms the traditional process algebra approach which captures only the communication behavior. We show how mobile programs can be exhaustively analyzed by using model checking techniques. The LSKs are readily usable from within the SATABS toolset. SATABS implements the SAT-based counterexample-guided abstraction refinement framework (CEGAR for short) for ANSI-C programs, and supports verification of multi-threaded programs with unbounded thread creation. We are currently developing a front-end to SATABS that allows for languages with explicit location features, such as mobile agents. To the best of our knowledge, this is the first approach that allows modeling and verification of the full spectrum of mobile systems properties.
12:00‑12:30	Frederic Dabrowski (INRIA) Frederic Boussinot (INRIA - Ecole des mines) Cooperative threads and preemptive computations A two-level model for reactive systems programming is introduced in which threads linked to the same scheduler are run cooperatively and have the possibility to escape from the scheduler control to run preemptively. We present a type and effect system to enforce a logical separation of the memory which ensures that, when running in preemptive mode, threads do not interfere with those running in cooperative mode. Thus, the atomicity property at the basis of the cooperative model is preserved.

Lunch break (12:30‑14:00)

Session 3: Checkpointing, Transactions II (14:00‑14:30)

14:00‑14:30

Lukasz Ziarek (Purdue University) Philip Schatz (Purdue University) Suresh Jagannathan (Purdue University) Modular Checkpointing for Atomicity Transient faults that arise in large-scale software systems can often be repaired by re-executing the code in which they occur. Ascribing a meaningful semantics for safe re-execution in multi-threaded code is not obvious, however. For a thread to correctly re-execute a region of code, it must ensure that all other threads which have witnessed its unwanted effects within that region are also reverted to a meaningful earlier state. If not done properly, data inconsistencies and other undesirable behavior may result. However, automatically determining what constitutes a consistent global checkpoint is not straightforward since thread interactions are a dynamic property of the program. In this paper, we present a safe and efficient checkpointing mechanism for Concurrent ML (CML) that can be used to recover from transient faults. We introduce a new linguistic abstraction called {\em stabilizers} that permits the specification of per-thread monitors and the restoration of globally consistent checkpoints. Global states are computed through lightweight monitoring of communication events among threads (e.g. message-passing operations or updates to shared variables). Our checkpointing abstraction provides atomicity and isolation guarantees during state restoration ensuring restored global states are safe. Our experimental results on several realistic, multithreaded, server-style CML applications, including a web server and a windowing toolkit, show that the overheads to use stabilizers are small, and lead us to conclude that they are a viable mechanism for defining safe checkpoints in concurrent functional programs. Our experiments conclude with a case study illustrating how to build open nested transactions from our checkpointing mechanism.

Invited Talk (14:30‑15:30)

14:30‑15:30

Nir Shavit (Sun Microsystems) Transactional Locking

Break (15:30‑16:00)

Session 4: Invited Talk (16:00‑17:00)

16:00‑17:00

Wolfram Schulte and Bart Jacobs (Microsoft and Katholieke Universiteit Leuven) A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs. [ppt]

Open Mike (17:00‑18:00)

17:00‑18:00

Moderated 5-minute sessions open to all attendees