In this talk I will discuss automata models for the specification and (automated) analysis of the basic mechanism for synchronizing threads in Java.