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).
- A 25-pager including only pt-to-pt and collectives, and a summary of the rest is under submission is HERE.
- A 40-pager TR that elaborates on topology, process management, IO, one-sided, ... in summary form is in our TR UUCS 09-003.
- 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
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
- Geof Sawaya’s ongoing efforts to document the Intel TBB are listed HERE.
This document was translated from LATEX by HEVEA.