I am sorry that I oversimplified my example, but I am not going to enumerate all possible value of 32b-integer. I am aware of the state-space explosion problem. My nondeterminism comes from communication between processes and such state-space can be efficiently pruned by partial-order reduction methods for many practical examples. But I did not want to complicate the description of my problem in Valgrind. I am also interested in concrete values; therefore I am not interested in abstract interpretation or other static analytical methods.
Thank you for the reply, Stanislav Bohm On 06/04/2014 12:39 AM, Ben Stanley wrote: > This idea sounds a little bit like Polyspace, which performs static > code analysis. > > http://www.mathworks.com.au/products/polyspace/ > > Polyspace performs static analysis on the code using interval > arithmetic, and looks for domain errors on type conversions, division > by an interval containing 0, and many other things. > > I do not know of any open source equivalent for this process. > > I am concerned that it will not be feasible to perform this analysis > at run time due to the combinatorial explosion of states that you will > encounter. For instance, consider the possible number of states with > just two 32 bit integer variables. Polyspace copes with this by > lumping many states together as an interval. It can also cope with > disjoint sets. > > I am sorry that I cannot help you with how to do this in valgrind. I > hope others can contribute there. > > I do not represent the Mathworks, but I have done the training course > for their Polyspace product. > > Ben Stanley > > > On 4 June 2014 5:08:28 AM Stanislav Bohm <stanislav.b...@vsb.cz> wrote: > >> Hello, >> >> I plan to build an experimental tool and I am considering to build my >> work on Valgrind. Hence I would like to ask you for comments, if my >> idea is feasible. I plan to build a dynamic verifier of C/C++ >> programs with a non-deterministic behaviour (e.g. MPI programs). >> Generally I want to explore all possible runs of a program in a >> single run. >> >> I would like to achieve something like this. >> >> int main() >> { >> int x = nondeterministic_choice(0, 1); // set to x 0 or 1 >> if (x > 0) { >> printf("%i\n", x); >> } >> return 0; >> } >> >> When the program arrives to nondeterministic_choice, its state is >> remembered and the program continues with the first choice (x=0). >> When it terminates, the program returns to the saved position and the >> execution continues with x=1. (I am now interested only in single >> threaded programs that do not communicate with the system.) >> >> I do not want to simply use system "fork", because I am expecting a >> large number of branching and I want to understand a memory layout to >> have possibility to merge executions. >> >> As far I understand Valgrind implementation, I can implement my idea >> as Valgrind tool like this: >> >> - nondeterministic_choice is the client request. It stores the >> current state of thread (everything in struct ThreadState) and then >> it continues with the first choice of nondeterministic_choice. >> - The memory in the the following run can be monitored in a similar >> way as in memcheck. It allows to implemented a copy-on-write >> mechanism and backup changed memory. >> - When the program terminates, the thread state and changed memory >> will be restored to the point when it was saved and the another path >> is executed. >> >> I would like to ask you for any comments but I have also the >> following questions: >> - It is sufficient to backup struct ThreadState (and its members) + >> memory state to fully catch program state in a restorable form? >> - It is possible to set a callback (in Valgrind tool) for an event >> directly after program termination (return in main/exit call), but >> still have Valgrind in a fully functional form, where I can restore >> my saved thread and normally continue in computation. >> >> Thank you, >> Stanislav Bohm >> >> >> ------------------------------------------------------------------------------ >> >> >> Learn Graph Databases - Download FREE O'Reilly Book >> "Graph Databases" is the definitive new guide to graph databases and >> their applications. Written by three acclaimed leaders in the field, >> this first edition is now available. Download your free book today! >> http://p.sf.net/sfu/NeoTech >> _______________________________________________ >> Valgrind-users mailing list >> Valgrind-users@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/valgrind-users > > ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. Written by three acclaimed leaders in the field, this first edition is now available. Download your free book today! http://p.sf.net/sfu/NeoTech _______________________________________________ Valgrind-users mailing list Valgrind-users@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/valgrind-users
