Microsoft Research Projects of Interest – Concurrency

Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.

Concurrency

Chalice is an experimental language that explores specification and verification of concurrency in programs. The Chalice language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. It 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.

Poirot is a property checker for concurrent programs that uses language-independent techniques to efficiently search space of behaviors of a program for bugs. It works by first compiling the program in a supported language to a concurrent Boogie program. Next, it uses Corral, a symbolic exploration engine, to explore concurrent behaviors of the Boogie program looking for bugs. In case a bug is not found, Poirot produces a coverage report detailing the set of program behaviors that it covered.

The goal of tools for TLA+ specifications is to develop methods and tools that will permit engineers to apply formal specification and verification to high-level designs of concurrent algorithms and systems. The idea is to make the specification force a careful and rigorous examination of what an algorithm or system should do, separate from how it should do it and let the
verification catch bugs in an algorithm or a system design even before it is implemented, where one wants to catch and correct it.

Concurrent Revisions: Programming With Versioned Memory is a project that introduces a novel programming model for concurrent and/or parallel applications. It provides programmers with a simple, yet powerful and efficient mechanism (based on mutable snapshots and deterministic conflict resolution) to execute various application tasks in parallel even if those tasks