Tens of thousands of Microsoft engineers build and test hundreds of software products several times a day. It is essential that this continuous integration scales, guarantees short feedback cycles, and functions reliably with minimal human intervention. During the past three years TSE's charter has been to shorten this cycle time. We went after this goal in two ways: Evolution via CloudBuild and Revolution via Concord. CloudBuild is a build service infrastructure, now being used by all major product groups in Microsoft, like Azure, Bing, Office, SQL except for Windows. CloudBuild addresses all aspects of a continuous integration workflow, like builds, test and code analysis, but also drops, package and symbol creation and storage. CloudBuild supports multiple build languages as long as they fulfill a coarse grained IO based contract. CloudBuild uses content based caching to run build-related tasks only when needed. Lastly, it builds on many machines in parallel. The speed ups of build and testing range from 1.2x to 10x. CloudBuild aims to rapidly onboard teams and hence has to support non-deterministic build tools and specification languages that under-declare dependencies. CloudBuild, being a reliable build service in the presence of unreliable components, currently achieves service availability better than 99%. Windows went a different path. Their past build exhaust was so massive that building Windows in the cloud and bringing the build results back for testing on corp.-net. was considered infeasible. So they decided to move to a new build language, codename Concord. By construction, Concord guarantees reliable builds, no over-build, and allows for efficient distribution. Adopting Concord has led to immense performance improvements, we have seen up to 100X speedup for Windows builds. But the path has been long and rocky, since it not only requires a substantial rewrite of existing build logic, but also all related developer and build lab processes have to change. Whether evolution or revolution is the right path forward -- the verdict is still out.

A finite-state machine (FSM) is an important abstraction for solving several problems, including regular-expression matching, tokenizing text, and Huffman decoding. FSM computations typically involve data-dependent iterations with unpredictable memory-access patterns making them difficult to parallelize. This paper describes a parallel algorithm for FSMs that breaks dependences across iterations by efficiently enumerating transitions from all possible states on each input symbol. This allows the algorithm to utilize various sources of data parallelism available on modern hardware, including vector instructions and multiple processors/cores. For instance, on benchmarks from three FSM applications: regular expressions, Huffman decoding, and HTML tokenization, the parallel algorithm achieves up to a 3x speedup over optimized sequential baselines on a single core, and linear speedups up to 21x on 8 cores.

The efficiency of a build system is an important factor for developer productivity. As a result, developer teams have been increasingly adopting new build systems that allow higher build parallelization. However, migrating the existing legacy build scripts to new build systems is a tedious and error-prone process. Unfortunately, there is insufficient support for automated migration of build scripts, making the migration more problematic.

Fine-grained data parallelism is increasingly common in mainstream processors in the form of longer vectors and on-chip GPUs. This paper develops support for exploiting such data parallelism for a class of non-numeric, non-graphic applications, which perform computations while traversing many independent, irregular data structures. While the traversal of any one irregular data structure does not give opportunity for parallelization, traversing a set of these does. However, mapping such parallelism to SIMD units is nontrivial and not addressed in prior work. We address this problem by developing an intermediate language for specifying such traversals, followed by a run-time scheduler that maps traversals to SIMD units. A key idea in our run-time scheme is converting branches to arithmetic operations, which then allows us to use SIMD hardware. In order to make our approach fast, we demonstrate several optimizations including a stream compaction method that aids with control flow in SIMD, a set of layouts that reduce memory latency, and a tiling approach that enables more effective prefetching. Using our approach, we demonstrate significant increases in single-core performance over optimized baselines for two applications.

Fine-grain data parallelism is increasingly common in mainstream processors in the form of long vectors and on-chip GPUs. This paper develops compiler and runtime support to exploit such data parallelism for non-numeric, non-graphic, irregular parallel tasks that perform simple computations while traversing many independent, irregular data structures, like trees and graphs. We vectorize the traversal of trees and graphs by treating a set of irregular data structures as a parallel control-flow graph and compiling the traversal into a domain-specific bytecodes. We produce a SIMD interpreter for these bytecodes, so each lane of a SIMD unit traverses one irregular data structure. Despite the overhead of interpretation, we demonstrate significant increases in single-core performance over optimized baselines.

