armiya
شنبه 10 اردیبهشت 1390, 00:38 صبح
با سلام :
من دارم روی یه مقاله کار میکنم لطفا ممکنه کسی این بخش رو تشریح کنه درست درک نمی کنم:
bugs in MPI programs arise due to many reasons,for example(i)during manual optimizations that turn blocking send/receives into their non-blocking counterparts ,(ii) in the context of using wild-card
communications (and the resulting non-determinism),and(iii) in programs that use one-side
comunication.programmers are acutely aware of the need to test parallel programs over all their
interleavings. they also know that this is impossible ,thus confining testing to interleavings that are
guessed to be adequate very often incorrectly,as it turn out.model checking has helped debug many
concurrent system by relying on an exhaustive search of all possible interleavings-albieit on a suitably
abstracted system model. for example the SPIN system which recently won ACM 's prestigious
software award has been used to verify many real-world protocols.for model checking to successful in
practies:(i)designers mut have modestly expensive techniques to create models of the protocols to be
verified.they must be able to examine a fraction of the interleavings in a concurrent system ,and be
able to claim that remaining interleavings are eqivalent and hence need not be examined,using a
suitable partial order reduction algorithm.
we have developed a tool called ISP (in-situ)partial order)which aspirs to grow into a practical MPI
model checker . IT the only other active research effort on developing a model checker for MPI
programs,the following approach is taken:(i)they model MPI primitives directly in promela(SPIN"S
modeling language)and uses SPIN for verification ;(ii)they use the C extension features of SPIN to
model advanced features such as non-blocking communication commands. while these efforts ride on
the success of SPIN (i)they incur a non -trivial amount of work to accurately model MPI primitives in
either promela or C ;(ii)an MPI program may be buggy becuse of faulty library function.(iii)accurately
modeling the C++ (usually ) code that embeds MPI primitives is tedious and error - prone; and (iv)
many MPI accurately modeling them is tedious upfront effort
من دارم روی یه مقاله کار میکنم لطفا ممکنه کسی این بخش رو تشریح کنه درست درک نمی کنم:
bugs in MPI programs arise due to many reasons,for example(i)during manual optimizations that turn blocking send/receives into their non-blocking counterparts ,(ii) in the context of using wild-card
communications (and the resulting non-determinism),and(iii) in programs that use one-side
comunication.programmers are acutely aware of the need to test parallel programs over all their
interleavings. they also know that this is impossible ,thus confining testing to interleavings that are
guessed to be adequate very often incorrectly,as it turn out.model checking has helped debug many
concurrent system by relying on an exhaustive search of all possible interleavings-albieit on a suitably
abstracted system model. for example the SPIN system which recently won ACM 's prestigious
software award has been used to verify many real-world protocols.for model checking to successful in
practies:(i)designers mut have modestly expensive techniques to create models of the protocols to be
verified.they must be able to examine a fraction of the interleavings in a concurrent system ,and be
able to claim that remaining interleavings are eqivalent and hence need not be examined,using a
suitable partial order reduction algorithm.
we have developed a tool called ISP (in-situ)partial order)which aspirs to grow into a practical MPI
model checker . IT the only other active research effort on developing a model checker for MPI
programs,the following approach is taken:(i)they model MPI primitives directly in promela(SPIN"S
modeling language)and uses SPIN for verification ;(ii)they use the C extension features of SPIN to
model advanced features such as non-blocking communication commands. while these efforts ride on
the success of SPIN (i)they incur a non -trivial amount of work to accurately model MPI primitives in
either promela or C ;(ii)an MPI program may be buggy becuse of faulty library function.(iii)accurately
modeling the C++ (usually ) code that embeds MPI primitives is tedious and error - prone; and (iv)
many MPI accurately modeling them is tedious upfront effort