Large Scale Verification of MPI Programs Using Lamport Clocks with Lazy Update

We propose a dynamic verification approach for large-scale message passing programs to locate correctness bugs caused by unforeseen nondeterministic interactions. This approach hinges on an efficient protocol to track the causality between nondeterministic message receive operations and potentially matching send operations. We show that causality tracking protocols that rely solely on logical clocks fail to capture all nuances of MPI program behavior, including the variety of ways in which nonblocking calls can complete. Our approach is hinged on formally defining the matches-before relation underlying the MPI standard, and devising lazy update logical clock based algorithms that can correctly discover all potential outcomes of nondeterministic receives in practice. can achieve the same coverage as a vector clock based algorithm while maintaining good scalability. LLCP allows us to analyze realistic MPI programs involving a thousand MPI processes, incurring only modest overheads in terms of communication bandwidth, latency, and memory consumption. © 2011 IEEE.

Microstructural analysis of non-woven fabrics using scanning electron microscopy and image processing. Part 1:Development and verification of the methods

This paper reports image analysis methods that have been developed to study the microstructural changes of non-wovens made by the hydroentanglement process. The validity of the image processing techniques has been ascertained by applying them to test images with known properties. The parameters in preprocessing of the scanning electron microscope (SEM) images used in image processing have been tested and optimized. The fibre orientation distribution is estimated using fast Fourier transform (FFT) and Hough transform (HT) methods. The results obtained using these two methods are in good agreement. The HT method is more demanding in computational time compared with the Fourier transform (FT) method. However, the advantage of the HT method is that the actual orientation of the lines can be concluded directly from the result of the transform without the need for any further computation. The distribution of the length of the straight fibre segments of the fabrics is evaluated by the HT method. The effect of curl of the fibres on the result of this evaluation is shown.