BEGIN:VCALENDAR
PRODID:-//Microsoft Corporation//Outlook MIMEDIR//EN
VERSION:1.0
BEGIN:VEVENT
DTSTART:20121114T001500Z
DTEND:20121114T020000Z
LOCATION:East Entrance
DESCRIPTION;ENCODING=QUOTED-PRINTABLE:ABSTRACT: Formal dynamic analysis of MPI programs is critically important since conventional testing tools for message passing programs don't cover the space of possible non-deterministic communication matches, thus may miss bugs in the unexamined execution scenarios. While modern dynamic verification techniques guarantee the coverage of non-deterministic communication matches, they do so indiscriminately, inviting exponential interleaving explosion. Though the general problem is difficult to solve, we show that a specialized dynamic analysis method can be developed for dramatically reducing the number of interleavings when looking for certain safety properties such as deadlocks. Our MAAPED (Messaging Application Analysis with Predictive Error Discovery) tool collects a single program trace and predicts deadlock presence in other (unexplored) traces of an MPI program. MAAPED hinges on initially computing the potential alternate matches for non-deterministic communication operations and then analyzes such matches which may lead to a deadlock. The results collected are encouraging.
SUMMARY:MAAPED: A Predictive Dynamic Analysis Tool for MPI Applications
PRIORITY:3
END:VEVENT
END:VCALENDAR
BEGIN:VCALENDAR
PRODID:-//Microsoft Corporation//Outlook MIMEDIR//EN
VERSION:1.0
BEGIN:VEVENT
DTSTART:20121114T001500Z
DTEND:20121114T020000Z
LOCATION:East Entrance
DESCRIPTION;ENCODING=QUOTED-PRINTABLE:ABSTRACT: Formal dynamic analysis of MPI programs is critically important since conventional testing tools for message passing programs don't cover the space of possible non-deterministic communication matches, thus may miss bugs in the unexamined execution scenarios. While modern dynamic verification techniques guarantee the coverage of non-deterministic communication matches, they do so indiscriminately, inviting exponential interleaving explosion. Though the general problem is difficult to solve, we show that a specialized dynamic analysis method can be developed for dramatically reducing the number of interleavings when looking for certain safety properties such as deadlocks. Our MAAPED (Messaging Application Analysis with Predictive Error Discovery) tool collects a single program trace and predicts deadlock presence in other (unexplored) traces of an MPI program. MAAPED hinges on initially computing the potential alternate matches for non-deterministic communication operations and then analyzes such matches which may lead to a deadlock. The results collected are encouraging.
SUMMARY:MAAPED: A Predictive Dynamic Analysis Tool for MPI Applications
PRIORITY:3
END:VEVENT
END:VCALENDAR