Write, analyze, test, and verify shared memory as well as distributed programs.
|
CHESS is an automated tool for finding errors in multithreaded software by systematic exploration of thread schedules. It finds errors, such as data-races, deadlocks, hangs, and data-corruption induced access violations, that are extremely hard to find with current testing tools. CHESS will be shown at PDC 2008. |
|
|
The Task Parallel Library is designed to make it much easier to write managed code that can automatically use multiple processors. Using the library, you can conveniently express potential parallelism in existing sequential code, where the exposed parallel tasks will be run concurrently on all available processors. The TPL can be seen as a domain specific embedded language for expressing concurrency through the use of first-class anonymous functions (delegates) and parametric polymorphism (generics). Currently, the TPL library is part of the Parallel extensions to .NET that will ship as part of .NET 4.0. |
|
|
Singularity is a research project focused on the construction of dependable systems through innovation in the areas of systems, languages, and tools. We are building a research operating system prototype (called Singularity), extending programming languages, and developing new techniques and tools for specifying and verifying program behavior. |
|
|
Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained locking via specifications that track fractional permissions for memory locations. The research project also includes an automatic static program verifier for Chalice. |
|
