[Valgrind-users] statespace analysis with Valgrind

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

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