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

  1. LTSmin website (Digital version available here)
  2. Vercors project (Digital version available here)
  3. Paper on our concurrent hashtable (Digital version available here)

Additional Resources

  1. The paper