Tag Archives: parallel

Verification Challenge 3: cbmc

The first and second verification challenges were directed to people working on verification tools, but this one is instead directed at developers. It turns out that there are a number of verification tools that have seen heavy use. For example, … Continue reading

Posted in Uncategorized | Tagged , , , , | Comments Off on Verification Challenge 3: cbmc

Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE

I suppose that I might as well get the “But what about Verification Challenge 1?” question out of the way to start with. You will find Verification Challenge 1 here. Now, Verification Challenge 1 was about locating a known bug. … Continue reading

Posted in Uncategorized | Tagged , , , , , | Comments Off on Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE

Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE

I suppose that I might as well get the “But what about Verification Challenge 1?” question out of the way to start with. You will find Verification Challenge 1 here. Now, Verification Challenge 1 was about locating a known bug. … Continue reading

Posted in Uncategorized | Tagged , , , , , | Comments Off on Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE

A practitioner at a formal-methods conference

I had the privilege of being asked to present on ordering, RCU, and validation at a joint meeting of the REORDER (Third International Workshop on Memory Consistency Models) and EC2 (7th International Workshop on Exploiting Concurrency Efficiently and Correctly) workshops. … Continue reading

Posted in Uncategorized | Tagged , , , , , | Comments Off on A practitioner at a formal-methods conference

A practitioner at a formal-methods conference

I had the privilege of being asked to present on ordering, RCU, and validation at a joint meeting of the REORDER (Third International Workshop on Memory Consistency Models) and EC2 (7th International Workshop on Exploiting Concurrency Efficiently and Correctly) workshops. … Continue reading

Posted in Uncategorized | Tagged , , , , , | Comments Off on A practitioner at a formal-methods conference

Stupid RCU Tricks: Bug Found by Refactored Tests

I recently refactored my rcutorture tests, getting that item off of my todo list after “only” three or four years. To my surprise, one (but only one) of the new rcutorture test scenarios failed, namely the one creatively named TREE08: … Continue reading

Posted in Uncategorized | Tagged , , , | Comments Off on Stupid RCU Tricks: Bug Found by Refactored Tests

HOTPAR 2013

I had the privilege of attending this year’s USENIX Workshop on Hot Topics in Parallelism (HOTPAR), which was as always an interesting gathering. One very positive change compared to the first HOTPAR in 2009 is that the participants seemed much … Continue reading

Posted in Uncategorized | Tagged , , , | Comments Off on HOTPAR 2013

Stupid RCU Tricks: Read-Side Ordering Constraints

Suppose that you have an initially empty RCU-protected hash table with per-bucket-locked updates. Suppose that one thread concurrently inserts items A and B in that order (but into different buckets) while a second thread concurrently looks up item A then item B—and while yet … Continue reading

Posted in Uncategorized | Tagged , | Comments Off on Stupid RCU Tricks: Read-Side Ordering Constraints

RCU and Crowds

“A Read-Copy Update based parallel server for distributed crowd simulations” (paywalled) recently appeared in Journal of Supercomputing. Vigueras et al. apply RCU to crowd simulation (as you might guess from the title), which combines throughput (“faster is better”) and response-time … Continue reading

Posted in Uncategorized | Tagged , , | Comments Off on RCU and Crowds

Off to the races!

I was fortunate enough to be able to attend the first workshop on Relaxing Synchronization for Multicore and Manycore Scalability (also known as “RACES’12”), which drew concurrency researchers from across academia and industry. The topic was somewhat controversial, quoting from … Continue reading

Posted in Uncategorized | Tagged , , , | 1 Comment