Group Members

Faculty

• Professor Ganesh Gopalakrishnan

PhD Students

• Sriram Aananthakrishnan (Make website, keep wiki, keep weeklies)

• Wei-Fan Chiang (keep weeklies)

• Peng Li (Make website, keep wiki, keep weeklies)

MS Students

• Brandon Gibson (ditto)

• Ashwin Kumar (ditto)

• Jeffrey (Geof) Sawaya (ditto)

• Tyler Sorensen

CURRENT PROJECTS

Analysis of GPU programs

Our project, GKLEE, is to check various error like race, memory coalesce, or run-time failure for GPU programs.

• Our GKLEE webpage + download site is here.
• An architecture overview is here.
• We STRONGLY recommend using our GKLEE remote execution portal or our CDE package (here).

All these links are also available on GKLEE webpage. But a detail instruction for installing GKLEE from our source code package is here.

HPC Analysis Tool Integration

OLDER PROJECTS

Dynamic Formal Verification of MPI Programs using ISP

ISP is our main MPI dynamic formal analyzer.

• Our ISP webpage provides all the info you need on ISP + the download links [1]
• The EuroPVM/MPI webpage [2] and look for our tutorial + papers
• ISP Discussion is for talk on the development of the ISP formal verification tool
• MPI-Benchmarks Analysis: Here we discuss a large collection of MPI Benchmarks employing communication non-determinism and the kind of patterns used in them.

We also have a great Eclipse GUI for ISP which named GEM. The GEM's webpage is here.

We have an old version of Java based ISP GUI. But we highly recommend using GEM to try our ISP.

Dynamic Formal Verification of thread programs using Inspect

Inspect is our project on applying optimized versions of the Dynamic Partial Order Reduction algorithm (DPOR) to Pthread/C programs. You may download Inspect from [3]

MCAPI

• A multicore hardware development project has been undertaken which provides support for MCAPI communication primitives to be implemented with direct hardware support through the instruction set. This project also provides a base for multicore hardware verification research with Sixthsense.

Eddy Murphi

The distributed version of the Murphi verification tool

MiniMPI

MiniMPI is a C# simulation of an MPI runtime using threads

Education

• Out work pertaining to Concurrency Education is at Concurrency Education

• MPI Examples -- Collection of MPI examples can be found at Tests

• Model Checking - E. M. Clarke, O. Grumberg, D. A. Peled -- Click here to download the Chapter 10 of Model Checking's book.

• Book Reading -- Click here to go to our book reading section

• MCAPI -- Observations and findings regarding MCAPI specification.

• MPI_Notes -- a summary of common MPI API calls, located here: .pdf.tex

• PPCP, (Practical Parallel and Concurrent Programming) -- here are notes on the concurrency curriculum being developed by Microsoft Research

and collaborators.

Tool Tutorials

This is a collection of tutorials for an assortment of verification and analysis tools

• Jumpshot-4 -- Here is an overview and example of using Jumpshot-4 for visualizing MPI programs

• RuleBase -- This is a 'mini-tutorial' on using the hardware verification tool RuleBase

• SixthSense -- This is a 'mini-tutorial' on using the hardware verification tool SixthSense

• CHESS Guide -- Installation and usage instructions for CHESS from Microsoft Research

• SAL -- A tutorial on using SAL tool from SRI.

• Windows Azure -- Here is a tutorial of writing cloud applications and services with Windows Azure

• Windows WCF -- Some information on creating WCF (Windows Communication Foundation) client/server applications

Group's Help Center

ALL NEW MEMBERS OF OUR GROUP MAY PLEASE READ THESE Getting Started PAGES. 

(office key, group disk space, server, svn repository.. etc.)