My Experiments
From PEL Wiki
Mike Jones and Tonglaga Bao with Disk-based Model Checking [1]
I went to the thesis defense of Tonglaga Bao (Tonga). Tonga makes the case for avoiding the Operating System's paging algorithm, and manually controlling which portion of the problem is in memory. She divides the large hash-tables necessary for model-checking into portions which fit into memory, and loads each portion from disk when necessary. Since the idea of DiskRam is that the programmer should not have to worry about the physical location of storage, it looked like a good fit.
I decided to replicate Tonga's experiments on my machine. Instead of comparing different disk-based model checking algorithms, I wanted to compare Tonga's memory management to letting the Operating System swap and thrash. In order to make this comparison, I changed her Disk-based algorithm to allocate memory buffers instead of writing to files, and copy from them into the buffer instead of doing file reads. We then use the kernel parameter in Linux to limit the available memory of the machine.
It turns out that when memory is plentiful, the algorithm that uses files almost never accesses the disk, so they have nearly equivalent performance (disk is a little slower). As the amount of memory shrinks, however, the swapping algorithm begins to take much more time. In one of the experiments I did, it took 30 times longer to finish.
In order to understand this better, we are re-running the experiments on an instrumented kernel, which allows us to trace the disk traffic to understand if the main difference is disk locality, or some other difference.
Categories: Pel | Myles
