You could use TLA+ to model the data structure operations and check the invariant. Checking the invariant with assert is also useful in my limited experience with concurrency.

https://lamport.azurewebsites.net/tla/tla.html