Re: [Valgrind-users] statespace analysis with Valgrind

[Stanislav B. <sta...@vs...>]

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 <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
>
>