October 5-7, 2010
Organized by IBM R&D Labs in Israel

Abstracts

Understanding Transactional Memory
João Lourenço, University of Lisbon

The new muticore architectures came to stay, and to make the most out of these architectures software developers must now dip into multi-thrading and parallel programming. But parallel programming is some orders of magnitude harder than sequential programming. The multi-threading makes the program design and coding more demanding. The exponential set of program states makes code coverage and proper program testing much harder. The non-determinism and interference among concurrent threads makes debugging a nightmare. The community needs new programming models and tools to develop highly-parallel programs.

Transactional Memory (TM) is an increasingly popular technology that may become the key to unlock the full potential of multicore processors and highly parallel programs. TM gives the same programming model to access in-memory shared data that developers are used to for accessing transactional databases. TM works by wrapping sets of memory accesses in a memory transaction, which are managed by a memory transaction monitor. Like in databases, aborting a memory transaction undoes all pending memory changes, and committing a memory transaction makes the changes undoable and visible to the other threads in the system. Software Transactional Memory is the variant of Transactional Memory which does not require neither use hardware/processor support.

STM programs are free from some classical problems in concurrent programming, such as deadlocks. STM programs may still suffer from livelocks and dataraces, and these must be diagnosed and tackled. Although being interesting as a programming model, STM dos not perform well in specific contexts, such as in cases of high-contention in accessing shared memory. Also, sometimes there is an unclear semantic, such as how to proceed when an exception is triggered, or how to execute I/O and other irreversible operations within a memory transaction.

In this tutorial, we will start with the basics of Software Transactional Memory (STM), covering both the programming model and implementation techniques. Then, we will discuss what should we study in STM programs to understand their behavior, and how this can be achieved. In our study, we will target both correction and performance issues. We will illustrate the talk with some use cases and tools that can aid in understanding the behavior of software transactional memory programs. We will conclude with some final remarks on challenges and open issues in using and understanding software transactional memory.

Challenges and Solutions in uCode Verification
Eli Singerman, Intel

The validation of embedded software in VLSI designs is becoming increasingly important with their growing prevalence and complexity. This talk will provide an overview of several methods we have developed for verification of embedded SW in industrial microprocessors. I will talk about a compositional approach to generate a formal model of the design, formal property and equivalence verification techniques, and on employing formal methods for improving traditional simulation based validation methodologies through automatic coverage and test-generation. I will conclude by briefly describing the application of these techniques to two variants of embedded SW, namely microcode and firmware for power management.

Testing and Debugging Concurrent Software – Challenges and Solutions
Shmuel Ur

It started ten years ago when a colleagues spent half a man year on debugging a single "simple" bug. The main problem was that this bug appeared very rarely and was therefore very hard to locate. This frustration led to a technology called ConTest whose aim is to make intermittent bugs more likely to appear and to be able to repeat execution that exhibit these bugs. The talk starts by presenting the difficulties of testing multi-threaded programs and showing typical timing related bugs. We then show how to find such bugs. We start by presenting the common concurrent bug patterns and how to use them. Then explain about review for concurrent bugs. Then we show how to test for them.

A few advanced topics will be presented.

Feedback-based Coverage-Directed Test Generation: An Industrial Evaluation
Charalambos Ioannides, Geoff Barrett, and Kerstin Eder

Although there are quite a few approaches to Coverage Directed test Generation aided by Machine Learning which have been applied successfully to small and medium size digital designs, it is not clear how they would scale on more elaborate industrial-level designs. This paper evaluates one of these techniques, called MicroGP, on a fully fledged industrial design. The results indicate relative success evidenced by a good level of code coverage achieved with reasonably compact tests when compared to traditional test generation approaches. However, there is scope for improvement especially with respect to the diversity of the tests evolved.

Reaching Coverage Closure in Post-Silicon Validation
Allon Adir, Amir Nahir, Avi Ziv, Charles Meissner, and John Schumann

Obtaining coverage information in post-silicon validation is a difficult task. Adding coverage monitors to the silicon is costly in terms of timing, power, and area, and thus even if feasible, is limited to a small number of coverage monitors. We propose a new method for reaching coverage closure in post-silicon validation. The method is based on executing the post-silicon exercisers on a pre-silicon acceleration platform, collecting coverage information from these runs, and harvesting important test templates based on their coverage. This method was used in the verification of IBM's POWER7 processor. It contributed to the overall high-quality verification of the processor, and specifically to the post-silicon validation and bring-up.

vlogsl: A Strategy Language for Simulation-based Verification of Hardware
Michael Katelman and Jose Meseguer

