Messages in this thread | | | Date | Thu, 1 Jul 2004 18:01:00 -0700 (PDT) | From | Yichen Xie <> | Subject | [BUGS] [CHECKER] 99 synchronization bugs and a lock summary database |
| |
Hi all,
We are a group of researchers at Stanford working on program analysis algorithms. We have been building a precision enhanced program analysis engine at Stanford, and our first application was to derive mutex/lock behavior in the linux kernel. In the process, we found 99 likely synchronization errors in linux kernel version 2.6.5:
http://glide.stanford.edu/linux-lock/err1.html (69 errors) http://glide.stanford.edu/linux-lock/err2.html (30 errors)
err1.html consists of potential double locks/unlocks. Acquiring a lock twice in a row may result in a system hang, and releasing a lock more than once with certain mutex functions (e.g. up) may cause critical section violations.
err2.html consists of reports on inconsistent output lock states on function exit. These errors usually correspond to missed lock operations on error paths. (filenames in this report correspond to where a function is declared, so CTAGS may come in handy to find the actual implementation of the function).
In the error reports, functions are hyperlinked to their derived summaries, and those of their callees (since the analysis spans function calls, the error condition of a particular function usually depend on the locking behavior of its callees).
For example, in function "radeon_pm_program_v2clk" (first error report in err1.html), the tool flagged an error at line 323 of "drivers/video/aty/radeon_pm.c". Line 323 invokes two macros, OUTPLL, and INPLL. OUTPLL acquires "rinfo->reg_lock", and then evaluates "addr", which is calculated, in this case, by calling _INPLL. By clicking on the link "drivers/video/aty/radeon_pm.c:radeon_pm_program_v2clk", we can see that _INPLL requires "rinfo->reg_lock" be unheld on entry (confirmed by looking at its definition), which is not satisfied in this example. So this is a double lock error and could potentially lead to a deadlock on MP systems.
We also have a separate web interface to the summary database at:
http://glide.stanford.edu/linux-lock/
For example, typing "fh_put" in the input box gives
========= SUMMARY ========= FUNCTION SUMMARY: 'include/linux/nfsd/nfsfh.h:fh_put' { dcache_lock(global): [unlocked -> unlocked] fhp(param#0)->fh_dentry->d_lock: [unlocked -> unlocked] fhp(param#0)->fh_dentry->d_inode->i_sem: [locked -> unlocked] }
Each line in the function summary correspond to the requirements and effects on one particular lock. For example, fh_put requires that the global lock variable dcache_lock be unheld on entry, and it'll remain unheld on exit. It also requires fhp->fh_dentry->d_inode->i_sem be held on entry and it'll release it on exit. (note: please ignore summaries for lock premitives like spin_lock or down_interruptible; models for these functions are built into the checker and the derived summaries are not used).
We have found that some modules in the kernel has functions with complicated synchronization behavior (esp. in filesystems), and we hope summaries generated by this tool could be useful not only for bug finding, but also for documentation purposes as well.
The analysis is intraprocedurally "path sensitive", so it won't be fooled by cases like
if (flag & BLOCKING) spin_lock(&l); ... if (flag & BLOCKING) spin_unlock(&l);
or
if (!spin_trylock(&l)) return -EAGAIN; ... spin_unlock(&l);
The analysis algorithm models values (down to individual bits) and pointers in the program with a boolean satisfiability solver with high precision, and we're actively looking for other properties involving (heavy) data dependencies where naive analysis would fail. Suggestions and insights from the linux kernel community will be more than welcome!
As always, feedbacks and confirmations will be greatly appreciated!
Best regards, Yichen Xie <yxie@cs.stanford.edu>
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
| |