|title:||Correct and Efficient Concurrent Hash Tables in Java|
|topics:||Algorithms and Data Structures|
Jaco van de Pol
Model checking is an automated method to verify concurrent software and systems. The high-performance model checker LTSmin built in Twente has many multi-core algorithms, which are based on a concurrent hash-table implementation. A natural question would be: Can LTSmin verify its own implementation?
Currently this seems not yet feasible. There is a trade-off between efficiency and correctness:
- LTSmin, in particular its hash table, is programmed in C with the pthread library
- Verification tools, like Vercors (another Twente product) is aiming at Java code.
The research questions for this project are the following:
(obviously this is too much, so you can still make choices):
- Is it possible to reimplement the concurrent hash table in Java in such a way that the parallel speedup is maintained?
- Can the Java implementation be annotated and verified with tools like VerCors?
- Can the current C-implementation be model-checked, maybe with LTSmin itself?
- LTSmin website (Digital version available here)
- Vercors project (Digital version available here)
- Paper on our concurrent hashtable (Digital version available here)