Languages such as SystemVerilog and {\it e} play an important role in contemporary hardware verification methodology. Through direct, language-level support for notions like constrained randoms, functional coverage, assertions, and so forth, they help verification engineers adopt useful paradigms. This paper demonstrates the usefulness of a new \emph{strategy-based} paradigm for hardware test generation which is not directly supported by any language we are aware of. A strategy is formed by coordinating multiple simulations toward achieving a high-level goal, such as the generation of a targeted stimulus driving the device through a specific behavior. Strategies are made possible at the language level through constructs exerting meta-level control over simulation, making simulation traces \emph{first-class} data objects that can be stored, queried, and otherwise manipulated programmatically. These ideas are embodied in a our language and tool, called vlogsl. vlogsl is a domain-specific embedded language in Haskell, providing a sophisticated set of strategy language features, including first-order \emph{symbolic} simulation and integration with an SMT solver. We motivate strategies, describe vlogsl, present several pedagogical examples using vlogsl, and finally a larger example involving an open-source I${}^2$C bus master.

Advances in Simultaneous Multithreading Testcase Generation Methods
John Ludden, Michal Rimon, Bryan Hickerson, and Allon Adir

Many modern microprocessor architectures utilize simultaneous multithreading (SMT) for increased performance. This trend is exemplified in IBM's Power series of high-end microprocessors which steadily increased the number of threads in a system in its POWER5, POWER6 and POWER7 designs. In this paper we discuss the steady increase in functional verification complexity introduced by each of these designs and the corresponding improvements to SMT verification methods that were necessary in order to cope with the growing verification challenge. We review three different verification technologies which were specifically developed to target SMT aspects of processor designs, and compare their relative advantages and drawbacks. Our focus is on the novel Thread Irritation technique – we demonstrate its effectiveness in finding high quality SMT bugs early in the verification cycle, and show how it was adopted to the post-silicon platform.

Invited Talk: Verification Failures: What to Do When Things Go Wrong
Valeria Bertacco, University of Michigan

Every integrated circuit is released with latent bugs. The damage and risk implied by an escaped bug ranges from almost imperceptible to potential tragedy; unfortunately it is impossible to discern within this range before a bug has been exposed and analyzed. While the past few decades have witnessed significant efforts to improve verification methodology for hardware systems, these efforts have been far outstripped by the massive complexity of modern digital designs, leading to product releases for which an always smaller fraction of system's states has been verified. The news of escaped bugs in large market designs and/or safety critical domains is alarming because of safety and cost implications (due to replacements, lawsuits, etc.).

This talk will describe our solutions to solve the verification challenge, such that users of future designs can be assured that their devices can operate completely free of bugs. We will attack the problem both at design-time, by presenting techniques to boost the fraction of the state space that can be verified before tape-out, and after deployment in the field, discussing novel solutions which can correct escaped bugs after a system has been shipped. Our ultimate vision for this technology is to make hardware as malleable as software.

Debugging Unrealizable Specifications with Model-Based Diagnosis
Robert Koenighofer, Georg Hofferek, and Roderick Bloem

Creating a formal specification for a design is difficult and mistakes happen frequently. Yet, aids for specification debugging are rare. In this paper, we show how model-based diagnosis can be applied to localize errors in unrealizable specifications of reactive systems. An implementation of the design is not required. Our approach identifies properties and signals that can be responsible for unrealizability. It can also be used to debug specifications which forbid desired behavior. We analyze specifications given as one set of properties as well as specifications consisting of assumptions and guarantees. For GR(1) specifications we describe how realizability and unrealizable cores can be computed quickly, using approximations. This technique is not specific to GR(1), though. Finally, we present experimental results where the error localization precision is doubled when compared to unrealizable cores.

Revisiting Synthesis of GR(1) Specifications
Uri Klein and Amir Pnueli

The last few years have seen a rising interest in the problem of synthesizing systems from temporal logic specifications. One major contributor to this is the recent work of Piterman et al., which showed how polynomial time synthesis could be achieved for a class of LTL specifications that is large enough and expressive enough to cover an extensive number of complex, real-world, applications (despite a known doubly-exponential time lower bound for general LTL formulae). That approach has already been used extensively for the synthesis of various applications and as basis for further theoretical work on synthesis.

Here, we expose a fundamental flaw in the initial processing of specifications in that paper and demonstrate how it may produce incorrect results, declaring that specifications could not be synthesized when, in fact, they could. We then identify a class of specifications for which this initial processing is sound and complete. Thus, giving an insight to the reason that this problem arises in the first place. We also show that it can be easily checked whether specifications belong to the sound and complete class by using the same synthesis techniques. Finally, we show in the cases that specifications do not fall into this category how to modify them so that their processing is, indeed, both sound and complete.

