When you simulate your application, that's to see its behavior on a given platform. There are two things that you may want to see: its correction (whether it works – lack of deadlocks or segfaults) and its performance (throughput, achieved flops, etc). SimGrid is a great tool to assess the performance, but since you test your application in a given scenario only (or on a given set of scenarios), it may happen that your application is still bugged for rare execution paths. That's where model-checking becomes interesting.

Indeed, the used platform forces one order of events (message A arrives before message B but after message C, and so on). Model-checking removes the idea of platform altogether, and test every possible event orders. Of course, there is an exponential amount of possible event ordering. But the good news is that the vast majority of these ordering are regardless to the semantic of your application: Given for example 4 processes A,B,C and D, when A speaks with B and C with D, the fact that the events linking A and B arrive before or after the events linking C and D will have no impact on the application if (AB) and (CD) are separated enough.

All this is the PhD topic of Cristian Rosa, in Nancy. He implemented a basic model-checker in SimGrid, and also a powerful mechanism to reduce the state exploration explosion called DPOR (for Dynamic Partial Ordering Reduction). This work is integrated in the SVN version of SimGrid and will be released with SimGrid v3.5 (expected soon, when it's ready).

To use it, you need to follow the following steps:

1. You need to activate the support at configuration time in ccmake.
2. The main function looks as usual:
   • MSG_init(), to initialize the library;
   • MSG_create_environment(), simply to declare the existing host machines, the topology and powers are not used;
   • MSG_function_register() to teach SimGrid about your agent functions;
   • MSG_launch_application() to load the deployment file and MSG_main() to run everything.
3. Then, you can activate the model-checking by passing following command line argument: –cfg=model-check:1
4. For now, you can only check for invariants, ie for functions that are to be true at every steps of your program execution, using MC_assert().

Unfortunately, this feature is not exactly as well documented as it should. You can see some examples in the examples/msg/mc directory.

Long-term future work include the ability to check for liveness properties, i.e., properties linking states together using a temporal logic. They can be used to express things like "if a process requests the lock, it will eventually get it". But expressing them in C about C functions is not trivial. Also, model-checking Java or Ruby applications may work, but nobody tested it yet.

SimGrid will be present at SuperComputing 10 in New Orleans, Louisiana from Nov, 18 to Nov 21 (more details on SC'10: http://sc10.supercomputing.org/).

Please make sure to stop at the INRIA booth (Booth #2751) to say hello if you're there. We will be happy to present you the last improvements of your preferred simulation toolkit, and the visualization facility through a bunch of live demos.

There is a lot of new cool stuff in the SVN already, and we would like to release it soon. Pierre Navarro is working on this, and we hope to get it working before the end of this month. Will see how it works.

A few weeks back, Frédéric Suter emailed this list to gather ideas that we could use to print SimGrid T-shirts, but we didn't get any feedback yet. Come on people, don't try to pretend you are too serious to come up with some stupid pun about SimGrid, we don't believe you! The initial list of ideas is still available, please add your own to that list. Fred email

From November 29 to December 3, a dozen of people from the USS-SimGrid project (currently funding most of the research effort around SimGrid – thanks to the ANR for that) will gather in Frejus for a coding sprint. We already have ideas about what to do during that week, but if you have your own idea, please drop us an email!

Further issues of this newsletter are planned to spread the SimGrid Insider News. Of course, we need to be aware of your news to spread them. Please mail us about anything that you may want to get published in the next issues of the SIN.