OSmosis Model + Debugging

[astevins]

This thread is for tracking scenarios where the model helped us to track down a bug.

For this thread to be a standalone contribution to a paper, we need to show how some existing OS bugs (preferably Linux) would have shown up in the model in a way that existing tools wouldn't have caught.

[astevins]

Resource Cleanup

After running a test, the system prints out a list of all resources left in the system. This has helped identify several bugs where resources have not been cleaned up properly.

For example:

• After running a test that starts a resource server, forgetting to shut down the server at the end of the test.
• Internal bug where the reference count of MOs was incorrect, and they were not being properly freed.

[sid-agrawal]

Here are two from the paper

• When we first imported the HighJMP scenario’s model state into Neo4j, it uncovered a bug where the PDs had independent physical pages for their code and data sections, instead of shared pages as we had intended. In this case, the RSI metric was 0.46, expressing the lesser degree of sharing.

• Similarly, when debugging the failure of HighJMP’s address space switch, the model state exposed the culprit: the PDs were not sharing the same page for their IPC buffer. The system call to switch address spaces used the IPC buffer and failed when its contents were not as expected.