User Tools

Site Tools


null-pointer_analysis_for_concurrent_programs

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

null-pointer_analysis_for_concurrent_programs [2015/03/10 14:49] (current)
bjowac created
Line 1: Line 1:
 +
 +
 +The Software Verification Competition provides implementations of concurrent data structures,
 +which we have analysed in our experiments.
 +
 +The implementations of concurrent data structures in SVCOMP are mostly ​
 +lock-based. Pointer accesses are not shared. A conventional
 +dependence relation based on read-write sets would still find dependencies.
 +However, the corresponding accesses do not affect the value or even nullness
 +of pointers. By using an abstract independence relation, no more dependencies
 +are discovered. These examples therefore do not require backtracking with the abstract
 +independence relation for pointers.
 +
 +However, real-world code does lead to backtracks with the abstract dependence relation.
 +To this end, we have analysed code from the Linux kernel.
 +//and Debian packages //
 +
 +A common mechanism in the Linux kernel is RCU.
 +Read-copy-update (RCU) is a synchronization mechanism implementing a kind of mutual exclusion.
 +RCU is low overhead because it allows wait-free reads.
 +Readers can access a data structure even when it is being updated: RCU updaters cannot block readers or force them to retry their accesses.
 +The Linux kernel contains an RCU API, which is used very frequently used, e.g., 
 +in the network protocol stack.
 +RCU contains potential conflicts affecting pointer variables.
 +The code we are analysing is extracted from Linux kernel 3.2.21
 +and features two threads performing shared accesses on an RCU data structure.
 +
  
null-pointer_analysis_for_concurrent_programs.txt ยท Last modified: 2015/03/10 14:49 by bjowac