Concurrency Education Links
Gauss Group
School of Computing, University of Utah, Salt Lake City, UT 84112, USA

Contents

1  Information pertaining to (EC)2 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.

3  Verification Tools We Offer

For more information on our fv tools, please go to SOFTWARE/SYSTEMS on our homepage HERE

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


This document was translated from LATEX by HEVEA.