The first test: The dining Philosophers Problem

For a detailed description of the problem see The Dining philosophers problem on Wikipedia .

Our implementation

We implemented the model in the following way:

The forks are global variables, which can be locked, or unlocked with the VLOCK or the VUNLOCK Statements in StEAM. The philosophers are represented as a C++ class, whose task is to lock and unlock variables. The main method initializes the given number of philosophers as threads.

You can download the code as a .tar.gz file from here

You can also download the igcc compiled binary from here.

The experiments

All experiments are conducted on AMD dual-processor Opteron machine with 4GB RAM, 4GB swap and a 3 Tera bytes hard disk made available through NFS.

To show the improvements in performance by using the externalization implemented in StEAM-XXL we have run the test cases with all three methods available in StEAM.

Memory usage

This graph describes the internal memory usage for finding the deadlock. For the experiments the most blocked heuristic was used. As we see, we were able to find a deadlock in an instance for 300 philosophers. This number can be increased by setting the capacity of the cache to a smaller number, trading space for time this way.

Internal memory usage using most blocked
As we see, with the internal method it is only possible to solve instances up to 150 philosophers. With collapse compression 200 philosophers are possible. Using externalization we can find a deadlock in much larger instances.


One might think that externalizing takes time. Not so with our algorithm. As we see in the next graph, the duration to find a deadlock is nearly the same in all three cases.

Internal memory usage using most blocked

The graph shows that the time to find a deadlock is nearly the same in all three cases.

Searching speed

We present a graph, which shows us the expanded states for an instance of 150 philosophers. We choose 150 philosophers because this is the only instance solved by all the methods.

Internal memory usage using most blocked

In all three cases the expansion rate remained linear. This implies that externalizing the states to disk does not slow down the performance of the search algorithm.

Memory usage

The last graph shown here will be the usage of internal memory while expanding the states.

Internal memory usage using most blocked

In this graph we see that the memory usage for externalization is not only very low, but also remained nearly constant.


StEAM is able to find a deadlock in very large instances of the model. Also the algorithm for externalization does not slowdown the searching process, the experiments show that externalizing a software, does not mean trading time for space. If the algorithm fits well with the problem, it can be very effective.