RE: Thread Safety Analysis and the Linux kernel

> From: Peter Zijlstra <[email protected]>
> Right, that would work if you then also introduce __guarded_shared_by()
> to express the requirements for access, it then becomes:
> 
> 	cpumask_t	cpus_allowed __guarded_by(pi_lock && rq->__lock)
> 				     __guarded_shared_by(pi_lock || rq->__lock);
> 
> Which is a little more verbose over all, but entirely more flexible.

Would be interesting to see if you have patterns that require this additional flexibility. So perhaps we should wait with implementing something until we've seen a bit more.

> > Your idea on the other hand sounds pretty reasonable to me. We already
> > support multiple arguments in many other attributes, so it seems like
> > a consistent extension. And semantically it makes sense to me as well:
> > if a writer is required to hold all capabilities, then a reader should
> > be fine if they hold any one. I'll have to think a bit more about
> > whether this is always the right thing to do, but if it is, we have an
> > easy way out.
> 
> If not all required locks are exclusive it comes apart.
> 
> Say, it needs a shared capability to satisfy existence (refcount, rcu,
> whatever) and an object internal lock to serialize state.

Currently we categorize accesses into reads and writes, and reads need shared capabilities while writes need exclusive capabilities. (Reads are "lvalue-to-rvalue conversions" in C++ or "lvalue conversions" in C, writes are assignments and a bit more.) Am I reading this correct that you have operations (read or write?) that need a shared capability and an exclusive capability? Although you can put whatever requirements you want on functions:

void f() __requires(m1) __requires_shared(m2);

One concept that we have though is separate capabilities for a pointer and pointee:

int *p __guarded_by(m1) __pt_guarded_by(m2);

p; // shared m1
*p; // shared m1 & m2
p = &x; // exclusive m1
*p = 5; // shared m1, exclusive m2

// With alias analysis:
int* const copy = p; // shared m1
*copy; // shared m2

> Right, so we have a per-cpu struct rq, and a task has a member
> indicating which cpu it currently belongs to.
> 
> struct rq {
> 	raw_spinlock_t __lock;
> };
> 
> DEFINE_PER_CPU(struct rq, runqueues);
> 
> #define cpu_rq(cpu)	(&per_cpu(runqueues, (cpu)))
> 
> /*
>  * And I suppose we can imagine runqueues to simply be an array
>  * and per_cpu() to index into said array. Although the reality is that
>  * it is much more like thread-local-storage in userspace.
>  */
> 
> struct task_struct {
> 	raw_spinlock_t pi_lock;
> 	int cpu;
> }
> 
> int task_cpu(struct task_struct *p)
> {
> 	return p->cpu;
> }
> 
> #define task_rq(p) cpu_rq(task_cpu(p))

Ok, so then we can refer to the member: where you wanted to write rq->__lock, we write cpu_rq(cpu)->__lock.

However, I suppose the macros go quite deep and then we can come across a statement expression (or worse).

Another issue is aliasing. Maybe the caller has obtained the runqueue in a different way, and then it's not clear that it equals cpu_rq(cpu).

> One thing we could do is add a struct rq pointer -- duplicating the cpu
> member state, like:
> 
> struct task_struct {
> 	raw_spinlock_t pik;
> 	int cpu;
> 	struct rq *rq;
> };

I don't think we need this. You can write expressions of some complexity, including opaque function calls. (Just avoid statement expressions.) They're compared symbolically, which in the case of function calls implies they're pure. To play a bit with your example:

                rq = task_rq(p);
                raw_spin_rq_lock(rq);
                p->cpus_allowed = 0; // let's pretend it's an integer.

The second line acquires rq.__lock, which expands to cpu_rq(task_cpu(p)).__lock once we have alias analysis. For the write to cpus_allowed we need an exclusive lock on cpu_rq(p->cpu)->__lock by substitution. Suppose we make task_cpu a macro and cpu_rq a function (for sake of exposition). Then our existing lock is cpu_rq(p->cpu)->__lock and matches what we need. If we want to leave task_cpu a function, an __attribute__((return_capability)) might work there. (It's not a capability, but I think we only use the attribute for substitution and don't check the type.)

It might need some playing around what needs to be transparent to the analysis and what better stay opaque.

Aaron