How does the analysis handle threads that are not annotated? For example, threads inside the DDS implementation.
I noticed in your proof of concept that there are places where locks have been added and places where they have been removed. Is this for the analysis or because the analysis found errors?