Summary form only given. Based on a unique video stream analysis and combined with the Sony Smartcamera architecture, Blue Eye Video stand alone solution is able to determine how many persons are waiting in a queue, the customer behaviour when moving in a department store, airports, theatre or stadium.

Tracing just-in-time compilers (TJITs) determine frequently executed traces (hot paths and loops) in running programs and focus their optimization effort by emitting optimized machine code specialized to these traces. Prior work has established this strategy to be especially beneficial for dynamic languages such as JavaScript, where the TJIT interfaces with the interpreter and produces machine code from the JavaScript trace.

Abstract Framing in the presence of data abstraction is a challenging and important problem in the verification of object-oriented programs Leavens et al. (Formal Aspects Comput (FACS) 19:159–189, 2007). The dynamic frames approach is a promising solution to this problem. However, the approach is formalized in the context of an idealized logical framework. In particular, it is not clear the solution is suitable for use within a program verifier for a Java-like language based on verification condition generation and automated, first-order theorem proving. In this paper, we demonstrate that the dynamic frames approach can be integrated into an automatic verifier based on verification condition generation and automated theorem proving. The approach has been proven sound and has been implemented in a verifier prototype. The prototype has been used to prove correctness of several programming patterns considered challenging in related work.

Dynamic symbolic execution is a structural testing technique that systematically explores feasible paths of the program under test by running the program with different test inputs to improve code coverage. To address the space-explosion issue in path exploration, we propose a novel approach called Fitnex, a search strategy that uses state-dependent fitness values (computed through a fitness function) to guide path exploration. The fitness function measures how close an already discovered feasible path is to a particular test target (e.g., covering a not-yet-covered branch). Our new fitness-guided search strategy is integrated with other strategies that are effective for exploration problems where the fitness heuristic fails. We implemented the new approach in Pex, an automated structural testing tool developed at Microsoft Research. We evaluated our new approach by comparing it with existing search strategies. The empirical results show that our approach is effective since it consistently achieves high code coverage faster than existing search strategies.

Test coverage such as branch coverage is commonly measured to assess the sufficiency of test inputs. To reduce tedious manual efforts in generating high-covering test inputs, various automated techniques have been proposed. Some recent effective techniques include Dynamic Symbolic Execution (DSE) based on path exploration. However, these existing DSE techniques cannot generate high-covering test inputs for programs using complex regular expressions due to large exploration space; these complex regular expressions are commonly used for input validation and information extraction. To address this issue, we propose an approach, named Reggae, to reduce the exploration space of DSE in test generation. In our evaluation, we apply Reggae on various input-validation programs that use complex regular expressions. Empirical results show that Reggae helps a test-generation tool generate test inputs to achieve 79% branch coverage of validators, improved from 29% achieved without the help of Reggae.

The Task Parallel Library (TPL) is a library for .NET that makes it easy to take advantage of potential parallelism in a program. The library relies heavily on generics and delegate expressions to provide custom control structures expressing structured parallelism such as map-reduce in user programs. The library implementation is built around the notion of a task as a finite CPU-bound computation. To capture the ubiquitous apply-to-all pattern the library also introduces the novel concept of a replicable task. Tasks and replicable tasks are assigned to threads using work stealing techniques, but unlike traditional implementations based on the THE protocol, the library uses a novel data structure called a 'duplicating queue'. A surprising feature of duplicating queues is that they have sequentially inconsistent behavior on architectures with weak memory models, but capture this non-determinism in a benign way by sometimes duplicating elements. TPL ships as part of the Microsoft Parallel Extensions for the .NET framework 4.0, and forms the foundation of Parallel LINQ queries (however, note that the productized TPL library may differ in significant ways from the basic design described in this article).

