Couldn't find any documentation on behavior of clang static analyzer core when it observes multi-threading programming constructs. Does the core identify them and create separate paths for each thread?
No, the Clang Static Analyzer does not attempt to directly analyze the simultaneous execution of multiple threads. Instead, it analyzes one path at a time. Quoting the developer manual:
The analyzer core performs symbolic execution of the given program. All the input values are represented with symbolic values; further, the engine deduces the values of all the expressions in the program based on the input symbols and the path. The execution is path sensitive and every possible path through the program is explored.
The thread-related checks that Clang performs are done within the context of a single path. Skimming the list of available checkers, I found three that relate to C/C++ threading (there are also some for Objective C):
alpha.core.C11Lock: Checks use of the mtx_t API, particularly double-locking and (I assume) failing to release locks.
alpha.unix.PthreadLock: Similar checking for pthread_mutex_lock and related functions.
optin.mpi.MPI-Checker: Checks use of the MPI API, for example that the code waits for a message receive operation to complete before using the data.
In addition to these checkers, there is the Clang Thread Safety Analysis system, which relies on programmer-provided annotations to (mainly) enforce correct usage of mutexes to protect shared data.
What all of these have in common is that the properties being enforced entail the correct usage of an API within the context of a single thread. The analyzer does not need to consider what other threads might be doing to diagnose these issues.
Some commercial static analysis tools have more numerous and sophisticated analyses for detecting issues with threaded code, and may consider what happens along multiple independent (and potentially concurrent) paths, but they also do not directly analyze the interleaving possibilities.
There are techniques that directly consider concurrent execution and interleaving, usually with some variant of a model checking algorithm, but getting such techniques to scale to programs larger than a few tens of lines of code is an open area of research.