[Avrora] Questions regarding AVRora

[John Regehr]

Hi Gückel-

Although I don't have answers to most of your questions, this is great to 
see.  I hope you'll contribute some checking work back to Avrora.

I have a student who is working on model checking TinyOS applications, but 
much low-level code is abstracted away in our approach.  It would be very 
interesting to compare and contrast this approach with your assembly-level 
work at some point.

> 3)  We cannot model time due to the very high number of states 
> encountered in model checking. Hence, if we were to use the AVRora, we 
> would need to remove cycle-accuracy. How difficult do you estimate would 
> this be?

Since time is only visible to an AVR program when it reads a 
time-dependent device register, the cycle accuracy should not get in your 
way at all.

Obviously you'll need to be clever to deal with programs that perform 
interesting computations based on values that come from timer registers.

> 4)  How difficult is fetching and restoring the entire state of the 
> simulated microcontroller? The reason for this is that after each 
> instruction execution step or an interrupt, we need to store system 
> states in our state space, and restore them later from there. The AVRora 
> documentation indicates that it is based on a thoroughly object-oriented 
> design. I assume that if this is the case, fetch/restore might be 
> difficult.

I strongly doubt that this poses significant problems.

> 5)  For instruction execution, we would need to extend the simulator by 
> symbolic execution. This means that a register may hold not only values 
> 0...255 but also something such as 0n10nn00. This would indicate that 
> bits 2, 3 and 6 are nondeterministic. In your opinion, how difficult 
> would it be to adapt AVRora such that it supports such things?

I believe Avrora already includes bitwise domain representations and 
transfer functions in its stack depth estimator.  You'll need to dig into 
the code to find out more.

Also, please consider using our bitwise domain transfer functions for AVR 
instructions:

   http://www.cs.utah.edu/~regehr/papers/asplos04/

These are likely to be more correct and more precise than whatever you 
write by hand!  Bastian and I chatted about this in 2007 but I never 
followed up.  Currently our transfer functions are in C but translating to 
Java would be easy.  If you will use the results, I'll do the translation.

You should consider adding abstract domains that are more expressive than 
0/1/unknown bits.  For example, intervals and bounded-size value sets will 
give you good results for some kinds of code where the bitwise approach 
explodes.  The problem is that no domain is uniformly best: you'll need to 
support several different ones and adaptively switch between them.

John Regehr