ClangBuiltLinux / thread-safety-analysis

A research project into applying Clang's Thread Safety Analysis to the Linux Kernel
Other
6 stars 0 forks source link

Determine how to annotate code for use with sparse and clang thread safety analysis #137

Open bulwahn opened 5 years ago

bulwahn commented 5 years ago

The tool sparse and clang thread safety analysis both use annotations on their function signatures to execute their function local analysis.

Although both tools have very different internal analysis and a different interpretation of the provided argument to the annotations, it seems that these three annotations, acquires, releases, __must_hold (__requires in clang) itself could be translated 1:1.

For the arguments to the annotations, sparse is more relaxed than clang. Sparse takes any string as argument. Clang required the argument to be defined in the scope of the annotation, i.e., a global definition or function argument, and it does a type check against the expected type.

The task here is develop a strategy how sparse and clang could use the same annotations and how to set up macros and modify the current kernel sources that both tools would work.

bulwahn commented 5 years ago

My first observation was that for the translation of __acquires, __releases and __must_hold needs that __must_hold needs to used instead of the combination of __releases and __acquires.

bulwahn commented 5 years ago

A second investigation could be to determine if there is a term x that simply makes an __acquires(x) annotation skipped by clang. E.g., __acquires(void) is not further interpreted by clang.

Then, some macro unreal(x) (name is subject to discussion and change) could be expanded to x for sparse and to void for clang, when clang cannot handle the argument properly.

himanshujha199640 commented 5 years ago

There is no __acquires(void) in the kernel. If we want to combine sparse and clang analysis, then major problem is the scope of annotation. So the question would be what shall we do with the existing sparse annotations which doesn't obey the scoping rules.

bulwahn commented 5 years ago

Yes, I would hope that for existing sparse annotations that do not obey the scoping rules, we can create a macro/build setup for clang that makes clang silently ignore those and only act upon the ones that make sense to clang.

himanshujha199640 commented 5 years ago

I like this idea of using single set of annotations for both tools. Macro/build setup would be something like if:

if (scoping rules)
    same_annotations();
else
    expand_macros_to_no_thread_safety_analysis();

Determing scoping rule is a challenge, and we get to know about it only by failure of compilation process with an error of undeclared identifier. I don't know if it possible to determine it with the help of kbuild or something like that.

bulwahn commented 5 years ago

I am first aiming at solving the issue to possibly just use an extended annotation that states that the actual annotation violates the scoping rules.

bulwahn commented 5 years ago

What did you mean by scoping rules? It could be that we are talking about different things here.

himanshujha199640 commented 5 years ago

What did you mean by scoping rules?

Annotations requires the argument either be globally defined(DEFINE_SPINLOCK or static spinlock foo) or present as an argument which sparse doesn't care about.