Table of Contents

• 1  Information pertaining to (EC)² Challenges
• 2  MPI Teaching Resources
• 3  Verification Tools We Offer
• 4  PADTAD 2009 paper on Concurrency Education
• 5  Hardware Design Efforts: Multicore Networks
• 6  MCC : An MCAPI Application Verifier
• 7  Resources for teaching Intel Thread Building Blocks

1  Information pertaining to (EC)² Challenges

Steve's Matrix Challenges:

• Simone Atzeni's preliminary attempt (an instance verification -- not a full proof) is HERE.
• The challenge is to turn this initial confirmation into a full proof.

Formal Semantics Challenge:

• Steve's Operational Semantics appears in his paper Model Checking Nonblocking MPI Programs. The idea would be to devise a way to formally compare his work against the TLA+ work mentioned below.
  
  
• Guodong Li has created three versions of his work. These serve to introduce the formal semantics of a subset of MPI in TLA+ (some material under review in a journal).
  1. A 25-pager including only pt-to-pt and collectives, and a summary of the rest is under submission is HERE.
     
     
  2. A 40-pager TR that elaborates on topology, process management, IO, one-sided, ... in summary form is in our TR UUCS 09-003.
     
     
  3. The full TLA PDF printout (200 pages or so) of the 150 or so MPI functions are HERE.
  
  History: Robert and Michael DeLisi did the initial 50+ functions, and a C front-end to run the semantics against small C/MPI programs (our FMICS 2007 Best Paper). Guodong did a major rewrite and did the 150+ functions (the C front-end has not been maintained).

Alur's Challenges:

Our Group's Work Involving the Microsoft Research tool CHESS is listed here. This may help you address Rajeev Alur's Challenge.

• Michael Bentley's and Carson Jones's work is reported by MSR HERE.

2  MPI Teaching Resources

Resources to teach MPI are listed here.

• Included is a report ISP Takes Steve's Midterm Exam and other goodies.
  
  
• Geof Sawaya's ongoing efforts to have ISP go through all examples from Peter Pacheco's book are listed HERE.

3  Verification Tools We Offer

We offer many tools which can be invaluable for concurrency education. For a full list of our tools, see HERE. The latest efforts are on these tools.

• Inspect thread program verifier.
• ISP MPI program verifier. A direct download link is HERE.
• Eddy Murphi parallel and distributed model checker, with new 64-bit port and termination algorithm.

4  PADTAD 2009 paper on Concurrency Education

A position paper will appear in PADTAD 2009 on concurrency education. It is an experience report from a recent class offered to UG and Grad students. It is being provided HERE.

5  Hardware Design Efforts: Multicore Networks

Ben Meakin's ongoing work is reported HERE. Several FPGA realizations of the Multicore Communications API MCAPI protocol and NOCs are reported HERE.

6  MCC : An MCAPI Application Verifier

Subodh Sharma's ongoing work on verifying MCAPI applications is reported HERE.

7  Resources for teaching Intel Thread Building Blocks

• Geof Sawaya's ongoing efforts to document the Intel TBB are listed HERE.

This document was translated from L^AT_EX by H^EV^EA.