Mini-Project for Verification Techniques VT 10
The mini-project can be choosen to be something connected to the course
which takes 2-3 weeks to do.
A possible suggestion for mini-project is to take an interesting concurrent algorithm
or piece of software which you model and analyze using SPIN.
Here are some suggestions with links to papers:
Please go about doing the project as follows:
David Detlefs , Christine H. Flood , Alex Garthwaite , Paul Martin , Nir Shavit , Guy L. Steele, Jr., Even Better DCAS-Based Concurrent Deques, Proceedings of the 14th International Conference on Distributed Computing, p.59-73, October 04-06, 2000 describes a deque (double ended queue, which can be pushed and poped at both ends). It uses a stronger synchronization primitive for the commit action. It is not trivial how it works, since double-endedness allow much more interaction between threads than a single-direction queue.
Edya Ladan-Mozes, Nir Shavit: An optimistic approach to lock-free FIFO queues. Distributed Computing 20(5): 323-341 (2008)
This is a slightly more complicated FIFO queue, with slightly better efficiency (maybe).
Maurice Herlihy, Yossi Lev, Victor Luchangco, Nir Shavit: A Simple Optimistic Skiplist Algorithm. SIROCCO 2007: 124-138
This is an implementation of a set in the form of a skip-list. Not too simple, has not had any serious proof yet.
Danny Hendler, Yossi Lev, Mark Moir, Nir Shavit: A dynamic-sized nonblocking work stealing deque. Distributed Computing 18(3): 189-207 (2006)
A flexible implementation of a work-stealing dequeue for use in load-balancing implementations.
At the end, we will book a 2-hr slot where we show our projects to each other (and maybe to others).
- Decide on a project, and read the material.
- Book a meeting with Jonathan, and explain to him what the algorithms is about and what you will do. (do this in week 8)
- Work on your project
- Book a meeting with Jonathan when you are halfway, to discuss progress during week 9-10
- finish your project by handing in a report (a couple of pages). The deadline is March 26.