Deadlock analysis of concurrent objects: Theory and practice