| Alan,
Many thanks for the update. Glad to see that you're making progress.
Looking forward to hearing about your experiences and successes in the future.
Cheers,
Greg On May 11, 2009, at 9:41 PM, Alan Humphrey wrote: Hello,
This is Alan Humphrey from the School of Computing at the University of Utah. I sat in on last month's PTP status call, introduced myself, and briefly described part of what our research group will be doing this summer. We've begun adapting our tool, In-situ Partial Order (ISP), a formal verification tool for MPI programs to Eclipse via the PTP External Tools Framework.
[ 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. ]
I won't be able to join in tomorrow's PTP status call, but wanted to let you all know we've begun this effort. Initially we'd like to have basic functionality for ISP incorporated into our plug-in, including a source code analyzer which visually displays the output that ISP generates by highlighting lines in the source file. It should show both the current MPI call, and any matching point-to-point or collective operation. It will also allow the user to fire our Java GUI, ispUI, which is already written, that allows loading a log file to examine the MPI calls made during the execution. This GUI also allows one to view intraCB edges or interCB edges for one or more MPI calls.
Ultimately, our goal would be to study the Debug API and also tie into the PTP parallel debugger. The combination of these features, we hope, should be a useful combined informal and formal verification tool and a solid contribution to the Eclipse PTP.
We look forward to being in touch. 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
#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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
int MPIAPI ISP_Start(MPI_Request *request, const char *file, int line);
#define MPI_Startall(count, request) ISP_Startall(count, request, __FILE__, __LINE__)
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__)
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__)
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__)
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__)
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__)
int MPIAPI ISP_Comm_free (MPI_Comm *comm, const char *file, int line);
#define MPI_Bcast(buffer, count, datatype, root, comm) ISP_Bcast(buffer, count, datatype, root, comm, __FILE__, __LINE__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
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__)
int MPIAPI ISP_Request_free (MPI_Request *request, const char *file, int line);
#define MPI_Abort(comm, errorcode) ISP_Abort(comm, errorcode, __FILE__, __LINE__)
int MPIAPI ISP_Abort (MPI_Comm comm, int errorcode, const char *file, int line);
#define MPI_Finalize() ISP_Finalize(__FILE__, __LINE__)
int MPIAPI ISP_Finalize (const char *file, int line);
#ifdef __cplusplus
}
#endif
#endif
_______________________________________________
ptp-dev mailing list
ptp-dev@xxxxxxxxxxx
https://dev.eclipse.org/mailman/listinfo/ptp-dev
|
