Greg,
Thanks for your email. Our group genuinely looks forward to
this opportunity. We'll get the process started and let you
know as soon as the source code archive has been attached to a bug
against PTP.
Regards,
-Alan
Greg Watson wrote:
Alan,
That's great news! PTP welcomes contributions of new
functionality, and we look forward to working with you to enhance the
integration and capabilities of your tool.
A few notes on contributions:
2. You will need to establish the authorship of the code. If
multiple authors have worked on it, we will need the contact
information of each author
When you are ready to make the contribution, please open a bug
against PTP (component "Tools", severity "enhancement") and attach a
tar or zip file containing the source code. Make sure there are no
nested zip or tar files, and that there are no other licenses or
copyright notices in the source. Please also review the Due Diligence
process ( http://www.eclipse.org/legal/EclipseLegalProcessPoster.pdf)
so you understand the steps that will be taken.
Once this is done, I will begin the legal process for getting
the contribution approved. While it would be great to include the tool
in the 3.0, ultimately it will be determined by how long this process
takes.
Regards,
Greg
On Aug 13, 2009, at 12:00 PM, Alan Humphrey wrote:
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
_______________________________________________
ptp-dev mailing list
ptp-dev@xxxxxxxxxxx
https://dev.eclipse.org/mailman/listinfo/ptp-dev
|
