IV101 Projects -- Spring 2012

Imagine an X-shape crossroad with no priority directions. All incomming cars are therefore subjects to the give-way-to-the-right rule if necessary. Using the SPIN model checker, demonstrate that if multiple cars are at the crossroad they may end-up giving way (giving priority) to each other (deadlock).

Using model checker of your choice, analyze and verify protocol for POSIX Thread implementation of Read-Write Locks as published in book Introduction to Parallel Computing by A. Grama, A. Gupta, G. Karypis, V. Kumar.

Using model checker of your choice (preferably DiVinE), model Peterson's algorithm for mutual exclusion problem that is applied to the environment with delayed memory writes and verify that the algorithm still guarantees mutual exclusion property.