M. Eslamimehr (home page), J. Palsberg (home page). UCLA, Univercity of California. See also M. Eslamimehr PhD: PDF online, Sherlock.

1 Deadlock detection. Many deadlock detectors requires annotations. They don't use annotations. Dynamic analysis good for this because it reports only real deadlocks. Schedule is a sequence of events that must be executed in order. Real deadlock is a combination of deadlock pattern and executable schedule. 2 They use GoodLock to quickly produce deadlock candidates. They use concolic execution and new constraint-based approach to drive execution towards a deadlock candidate. Oh, it's look like Leonid's work! They check static analyzer defect candidates! They can replay founded deadlock. They produce a set of deadlock candidates and then use separate search for each one.

They have initial schedule. It is executed and permuted iteratively until execution found deadlock. Schedule is not actually execution path, it is sequence of concurrency events. 3 GoodLock is not static, it combines DA and model checking and can produce FP and FN. They control the thread scheduler to ensure that events are executed in right order. Wow, they are cool guys!

They major innovation is premute function. Said et al. in Generating data race withesses by an SMT-based analysis show how to use SMT-solvers to premutate traces to find data races. I think, it very similar to Mikhail's work to mixing events for GUITar. Other guys use static analysis to build locks graph and use SMT-solver to find cycles (i.e. deadlocks) in graph. Author combine these two approaches!

Sergey Vartanov, 2007–2020