(published on November 4, 2010)

Welcome to the first issue of the SimGrid Insider News. The goal of this newsletter is to give to anyone interested a good overview of what's going on in the SimGrid community. It's titled it SimGrid Insider News, in the hope that everyone on this list can become an insider.

This issue is split in two main parts: the first one highlights a feature which is cool but probably not widely known while the second one will list the latest news of the community (new publications, upcoming releases, etc).

1 Cool feature highlight: Model-Checking

1.1 Why/when do I need Model-Checking?

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.

1.2 Model-Checking in SimGrid

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.

2 Community News

2.1 SimGrid presence at SuperComputing

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.

2.2 Recent publications

2.2.1 Generating platforms with Simulacrum

Generating platforms ready to use with SimGrid is a difficult task. This paper describes the Simulacrum tool, which aims at easing this.


2.2.2 Simulating MPI

SMPI is getting mature! It was in a prototypal state since ages in SimGrid, but things did greatly improve. For more details on this, check the publication recently submitted to IPDPS. The acceptance results are not known yet, but a preliminary version of the paper is already available as research report.


2.2.3 Visualizing and understanding SimGrid simulations with Triva

Understanding the results produced by SimGrid is challenging, and deducing the causes of the observed effects is even more daunting. A paper recently submitted to the TPDS journal describes how Triva can be used for this, from the data gathering process to their graphical representation. Once again, acceptance results are not known yet, but a preliminary version of the paper is already available as research report.


2.2.4 Model-Checking in SimGrid

Model-checking distributed algorithms is feasible only if the set of executions tha t the model checker explores is aggressively reduced to a subset of representative executions. This paper proposes a small set of core primitives in terms of which SimGrid's APIs can be defined and formally specifies these primitives in TLA+ . From this specification we derive theorems about the (in)dependence of invocations of the primitives, and use them in a DPOR-based verifier that runs within SimGrid.


2.3 Status of the next release

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.

3 Getting involved

3.1 Contribute a good punch line for SimGrid

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

3.2 Contribute ideas for the upcoming SimGrid coding sprint

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!

3.3 Commit (to) the SIN

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.