|
|
|
Software Tools - Silicon Valley
Overview
We are currently investigating various topics related to the correctness and performance of software systems, especially in the area of concurrent systems. We place a high value on producing tools and methodologies that can be used by software developers and researchers. Contributors
Martín Abadi, Andrew Birrell, Mihai Budiu, Michael Isard, Leslie Lamport, Tom Rodeheffer, Yuan Yu, Lintao Zhang Projects
This project is exploring a new concurrent programming model, Automatic Mutual Exclusion (AME). In contrast to lock-based programming, and to other programming models built over software transactional memory (STM), we arrange that all shared state is implicitly protected unless the programmer explicitly specifies otherwise. An AME program is composed from serializable atomic fragments. We include features allowing the programmer to delimit and manage the fragments to achieve appropriate program structure and performance. The resulting programming model makes it easier to write correct code than incorrect code. It favors correctness over performance for simple programs, while allowing advanced programmers the expressivity they need. The goal of DryadLINQ is to make distributed computing on large compute cluster simple enough for ordinary programmers. DryadLINQ combines two important pieces of Microsoft technology: the Dryad distributed execution engine and the .NET Language Integrated Query (LINQ). Dryad provides reliable, distributed computing on thousands of servers for large-scale data parallel applications. LINQ enables developers to write and debug their applications in a SQL-like query language, relying on the entire .NET library and using Visual Studio. DryadLINQ is a simple, powerful, and elegant programming environment for writing large-scale data parallel applications running on large PC clusters. We present a practical FPGA-based accelerator for solving Boolean Satisfiability problems (SAT). Unlike previous efforts for hardware accelerated SAT solving, our design focuses on accelerating the Boolean Constraint Propagation (BCP) part of the SAT solver, leaving the choices of heuristics such as branching order, restarting policy and learning and backtracking to software. Our novel approach uses an application-specific architecture instead of an instance-specific one to avoid time-consuming FPGA synthesis for each SAT instance. By careful pipelining and avoiding global signal wires, our design is able to achieve much higher clock frequency than that of previous work. Our co-processor can load SAT instances in milliseconds, can handle SAT instances with tens of thousands of variables and clauses using a single FPGA, and can easily be scaled-up to handle more clauses by using multiple FPGAs. Our evaluation using a cycle-accurate simulator shows that the FPGA co-processor can achieve 3.7-38.6x speed up on BCP compared with state-of-the-art software SAT solvers. Single FPGA implementation of the co-processor only consumes 7.16 watt power in the worst case, which is an order of magnitude lower than modern CPU. Probably the most difficult error to debug in a multithreaded program is a data race in which the effect of the bug depends on a subtle timing relation between threads and hence is not reproducible. The RaceTrack research project addresses the problem of detecting these bugs by instrumenting the execution of the program in order to detect suspicious access patterns to shared variables. A suspicious access pattern indicates that a data race might be possible and that the relevant code should be examined closely. The research aims to find a good balance between real races detected, false alarms generated, and the overhead of decreased execution speed and increased memory usage due to instrumentation. RaceTrack has been implemented in a version of the .NET runtime and experiments using it with large .NET programs are in progress. The TLA Tools project aims to develop methods and tools that will permit engineers to apply formal specification and verification to high-level designs of concurrent algorithms and systems. In a previous incarnation, TLA+, a complete formal language for specifying and reasoning about concurrent systems, was developed along with an associated set of tools for parsing, pretty printing, and model checking TLA+ specifications. The model checker, TLC, accepts a large subclass of TLA+ specifications including many that people write of real systems. To address some of the limitations of TLC, we are currently working on BTLC, a SAT-based symbolic model checker for TLA+. We are currently investigating possible uses of TLA at Microsoft. Former Projects
We worked with the XML Web Services team on specifying and checking their protocols using TLA. A paper was published. Critical Path This project investigates the use of the global critical path for analysis and optimization of complex, highly parallel hardware devices. We are exploring methods for automatically extracting the critical path, and for automatically using the critical path for optimizing the device power and performance. QBFsolver This project is an extension of our SAT solver work into the domain of Quantified Boolean Formulae (QBF). Prior QBF solvers often exhibit wildly unsymmetric performance: taking, for example, many orders of magnitude longer to solve the negation of a formula than to solve the original formula. We developed a new clausal representation fix this problem and implemented a prototype QBF solver. SATsolver Often a problem in software verification can be posed as a boolean formula (representing something bad) that should not be satisfiable. Observing that modern advances have produced quite capable SAT solvers, in the SATsolver project we aimed to apply this technology to the domain of software verification. We wrote a SAT solver in C# using all of the modern techniques in addition to new techniques that we developed specifically for software verification problems. This solver has been incorporated as a core component for further software verification research at Microsoft. Selected Publications
|
