Sound, precise and efficient static race detection for multi-threaded programs