SAT-solving Based on Boundary Point Elimination
Eugene Goldberg and Panagiotis Manolios

We study the problem of building structure-aware SAT-solvers based on resolution. In this study, we use the idea of treating a resolution proof as a process of Boundary Point Elimination (BPE). We identify two problems of using SAT-algorithms with Conflict Driven Clause Learning (CDCL) for structure-aware SAT-solving. We introduce a template of resolution based SAT-solvers called BPE-SAT that is based on a few generic implications of the BPE concept. BPE-SAT can be viewed as a generalization of CDCL SAT-solvers and is meant for building new structure-aware SAT-algorithms. We give experimental results substantiating the ideas of the BPE approach. In particular, to show the importance of structural information we compare an implementation of BPE-SAT and state-of-the-art SAT-solvers on narrow CNF formulas.

Parallelizing A Symbolic Compositional Model-Checking Algorithm
Ariel Cohen, Kedar Namjoshi, Yaniv Sa'ar, Lenore Zuck, and Katya Kisyova

We describe a parallel, symbolic, model-checking algorithm, built around a compositional reasoning method. The method constructs a collection of per-process (i.e., local) invariants, which together imply a desired global safety property. The local invariant computation is a simultaneous fixpoint evaluation, which easily lends itself to parallelization. Moreover, locality of reasoning helps limit both the frequency and the amount of cross-thread synchronization, leading to good parallel performance. Experimental results show that the parallelized computation can achieve substantial speed-up, with reasonably small memory overhead.

Invited Talk: Abstraction-Guided Synthesis of Synchronization
Eran Yahav, IBM T.J. Watson Research Center

We present a novel framework for synthesizing efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually. Our framework is based on abstract interpretation and can infer synchronization for infinite state programs. Given a program, a specification, and an abstraction, we infer synchronization that avoids all (abstract) interleavings that may violate the specification, but permits as many valid interleavings as possible. In this talk, I will show application of this general idea for automatic inference of atomic sections and memory fences in programs running over relaxed memory models.

Invited Talk: Schizophrenic Perspective on Software Testing
Yossi Gil, Technion

In this talk, I will present my personal perspective on the state of the art of software testing, a perspective which is torn between being an academic interested in programming languages, and my earthly experience, working for the last two years as a programmer in the trenches with Google and IBM.

Invited Talk: Static and Dynamic Verification Challenges in Securing Web Applications
Omri Weisman, Watchfire

Organizations everywhere are challenged when it comes to writing secure web applications. Security vulnerabilities are everywhere, costing billions of dollars. In this presentation I will discuss the state of the art of static and dynamic verification technologies that are being applied to detect security vulnerabilities in web applications. I will present the key capabilities that are available today, and some of the exciting innovations that are coming soon.

An Efficient and Flexible Approach to Resolution Proof Reduction
Simone Fulvio Rollini, Roberto Bruttomesso, and Natasha Sharygina

A propositional proof of unsatisfiability is a certificate of the unsatisfiability of a Boolean formula; resolution proofs, as generated by modern SAT solvers, find application in many verification techniques where the size of the proofs considerably affects efficiency.
This paper presents a new approach to proof reduction, situated among the purely post-processing methods. The main idea is to reduce the proof size by eliminating redundancies of occurrences of pivots along the proof paths. This is achieved by matching and rewriting local contexts into simpler ones. In our approach, rewriting can be easily customised in the way local contexts are matched, in the amount of transformations to be performed, or in the different application of the rewrite rules. We provide an extensive experimental evaluation of our technique on a set of SMT benchmarks, which shows considerable reduction in the proofs size.

Variants of LTL Query Checking
Hana Chockler, Arie Gurfinkel, and Ofer Strichman

Given a model $M$ and a temporal logic formula $\q$, where \place is a placeholder, the query checking problem, as defined for the case of CTL by Chan in 2000, is to find the strongest propositional formula $f$ such that $M \models \varphi[? \leftarrow f]$. The motivation for solving this problem is, among other things, to get insight on the model.

We consider various objectives to the LTL query-checking problem, and study the question of whether there is a better solution then simply enumerating all possible formulas (modulo logical equivalence). It turns out that in most cases the answer is no, but there is one particular objective for which the answer -- in practice -- is definitely yes. The solution is based on a reduction to a Pseudo-Boolean Solving problem.

• Sharon Barner

  General Chair

• Daniel Kroening

  Program Chair

• Ian G. Harris

  Program Chair

• Efrat Maimon

  Webmaster

Springer Lecture Notes in Computer Science