An objective of unit testing is to achieve high structural coverage of the code under test. Achieving high structural overage of object-oriented code requires desirable method-call sequences that create and mutate objects. These sequences help generate target object states such as argument or receiver object states (in short as target states) of a method under test. Automatic generation of sequences for achieving target states is often challenging due to a large search space of possible sequences. On the other hand, code bases using object types (such as receiver or argument object types) include sequences that can be used to assist automatic test-generation approaches in achieving target states. In this paper, we propose a novel approach, called MSeqGen, that mines code bases and extracts sequences related to receiver or argument object types of a method under test. Our approach uses these extracted sequences to enhance two state-of-the-art test-generation approaches: random testing and dynamic symbolic execution. We conduct two evaluations to show the effectiveness of our approach. Using sequences extracted by our approach, we show that a random testing approach achieves 8.7% (with a maximum of 20.0% for one namespace) higher branch coverage and a dynamic-symbolic-execution-based approach achieves 17.4% (with a maximum of 22.5% for one namespace) higher branch coverage than without using our approach. Such an improvement is significant as the branches that are not covered by these state-of-the-art approaches are generally quite difficult to cover.

SSEAT 2008 is a workshop that focuses on the recent research approaches to automated testing using state-space exploration techniques. The goal of the workshop is to bring together researchers from both industry and academia to informally discuss the latest successes and remaining challenges in this domain. One important aspect of the workshop is to discuss techniques that were tried but did not work well in certain contexts. Another important aspect is to try to identify a set of programs that can be used for comparing various tools and techniques. There will be no proceedings, but a brief summary of the workshop will appear at the workshop web page.

Reasoning about multithreaded object-oriented programs is difficult, due to the nonlocal nature of object aliasing and data races. We propose a programming regime (or programming model ) that rules out data races, and enables local reasoning in the presence of object aliasing and concurrency. Our programming model builds on the multithreading and synchronization primitives as they are present in current mainstream programming languages. Java or C# programs developed according to our model can be annotated by means of stylized comments to make the use of the model explicit. We show that such annotated programs can be formally verified to comply with the programming model. If the annotated program verifies, the underlying Java or C# program is guaranteed to be free from data races, and it is sound to reason locally about program behavior. Verification is modular: a program is valid if all methods are valid, and validity of a method does not depend on program elements that are not visible to the method. We have implemented a verifier for programs developed according to our model in a custom build of the Spec# programming system, and we have validated our approach on a case study.

Summary form only given. Pex takes test-driven development to the next level. Pex analyzes .NET applications. From a parameterized unit test, which serves as a specification, it automatically produces traditional unit tests cases with high code coverage. Moreover, when a generated test fails, Pex can often suggest a bug fix. To do so Pex performs a systematic program analysis (similar to path bounded model-checking). It records detailed execution traces of test cases. Pex learns the program behavior from the traces, and a constraint solver produces new test cases with different behavior. The result is a minimal test suite with maximal code coverage. For information about Pex, see http://research.microsoft.com/Pex/.

Summary form only given. The Verified C project adds design by contract programming to C. The program verifier VCC accepts annotated C programs, generates logical verification conditions from them and passes them on to an automatic theorem prover to either prove the correctness of the program or find errors in it. VCC is build to verify the functional correctness of Microsoft's hypervisor code base. The first step in developing VCC so far has been the efficient encoding of a faithful memory model. The next step is the development of a programming methodology which allows for automatic verification of annotated low level concurrent code. In this talk, I will report on the design of VCC, and on first experiments in applying it.

Unit testing is a popular way to guide software development and testing. Each unit test should target a single feature, but in practice it is difficult to test features in isolation. Mock objects are a well-known technique to substitute parts of a program which are irrelevant for a particular unit test. Today mock objects are usually written manually supported by tools that generate method stubs or distill behavior from existing programs. We have developed a prototype tool based on symbolic execution of .NET code that generates mock objects including their behavior by analyzing all uses of the mock object in a given unit test. It is not required that an actual implementation of the mocked behavior exists. We are working towards an integration of our tool into Visual Studio Team System

Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a flexible methodology for object-oriented programs that protects object structures against inconsistency due to race conditions. It is based on a recent methodology for single-threaded programs where developers define aggregate object structures using an ownership system and declare invariants over them. The methodology is supported by a set of language elements and by both a sound modular static verification method and run-time checking support. The paper reports on preliminary experience with a prototype implementation.

