How Formal Dynamic Verification Tools Facilitate Novel Concurrency Visualizations
With the exploding scale of concurrency, presenting valu- able pieces of information collected by formal methods tools intuitively and graphically can greatly enhance concurrent system debugging. Tra- ditional MPI program debuggers present trace views of MPI program executions. Such views are redundant, often containing equivalent traces that permute independent MPI calls. In our ISP formal dynamic verier for MPI programs, we present a collection of alternate views made pos- sible by the use of formal dynamic verication. Some of ISP's views help pinpoint errors, some facilitate discerning errors by eliminating redun- dancy, while others help understand the program better by displaying concurrent even orderings that must be respected by all MPI implemen- tations, in the form of completes-before graphs. In this paper, we describe ISP's GUI capabilities in all these areas which are currently supported by a portable Java based GUI, a Microsoft Visual Studio GUI, and an Eclipse based GUI whose development is in progress.