Paul E. McKenney – Verifying Parallel Software: Can Theory Meet Practice?

 

Objective of presentation:

To advocate for a deeper theoretical toolchest for those who would validate parallel programs.

 

Abstract:

The advent of low-cost readily available multicore hardware has brought new urgency to the question of validating parallel software. The traditional validation approaches leverage linearizability, commutativity, lock freedom, and wait freedom, each of which has attractive theoretical properties, but which collectively suffer from the minor shortcoming of being unable to address common parallel-programming techniques. Given that these techniques include RCU, I have a vested interest in this debate. This talk will discuss what might be done to bridge this researcher-practitioner divide.

 

Outline:

-Quotes:

  • “So read_barrier_depends() stuff in Linux is also totally busted. (Just like refcounting, etc.)” (2005)
  • “And I don’t believe that the semantics of read_barrier_depends() are actually definable” (2006)
  • “And I think that does work for RCU, at least for conventional optimizations. But the more I think about, the less I’m convinced that it’s 100% reliable.” (2007)

-Hardware/physics issues with traditional validation approaches.

-Mechanical-engineering viewpoint: if there are many jobs, there just might be more than one tool required.

-A few new validation tools.

 

Target audience:

Parallel developers, sequential developers, academics, users, and most especially innocent bystanders caught in the crossfire.

 

Project homepage / blog:

http://www.rdrop.com/user/paulmck/RCU

http://kernel.org/pub/linux/kernel/people/paulmck/perfbook/perfbook.html

http://paulmck.livejournal.com/

Advertisements