Parameterized unit tests extend the current industry practice of using closed unit tests defined as parameterless methods. Traditional closed unit tests are re-obtained by instantiating the parameterized unit tests. We have developed the prototype tool Unit Meister, which uses symbolic execution and constraint solving to automatically compute a minimal set of inputs that exercise a parameterized unit test given certain coverage criteria. In addition, the parameterized unit tests can be used as symbolic summaries during symbolic execution, which allows our approach to scale for arbitrary abstraction levels. Unit Meister has a command-line interface, and is also integrated into Visual Studio 2005 Team System.

Parameterized unit tests extend the current industry practice of using closed unit tests defined as parameterless methods. Parameterized unit tests separate two concerns: 1) They specify the external behavior of the involved methods for all test arguments. 2) Test cases can be re-obtained as traditional closed unit tests by instantiating the parameterized unit tests. Symbolic execution and constraint solving can be used to automatically choose a minimal set of inputs that exercise a parameterized unit test with respect to possible code paths of the implementation. In addition, parameterized unit tests can be used as symbolic summaries which allows symbolic execution to scale for arbitrary abstraction levels. We have developed a prototype tool which computes test cases from parameterized unit tests. We report on its first use testing parts of the .NET base class library.

Online testing is a technique in which test derivation from a model program and test execution are combined into a single algorithm. We describe a practical online testing algorithm that is implemented in the model-based testing tool developed at Microsoft Research called Spec Explorer. Spec Explorer is being used daily by several Microsoft product groups. Model programs in Spec Explorer are written in the high level specification languages AsmL or Spec\#. We view model programs as implicit definitions of interface automata. The conformance relation between a model and an implementation under test is formalized in terms of refinement between interface automata. Testing then amounts to a game between the test tool and the implementation under test.

The Abstract State Machine Language, AsmL, is a novel executable specification language based on the theory of Abstract State Machines. AsmL is object-oriented, provides high-level mathematical data-structures, and is built around the notion of synchronous updates and finite choice. AsmL is fully integrated into the .NET framework and Microsoft development tools. In this paper, we explain the design rationale of AsmL and provide static and dynamic semantics for a kernel of the language.

This paper deals with testing of nondeterministic software systems. We assume that a model of the nondeterministic system is given by a directed graph with two kind of vertices: states and choice points. Choice points represent the nondeterministic behaviour of the implementation under test (IUT). Edges represent transitions. They have costs and probabilities. Test case generation in this setting amounts to generation of a game strategy. The two players are the testing tool (TT) and the IUT. The game explores the graph. The TT leads the IUT by selecting an edge at the state vertices. At the choice points the control goes to the IUT. A game strategy decides which edge should be taken by the TT in each state. This paper presents three novel algorithms 1) to determine an optimal strategy for the bounded reachability game, where optimality means maximizing the probability to reach any of the given final states from a given start state while at the same time minimizing the costs of traversal; 2) to determine a winning strategy for the bounded reachability game, which guarantees that given final vertices are reached, regardless how the IUT reacts; 3) to determine a fast converging edge covering strategy, which guarantees that the probability to cover all edges quickly converges to 1 if TT follows the strategy.

We give an algorithm that derives a finite state machine (FSM) from a given abstract state machine (ASM) specification. This allows us to integrate ASM specs with the existing tools for test case generation from FSMs. ASM specs are executable but have typically too many, often infinitely many states. We group ASM states into finitely many hyperstates which are the nodes of the FSM. The links of the FSM are induced by the ASM state transitions.

We provide a rigorous framework for language and platform independent design and analysis of exception handling mechanisms in modern programming languages and their implementations. To illustrate the practicality of the method we develop it for the exception handling mechanism of Java and show that its implementation on the Java Virtual Machine (JVM) Is correct. For this purpose we define precise abstract models for exception handling in Java and in the JVM and define a compilation scheme of Java to JVM code which allows us to prove that, in corresponding runs, Java and the JVM throw the same exceptions and with equivalent effect. Thus, the compilation scheme can, with reasonable confidence, be used as a standard reference for Java exception handling compilation.