Verification of clvmd (LVM2's cluster locking & coordination daemon)
- old, complex codebase
- heavy use of pthread primitives (mutexes, condition variables)
- links to LVM code, with lots of system interaction that would need to be stubbed out or otherwise 'neutralised'
- talks to kernel's DLM (distributed lock manager), but this layer is modular and could be replaced
To upload designs, you'll need to enable LFS. More information