Back to University of Twente portal
| author: | Willem Siers |
| title: | Correct and Efficient Concurrent Hash Tables in Java |
| keywords: | |
| topics: | Algorithms and Data Structures |
| committee: |
Jaco van de Pol
, Wytse Oortwijn |
| started: | April 2016 |
| end: | July 2016 |
| type: | Bachelor Project |
Description
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?
References
- LTSmin website (Digital version available here)
- Vercors project (Digital version available here)
- Paper on our concurrent hashtable (Digital version available here)