Today, I managed to forget a password but I had a Icedove (Thunderbird) process running containing the password.

Read more…

In an attempt to simplify the development around the SimGrid model-checker, we were thinking about moving the model-checker out in a different process. Another different approach would be to use a dynamic-linker isolation of the different components of the process. Here is a summary of the goals, problems and design issues surrounding these topics.

Read more…

In the previous episode, I talked about the implementation of a same-page-merging page store. On top of this, we can build same-page-merging snapshots for the SimGrid model checker.

Read more…

The first (lower) layer of the per-page snapshot mechanism is a page store: its responsibility is to store immutable shareable reference-counted memory pages independently of the snapshoting logic. Snapshot management and representation, soft-dirty tracking will be handled in higher layer.

Read more…

I looked at my options to achieve efficient/cheap snapshots of the simulated application for the Simgrid model checker using copy-on-write. Here I look at another solution to achieve this without using copy-on-write.

Read more…

The SimGrid model checker explores the graph of possible executions of a simulated distributed application in order to verify safety and liveness properties. The model checker needs to store the state of the application in each node of the execution graph in order to detect cycles. However, saving the whole state of the application at each node of the graph leads to huge memory consumption and in some cases most of the time is spent copying data in order to take the snapshots of the application. We will see how we could solve this problem, using copy-on-write.

Read more…