Re: [Valgrind-users] statespace analysis with Valgrind

[Ben S. <Ben...@ex...>]

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 <sta...@vs...> 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
> Val...@li...
> https://lists.sourceforge.net/lists/listinfo/valgrind-users