[
Date Prev][
Date Next][
Thread Prev][
Thread Next][
Date Index][
Thread Index]
[
List Home]
[ptp-dev] Intent to Donate MPI Model Checker Plug-in to eclipse.org/ptp
|
Hello,
My name is Alan Humphrey from the School of Computing at the University
of
Utah. I've sat in on several PTP status calls throughout the summer
(excluding the most recent), and described part of what our research
group has been doing this
summer. We're currently finishing up adapting our tool, In-situ Partial
Order (ISP), a
formal verification tool for MPI programs to Eclipse as a plug-in. Beth
Tibbitts gave an overview of our project at this month's PTP status
call. We would like to gratefully acknowledge all the help and support
she has given us throughout this project's life-cycle!
[ To recap a bit about ISP :
The current release of ISP is for MPICH2, but has been
successfully tested with OpenMPI and MSMPI. ISP works by “hijacking”
the MPI scheduler, using the PMPI mechanism and then running all *relevant* interleavings of various possible MPI
process schedules. The list of MPI
commands that are explicitly trapped may be found within the attached
header file (isp.h)
End of Recap. ]
Our intent is to donate our plug-in to eclipse.org/ptp, that it
would be considered for inclusion in the 3.0 release of PTP. The ISP
plug-in has been written with RFRS considerations in mind and also has
extensive Eclipse-integrated help. ISP's primary purpose is to flag
deadlocks, assertion violations and resource leaks using a Partial
Order Reduction algorithm called Partial Order avoiding Elusive
interleavings (POE), which is based on exploiting MPI’s
out-of-order completion semantics. Our,PPoPP09
paper explains
ISP in detail.
A more condensed description of the POE algorithm can be found here. Please
also see our group's EuroPVM
tutorials page.
Like TAU, ISP itself is installed separately. The plug-in offers a rich
graphical front end for ISP with tools for exploring interleavings and
tracking
down bugs in MPI programs. Of particular interest is the Code
Analyzer view.
This is a unique user interface which visually displays the
output that ISP generated by highlighting
lines in the source file. It shows both the current MPI call, and any
matching point-to-point
or collective operation. It also allows the user to examine MPI calls
for a particular rank with
an easy to use Rank Locking feature.
The source code analyzer also allows examination of flagged
errors with
one click. The Examine Error button takes
the user to the suspect line
of code in the Eclipse editor. In addition, it offers
features to browse calls by rank and by interleaving as well as listing
any resource leaks found in the
source code. One click on the flagged leak in the Resource Leak
Browser also takes the user to the suspect line of code in the
Eclipse
editor. An image showing the Code Analyzer View can be viewed here.
We should be finishing up our Linux/Mac OSX version within the next
few days and will announce the update site sometime next week.
We look forward to hearing from you.
All your suggestions would meanwhile be gratefully accepted.
Alan Humphrey
University of Utah
School of Computing
http://www.cs.utah.edu/formal_verification
|
/*
* Copyright (c) 2008-2009
*
* School of Computing, University of Utah,
* Salt Lake City, UT 84112, USA
*
* and the Gauss Group
* http://www.cs.utah.edu/formal_verification
*
* See LICENSE for licensing information
*/
/*
* ISP: MPI Dynamic Verification Tool
*
* File: isp.h
* Description: Replacement mpi.h file, enabling filename and line number input
* Contact: isp-dev@xxxxxxxxxxx
*/
#ifndef _ISP_H
#define _ISP_H
#include <mpi.h>
/*
* MPIAPI is used for MSMPI
*/
#ifndef MPIAPI
#define MPIAPI
#endif
#if defined (_USRDLL) && defined (WIN32)
#define DLLAPI _declspec(dllexport)
#else
#define DLLAPI
#endif
#ifdef __cplusplus
extern "C" {
#endif
/*
* This code will be used with the C version of the actual MPI code.
*/
int ISP_Assert (const char *assertion, const char *function, const char *file, int line);
#define MPI_Init(argc, argv) ISP_Init(argc, argv, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Init (int *argc, char ***argv, const char *file, int line);
#define MPI_Send(buffer, count, datatype, dest, tag, comm) ISP_Send(buffer, count, datatype, dest, tag, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Send (void * buffer, int count, MPI_Datatype datatype, int dest,
int tag, MPI_Comm comm, const char *file, int line);
#define MPI_Rsend(buffer, count, datatype, dest, tag, comm) ISP_Rsend(buffer, count, datatype, dest, tag, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Rsend (void * buffer, int count, MPI_Datatype datatype, int dest,
int tag, MPI_Comm comm, const char *file, int line);
#define MPI_Isend(buf, count, datatype, dest, tag, comm, request) ISP_Isend(buf, count, datatype, dest, tag, comm, request, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Isend (void *buf, int count, MPI_Datatype datatype, int dest,
int tag, MPI_Comm comm, MPI_Request *request, const char *file, int line);
#define MPI_Send_init(buf, count, datatype, dest, tag, comm, request) ISP_Send_init(buf, count, datatype, dest, tag, comm, request, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Send_init (void *buf, int count, MPI_Datatype datatype, int dest,
int tag, MPI_Comm comm, MPI_Request *request, const char *file, int line);
#define MPI_Irecv(buf, count, datatype, source, tag, comm, request) ISP_Irecv(buf, count, datatype, source, tag, comm, request, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Irecv (void *buf, int count, MPI_Datatype datatype, int source,
int tag, MPI_Comm comm, MPI_Request *request, const char *file, int line);
#define MPI_Recv(buffer, count, datatype, source, tag, comm, status) ISP_Recv(buffer, count, datatype, source, tag, comm, status, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Recv (void *buffer, int count, MPI_Datatype datatype, int source,
int tag, MPI_Comm comm, MPI_Status *status, const char *file, int line);
#define MPI_Recv_init(buf, count, datatype, src, tag, comm, request) ISP_Recv_init(buf, count, datatype, src, tag, comm, request, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Recv_init (void *buf, int count, MPI_Datatype datatype, int src,
int tag, MPI_Comm comm, MPI_Request *request, const char *file, int line);
#define MPI_Probe(source, tag, comm, status) ISP_Probe (source, tag, comm, status, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Probe(int source, int tag, MPI_Comm comm, MPI_Status *status,
const char* file, int line);
#define MPI_Iprobe(source, tag, comm, flag, status) ISP_Iprobe (source, tag, comm, flag, status, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Iprobe(int source, int tag, MPI_Comm comm, int *flag,
MPI_Status *status, const char* file, int line);
#define MPI_Wait(request, status) ISP_Wait(request, status, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Wait (MPI_Request *request, MPI_Status *status, const char *file,
int line);
#define MPI_Test(request, flag, status) ISP_Test(request, flag, status, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Test (MPI_Request *request, int *flag, MPI_Status *status,
const char *file, int line);
#if 0
#define MPI_Bsend(buffer, count, datatype, dest, tag, comm) ISP_Bsend(buffer, count, datatype, dest, tag, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Bsend (void * buffer, int count, MPI_Datatype datatype, int dest,
int tag, MPI_Comm comm, const char *file, int line);
#endif
#define MPI_Ssend(buffer, count, datatype, dest, tag, comm) ISP_Ssend(buffer, count, datatype, dest, tag, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Ssend (void *buffer, int count, MPI_Datatype datatype, int dest,
int tag, MPI_Comm comm, const char *file, int line);
#define MPI_Sendrecv(sendbuf, sendcount, sendtype, dest, sendtag, recvbuf, recvcount, recvtype, source, recvtag, comm, status) ISP_Sendrecv(sendbuf, sendcount, sendtype, dest, sendtag, recvbuf, recvcount, recvtype, source, recvtag, comm, status, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Sendrecv (void * sendbuf, int sendcount, MPI_Datatype sendtype,
int dest, int sendtag, void * recvbuf, int recvcount,
MPI_Datatype recvtype, int source, int recvtag, MPI_Comm comm,
MPI_Status *status, const char *file, int line);
#define MPI_Start(request) ISP_Start(request, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Start(MPI_Request *request, const char *file, int line);
#define MPI_Startall(count, request) ISP_Startall(count, request, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Startall(int count, MPI_Request *array_of_requests, const char *file, int line);
#define MPI_Barrier(comm) ISP_Barrier(comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Barrier (MPI_Comm comm, const char *file, int line);
#define MPI_Comm_create(comm, group, comm_out) ISP_Comm_create(comm, group, comm_out, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Comm_create (MPI_Comm comm, MPI_Group group, MPI_Comm *comm_out,
const char *file, int line);
#define MPI_Comm_dup(comm, comm_out) ISP_Comm_dup(comm, comm_out, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Comm_dup (MPI_Comm comm, MPI_Comm *comm_out, const char *file, int line);
#define MPI_Comm_split(comm, color, key, comm_out) ISP_Comm_split(comm, color, key, comm_out, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Comm_split (MPI_Comm comm, int color, int key, MPI_Comm *comm_out,
const char *file, int line);
#define MPI_Comm_free(comm) ISP_Comm_free(comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Comm_free (MPI_Comm *comm, const char *file, int line);
#define MPI_Type_commit(datatype) ISP_Type_commit(datatype, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Type_commit (MPI_Datatype *datatype, const char *file, int line);
#define MPI_Type_free(datatype) ISP_Type_free(datatype, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Type_free (MPI_Datatype *datatype, const char *file, int line);
#define MPI_Bcast(buffer, count, datatype, root, comm) ISP_Bcast(buffer, count, datatype, root, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Bcast (void *buffer, int count, MPI_Datatype datatype, int root,
MPI_Comm comm, const char *file, int line);
#define MPI_Scatter(sendbuf, sendcnt, sendtype, recvbuf, recvcount, recvtype, root, comm) ISP_Scatter(sendbuf, sendcnt, sendtype, recvbuf, recvcount, recvtype, root, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Scatter (void *sendbuf, int sendcnt, MPI_Datatype sendtype,
void *recvbuf, int recvcount, MPI_Datatype recvtype,
int root, MPI_Comm comm, const char *file, int line);
#define MPI_Scatterv(sendbuf, sendcnt, displs, sendtype, recvbuf, recvcount, recvtype, root, comm) ISP_Scatterv(sendbuf, sendcnt, displs, sendtype, recvbuf, recvcount, recvtype, root, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Scatterv (void *sendbuf, int *sendcnt, int *displs, MPI_Datatype sendtype,
void *recvbuf, int recvcount, MPI_Datatype recvtype, int root, MPI_Comm comm,
const char *file, int line);
#define MPI_Gatherv(sendbuf, sendcnt, sendtype, recvbuf, recvcount, displs, recvtype, root, comm) ISP_Gatherv(sendbuf, sendcnt, sendtype, recvbuf, recvcount, displs, recvtype, root, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Gatherv (void *sendbuf, int sendcnt, MPI_Datatype sendtype,
void *recvbuf, int *recvcount, int *displs, MPI_Datatype recvtype,
int root, MPI_Comm comm, const char *file, int line);
#define MPI_Gather(sendbuf, sendcnt, sendtype, recvbuf, recvcount, recvtype, root, comm) ISP_Gather(sendbuf, sendcnt, sendtype, recvbuf, recvcount, recvtype, root, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Gather (void *sendbuf, int sendcnt, MPI_Datatype sendtype,
void *recvbuf, int recvcount, MPI_Datatype recvtype, int root,
MPI_Comm comm, const char *file, int line);
#define MPI_Allgather(sendbuf, sendcnt, sendtype, recvbuf, recvcount, recvtype, comm) ISP_Allgather(sendbuf, sendcnt, sendtype, recvbuf, recvcount, recvtype, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Allgather (void *sendbuf, int sendcnt, MPI_Datatype sendtype,
void *recvbuf, int recvcount, MPI_Datatype recvtype, MPI_Comm comm,
const char *file, int line);
#define MPI_Allgatherv(sendbuf, sendcnt, sendtype, recvbuf, recvcount, displs, recvtype, comm) ISP_Allgatherv(sendbuf, sendcnt, sendtype, recvbuf, recvcount, displs, recvtype, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Allgatherv (void *sendbuf, int sendcnt, MPI_Datatype sendtype,
void *recvbuf, int *recvcount, int *displs, MPI_Datatype recvtype,
MPI_Comm comm, const char *file, int line);
#define MPI_Alltoall(sendbuf, sendcnt, sendtype, recvbuf, recvcount, recvtype, comm) ISP_Alltoall(sendbuf, sendcnt, sendtype, recvbuf, recvcount, recvtype, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Alltoall (void *sendbuf, int sendcnt, MPI_Datatype sendtype,
void *recvbuf, int recvcount, MPI_Datatype recvtype, MPI_Comm comm,
const char *file, int line);
#define MPI_Alltoallv(sendbuf, sendcnt, sdispls, sendtype, recvbuf, recvcount, rdispls, recvtype, comm) ISP_Alltoallv(sendbuf, sendcnt, sdispls, sendtype, recvbuf, recvcount, rdispls, recvtype, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Alltoallv (void *sendbuf, int *sendcnt, int *sdispls, MPI_Datatype sendtype,
void *recvbuf, int *recvcount, int *rdispls, MPI_Datatype recvtype,
MPI_Comm comm, const char *file, int line);
#define MPI_Scan(sendbuff, recvbuff, count, datatype, op, comm) ISP_Scan(sendbuff, recvbuff, count, datatype, op, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Scan (void *sendbuff, void *recvbuff, int count, MPI_Datatype datatype,
MPI_Op op, MPI_Comm comm, const char *file, int line);
#define MPI_Reduce(sendbuff, recvbuff, count, datatype, op, root, comm) ISP_Reduce(sendbuff, recvbuff, count, datatype, op, root, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Reduce (void *sendbuff, void *recvbuff, int count,
MPI_Datatype datatype, MPI_Op op, int root, MPI_Comm comm,
const char *file, int line);
#define MPI_Reduce_scatter(sendbuff, recvbuff, recvcnt, datatype, op, comm) ISP_Reduce_scatter(sendbuff, recvbuff, recvcnt, datatype, op, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Reduce_scatter (void *sendbuff, void *recvbuff, int *recvcnt,
MPI_Datatype datatype, MPI_Op op, MPI_Comm comm, const char *file, int line);
#define MPI_Allreduce(sendbuff, recvbuff, count, datatype, op, comm) ISP_Allreduce(sendbuff, recvbuff, count, datatype, op, comm, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Allreduce (void *sendbuff, void *recvbuff, int count,
MPI_Datatype datatype, MPI_Op op, MPI_Comm comm, const char *file, int line);
#define MPI_Waitall(count, array_of_requests, array_of_statuses) ISP_Waitall(count, array_of_requests, array_of_statuses, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Waitall (int count, MPI_Request *array_of_requests,
MPI_Status *array_of_statuses, const char *file, int line);
#define MPI_Waitany(count, array_of_requests, index, status) ISP_Waitany(count, array_of_requests, index, status, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Waitany (int count, MPI_Request *array_of_requests,
int *index, MPI_Status *status, const char *file, int line);
#define MPI_Waitsome(incount, array_of_requests, outcount, array_of_indices, array_of_statuses) ISP_Waitsome(incount, array_of_requests, outcount, array_of_indices, array_of_statuses, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Waitsome (int incount, MPI_Request *array_of_requests,
int *outcount, int *array_of_indices, MPI_Status *array_of_statuses,
const char *file, int line);
#define MPI_Testany(count, array_of_requests, index, flag, array_of_statuses) ISP_Testany(count, array_of_requests, index, flag, array_of_statuses, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Testany (int count, MPI_Request *array_of_requests, int *index,
int *flag, MPI_Status *array_of_statuses, const char *file, int line);
#define MPI_Testsome(incount, array_of_requests, outcount, array_of_indices, array_of_statuses) ISP_Testsome(incount, array_of_requests, outcount, array_of_indices, array_of_statuses, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Testsome (int incount, MPI_Request *array_of_requests,
int *outcount, int *array_of_indices,MPI_Status *array_of_statuses,
const char *file, int line);
#define MPI_Testall(count, array_of_requests, flag, array_of_statuses) ISP_Testall(count, array_of_requests, flag, array_of_statuses, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Testall (int count, MPI_Request *array_of_requests, int *flag,
MPI_Status *array_of_statuses, const char *file, int line);
#define MPI_Request_free(request) ISP_Request_free(request, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Request_free (MPI_Request *request, const char *file, int line);
#define MPI_Abort(comm, errorcode) ISP_Abort(comm, errorcode, __FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Abort (MPI_Comm comm, int errorcode, const char *file, int line);
#define MPI_Finalize() ISP_Finalize(__FILE__, __LINE__)
DLLAPI int MPIAPI ISP_Finalize (const char *file, int line);
#ifdef __cplusplus
}
#endif
#endif